This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem normcan

Description: Cancellation-type law that "extracts" a vector A from its inner product with a proportional vector B . (Contributed by NM, 18-Mar-2006) (New usage is discouraged.)

Ref Expression
Assertion normcan ( ( 𝐵 ∈ ℋ ∧ 𝐵 ≠ 0ℎ ∧ 𝐴 ∈ ( span ‘ { 𝐵 } ) ) → ( ( ( 𝐴 ·ih 𝐵 ) / ( ( normℎ ‘ 𝐵 ) ↑ 2 ) ) ·ℎ 𝐵 ) = 𝐴 )

Proof

Step Hyp Ref Expression
1 elspansn ⊢ ( 𝐵 ∈ ℋ → ( 𝐴 ∈ ( span ‘ { 𝐵 } ) ↔ ∃ 𝑥 ∈ ℂ 𝐴 = ( 𝑥 ·ℎ 𝐵 ) ) )
2 1 adantr ⊢ ( ( 𝐵 ∈ ℋ ∧ 𝐵 ≠ 0ℎ ) → ( 𝐴 ∈ ( span ‘ { 𝐵 } ) ↔ ∃ 𝑥 ∈ ℂ 𝐴 = ( 𝑥 ·ℎ 𝐵 ) ) )
3 oveq1 ⊢ ( 𝐴 = ( 𝑥 ·ℎ 𝐵 ) → ( 𝐴 ·ih 𝐵 ) = ( ( 𝑥 ·ℎ 𝐵 ) ·ih 𝐵 ) )
4 simpr ⊢ ( ( 𝐵 ∈ ℋ ∧ 𝑥 ∈ ℂ ) → 𝑥 ∈ ℂ )
5 simpl ⊢ ( ( 𝐵 ∈ ℋ ∧ 𝑥 ∈ ℂ ) → 𝐵 ∈ ℋ )
6 ax-his3 ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( ( 𝑥 ·ℎ 𝐵 ) ·ih 𝐵 ) = ( 𝑥 · ( 𝐵 ·ih 𝐵 ) ) )
7 4 5 5 6 syl3anc ⊢ ( ( 𝐵 ∈ ℋ ∧ 𝑥 ∈ ℂ ) → ( ( 𝑥 ·ℎ 𝐵 ) ·ih 𝐵 ) = ( 𝑥 · ( 𝐵 ·ih 𝐵 ) ) )
8 3 7 sylan9eqr ⊢ ( ( ( 𝐵 ∈ ℋ ∧ 𝑥 ∈ ℂ ) ∧ 𝐴 = ( 𝑥 ·ℎ 𝐵 ) ) → ( 𝐴 ·ih 𝐵 ) = ( 𝑥 · ( 𝐵 ·ih 𝐵 ) ) )
9 normsq ⊢ ( 𝐵 ∈ ℋ → ( ( normℎ ‘ 𝐵 ) ↑ 2 ) = ( 𝐵 ·ih 𝐵 ) )
10 9 ad2antrr ⊢ ( ( ( 𝐵 ∈ ℋ ∧ 𝑥 ∈ ℂ ) ∧ 𝐴 = ( 𝑥 ·ℎ 𝐵 ) ) → ( ( normℎ ‘ 𝐵 ) ↑ 2 ) = ( 𝐵 ·ih 𝐵 ) )
11 8 10 oveq12d ⊢ ( ( ( 𝐵 ∈ ℋ ∧ 𝑥 ∈ ℂ ) ∧ 𝐴 = ( 𝑥 ·ℎ 𝐵 ) ) → ( ( 𝐴 ·ih 𝐵 ) / ( ( normℎ ‘ 𝐵 ) ↑ 2 ) ) = ( ( 𝑥 · ( 𝐵 ·ih 𝐵 ) ) / ( 𝐵 ·ih 𝐵 ) ) )
12 11 adantllr ⊢ ( ( ( ( 𝐵 ∈ ℋ ∧ 𝐵 ≠ 0ℎ ) ∧ 𝑥 ∈ ℂ ) ∧ 𝐴 = ( 𝑥 ·ℎ 𝐵 ) ) → ( ( 𝐴 ·ih 𝐵 ) / ( ( normℎ ‘ 𝐵 ) ↑ 2 ) ) = ( ( 𝑥 · ( 𝐵 ·ih 𝐵 ) ) / ( 𝐵 ·ih 𝐵 ) ) )
13 simpr ⊢ ( ( ( 𝐵 ∈ ℋ ∧ 𝐵 ≠ 0ℎ ) ∧ 𝑥 ∈ ℂ ) → 𝑥 ∈ ℂ )
14 hicl ⊢ ( ( 𝐵 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( 𝐵 ·ih 𝐵 ) ∈ ℂ )
15 14 anidms ⊢ ( 𝐵 ∈ ℋ → ( 𝐵 ·ih 𝐵 ) ∈ ℂ )
16 15 ad2antrr ⊢ ( ( ( 𝐵 ∈ ℋ ∧ 𝐵 ≠ 0ℎ ) ∧ 𝑥 ∈ ℂ ) → ( 𝐵 ·ih 𝐵 ) ∈ ℂ )
17 his6 ⊢ ( 𝐵 ∈ ℋ → ( ( 𝐵 ·ih 𝐵 ) = 0 ↔ 𝐵 = 0ℎ ) )
18 17 necon3bid ⊢ ( 𝐵 ∈ ℋ → ( ( 𝐵 ·ih 𝐵 ) ≠ 0 ↔ 𝐵 ≠ 0ℎ ) )
19 18 biimpar ⊢ ( ( 𝐵 ∈ ℋ ∧ 𝐵 ≠ 0ℎ ) → ( 𝐵 ·ih 𝐵 ) ≠ 0 )
20 19 adantr ⊢ ( ( ( 𝐵 ∈ ℋ ∧ 𝐵 ≠ 0ℎ ) ∧ 𝑥 ∈ ℂ ) → ( 𝐵 ·ih 𝐵 ) ≠ 0 )
21 13 16 20 divcan4d ⊢ ( ( ( 𝐵 ∈ ℋ ∧ 𝐵 ≠ 0ℎ ) ∧ 𝑥 ∈ ℂ ) → ( ( 𝑥 · ( 𝐵 ·ih 𝐵 ) ) / ( 𝐵 ·ih 𝐵 ) ) = 𝑥 )
22 21 adantr ⊢ ( ( ( ( 𝐵 ∈ ℋ ∧ 𝐵 ≠ 0ℎ ) ∧ 𝑥 ∈ ℂ ) ∧ 𝐴 = ( 𝑥 ·ℎ 𝐵 ) ) → ( ( 𝑥 · ( 𝐵 ·ih 𝐵 ) ) / ( 𝐵 ·ih 𝐵 ) ) = 𝑥 )
23 12 22 eqtrd ⊢ ( ( ( ( 𝐵 ∈ ℋ ∧ 𝐵 ≠ 0ℎ ) ∧ 𝑥 ∈ ℂ ) ∧ 𝐴 = ( 𝑥 ·ℎ 𝐵 ) ) → ( ( 𝐴 ·ih 𝐵 ) / ( ( normℎ ‘ 𝐵 ) ↑ 2 ) ) = 𝑥 )
24 23 oveq1d ⊢ ( ( ( ( 𝐵 ∈ ℋ ∧ 𝐵 ≠ 0ℎ ) ∧ 𝑥 ∈ ℂ ) ∧ 𝐴 = ( 𝑥 ·ℎ 𝐵 ) ) → ( ( ( 𝐴 ·ih 𝐵 ) / ( ( normℎ ‘ 𝐵 ) ↑ 2 ) ) ·ℎ 𝐵 ) = ( 𝑥 ·ℎ 𝐵 ) )
25 simpr ⊢ ( ( ( ( 𝐵 ∈ ℋ ∧ 𝐵 ≠ 0ℎ ) ∧ 𝑥 ∈ ℂ ) ∧ 𝐴 = ( 𝑥 ·ℎ 𝐵 ) ) → 𝐴 = ( 𝑥 ·ℎ 𝐵 ) )
26 24 25 eqtr4d ⊢ ( ( ( ( 𝐵 ∈ ℋ ∧ 𝐵 ≠ 0ℎ ) ∧ 𝑥 ∈ ℂ ) ∧ 𝐴 = ( 𝑥 ·ℎ 𝐵 ) ) → ( ( ( 𝐴 ·ih 𝐵 ) / ( ( normℎ ‘ 𝐵 ) ↑ 2 ) ) ·ℎ 𝐵 ) = 𝐴 )
27 26 rexlimdva2 ⊢ ( ( 𝐵 ∈ ℋ ∧ 𝐵 ≠ 0ℎ ) → ( ∃ 𝑥 ∈ ℂ 𝐴 = ( 𝑥 ·ℎ 𝐵 ) → ( ( ( 𝐴 ·ih 𝐵 ) / ( ( normℎ ‘ 𝐵 ) ↑ 2 ) ) ·ℎ 𝐵 ) = 𝐴 ) )
28 2 27 sylbid ⊢ ( ( 𝐵 ∈ ℋ ∧ 𝐵 ≠ 0ℎ ) → ( 𝐴 ∈ ( span ‘ { 𝐵 } ) → ( ( ( 𝐴 ·ih 𝐵 ) / ( ( normℎ ‘ 𝐵 ) ↑ 2 ) ) ·ℎ 𝐵 ) = 𝐴 ) )
29 28 3impia ⊢ ( ( 𝐵 ∈ ℋ ∧ 𝐵 ≠ 0ℎ ∧ 𝐴 ∈ ( span ‘ { 𝐵 } ) ) → ( ( ( 𝐴 ·ih 𝐵 ) / ( ( normℎ ‘ 𝐵 ) ↑ 2 ) ) ·ℎ 𝐵 ) = 𝐴 )