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 ( ( ๐ด โˆˆ โ„‹ โˆง ๐ต โˆˆ โ„‹ โˆง ๐ด โ‰  0โ„Ž ) โ†’ ( ( projโ„Ž โ€˜ ( span โ€˜ { ๐ด } ) ) โ€˜ ๐ต ) = ( ( ( ๐ต ยทih ๐ด ) / ( ( normโ„Ž โ€˜ ๐ด ) โ†‘ 2 ) ) ยทโ„Ž ๐ด ) )

Proof

Step Hyp Ref Expression
1 spansnch โŠข ( ๐ด โˆˆ โ„‹ โ†’ ( span โ€˜ { ๐ด } ) โˆˆ Cโ„‹ )
2 1 3ad2ant1 โŠข ( ( ๐ด โˆˆ โ„‹ โˆง ๐ต โˆˆ โ„‹ โˆง ๐ด โ‰  0โ„Ž ) โ†’ ( span โ€˜ { ๐ด } ) โˆˆ Cโ„‹ )
3 simp2 โŠข ( ( ๐ด โˆˆ โ„‹ โˆง ๐ต โˆˆ โ„‹ โˆง ๐ด โ‰  0โ„Ž ) โ†’ ๐ต โˆˆ โ„‹ )
4 eqid โŠข ( ( projโ„Ž โ€˜ ( span โ€˜ { ๐ด } ) ) โ€˜ ๐ต ) = ( ( projโ„Ž โ€˜ ( span โ€˜ { ๐ด } ) ) โ€˜ ๐ต )
5 pjeq โŠข ( ( ( span โ€˜ { ๐ด } ) โˆˆ Cโ„‹ โˆง ๐ต โˆˆ โ„‹ ) โ†’ ( ( ( projโ„Ž โ€˜ ( span โ€˜ { ๐ด } ) ) โ€˜ ๐ต ) = ( ( projโ„Ž โ€˜ ( span โ€˜ { ๐ด } ) ) โ€˜ ๐ต ) โ†” ( ( ( projโ„Ž โ€˜ ( span โ€˜ { ๐ด } ) ) โ€˜ ๐ต ) โˆˆ ( span โ€˜ { ๐ด } ) โˆง โˆƒ ๐‘ฆ โˆˆ ( โŠฅ โ€˜ ( span โ€˜ { ๐ด } ) ) ๐ต = ( ( ( projโ„Ž โ€˜ ( span โ€˜ { ๐ด } ) ) โ€˜ ๐ต ) +โ„Ž ๐‘ฆ ) ) ) )
6 4 5 mpbii โŠข ( ( ( span โ€˜ { ๐ด } ) โˆˆ Cโ„‹ โˆง ๐ต โˆˆ โ„‹ ) โ†’ ( ( ( projโ„Ž โ€˜ ( span โ€˜ { ๐ด } ) ) โ€˜ ๐ต ) โˆˆ ( span โ€˜ { ๐ด } ) โˆง โˆƒ ๐‘ฆ โˆˆ ( โŠฅ โ€˜ ( span โ€˜ { ๐ด } ) ) ๐ต = ( ( ( projโ„Ž โ€˜ ( span โ€˜ { ๐ด } ) ) โ€˜ ๐ต ) +โ„Ž ๐‘ฆ ) ) )
7 6 simprd โŠข ( ( ( span โ€˜ { ๐ด } ) โˆˆ Cโ„‹ โˆง ๐ต โˆˆ โ„‹ ) โ†’ โˆƒ ๐‘ฆ โˆˆ ( โŠฅ โ€˜ ( span โ€˜ { ๐ด } ) ) ๐ต = ( ( ( projโ„Ž โ€˜ ( span โ€˜ { ๐ด } ) ) โ€˜ ๐ต ) +โ„Ž ๐‘ฆ ) )
8 2 3 7 syl2anc โŠข ( ( ๐ด โˆˆ โ„‹ โˆง ๐ต โˆˆ โ„‹ โˆง ๐ด โ‰  0โ„Ž ) โ†’ โˆƒ ๐‘ฆ โˆˆ ( โŠฅ โ€˜ ( span โ€˜ { ๐ด } ) ) ๐ต = ( ( ( projโ„Ž โ€˜ ( span โ€˜ { ๐ด } ) ) โ€˜ ๐ต ) +โ„Ž ๐‘ฆ ) )
9 oveq1 โŠข ( ๐ต = ( ( ( projโ„Ž โ€˜ ( span โ€˜ { ๐ด } ) ) โ€˜ ๐ต ) +โ„Ž ๐‘ฆ ) โ†’ ( ๐ต ยทih ๐ด ) = ( ( ( ( projโ„Ž โ€˜ ( span โ€˜ { ๐ด } ) ) โ€˜ ๐ต ) +โ„Ž ๐‘ฆ ) ยทih ๐ด ) )
10 9 ad2antll โŠข ( ( ( ๐ด โˆˆ โ„‹ โˆง ๐ต โˆˆ โ„‹ โˆง ๐ด โ‰  0โ„Ž ) โˆง ( ๐‘ฆ โˆˆ ( โŠฅ โ€˜ ( span โ€˜ { ๐ด } ) ) โˆง ๐ต = ( ( ( projโ„Ž โ€˜ ( span โ€˜ { ๐ด } ) ) โ€˜ ๐ต ) +โ„Ž ๐‘ฆ ) ) ) โ†’ ( ๐ต ยทih ๐ด ) = ( ( ( ( projโ„Ž โ€˜ ( span โ€˜ { ๐ด } ) ) โ€˜ ๐ต ) +โ„Ž ๐‘ฆ ) ยทih ๐ด ) )
11 pjhcl โŠข ( ( ( span โ€˜ { ๐ด } ) โˆˆ Cโ„‹ โˆง ๐ต โˆˆ โ„‹ ) โ†’ ( ( projโ„Ž โ€˜ ( span โ€˜ { ๐ด } ) ) โ€˜ ๐ต ) โˆˆ โ„‹ )
12 2 3 11 syl2anc โŠข ( ( ๐ด โˆˆ โ„‹ โˆง ๐ต โˆˆ โ„‹ โˆง ๐ด โ‰  0โ„Ž ) โ†’ ( ( projโ„Ž โ€˜ ( span โ€˜ { ๐ด } ) ) โ€˜ ๐ต ) โˆˆ โ„‹ )
13 12 adantr โŠข ( ( ( ๐ด โˆˆ โ„‹ โˆง ๐ต โˆˆ โ„‹ โˆง ๐ด โ‰  0โ„Ž ) โˆง ๐‘ฆ โˆˆ ( โŠฅ โ€˜ ( span โ€˜ { ๐ด } ) ) ) โ†’ ( ( projโ„Ž โ€˜ ( span โ€˜ { ๐ด } ) ) โ€˜ ๐ต ) โˆˆ โ„‹ )
14 choccl โŠข ( ( span โ€˜ { ๐ด } ) โˆˆ Cโ„‹ โ†’ ( โŠฅ โ€˜ ( span โ€˜ { ๐ด } ) ) โˆˆ Cโ„‹ )
15 1 14 syl โŠข ( ๐ด โˆˆ โ„‹ โ†’ ( โŠฅ โ€˜ ( span โ€˜ { ๐ด } ) ) โˆˆ Cโ„‹ )
16 15 3ad2ant1 โŠข ( ( ๐ด โˆˆ โ„‹ โˆง ๐ต โˆˆ โ„‹ โˆง ๐ด โ‰  0โ„Ž ) โ†’ ( โŠฅ โ€˜ ( span โ€˜ { ๐ด } ) ) โˆˆ Cโ„‹ )
17 chel โŠข ( ( ( โŠฅ โ€˜ ( span โ€˜ { ๐ด } ) ) โˆˆ Cโ„‹ โˆง ๐‘ฆ โˆˆ ( โŠฅ โ€˜ ( span โ€˜ { ๐ด } ) ) ) โ†’ ๐‘ฆ โˆˆ โ„‹ )
18 16 17 sylan โŠข ( ( ( ๐ด โˆˆ โ„‹ โˆง ๐ต โˆˆ โ„‹ โˆง ๐ด โ‰  0โ„Ž ) โˆง ๐‘ฆ โˆˆ ( โŠฅ โ€˜ ( span โ€˜ { ๐ด } ) ) ) โ†’ ๐‘ฆ โˆˆ โ„‹ )
19 simpl1 โŠข ( ( ( ๐ด โˆˆ โ„‹ โˆง ๐ต โˆˆ โ„‹ โˆง ๐ด โ‰  0โ„Ž ) โˆง ๐‘ฆ โˆˆ ( โŠฅ โ€˜ ( span โ€˜ { ๐ด } ) ) ) โ†’ ๐ด โˆˆ โ„‹ )
20 ax-his2 โŠข ( ( ( ( projโ„Ž โ€˜ ( span โ€˜ { ๐ด } ) ) โ€˜ ๐ต ) โˆˆ โ„‹ โˆง ๐‘ฆ โˆˆ โ„‹ โˆง ๐ด โˆˆ โ„‹ ) โ†’ ( ( ( ( projโ„Ž โ€˜ ( span โ€˜ { ๐ด } ) ) โ€˜ ๐ต ) +โ„Ž ๐‘ฆ ) ยทih ๐ด ) = ( ( ( ( projโ„Ž โ€˜ ( span โ€˜ { ๐ด } ) ) โ€˜ ๐ต ) ยทih ๐ด ) + ( ๐‘ฆ ยทih ๐ด ) ) )
21 13 18 19 20 syl3anc โŠข ( ( ( ๐ด โˆˆ โ„‹ โˆง ๐ต โˆˆ โ„‹ โˆง ๐ด โ‰  0โ„Ž ) โˆง ๐‘ฆ โˆˆ ( โŠฅ โ€˜ ( span โ€˜ { ๐ด } ) ) ) โ†’ ( ( ( ( projโ„Ž โ€˜ ( span โ€˜ { ๐ด } ) ) โ€˜ ๐ต ) +โ„Ž ๐‘ฆ ) ยทih ๐ด ) = ( ( ( ( projโ„Ž โ€˜ ( span โ€˜ { ๐ด } ) ) โ€˜ ๐ต ) ยทih ๐ด ) + ( ๐‘ฆ ยทih ๐ด ) ) )
22 spansnsh โŠข ( ๐ด โˆˆ โ„‹ โ†’ ( span โ€˜ { ๐ด } ) โˆˆ Sโ„‹ )
23 22 adantr โŠข ( ( ๐ด โˆˆ โ„‹ โˆง ๐‘ฆ โˆˆ ( โŠฅ โ€˜ ( span โ€˜ { ๐ด } ) ) ) โ†’ ( span โ€˜ { ๐ด } ) โˆˆ Sโ„‹ )
24 spansnid โŠข ( ๐ด โˆˆ โ„‹ โ†’ ๐ด โˆˆ ( span โ€˜ { ๐ด } ) )
25 24 adantr โŠข ( ( ๐ด โˆˆ โ„‹ โˆง ๐‘ฆ โˆˆ ( โŠฅ โ€˜ ( span โ€˜ { ๐ด } ) ) ) โ†’ ๐ด โˆˆ ( span โ€˜ { ๐ด } ) )
26 simpr โŠข ( ( ๐ด โˆˆ โ„‹ โˆง ๐‘ฆ โˆˆ ( โŠฅ โ€˜ ( span โ€˜ { ๐ด } ) ) ) โ†’ ๐‘ฆ โˆˆ ( โŠฅ โ€˜ ( span โ€˜ { ๐ด } ) ) )
27 shocorth โŠข ( ( span โ€˜ { ๐ด } ) โˆˆ Sโ„‹ โ†’ ( ( ๐ด โˆˆ ( span โ€˜ { ๐ด } ) โˆง ๐‘ฆ โˆˆ ( โŠฅ โ€˜ ( span โ€˜ { ๐ด } ) ) ) โ†’ ( ๐ด ยทih ๐‘ฆ ) = 0 ) )
28 27 3impib โŠข ( ( ( span โ€˜ { ๐ด } ) โˆˆ Sโ„‹ โˆง ๐ด โˆˆ ( span โ€˜ { ๐ด } ) โˆง ๐‘ฆ โˆˆ ( โŠฅ โ€˜ ( span โ€˜ { ๐ด } ) ) ) โ†’ ( ๐ด ยทih ๐‘ฆ ) = 0 )
29 23 25 26 28 syl3anc โŠข ( ( ๐ด โˆˆ โ„‹ โˆง ๐‘ฆ โˆˆ ( โŠฅ โ€˜ ( span โ€˜ { ๐ด } ) ) ) โ†’ ( ๐ด ยทih ๐‘ฆ ) = 0 )
30 15 17 sylan โŠข ( ( ๐ด โˆˆ โ„‹ โˆง ๐‘ฆ โˆˆ ( โŠฅ โ€˜ ( span โ€˜ { ๐ด } ) ) ) โ†’ ๐‘ฆ โˆˆ โ„‹ )
31 orthcom โŠข ( ( ๐ด โˆˆ โ„‹ โˆง ๐‘ฆ โˆˆ โ„‹ ) โ†’ ( ( ๐ด ยทih ๐‘ฆ ) = 0 โ†” ( ๐‘ฆ ยทih ๐ด ) = 0 ) )
32 30 31 syldan โŠข ( ( ๐ด โˆˆ โ„‹ โˆง ๐‘ฆ โˆˆ ( โŠฅ โ€˜ ( span โ€˜ { ๐ด } ) ) ) โ†’ ( ( ๐ด ยทih ๐‘ฆ ) = 0 โ†” ( ๐‘ฆ ยทih ๐ด ) = 0 ) )
33 29 32 mpbid โŠข ( ( ๐ด โˆˆ โ„‹ โˆง ๐‘ฆ โˆˆ ( โŠฅ โ€˜ ( span โ€˜ { ๐ด } ) ) ) โ†’ ( ๐‘ฆ ยทih ๐ด ) = 0 )
34 33 3ad2antl1 โŠข ( ( ( ๐ด โˆˆ โ„‹ โˆง ๐ต โˆˆ โ„‹ โˆง ๐ด โ‰  0โ„Ž ) โˆง ๐‘ฆ โˆˆ ( โŠฅ โ€˜ ( span โ€˜ { ๐ด } ) ) ) โ†’ ( ๐‘ฆ ยทih ๐ด ) = 0 )
35 34 oveq2d โŠข ( ( ( ๐ด โˆˆ โ„‹ โˆง ๐ต โˆˆ โ„‹ โˆง ๐ด โ‰  0โ„Ž ) โˆง ๐‘ฆ โˆˆ ( โŠฅ โ€˜ ( span โ€˜ { ๐ด } ) ) ) โ†’ ( ( ( ( projโ„Ž โ€˜ ( span โ€˜ { ๐ด } ) ) โ€˜ ๐ต ) ยทih ๐ด ) + ( ๐‘ฆ ยทih ๐ด ) ) = ( ( ( ( projโ„Ž โ€˜ ( span โ€˜ { ๐ด } ) ) โ€˜ ๐ต ) ยทih ๐ด ) + 0 ) )
36 hicl โŠข ( ( ( ( projโ„Ž โ€˜ ( span โ€˜ { ๐ด } ) ) โ€˜ ๐ต ) โˆˆ โ„‹ โˆง ๐ด โˆˆ โ„‹ ) โ†’ ( ( ( projโ„Ž โ€˜ ( span โ€˜ { ๐ด } ) ) โ€˜ ๐ต ) ยทih ๐ด ) โˆˆ โ„‚ )
37 13 19 36 syl2anc โŠข ( ( ( ๐ด โˆˆ โ„‹ โˆง ๐ต โˆˆ โ„‹ โˆง ๐ด โ‰  0โ„Ž ) โˆง ๐‘ฆ โˆˆ ( โŠฅ โ€˜ ( span โ€˜ { ๐ด } ) ) ) โ†’ ( ( ( projโ„Ž โ€˜ ( span โ€˜ { ๐ด } ) ) โ€˜ ๐ต ) ยทih ๐ด ) โˆˆ โ„‚ )
38 37 addridd โŠข ( ( ( ๐ด โˆˆ โ„‹ โˆง ๐ต โˆˆ โ„‹ โˆง ๐ด โ‰  0โ„Ž ) โˆง ๐‘ฆ โˆˆ ( โŠฅ โ€˜ ( span โ€˜ { ๐ด } ) ) ) โ†’ ( ( ( ( projโ„Ž โ€˜ ( span โ€˜ { ๐ด } ) ) โ€˜ ๐ต ) ยทih ๐ด ) + 0 ) = ( ( ( projโ„Ž โ€˜ ( span โ€˜ { ๐ด } ) ) โ€˜ ๐ต ) ยทih ๐ด ) )
39 21 35 38 3eqtrd โŠข ( ( ( ๐ด โˆˆ โ„‹ โˆง ๐ต โˆˆ โ„‹ โˆง ๐ด โ‰  0โ„Ž ) โˆง ๐‘ฆ โˆˆ ( โŠฅ โ€˜ ( span โ€˜ { ๐ด } ) ) ) โ†’ ( ( ( ( projโ„Ž โ€˜ ( span โ€˜ { ๐ด } ) ) โ€˜ ๐ต ) +โ„Ž ๐‘ฆ ) ยทih ๐ด ) = ( ( ( projโ„Ž โ€˜ ( span โ€˜ { ๐ด } ) ) โ€˜ ๐ต ) ยทih ๐ด ) )
40 39 adantrr โŠข ( ( ( ๐ด โˆˆ โ„‹ โˆง ๐ต โˆˆ โ„‹ โˆง ๐ด โ‰  0โ„Ž ) โˆง ( ๐‘ฆ โˆˆ ( โŠฅ โ€˜ ( span โ€˜ { ๐ด } ) ) โˆง ๐ต = ( ( ( projโ„Ž โ€˜ ( span โ€˜ { ๐ด } ) ) โ€˜ ๐ต ) +โ„Ž ๐‘ฆ ) ) ) โ†’ ( ( ( ( projโ„Ž โ€˜ ( span โ€˜ { ๐ด } ) ) โ€˜ ๐ต ) +โ„Ž ๐‘ฆ ) ยทih ๐ด ) = ( ( ( projโ„Ž โ€˜ ( span โ€˜ { ๐ด } ) ) โ€˜ ๐ต ) ยทih ๐ด ) )
41 10 40 eqtrd โŠข ( ( ( ๐ด โˆˆ โ„‹ โˆง ๐ต โˆˆ โ„‹ โˆง ๐ด โ‰  0โ„Ž ) โˆง ( ๐‘ฆ โˆˆ ( โŠฅ โ€˜ ( span โ€˜ { ๐ด } ) ) โˆง ๐ต = ( ( ( projโ„Ž โ€˜ ( span โ€˜ { ๐ด } ) ) โ€˜ ๐ต ) +โ„Ž ๐‘ฆ ) ) ) โ†’ ( ๐ต ยทih ๐ด ) = ( ( ( projโ„Ž โ€˜ ( span โ€˜ { ๐ด } ) ) โ€˜ ๐ต ) ยทih ๐ด ) )
42 41 oveq1d โŠข ( ( ( ๐ด โˆˆ โ„‹ โˆง ๐ต โˆˆ โ„‹ โˆง ๐ด โ‰  0โ„Ž ) โˆง ( ๐‘ฆ โˆˆ ( โŠฅ โ€˜ ( span โ€˜ { ๐ด } ) ) โˆง ๐ต = ( ( ( projโ„Ž โ€˜ ( span โ€˜ { ๐ด } ) ) โ€˜ ๐ต ) +โ„Ž ๐‘ฆ ) ) ) โ†’ ( ( ๐ต ยทih ๐ด ) / ( ( normโ„Ž โ€˜ ๐ด ) โ†‘ 2 ) ) = ( ( ( ( projโ„Ž โ€˜ ( span โ€˜ { ๐ด } ) ) โ€˜ ๐ต ) ยทih ๐ด ) / ( ( normโ„Ž โ€˜ ๐ด ) โ†‘ 2 ) ) )
43 42 oveq1d โŠข ( ( ( ๐ด โˆˆ โ„‹ โˆง ๐ต โˆˆ โ„‹ โˆง ๐ด โ‰  0โ„Ž ) โˆง ( ๐‘ฆ โˆˆ ( โŠฅ โ€˜ ( span โ€˜ { ๐ด } ) ) โˆง ๐ต = ( ( ( projโ„Ž โ€˜ ( span โ€˜ { ๐ด } ) ) โ€˜ ๐ต ) +โ„Ž ๐‘ฆ ) ) ) โ†’ ( ( ( ๐ต ยทih ๐ด ) / ( ( normโ„Ž โ€˜ ๐ด ) โ†‘ 2 ) ) ยทโ„Ž ๐ด ) = ( ( ( ( ( projโ„Ž โ€˜ ( span โ€˜ { ๐ด } ) ) โ€˜ ๐ต ) ยทih ๐ด ) / ( ( normโ„Ž โ€˜ ๐ด ) โ†‘ 2 ) ) ยทโ„Ž ๐ด ) )
44 simpl1 โŠข ( ( ( ๐ด โˆˆ โ„‹ โˆง ๐ต โˆˆ โ„‹ โˆง ๐ด โ‰  0โ„Ž ) โˆง ( ๐‘ฆ โˆˆ ( โŠฅ โ€˜ ( span โ€˜ { ๐ด } ) ) โˆง ๐ต = ( ( ( projโ„Ž โ€˜ ( span โ€˜ { ๐ด } ) ) โ€˜ ๐ต ) +โ„Ž ๐‘ฆ ) ) ) โ†’ ๐ด โˆˆ โ„‹ )
45 simpl3 โŠข ( ( ( ๐ด โˆˆ โ„‹ โˆง ๐ต โˆˆ โ„‹ โˆง ๐ด โ‰  0โ„Ž ) โˆง ( ๐‘ฆ โˆˆ ( โŠฅ โ€˜ ( span โ€˜ { ๐ด } ) ) โˆง ๐ต = ( ( ( projโ„Ž โ€˜ ( span โ€˜ { ๐ด } ) ) โ€˜ ๐ต ) +โ„Ž ๐‘ฆ ) ) ) โ†’ ๐ด โ‰  0โ„Ž )
46 axpjcl โŠข ( ( ( span โ€˜ { ๐ด } ) โˆˆ Cโ„‹ โˆง ๐ต โˆˆ โ„‹ ) โ†’ ( ( projโ„Ž โ€˜ ( span โ€˜ { ๐ด } ) ) โ€˜ ๐ต ) โˆˆ ( span โ€˜ { ๐ด } ) )
47 2 3 46 syl2anc โŠข ( ( ๐ด โˆˆ โ„‹ โˆง ๐ต โˆˆ โ„‹ โˆง ๐ด โ‰  0โ„Ž ) โ†’ ( ( projโ„Ž โ€˜ ( span โ€˜ { ๐ด } ) ) โ€˜ ๐ต ) โˆˆ ( span โ€˜ { ๐ด } ) )
48 47 adantr โŠข ( ( ( ๐ด โˆˆ โ„‹ โˆง ๐ต โˆˆ โ„‹ โˆง ๐ด โ‰  0โ„Ž ) โˆง ( ๐‘ฆ โˆˆ ( โŠฅ โ€˜ ( span โ€˜ { ๐ด } ) ) โˆง ๐ต = ( ( ( projโ„Ž โ€˜ ( span โ€˜ { ๐ด } ) ) โ€˜ ๐ต ) +โ„Ž ๐‘ฆ ) ) ) โ†’ ( ( projโ„Ž โ€˜ ( span โ€˜ { ๐ด } ) ) โ€˜ ๐ต ) โˆˆ ( span โ€˜ { ๐ด } ) )
49 normcan โŠข ( ( ๐ด โˆˆ โ„‹ โˆง ๐ด โ‰  0โ„Ž โˆง ( ( projโ„Ž โ€˜ ( span โ€˜ { ๐ด } ) ) โ€˜ ๐ต ) โˆˆ ( span โ€˜ { ๐ด } ) ) โ†’ ( ( ( ( ( projโ„Ž โ€˜ ( span โ€˜ { ๐ด } ) ) โ€˜ ๐ต ) ยทih ๐ด ) / ( ( normโ„Ž โ€˜ ๐ด ) โ†‘ 2 ) ) ยทโ„Ž ๐ด ) = ( ( projโ„Ž โ€˜ ( span โ€˜ { ๐ด } ) ) โ€˜ ๐ต ) )
50 44 45 48 49 syl3anc โŠข ( ( ( ๐ด โˆˆ โ„‹ โˆง ๐ต โˆˆ โ„‹ โˆง ๐ด โ‰  0โ„Ž ) โˆง ( ๐‘ฆ โˆˆ ( โŠฅ โ€˜ ( span โ€˜ { ๐ด } ) ) โˆง ๐ต = ( ( ( projโ„Ž โ€˜ ( span โ€˜ { ๐ด } ) ) โ€˜ ๐ต ) +โ„Ž ๐‘ฆ ) ) ) โ†’ ( ( ( ( ( projโ„Ž โ€˜ ( span โ€˜ { ๐ด } ) ) โ€˜ ๐ต ) ยทih ๐ด ) / ( ( normโ„Ž โ€˜ ๐ด ) โ†‘ 2 ) ) ยทโ„Ž ๐ด ) = ( ( projโ„Ž โ€˜ ( span โ€˜ { ๐ด } ) ) โ€˜ ๐ต ) )
51 43 50 eqtr2d โŠข ( ( ( ๐ด โˆˆ โ„‹ โˆง ๐ต โˆˆ โ„‹ โˆง ๐ด โ‰  0โ„Ž ) โˆง ( ๐‘ฆ โˆˆ ( โŠฅ โ€˜ ( span โ€˜ { ๐ด } ) ) โˆง ๐ต = ( ( ( projโ„Ž โ€˜ ( span โ€˜ { ๐ด } ) ) โ€˜ ๐ต ) +โ„Ž ๐‘ฆ ) ) ) โ†’ ( ( projโ„Ž โ€˜ ( span โ€˜ { ๐ด } ) ) โ€˜ ๐ต ) = ( ( ( ๐ต ยทih ๐ด ) / ( ( normโ„Ž โ€˜ ๐ด ) โ†‘ 2 ) ) ยทโ„Ž ๐ด ) )
52 8 51 rexlimddv โŠข ( ( ๐ด โˆˆ โ„‹ โˆง ๐ต โˆˆ โ„‹ โˆง ๐ด โ‰  0โ„Ž ) โ†’ ( ( projโ„Ž โ€˜ ( span โ€˜ { ๐ด } ) ) โ€˜ ๐ต ) = ( ( ( ๐ต ยทih ๐ด ) / ( ( normโ„Ž โ€˜ ๐ด ) โ†‘ 2 ) ) ยทโ„Ž ๐ด ) )