Theorem pjopytht 9665

Description: Pythagorean theorem for projections on orthogonal subspaces.

Assertion

Ref	Expression
pjopytht	|- ((H e. CH /\ G e. CH /\ A e. H~) -> (H (_ (_|_` G) -> ((normh` (((proj` H)` A) +h ((proj` G)` A)))^2) = (((normh` ((proj` H)` A))^2) + ((normh` ((proj` G)` A))^2))))

Proof of Theorem pjopytht

Step	Hyp	Ref	Expression
1		sseq1 2082	. . 3 |- (H = if(H e. CH, H, H~) -> (H (_ (_|_` G) <-> if(H e. CH, H, H~) (_ (_|_` G)))
2		fveq2 3724	. . . . . . . 8 |- (H = if(H e. CH, H, H~) -> (proj` H) = (proj` if(H e. CH, H, H~)))
3	2	fveq1d 3726	. . . . . . 7 |- (H = if(H e. CH, H, H~) -> ((proj` H)` A) = ((proj` if(H e. CH, H, H~))` A))
4	3	opreq1d 3975	. . . . . 6 |- (H = if(H e. CH, H, H~) -> (((proj` H)` A) +h ((proj` G)` A)) = (((proj` if(H e. CH, H, H~))` A) +h ((proj` G)` A)))
5	4	fveq2d 3728	. . . . 5 |- (H = if(H e. CH, H, H~) -> (normh` (((proj` H)` A) +h ((proj` G)` A))) = (normh` (((proj` if(H e. CH, H, H~))` A) +h ((proj` G)` A))))
6	5	opreq1d 3975	. . . 4 |- (H = if(H e. CH, H, H~) -> ((normh` (((proj` H)` A) +h ((proj` G)` A)))^2) = ((normh` (((proj` if(H e. CH, H, H~))` A) +h ((proj` G)` A)))^2))
7	3	fveq2d 3728	. . . . . 6 |- (H = if(H e. CH, H, H~) -> (normh` ((proj` H)` A)) = (normh` ((proj` if(H e. CH, H, H~))` A)))
8	7	opreq1d 3975	. . . . 5 |- (H = if(H e. CH, H, H~) -> ((normh` ((proj` H)` A))^2) = ((normh` ((proj` if(H e. CH, H, H~))` A))^2))
9	8	opreq1d 3975	. . . 4 |- (H = if(H e. CH, H, H~) -> (((normh` ((proj` H)` A))^2) + ((normh` ((proj` G)` A))^2)) = (((normh` ((proj` if(H e. CH, H, H~))` A))^2) + ((normh` ((proj` G)` A))^2)))
10	6, 9	eqeq12d 1489	. . 3 |- (H = if(H e. CH, H, H~) -> (((normh` (((proj` H)` A) +h ((proj` G)` A)))^2) = (((normh` ((proj` H)` A))^2) + ((normh` ((proj` G)` A))^2)) <-> ((normh` (((proj` if(H e. CH, H, H~))` A) +h ((proj` G)` A)))^2) = (((normh` ((proj` if(H e. CH, H, H~))` A))^2) + ((normh` ((proj` G)` A))^2))))
11	1, 10	imbi12d 626	. 2 |- (H = if(H e. CH, H, H~) -> ((H (_ (_|_` G) -> ((normh` (((proj` H)` A) +h ((proj` G)` A)))^2) = (((normh` ((proj` H)` A))^2) + ((normh` ((proj` G)` A))^2))) <-> (if(H e. CH, H, H~) (_ (_|_` G) -> ((normh` (((proj` if(H e. CH, H, H~))` A) +h ((proj` G)` A)))^2) = (((normh` ((proj` if(H e. CH, H, H~))` A))^2) + ((normh` ((proj` G)` A))^2)))))
12		fveq2 3724	. . . 4 |- (G = if(G e. CH, G, H~) -> (_|_` G) = (_|_` if(G e. CH, G, H~)))
13	12	sseq2d 2089	. . 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 3724	. . . . . . . 8 |- (G = if(G e. CH, G, H~) -> (proj` G) = (proj` if(G e. CH, G, H~)))
15	14	fveq1d 3726	. . . . . . 7 |- (G = if(G e. CH, G, H~) -> ((proj` G)` A) = ((proj` if(G e. CH, G, H~))` A))
16	15	opreq2d 3976	. . . . . 6 |- (G = if(G e. CH, G, H~) -> (((proj` if(H e. CH, H, H~))` A) +h ((proj` G)` A)) = (((proj` if(H e. CH, H, H~))` A) +h ((proj` if(G e. CH, G, H~))` A)))
17	16	fveq2d 3728	. . . . 5 |- (G = if(G e. CH, G, H~) -> (normh` (((proj` if(H e. CH, H, H~))` A) +h ((proj` G)` A))) = (normh` (((proj` if(H e. CH, H, H~))` A) +h ((proj` if(G e. CH, G, H~))` A))))
18	17	opreq1d 3975	. . . 4 |- (G = if(G e. CH, G, H~) -> ((normh` (((proj` if(H e. CH, H, H~))` A) +h ((proj` G)` A)))^2) = ((normh` (((proj` if(H e. CH, H, H~))` A) +h ((proj` if(G e. CH, G, H~))` A)))^2))
19	15	fveq2d 3728	. . . . . 6 |- (G = if(G e. CH, G, H~) -> (normh` ((proj` G)` A)) = (normh` ((proj` if(G e. CH, G, H~))` A)))
20	19	opreq1d 3975	. . . . 5 |- (G = if(G e. CH, G, H~) -> ((normh` ((proj` G)` A))^2) = ((normh` ((proj` if(G e. CH, G, H~))` A))^2))
21	20	opreq2d 3976	. . . 4 |- (G = if(G e. CH, G, H~) -> (((normh` ((proj` if(H e. CH, H, H~))` A))^2) + ((normh` ((proj` G)` A))^2)) = (((normh` ((proj` if(H e. CH, H, H~))` A))^2) + ((normh` ((proj` if(G e. CH, G, H~))` A))^2)))
22	18, 21	eqeq12d 1489	. . 3 |- (G = if(G e. CH, G, H~) -> (((normh` (((proj` if(H e. CH, H, H~))` A) +h ((proj` G)` A)))^2) = (((normh` ((proj` if(H e. CH, H, H~))` A))^2) + ((normh` ((proj` G)` A))^2)) <-> ((normh` (((proj` if(H e. CH, H, H~))` A) +h ((proj` if(G e. CH, G, H~))` A)))^2) = (((normh` ((proj` if(H e. CH, H, H~))` A))^2) + ((normh` ((proj` if(G e. CH, G, H~))` A))^2))))
23	13, 22	imbi12d 626	. 2 |- (G = if(G e. CH, G, H~) -> ((if(H e. CH, H, H~) (_ (_|_` G) -> ((normh` (((proj` if(H e. CH, H, H~))` A) +h ((proj` G)` A)))^2) = (((normh` ((proj` if(H e. CH, H, H~))` A))^2) + ((normh` ((proj` G)` A))^2))) <-> (if(H e. CH, H, H~) (_ (_|_` if(G e. CH, G, H~)) -> ((normh` (((proj` if(H e. CH, H, H~))` A) +h ((proj` if(G e. CH, G, H~))` A)))^2) = (((normh` ((proj` if(H e. CH, H, H~))` A))^2) + ((normh` ((proj` if(G e. CH, G, H~))` A))^2)))))
24		fveq2 3724	. . . . . . 7 |- (A = if(A e. H~, A, 0h) -> ((proj` if(H e. CH, H, H~))` A) = ((proj` if(H e. CH, H, H~))` if(A e. H~, A, 0h)))
25		fveq2 3724	. . . . . . 7 |- (A = if(A e. H~