Metamath Proof Explorer

Theorem spansncol

Description: The singletons of collinear vectors have the same span. (Contributed by NM, 6-Jun-2004) (New usage is discouraged.)

Ref Expression
Assertion spansncol ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( span ‘ { ( 𝐵 ·ℎ 𝐴 ) } ) = ( span ‘ { 𝐴 } ) )

Proof

Step Hyp Ref Expression
1 mulcl ⊢ ( ( 𝑦 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝑦 · 𝐵 ) ∈ ℂ )
2 1 ancoms ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑦 · 𝐵 ) ∈ ℂ )
3 2 adantll ⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℂ ) ∧ 𝑦 ∈ ℂ ) → ( 𝑦 · 𝐵 ) ∈ ℂ )
4 ax-hvmulass ⊢ ( ( 𝑦 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐴 ∈ ℋ ) → ( ( 𝑦 · 𝐵 ) ·ℎ 𝐴 ) = ( 𝑦 ·ℎ ( 𝐵 ·ℎ 𝐴 ) ) )
5 4 3com13 ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( ( 𝑦 · 𝐵 ) ·ℎ 𝐴 ) = ( 𝑦 ·ℎ ( 𝐵 ·ℎ 𝐴 ) ) )
6 5 3expa ⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℂ ) ∧ 𝑦 ∈ ℂ ) → ( ( 𝑦 · 𝐵 ) ·ℎ 𝐴 ) = ( 𝑦 ·ℎ ( 𝐵 ·ℎ 𝐴 ) ) )
7 6 eqeq2d ⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℂ ) ∧ 𝑦 ∈ ℂ ) → ( 𝑥 = ( ( 𝑦 · 𝐵 ) ·ℎ 𝐴 ) ↔ 𝑥 = ( 𝑦 ·ℎ ( 𝐵 ·ℎ 𝐴 ) ) ) )
8 7 biimprd ⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℂ ) ∧ 𝑦 ∈ ℂ ) → ( 𝑥 = ( 𝑦 ·ℎ ( 𝐵 ·ℎ 𝐴 ) ) → 𝑥 = ( ( 𝑦 · 𝐵 ) ·ℎ 𝐴 ) ) )
9 oveq1 ⊢ ( 𝑧 = ( 𝑦 · 𝐵 ) → ( 𝑧 ·ℎ 𝐴 ) = ( ( 𝑦 · 𝐵 ) ·ℎ 𝐴 ) )
10 9 rspceeqv ⊢ ( ( ( 𝑦 · 𝐵 ) ∈ ℂ ∧ 𝑥 = ( ( 𝑦 · 𝐵 ) ·ℎ 𝐴 ) ) → ∃ 𝑧 ∈ ℂ 𝑥 = ( 𝑧 ·ℎ 𝐴 ) )
11 3 8 10 syl6an ⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℂ ) ∧ 𝑦 ∈ ℂ ) → ( 𝑥 = ( 𝑦 ·ℎ ( 𝐵 ·ℎ 𝐴 ) ) → ∃ 𝑧 ∈ ℂ 𝑥 = ( 𝑧 ·ℎ 𝐴 ) ) )
12 11 rexlimdva ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℂ ) → ( ∃ 𝑦 ∈ ℂ 𝑥 = ( 𝑦 ·ℎ ( 𝐵 ·ℎ 𝐴 ) ) → ∃ 𝑧 ∈ ℂ 𝑥 = ( 𝑧 ·ℎ 𝐴 ) ) )
13 12 3adant3 ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( ∃ 𝑦 ∈ ℂ 𝑥 = ( 𝑦 ·ℎ ( 𝐵 ·ℎ 𝐴 ) ) → ∃ 𝑧 ∈ ℂ 𝑥 = ( 𝑧 ·ℎ 𝐴 ) ) )
14 divcl ⊢ ( ( 𝑧 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( 𝑧 / 𝐵 ) ∈ ℂ )
15 14 3expb ⊢ ( ( 𝑧 ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) → ( 𝑧 / 𝐵 ) ∈ ℂ )
16 15 adantlr ⊢ ( ( ( 𝑧 ∈ ℂ ∧ 𝐴 ∈ ℋ ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) → ( 𝑧 / 𝐵 ) ∈ ℂ )
17 simprl ⊢ ( ( ( 𝑧 ∈ ℂ ∧ 𝐴 ∈ ℋ ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) → 𝐵 ∈ ℂ )
18 simplr ⊢ ( ( ( 𝑧 ∈ ℂ ∧ 𝐴 ∈ ℋ ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) → 𝐴 ∈ ℋ )
19 ax-hvmulass ⊢ ( ( ( 𝑧 / 𝐵 ) ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐴 ∈ ℋ ) → ( ( ( 𝑧 / 𝐵 ) · 𝐵 ) ·ℎ 𝐴 ) = ( ( 𝑧 / 𝐵 ) ·ℎ ( 𝐵 ·ℎ 𝐴 ) ) )
20 16 17 18 19 syl3anc ⊢ ( ( ( 𝑧 ∈ ℂ ∧ 𝐴 ∈ ℋ ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) → ( ( ( 𝑧 / 𝐵 ) · 𝐵 ) ·ℎ 𝐴 ) = ( ( 𝑧 / 𝐵 ) ·ℎ ( 𝐵 ·ℎ 𝐴 ) ) )
21 divcan1 ⊢ ( ( 𝑧 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( ( 𝑧 / 𝐵 ) · 𝐵 ) = 𝑧 )
22 21 3expb ⊢ ( ( 𝑧 ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) → ( ( 𝑧 / 𝐵 ) · 𝐵 ) = 𝑧 )
23 22 adantlr ⊢ ( ( ( 𝑧 ∈ ℂ ∧ 𝐴 ∈ ℋ ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) → ( ( 𝑧 / 𝐵 ) · 𝐵 ) = 𝑧 )
24 23 oveq1d ⊢ ( ( ( 𝑧 ∈ ℂ ∧ 𝐴 ∈ ℋ ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) → ( ( ( 𝑧 / 𝐵 ) · 𝐵 ) ·ℎ 𝐴 ) = ( 𝑧 ·ℎ 𝐴 ) )
25 20 24 eqtr3d ⊢ ( ( ( 𝑧 ∈ ℂ ∧ 𝐴 ∈ ℋ ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) → ( ( 𝑧 / 𝐵 ) ·ℎ ( 𝐵 ·ℎ 𝐴 ) ) = ( 𝑧 ·ℎ 𝐴 ) )
26 25 eqeq2d ⊢ ( ( ( 𝑧 ∈ ℂ ∧ 𝐴 ∈ ℋ ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) → ( 𝑥 = ( ( 𝑧 / 𝐵 ) ·ℎ ( 𝐵 ·ℎ 𝐴 ) ) ↔ 𝑥 = ( 𝑧 ·ℎ 𝐴 ) ) )
27 26 biimprd ⊢ ( ( ( 𝑧 ∈ ℂ ∧ 𝐴 ∈ ℋ ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) → ( 𝑥 = ( 𝑧 ·ℎ 𝐴 ) → 𝑥 = ( ( 𝑧 / 𝐵 ) ·ℎ ( 𝐵 ·ℎ 𝐴 ) ) ) )
28 oveq1 ⊢ ( 𝑦 = ( 𝑧 / 𝐵 ) → ( 𝑦 ·ℎ ( 𝐵 ·ℎ 𝐴 ) ) = ( ( 𝑧 / 𝐵 ) ·ℎ ( 𝐵 ·ℎ 𝐴 ) ) )
29 28 rspceeqv ⊢ ( ( ( 𝑧 / 𝐵 ) ∈ ℂ ∧ 𝑥 = ( ( 𝑧 / 𝐵 ) ·ℎ ( 𝐵 ·ℎ 𝐴 ) ) ) → ∃ 𝑦 ∈ ℂ 𝑥 = ( 𝑦 ·ℎ ( 𝐵 ·ℎ 𝐴 ) ) )
30 16 27 29 syl6an ⊢ ( ( ( 𝑧 ∈ ℂ ∧ 𝐴 ∈ ℋ ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) → ( 𝑥 = ( 𝑧 ·ℎ 𝐴 ) → ∃ 𝑦 ∈ ℂ 𝑥 = ( 𝑦 ·ℎ ( 𝐵 ·ℎ 𝐴 ) ) ) )
31 30 exp43 ⊢ ( 𝑧 ∈ ℂ → ( 𝐴 ∈ ℋ → ( 𝐵 ∈ ℂ → ( 𝐵 ≠ 0 → ( 𝑥 = ( 𝑧 ·ℎ 𝐴 ) → ∃ 𝑦 ∈ ℂ 𝑥 = ( 𝑦 ·ℎ ( 𝐵 ·ℎ 𝐴 ) ) ) ) ) ) )
32 31 com4l ⊢ ( 𝐴 ∈ ℋ → ( 𝐵 ∈ ℂ → ( 𝐵 ≠ 0 → ( 𝑧 ∈ ℂ → ( 𝑥 = ( 𝑧 ·ℎ 𝐴 ) → ∃ 𝑦 ∈ ℂ 𝑥 = ( 𝑦 ·ℎ ( 𝐵 ·ℎ 𝐴 ) ) ) ) ) ) )
33 32 3imp ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( 𝑧 ∈ ℂ → ( 𝑥 = ( 𝑧 ·ℎ 𝐴 ) → ∃ 𝑦 ∈ ℂ 𝑥 = ( 𝑦 ·ℎ ( 𝐵 ·ℎ 𝐴 ) ) ) ) )
34 33 rexlimdv ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( ∃ 𝑧 ∈ ℂ 𝑥 = ( 𝑧 ·ℎ 𝐴 ) → ∃ 𝑦 ∈ ℂ 𝑥 = ( 𝑦 ·ℎ ( 𝐵 ·ℎ 𝐴 ) ) ) )
35 13 34 impbid ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( ∃ 𝑦 ∈ ℂ 𝑥 = ( 𝑦 ·ℎ ( 𝐵 ·ℎ 𝐴 ) ) ↔ ∃ 𝑧 ∈ ℂ 𝑥 = ( 𝑧 ·ℎ 𝐴 ) ) )
36 hvmulcl ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐴 ∈ ℋ ) → ( 𝐵 ·ℎ 𝐴 ) ∈ ℋ )
37 36 ancoms ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℂ ) → ( 𝐵 ·ℎ 𝐴 ) ∈ ℋ )
38 elspansn ⊢ ( ( 𝐵 ·ℎ 𝐴 ) ∈ ℋ → ( 𝑥 ∈ ( span ‘ { ( 𝐵 ·ℎ 𝐴 ) } ) ↔ ∃ 𝑦 ∈ ℂ 𝑥 = ( 𝑦 ·ℎ ( 𝐵 ·ℎ 𝐴 ) ) ) )
39 37 38 syl ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℂ ) → ( 𝑥 ∈ ( span ‘ { ( 𝐵 ·ℎ 𝐴 ) } ) ↔ ∃ 𝑦 ∈ ℂ 𝑥 = ( 𝑦 ·ℎ ( 𝐵 ·ℎ 𝐴 ) ) ) )
40 39 3adant3 ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( 𝑥 ∈ ( span ‘ { ( 𝐵 ·ℎ 𝐴 ) } ) ↔ ∃ 𝑦 ∈ ℂ 𝑥 = ( 𝑦 ·ℎ ( 𝐵 ·ℎ 𝐴 ) ) ) )
41 elspansn ⊢ ( 𝐴 ∈ ℋ → ( 𝑥 ∈ ( span ‘ { 𝐴 } ) ↔ ∃ 𝑧 ∈ ℂ 𝑥 = ( 𝑧 ·ℎ 𝐴 ) ) )
42 41 3ad2ant1 ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( 𝑥 ∈ ( span ‘ { 𝐴 } ) ↔ ∃ 𝑧 ∈ ℂ 𝑥 = ( 𝑧 ·ℎ 𝐴 ) ) )
43 35 40 42 3bitr4d ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( 𝑥 ∈ ( span ‘ { ( 𝐵 ·ℎ 𝐴 ) } ) ↔ 𝑥 ∈ ( span ‘ { 𝐴 } ) ) )
44 43 eqrdv ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( span ‘ { ( 𝐵 ·ℎ 𝐴 ) } ) = ( span ‘ { 𝐴 } ) )