Metamath Proof Explorer

Theorem pjspansn

Description: A projection on the span of a singleton. (The proof ws shortened by Mario Carneiro, 15-Dec-2013.) (Contributed by NM, 28-May-2006) (Revised by Mario Carneiro, 15-Dec-2013) (New usage is discouraged.)

Ref Expression
Assertion pjspansn 
|- ( ( A e. ~H /\ B e. ~H /\ A =/= 0h ) -> ( ( projh ` ( span ` { A } ) ) ` B ) = ( ( ( B .ih A ) / ( ( normh ` A ) ^ 2 ) ) .h A ) )

Proof

Step Hyp Ref Expression
1 spansnch 
 |-  ( A e. ~H -> ( span ` { A } ) e. CH )
2 1 3ad2ant1 
 |-  ( ( A e. ~H /\ B e. ~H /\ A =/= 0h ) -> ( span ` { A } ) e. CH )
3 simp2 
 |-  ( ( A e. ~H /\ B e. ~H /\ A =/= 0h ) -> B e. ~H )
4 eqid 
 |-  ( ( projh ` ( span ` { A } ) ) ` B ) = ( ( projh ` ( span ` { A } ) ) ` B )
5 pjeq 
 |-  ( ( ( span ` { A } ) e. CH /\ B e. ~H ) -> ( ( ( projh ` ( span ` { A } ) ) ` B ) = ( ( projh ` ( span ` { A } ) ) ` B ) <-> ( ( ( projh ` ( span ` { A } ) ) ` B ) e. ( span ` { A } ) /\ E. y e. ( _|_ ` ( span ` { A } ) ) B = ( ( ( projh ` ( span ` { A } ) ) ` B ) +h y ) ) ) )
6 4 5 mpbii 
 |-  ( ( ( span ` { A } ) e. CH /\ B e. ~H ) -> ( ( ( projh ` ( span ` { A } ) ) ` B ) e. ( span ` { A } ) /\ E. y e. ( _|_ ` ( span ` { A } ) ) B = ( ( ( projh ` ( span ` { A } ) ) ` B ) +h y ) ) )
7 6 simprd 
 |-  ( ( ( span ` { A } ) e. CH /\ B e. ~H ) -> E. y e. ( _|_ ` ( span ` { A } ) ) B = ( ( ( projh ` ( span ` { A } ) ) ` B ) +h y ) )
8 2 3 7 syl2anc 
 |-  ( ( A e. ~H /\ B e. ~H /\ A =/= 0h ) -> E. y e. ( _|_ ` ( span ` { A } ) ) B = ( ( ( projh ` ( span ` { A } ) ) ` B ) +h y ) )
9 oveq1 
 |-  ( B = ( ( ( projh ` ( span ` { A } ) ) ` B ) +h y ) -> ( B .ih A ) = ( ( ( ( projh ` ( span ` { A } ) ) ` B ) +h y ) .ih A ) )
10 9 ad2antll 
 |-  ( ( ( A e. ~H /\ B e. ~H /\ A =/= 0h ) /\ ( y e. ( _|_ ` ( span ` { A } ) ) /\ B = ( ( ( projh ` ( span ` { A } ) ) ` B ) +h y ) ) ) -> ( B .ih A ) = ( ( ( ( projh ` ( span ` { A } ) ) ` B ) +h y ) .ih A ) )
11 pjhcl 
 |-  ( ( ( span ` { A } ) e. CH /\ B e. ~H ) -> ( ( projh ` ( span ` { A } ) ) ` B ) e. ~H )
12 2 3 11 syl2anc 
 |-  ( ( A e. ~H /\ B e. ~H /\ A =/= 0h ) -> ( ( projh ` ( span ` { A } ) ) ` B ) e. ~H )
13 12 adantr 
 |-  ( ( ( A e. ~H /\ B e. ~H /\ A =/= 0h ) /\ y e. ( _|_ ` ( span ` { A } ) ) ) -> ( ( projh ` ( span ` { A } ) ) ` B ) e. ~H )
14 choccl 
 |-  ( ( span ` { A } ) e. CH -> ( _|_ ` ( span ` { A } ) ) e. CH )
15 1 14 syl 
 |-  ( A e. ~H -> ( _|_ ` ( span ` { A } ) ) e. CH )
16 15 3ad2ant1 
 |-  ( ( A e. ~H /\ B e. ~H /\ A =/= 0h ) -> ( _|_ ` ( span ` { A } ) ) e. CH )
17 chel 
 |-  ( ( ( _|_ ` ( span ` { A } ) ) e. CH /\ y e. ( _|_ ` ( span ` { A } ) ) ) -> y e. ~H )
18 16 17 sylan 
 |-  ( ( ( A e. ~H /\ B e. ~H /\ A =/= 0h ) /\ y e. ( _|_ ` ( span ` { A } ) ) ) -> y e. ~H )
19 simpl1 
 |-  ( ( ( A e. ~H /\ B e. ~H /\ A =/= 0h ) /\ y e. ( _|_ ` ( span ` { A } ) ) ) -> A e. ~H )
20 ax-his2 
 |-  ( ( ( ( projh ` ( span ` { A } ) ) ` B ) e. ~H /\ y e. ~H /\ A e. ~H ) -> ( ( ( ( projh ` ( span ` { A } ) ) ` B ) +h y ) .ih A ) = ( ( ( ( projh ` ( span ` { A } ) ) ` B ) .ih A ) + ( y .ih A ) ) )
21 13 18 19 20 syl3anc 
 |-  ( ( ( A e. ~H /\ B e. ~H /\ A =/= 0h ) /\ y e. ( _|_ ` ( span ` { A } ) ) ) -> ( ( ( ( projh ` ( span ` { A } ) ) ` B ) +h y ) .ih A ) = ( ( ( ( projh ` ( span ` { A } ) ) ` B ) .ih A ) + ( y .ih A ) ) )
22 spansnsh 
 |-  ( A e. ~H -> ( span ` { A } ) e. SH )
23 22 adantr 
 |-  ( ( A e. ~H /\ y e. ( _|_ ` ( span ` { A } ) ) ) -> ( span ` { A } ) e. SH )
24 spansnid 
 |-  ( A e. ~H -> A e. ( span ` { A } ) )
25 24 adantr 
 |-  ( ( A e. ~H /\ y e. ( _|_ ` ( span ` { A } ) ) ) -> A e. ( span ` { A } ) )
26 simpr 
 |-  ( ( A e. ~H /\ y e. ( _|_ ` ( span ` { A } ) ) ) -> y e. ( _|_ ` ( span ` { A } ) ) )
27 shocorth 
 |-  ( ( span ` { A } ) e. SH -> ( ( A e. ( span ` { A } ) /\ y e. ( _|_ ` ( span ` { A } ) ) ) -> ( A .ih y ) = 0 ) )
28 27 3impib 
 |-  ( ( ( span ` { A } ) e. SH /\ A e. ( span ` { A } ) /\ y e. ( _|_ ` ( span ` { A } ) ) ) -> ( A .ih y ) = 0 )
29 23 25 26 28 syl3anc 
 |-  ( ( A e. ~H /\ y e. ( _|_ ` ( span ` { A } ) ) ) -> ( A .ih y ) = 0 )
30 15 17 sylan 
 |-  ( ( A e. ~H /\ y e. ( _|_ ` ( span ` { A } ) ) ) -> y e. ~H )
31 orthcom 
 |-  ( ( A e. ~H /\ y e. ~H ) -> ( ( A .ih y ) = 0 <-> ( y .ih A ) = 0 ) )
32 30 31 syldan 
 |-  ( ( A e. ~H /\ y e. ( _|_ ` ( span ` { A } ) ) ) -> ( ( A .ih y ) = 0 <-> ( y .ih A ) = 0 ) )
33 29 32 mpbid 
 |-  ( ( A e. ~H /\ y e. ( _|_ ` ( span ` { A } ) ) ) -> ( y .ih A ) = 0 )
34 33 3ad2antl1 
 |-  ( ( ( A e. ~H /\ B e. ~H /\ A =/= 0h ) /\ y e. ( _|_ ` ( span ` { A } ) ) ) -> ( y .ih A ) = 0 )
35 34 oveq2d 
 |-  ( ( ( A e. ~H /\ B e. ~H /\ A =/= 0h ) /\ y e. ( _|_ ` ( span ` { A } ) ) ) -> ( ( ( ( projh ` ( span ` { A } ) ) ` B ) .ih A ) + ( y .ih A ) ) = ( ( ( ( projh ` ( span ` { A } ) ) ` B ) .ih A ) + 0 ) )
36 hicl 
 |-  ( ( ( ( projh ` ( span ` { A } ) ) ` B ) e. ~H /\ A e. ~H ) -> ( ( ( projh ` ( span ` { A } ) ) ` B ) .ih A ) e. CC )
37 13 19 36 syl2anc 
 |-  ( ( ( A e. ~H /\ B e. ~H /\ A =/= 0h ) /\ y e. ( _|_ ` ( span ` { A } ) ) ) -> ( ( ( projh ` ( span ` { A } ) ) ` B ) .ih A ) e. CC )
38 37 addid1d 
 |-  ( ( ( A e. ~H /\ B e. ~H /\ A =/= 0h ) /\ y e. ( _|_ ` ( span ` { A } ) ) ) -> ( ( ( ( projh ` ( span ` { A } ) ) ` B ) .ih A ) + 0 ) = ( ( ( projh ` ( span ` { A } ) ) ` B ) .ih A ) )
39 21 35 38 3eqtrd 
 |-  ( ( ( A e. ~H /\ B e. ~H /\ A =/= 0h ) /\ y e. ( _|_ ` ( span ` { A } ) ) ) -> ( ( ( ( projh ` ( span ` { A } ) ) ` B ) +h y ) .ih A ) = ( ( ( projh ` ( span ` { A } ) ) ` B ) .ih A ) )
40 39 adantrr 
 |-  ( ( ( A e. ~H /\ B e. ~H /\ A =/= 0h ) /\ ( y e. ( _|_ ` ( span ` { A } ) ) /\ B = ( ( ( projh ` ( span ` { A } ) ) ` B ) +h y ) ) ) -> ( ( ( ( projh ` ( span ` { A } ) ) ` B ) +h y ) .ih A ) = ( ( ( projh ` ( span ` { A } ) ) ` B ) .ih A ) )
41 10 40 eqtrd 
 |-  ( ( ( A e. ~H /\ B e. ~H /\ A =/= 0h ) /\ ( y e. ( _|_ ` ( span ` { A } ) ) /\ B = ( ( ( projh ` ( span ` { A } ) ) ` B ) +h y ) ) ) -> ( B .ih A ) = ( ( ( projh ` ( span ` { A } ) ) ` B ) .ih A ) )
42 41 oveq1d 
 |-  ( ( ( A e. ~H /\ B e. ~H /\ A =/= 0h ) /\ ( y e. ( _|_ ` ( span ` { A } ) ) /\ B = ( ( ( projh ` ( span ` { A } ) ) ` B ) +h y ) ) ) -> ( ( B .ih A ) / ( ( normh ` A ) ^ 2 ) ) = ( ( ( ( projh ` ( span ` { A } ) ) ` B ) .ih A ) / ( ( normh ` A ) ^ 2 ) ) )
43 42 oveq1d 
 |-  ( ( ( A e. ~H /\ B e. ~H /\ A =/= 0h ) /\ ( y e. ( _|_ ` ( span ` { A } ) ) /\ B = ( ( ( projh ` ( span ` { A } ) ) ` B ) +h y ) ) ) -> ( ( ( B .ih A ) / ( ( normh ` A ) ^ 2 ) ) .h A ) = ( ( ( ( ( projh ` ( span ` { A } ) ) ` B ) .ih A ) / ( ( normh ` A ) ^ 2 ) ) .h A ) )
44 simpl1 
 |-  ( ( ( A e. ~H /\ B e. ~H /\ A =/= 0h ) /\ ( y e. ( _|_ ` ( span ` { A } ) ) /\ B = ( ( ( projh ` ( span ` { A } ) ) ` B ) +h y ) ) ) -> A e. ~H )
45 simpl3 
 |-  ( ( ( A e. ~H /\ B e. ~H /\ A =/= 0h ) /\ ( y e. ( _|_ ` ( span ` { A } ) ) /\ B = ( ( ( projh ` ( span ` { A } ) ) ` B ) +h y ) ) ) -> A =/= 0h )
46 axpjcl 
 |-  ( ( ( span ` { A } ) e. CH /\ B e. ~H ) -> ( ( projh ` ( span ` { A } ) ) ` B ) e. ( span ` { A } ) )
47 2 3 46 syl2anc 
 |-  ( ( A e. ~H /\ B e. ~H /\ A =/= 0h ) -> ( ( projh ` ( span ` { A } ) ) ` B ) e. ( span ` { A } ) )
48 47 adantr 
 |-  ( ( ( A e. ~H /\ B e. ~H /\ A =/= 0h ) /\ ( y e. ( _|_ ` ( span ` { A } ) ) /\ B = ( ( ( projh ` ( span ` { A } ) ) ` B ) +h y ) ) ) -> ( ( projh ` ( span ` { A } ) ) ` B ) e. ( span ` { A } ) )
49 normcan 
 |-  ( ( A e. ~H /\ A =/= 0h /\ ( ( projh ` ( span ` { A } ) ) ` B ) e. ( span ` { A } ) ) -> ( ( ( ( ( projh ` ( span ` { A } ) ) ` B ) .ih A ) / ( ( normh ` A ) ^ 2 ) ) .h A ) = ( ( projh ` ( span ` { A } ) ) ` B ) )
50 44 45 48 49 syl3anc 
 |-  ( ( ( A e. ~H /\ B e. ~H /\ A =/= 0h ) /\ ( y e. ( _|_ ` ( span ` { A } ) ) /\ B = ( ( ( projh ` ( span ` { A } ) ) ` B ) +h y ) ) ) -> ( ( ( ( ( projh ` ( span ` { A } ) ) ` B ) .ih A ) / ( ( normh ` A ) ^ 2 ) ) .h A ) = ( ( projh ` ( span ` { A } ) ) ` B ) )
51 43 50 eqtr2d 
 |-  ( ( ( A e. ~H /\ B e. ~H /\ A =/= 0h ) /\ ( y e. ( _|_ ` ( span ` { A } ) ) /\ B = ( ( ( projh ` ( span ` { A } ) ) ` B ) +h y ) ) ) -> ( ( projh ` ( span ` { A } ) ) ` B ) = ( ( ( B .ih A ) / ( ( normh ` A ) ^ 2 ) ) .h A ) )
52 8 51 rexlimddv 
 |-  ( ( A e. ~H /\ B e. ~H /\ A =/= 0h ) -> ( ( projh ` ( span ` { A } ) ) ` B ) = ( ( ( B .ih A ) / ( ( normh ` A ) ^ 2 ) ) .h A ) )