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