Metamath Proof Explorer


Theorem pjoi0

Description: The inner product of projections on orthogonal subspaces vanishes. (Contributed by NM, 30-Jun-2006) (New usage is discouraged.)

Ref Expression
Assertion pjoi0 G C H C A G H proj G A ih proj H A = 0

Proof

Step Hyp Ref Expression
1 pjrn G C ran proj G = G
2 1 adantr G C H C ran proj G = G
3 pjrn H C ran proj H = H
4 3 fveq2d H C ran proj H = H
5 4 adantl G C H C ran proj H = H
6 2 5 sseq12d G C H C ran proj G ran proj H G H
7 6 biimpar G C H C G H ran proj G ran proj H
8 7 3adantl3 G C H C A G H ran proj G ran proj H
9 id H C H C
10 3 9 eqeltrd H C ran proj H C
11 chsh ran proj H C ran proj H S
12 10 11 syl H C ran proj H S
13 12 3ad2ant2 G C H C A ran proj H S
14 13 adantr G C H C A ran proj G ran proj H ran proj H S
15 simpr G C H C A ran proj G ran proj H ran proj G ran proj H
16 pjfn G C proj G Fn
17 fnfvelrn proj G Fn A proj G A ran proj G
18 16 17 sylan G C A proj G A ran proj G
19 18 3adant2 G C H C A proj G A ran proj G
20 pjfn H C proj H Fn
21 fnfvelrn proj H Fn A proj H A ran proj H
22 20 21 sylan H C A proj H A ran proj H
23 22 3adant1 G C H C A proj H A ran proj H
24 19 23 jca G C H C A proj G A ran proj G proj H A ran proj H
25 24 adantr G C H C A ran proj G ran proj H proj G A ran proj G proj H A ran proj H
26 shorth ran proj H S ran proj G ran proj H proj G A ran proj G proj H A ran proj H proj G A ih proj H A = 0
27 14 15 25 26 syl3c G C H C A ran proj G ran proj H proj G A ih proj H A = 0
28 8 27 syldan G C H C A G H proj G A ih proj H A = 0