Theorem pjopytht 5662

Description: Pythagorean theorem for projections on orthogonal subspaces.

Assertion

Ref	Expression
pjopytht	|- ((H e. CH /\ G e. CH /\ A e. H~) -> (H (_ (_|_` G) -> ((norm` (((Proj` H)` A) +v ((Proj` G)` A)))^2) = (((norm` ((Proj` H)` A))^2) + ((norm` ((Proj` G)` A))^2))))

Proof of Theorem pjopytht

Step	Hyp	Ref	Expression
1		sseq1 1521	. . 3 |- (H = if(H e. CH, H, H~) -> (H (_ (_|_` G) <-> if(H e. CH, H, H~) (_ (_|_` G)))
2		fveq2 2832	. . . . . . . 8 |- (H = if(H e. CH, H, H~) -> (Proj` H) = (Proj` if(H e. CH, H, H~)))
3	2	fveq1d 2834	. . . . . . 7 |- (H = if(H e. CH, H, H~) -> ((Proj` H)` A) = ((Proj` if(H e. CH, H, H~))` A))
4	3	opreq1d 3012	. . . . . 6 |- (H = if(H e. CH, H, H~) -> (((Proj` H)` A) +v ((Proj` G)` A)) = (((Proj` if(H e. CH, H, H~))` A) +v ((Proj` G)` A)))
5	4	fveq2d 2836	. . . . 5 |- (H = if(H e. CH, H, H~) -> (norm` (((Proj` H)` A) +v ((Proj` G)` A))) = (norm` (((Proj` if(H e. CH, H, H~))` A) +v ((Proj` G)` A))))
6	5	opreq1d 3012	. . . 4 |- (H = if(H e. CH, H, H~) -> ((norm` (((Proj` H)` A) +v ((Proj` G)` A)))^2) = ((norm` (((Proj` if(H e. CH, H, H~))` A) +v ((Proj` G)` A)))^2))
7	3	fveq2d 2836	. . . . . 6 |- (H = if(H e. CH, H, H~) -> (norm` ((Proj` H)` A)) = (norm` ((Proj` if(H e. CH, H, H~))` A)))
8	7	opreq1d 3012	. . . . 5 |- (H = if(H e. CH, H, H~) -> ((norm` ((Proj` H)` A))^2) = ((norm` ((Proj` if(H e. CH, H, H~))` A))^2))
9	8	opreq1d 3012	. . . 4 |- (H = if(H e. CH, H, H~) -> (((norm` ((Proj` H)` A))^2) + ((norm` ((Proj` G)` A))^2)) = (((norm` ((Proj` if(H e. CH, H, H~))` A))^2) + ((norm` ((Proj` G)` A))^2)))
10	6, 9	cleq12d 1115	. . 3 |- (H = if(H e. CH, H, H~) -> (((norm` (((Proj` H)` A) +v ((Proj` G)` A)))^2) = (((norm` ((Proj` H)` A))^2) + ((norm` ((Proj` G)` A))^2)) <-> ((norm` (((Proj` if(H e. CH, H, H~))` A) +v ((Proj` G)` A)))^2) = (((norm` ((Proj` if(H e. CH, H, H~))` A))^2) + ((norm` ((Proj` G)` A))^2))))
11	1, 10	imbi12d 474	. 2 |- (H = if(H e. CH, H, H~) -> ((H (_ (_|_` G) -> ((norm` (((Proj` H)` A) +v ((Proj` G)` A)))^2) = (((norm` ((Proj` H)` A))^2) + ((norm` ((Proj` G)` A))^2))) <-> (if(H e. CH, H, H~) (_ (_|_` G) -> ((norm` (((Proj` if(H e. CH, H, H~))` A) +v ((Proj` G)` A)))^2) = (((norm` ((Proj` if(H e. CH, H, H~))` A))^2) + ((norm` ((Proj` G)` A))^2)))))
12		fveq2 2832	. . . 4 |- (G = if(G e. CH, G, H~) -> (_|_` G) = (_|_` if(G e. CH, G, H~)))
13	12	sseq2d 1528	. . 3 |- (G = if(G e. CH, G, H~) -> (if(H e. CH, H, H~) (_ (_|_` G) <-> if(H e. CH, H, H~) (_ (_|_` if(G e. CH, G, H~))))
14		fveq2 2832	. . . . . . . 8 |- (G = if(G e. CH, G, H~) -> (Proj` G) = (Proj` if(G e. CH, G, H~)))
15	14	fveq1d 2834	. . . . . . 7 |- (G = if(G e. CH, G, H~) -> ((Proj` G)` A) = ((Proj` if(G e. CH, G, H~))` A))
16	15	opreq2d 3013	. . . . . 6 |- (G = if(G e. CH, G, H~) -> (((Proj` if(H e. CH, H, H~))` A) +v ((Proj` G)` A)) = (((Proj` if(H e. CH, H, H~))` A) +v ((Proj` if(G e. CH, G, H~))` A)))
17	16	fveq2d 2836	. . . . 5 |- (G = if(G e. CH, G, H~) -> (norm` (((Proj` if(H e. CH, H, H~))` A) +v ((Proj` G)` A))) = (norm` (((Proj` if(H e. CH, H, H~))` A) +v ((Proj` if(G e. CH, G, H~))` A))))
18	17	opreq1d 3012	. . . 4 |- (G = if(G e. CH, G, H~) -> ((norm` (((Proj` if(H e. CH, H, H~))` A) +v ((Proj` G)` A)))^2) = ((norm` (((Proj` if(H e. CH, H, H~))` A) +v ((Proj` if(G e. CH, G, H~))` A)))^2))
19	15	fveq2d 2836	. . . . . 6 |- (G = if(G e. CH, G, H~) -> (norm` ((Proj` G)` A)) = (norm` ((Proj` if(G e. CH, G, H~))` A)))
20	19	opreq1d 3012	. . . . 5 |- (G = if(G e. CH, G, H~) -> ((norm` ((Proj` G)` A))^2) = ((norm` ((Proj` if(G e. CH, G, H~))` A))^2))
21	20	opreq2d 3013	. . . 4 |- (G = if(G e. CH, G, H~) -> (((norm` ((Proj` if(H e. CH, H, H~))` A))^2) + ((norm` ((Proj` G)` A))^2)) = (((norm` ((Proj` if(H e. CH, H, H~))` A))^2) + ((norm` ((Proj` if(G e. CH, G, H~))` A))^2)))
22	18, 21	cleq12d 1115	. . 3 |- (G = if(G e. CH, G, H~) -> (((norm` (((Proj` if(H e. CH, H, H~))` A) +v ((Proj` G)` A)))^2) = (((norm` ((Proj` if(H e. CH, H, H~))` A))^2) + ((norm` ((Proj` G)` A))^2)) <-> ((norm` (((Proj` if(H e. CH, H, H~))` A) +v ((Proj` if(G e. CH, G, H~))` A)))^2) = (((norm` ((Proj` if(H e. CH, H, H~))` A))^2) + ((norm` ((Proj` if(G e. CH, G, H~))` A))^2))))
23	13, 22	imbi12d 474	. 2 |- (G = if(G e. CH, G, H~) -> ((if(H e. CH, H, H~) (_ (_|_` G) -> ((norm` (((Proj` if(H e. CH, H, H~))` A) +v ((Proj` G)` A)))^2) = (((norm` ((Proj` if(H e. CH, H, H~))` A))^2) + ((norm` ((Proj` G)` A))^2))) <-> (if(H e. CH, H, H~) (_ (_|_` if(G e. CH, G, H~)) -> ((norm` (((Proj` if(H e. CH, H, H~))` A) +v ((Proj` if(G e. CH, G, H~))` A)))^2) = (((norm` ((Proj` if(H e. CH, H, H~))` A))^2) + ((norm` ((Proj` if(G e. CH, G, H~))` A))^2)))))
24		fveq2 2832	. . . . . . 7 |- (A = if(A e. H~, A, 0v)