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 ) ) ·ℎ 𝐵 ) = 𝐴 )