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 ) )