Metamath Proof Explorer

Theorem spansneleq

Description: Membership relation that implies equality of spans. (Contributed by NM, 6-Jun-2004) (New usage is discouraged.)

Ref Expression
Assertion spansneleq ⊢ B ∈ ℋ ∧ A ≠ 0 ℎ → A ∈ span ⁡ B → span ⁡ A = span ⁡ B

Proof

Step Hyp Ref Expression
1 elspansn ⊢ B ∈ ℋ → A ∈ span ⁡ B ↔ ∃ x ∈ ℂ A = x ⋅ ℎ B
2 1 adantr ⊢ B ∈ ℋ ∧ A ≠ 0 ℎ → A ∈ span ⁡ B ↔ ∃ x ∈ ℂ A = x ⋅ ℎ B
3 sneq ⊢ A = x ⋅ ℎ B → A = x ⋅ ℎ B
4 3 fveq2d ⊢ A = x ⋅ ℎ B → span ⁡ A = span ⁡ x ⋅ ℎ B
5 4 ad2antll ⊢ B ∈ ℋ ∧ A ≠ 0 ℎ ∧ x ∈ ℂ ∧ A = x ⋅ ℎ B → span ⁡ A = span ⁡ x ⋅ ℎ B
6 oveq1 ⊢ x = 0 → x ⋅ ℎ B = 0 ⋅ ℎ B
7 ax-hvmul0 ⊢ B ∈ ℋ → 0 ⋅ ℎ B = 0 ℎ
8 6 7 sylan9eqr ⊢ B ∈ ℋ ∧ x = 0 → x ⋅ ℎ B = 0 ℎ
9 8 ex ⊢ B ∈ ℋ → x = 0 → x ⋅ ℎ B = 0 ℎ
10 eqeq1 ⊢ A = x ⋅ ℎ B → A = 0 ℎ ↔ x ⋅ ℎ B = 0 ℎ
11 10 biimprd ⊢ A = x ⋅ ℎ B → x ⋅ ℎ B = 0 ℎ → A = 0 ℎ
12 9 11 sylan9 ⊢ B ∈ ℋ ∧ A = x ⋅ ℎ B → x = 0 → A = 0 ℎ
13 12 necon3d ⊢ B ∈ ℋ ∧ A = x ⋅ ℎ B → A ≠ 0 ℎ → x ≠ 0
14 13 ex ⊢ B ∈ ℋ → A = x ⋅ ℎ B → A ≠ 0 ℎ → x ≠ 0
15 14 com23 ⊢ B ∈ ℋ → A ≠ 0 ℎ → A = x ⋅ ℎ B → x ≠ 0
16 15 impd ⊢ B ∈ ℋ → A ≠ 0 ℎ ∧ A = x ⋅ ℎ B → x ≠ 0
17 16 adantr ⊢ B ∈ ℋ ∧ x ∈ ℂ → A ≠ 0 ℎ ∧ A = x ⋅ ℎ B → x ≠ 0
18 spansncol ⊢ B ∈ ℋ ∧ x ∈ ℂ ∧ x ≠ 0 → span ⁡ x ⋅ ℎ B = span ⁡ B
19 18 3expia ⊢ B ∈ ℋ ∧ x ∈ ℂ → x ≠ 0 → span ⁡ x ⋅ ℎ B = span ⁡ B
20 17 19 syld ⊢ B ∈ ℋ ∧ x ∈ ℂ → A ≠ 0 ℎ ∧ A = x ⋅ ℎ B → span ⁡ x ⋅ ℎ B = span ⁡ B
21 20 exp4b ⊢ B ∈ ℋ → x ∈ ℂ → A ≠ 0 ℎ → A = x ⋅ ℎ B → span ⁡ x ⋅ ℎ B = span ⁡ B
22 21 com23 ⊢ B ∈ ℋ → A ≠ 0 ℎ → x ∈ ℂ → A = x ⋅ ℎ B → span ⁡ x ⋅ ℎ B = span ⁡ B
23 22 imp43 ⊢ B ∈ ℋ ∧ A ≠ 0 ℎ ∧ x ∈ ℂ ∧ A = x ⋅ ℎ B → span ⁡ x ⋅ ℎ B = span ⁡ B
24 5 23 eqtrd ⊢ B ∈ ℋ ∧ A ≠ 0 ℎ ∧ x ∈ ℂ ∧ A = x ⋅ ℎ B → span ⁡ A = span ⁡ B
25 24 rexlimdvaa ⊢ B ∈ ℋ ∧ A ≠ 0 ℎ → ∃ x ∈ ℂ A = x ⋅ ℎ B → span ⁡ A = span ⁡ B
26 2 25 sylbid ⊢ B ∈ ℋ ∧ A ≠ 0 ℎ → A ∈ span ⁡ B → span ⁡ A = span ⁡ B