Metamath Proof Explorer


Theorem pjopyth

Description: Pythagorean theorem for projections on orthogonal subspaces. (Contributed by NM, 2-Nov-1999) (New usage is discouraged.)

Ref Expression
Assertion pjopyth H C G C A H G norm proj H A + proj G A 2 = norm proj H A 2 + norm proj G A 2

Proof

Step Hyp Ref Expression
1 sseq1 H = if H C H H G if H C H G
2 fveq2 H = if H C H proj H = proj if H C H
3 2 fveq1d H = if H C H proj H A = proj if H C H A
4 3 oveq1d H = if H C H proj H A + proj G A = proj if H C H A + proj G A
5 4 fveq2d H = if H C H norm proj H A + proj G A = norm proj if H C H A + proj G A
6 5 oveq1d H = if H C H norm proj H A + proj G A 2 = norm proj if H C H A + proj G A 2
7 3 fveq2d H = if H C H norm proj H A = norm proj if H C H A
8 7 oveq1d H = if H C H norm proj H A 2 = norm proj if H C H A 2
9 8 oveq1d H = if H C H norm proj H A 2 + norm proj G A 2 = norm proj if H C H A 2 + norm proj G A 2
10 6 9 eqeq12d H = if H C H norm proj H A + proj G A 2 = norm proj H A 2 + norm proj G A 2 norm proj if H C H A + proj G A 2 = norm proj if H C H A 2 + norm proj G A 2
11 1 10 imbi12d H = if H C H H G norm proj H A + proj G A 2 = norm proj H A 2 + norm proj G A 2 if H C H G norm proj if H C H A + proj G A 2 = norm proj if H C H A 2 + norm proj G A 2
12 fveq2 G = if G C G G = if G C G
13 12 sseq2d G = if G C G if H C H G if H C H if G C G
14 fveq2 G = if G C G proj G = proj if G C G
15 14 fveq1d G = if G C G proj G A = proj if G C G A
16 15 oveq2d G = if G C G proj if H C H A + proj G A = proj if H C H A + proj if G C G A
17 16 fveq2d G = if G C G norm proj if H C H A + proj G A = norm proj if H C H A + proj if G C G A
18 17 oveq1d G = if G C G norm proj if H C H A + proj G A 2 = norm proj if H C H A + proj if G C G A 2
19 15 fveq2d G = if G C G norm proj G A = norm proj if G C G A
20 19 oveq1d G = if G C G norm proj G A 2 = norm proj if G C G A 2
21 20 oveq2d G = if G C G norm proj if H C H A 2 + norm proj G A 2 = norm proj if H C H A 2 + norm proj if G C G A 2
22 18 21 eqeq12d G = if G C G norm proj if H C H A + proj G A 2 = norm proj if H C H A 2 + norm proj G A 2 norm proj if H C H A + proj if G C G A 2 = norm proj if H C H A 2 + norm proj if G C G A 2
23 13 22 imbi12d G = if G C G if H C H G norm proj if H C H A + proj G A 2 = norm proj if H C H A 2 + norm proj G A 2 if H C H if G C G norm proj if H C H A + proj if G C G A 2 = norm proj if H C H A 2 + norm proj if G C G A 2
24 fveq2 A = if A A 0 proj if H C H A = proj if H C H if A A 0
25 fveq2 A = if A A 0 proj if G C G A = proj if G C G if A A 0
26 24 25 oveq12d A = if A A 0 proj if H C H A + proj if G C G A = proj if H C H if A A 0 + proj if G C G if A A 0
27 26 fveq2d A = if A A 0 norm proj if H C H A + proj if G C G A = norm proj if H C H if A A 0 + proj if G C G if A A 0
28 27 oveq1d A = if A A 0 norm proj if H C H A + proj if G C G A 2 = norm proj if H C H if A A 0 + proj if G C G if A A 0 2
29 24 fveq2d A = if A A 0 norm proj if H C H A = norm proj if H C H if A A 0
30 29 oveq1d A = if A A 0 norm proj if H C H A 2 = norm proj if H C H if A A 0 2
31 25 fveq2d A = if A A 0 norm proj if G C G A = norm proj if G C G if A A 0
32 31 oveq1d A = if A A 0 norm proj if G C G A 2 = norm proj if G C G if A A 0 2
33 30 32 oveq12d A = if A A 0 norm proj if H C H A 2 + norm proj if G C G A 2 = norm proj if H C H if A A 0 2 + norm proj if G C G if A A 0 2
34 28 33 eqeq12d A = if A A 0 norm proj if H C H A + proj if G C G A 2 = norm proj if H C H A 2 + norm proj if G C G A 2 norm proj if H C H if A A 0 + proj if G C G if A A 0 2 = norm proj if H C H if A A 0 2 + norm proj if G C G if A A 0 2
35 34 imbi2d A = if A A 0 if H C H if G C G norm proj if H C H A + proj if G C G A 2 = norm proj if H C H A 2 + norm proj if G C G A 2 if H C H if G C G norm proj if H C H if A A 0 + proj if G C G if A A 0 2 = norm proj if H C H if A A 0 2 + norm proj if G C G if A A 0 2
36 ifchhv if H C H C
37 ifchhv if G C G C
38 ifhvhv0 if A A 0
39 36 37 38 pjopythi if H C H if G C G norm proj if H C H if A A 0 + proj if G C G if A A 0 2 = norm proj if H C H if A A 0 2 + norm proj if G C G if A A 0 2
40 11 23 35 39 dedth3h H C G C A H G norm proj H A + proj G A 2 = norm proj H A 2 + norm proj G A 2