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 addid1d ⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ≠ 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 ) ) ·ℎ 𝐴 ) )