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 e. CH /\ H e. CH /\ A e. ~H ) /\ G C_ ( _|_ ` H ) ) -> ( ( ( projh ` G ) ` A ) .ih ( ( projh ` H ) ` A ) ) = 0 )

Proof

Step Hyp Ref Expression
1 pjrn 
 |-  ( G e. CH -> ran ( projh ` G ) = G )
2 1 adantr 
 |-  ( ( G e. CH /\ H e. CH ) -> ran ( projh ` G ) = G )
3 pjrn 
 |-  ( H e. CH -> ran ( projh ` H ) = H )
4 3 fveq2d 
 |-  ( H e. CH -> ( _|_ ` ran ( projh ` H ) ) = ( _|_ ` H ) )
5 4 adantl 
 |-  ( ( G e. CH /\ H e. CH ) -> ( _|_ ` ran ( projh ` H ) ) = ( _|_ ` H ) )
6 2 5 sseq12d 
 |-  ( ( G e. CH /\ H e. CH ) -> ( ran ( projh ` G ) C_ ( _|_ ` ran ( projh ` H ) ) <-> G C_ ( _|_ ` H ) ) )
7 6 biimpar 
 |-  ( ( ( G e. CH /\ H e. CH ) /\ G C_ ( _|_ ` H ) ) -> ran ( projh ` G ) C_ ( _|_ ` ran ( projh ` H ) ) )
8 7 3adantl3 
 |-  ( ( ( G e. CH /\ H e. CH /\ A e. ~H ) /\ G C_ ( _|_ ` H ) ) -> ran ( projh ` G ) C_ ( _|_ ` ran ( projh ` H ) ) )
9 id 
 |-  ( H e. CH -> H e. CH )
10 3 9 eqeltrd 
 |-  ( H e. CH -> ran ( projh ` H ) e. CH )
11 chsh 
 |-  ( ran ( projh ` H ) e. CH -> ran ( projh ` H ) e. SH )
12 10 11 syl 
 |-  ( H e. CH -> ran ( projh ` H ) e. SH )
13 12 3ad2ant2 
 |-  ( ( G e. CH /\ H e. CH /\ A e. ~H ) -> ran ( projh ` H ) e. SH )
14 13 adantr 
 |-  ( ( ( G e. CH /\ H e. CH /\ A e. ~H ) /\ ran ( projh ` G ) C_ ( _|_ ` ran ( projh ` H ) ) ) -> ran ( projh ` H ) e. SH )
15 simpr 
 |-  ( ( ( G e. CH /\ H e. CH /\ A e. ~H ) /\ ran ( projh ` G ) C_ ( _|_ ` ran ( projh ` H ) ) ) -> ran ( projh ` G ) C_ ( _|_ ` ran ( projh ` H ) ) )
16 pjfn 
 |-  ( G e. CH -> ( projh ` G ) Fn ~H )
17 fnfvelrn 
 |-  ( ( ( projh ` G ) Fn ~H /\ A e. ~H ) -> ( ( projh ` G ) ` A ) e. ran ( projh ` G ) )
18 16 17 sylan 
 |-  ( ( G e. CH /\ A e. ~H ) -> ( ( projh ` G ) ` A ) e. ran ( projh ` G ) )
19 18 3adant2 
 |-  ( ( G e. CH /\ H e. CH /\ A e. ~H ) -> ( ( projh ` G ) ` A ) e. ran ( projh ` G ) )
20 pjfn 
 |-  ( H e. CH -> ( projh ` H ) Fn ~H )
21 fnfvelrn 
 |-  ( ( ( projh ` H ) Fn ~H /\ A e. ~H ) -> ( ( projh ` H ) ` A ) e. ran ( projh ` H ) )
22 20 21 sylan 
 |-  ( ( H e. CH /\ A e. ~H ) -> ( ( projh ` H ) ` A ) e. ran ( projh ` H ) )
23 22 3adant1 
 |-  ( ( G e. CH /\ H e. CH /\ A e. ~H ) -> ( ( projh ` H ) ` A ) e. ran ( projh ` H ) )
24 19 23 jca 
 |-  ( ( G e. CH /\ H e. CH /\ A e. ~H ) -> ( ( ( projh ` G ) ` A ) e. ran ( projh ` G ) /\ ( ( projh ` H ) ` A ) e. ran ( projh ` H ) ) )
25 24 adantr 
 |-  ( ( ( G e. CH /\ H e. CH /\ A e. ~H ) /\ ran ( projh ` G ) C_ ( _|_ ` ran ( projh ` H ) ) ) -> ( ( ( projh ` G ) ` A ) e. ran ( projh ` G ) /\ ( ( projh ` H ) ` A ) e. ran ( projh ` H ) ) )
26 shorth 
 |-  ( ran ( projh ` H ) e. SH -> ( ran ( projh ` G ) C_ ( _|_ ` ran ( projh ` H ) ) -> ( ( ( ( projh ` G ) ` A ) e. ran ( projh ` G ) /\ ( ( projh ` H ) ` A ) e. ran ( projh ` H ) ) -> ( ( ( projh ` G ) ` A ) .ih ( ( projh ` H ) ` A ) ) = 0 ) ) )
27 14 15 25 26 syl3c 
 |-  ( ( ( G e. CH /\ H e. CH /\ A e. ~H ) /\ ran ( projh ` G ) C_ ( _|_ ` ran ( projh ` H ) ) ) -> ( ( ( projh ` G ) ` A ) .ih ( ( projh ` H ) ` A ) ) = 0 )
28 8 27 syldan 
 |-  ( ( ( G e. CH /\ H e. CH /\ A e. ~H ) /\ G C_ ( _|_ ` H ) ) -> ( ( ( projh ` G ) ` A ) .ih ( ( projh ` H ) ` A ) ) = 0 )