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 ⊢ A ∈ ℋ ∧ B ∈ ℂ ∧ B ≠ 0 → span ⁡ B ⋅ ℎ A = span ⁡ A

Proof

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