Metamath Proof Explorer

Theorem elspansn4

Description: A span membership condition implying two vectors belong to the same subspace. (Contributed by NM, 17-Dec-2004) (New usage is discouraged.)

Ref Expression
Assertion elspansn4 ⊢ A ∈ S ℋ ∧ B ∈ ℋ ∧ C ∈ span ⁡ B ∧ C ≠ 0 ℎ → B ∈ A ↔ C ∈ A

Proof

Step Hyp Ref Expression
1 elspansn3 ⊢ A ∈ S ℋ ∧ B ∈ A ∧ C ∈ span ⁡ B → C ∈ A
2 1 3exp ⊢ A ∈ S ℋ → B ∈ A → C ∈ span ⁡ B → C ∈ A
3 2 com23 ⊢ A ∈ S ℋ → C ∈ span ⁡ B → B ∈ A → C ∈ A
4 3 imp ⊢ A ∈ S ℋ ∧ C ∈ span ⁡ B → B ∈ A → C ∈ A
5 4 ad2ant2r ⊢ A ∈ S ℋ ∧ B ∈ ℋ ∧ C ∈ span ⁡ B ∧ C ≠ 0 ℎ → B ∈ A → C ∈ A
6 spansnid ⊢ B ∈ ℋ → B ∈ span ⁡ B
7 6 ad2antrr ⊢ B ∈ ℋ ∧ C ≠ 0 ℎ ∧ C ∈ span ⁡ B → B ∈ span ⁡ B
8 spansneleq ⊢ B ∈ ℋ ∧ C ≠ 0 ℎ → C ∈ span ⁡ B → span ⁡ C = span ⁡ B
9 8 imp ⊢ B ∈ ℋ ∧ C ≠ 0 ℎ ∧ C ∈ span ⁡ B → span ⁡ C = span ⁡ B
10 7 9 eleqtrrd ⊢ B ∈ ℋ ∧ C ≠ 0 ℎ ∧ C ∈ span ⁡ B → B ∈ span ⁡ C
11 elspansn3 ⊢ A ∈ S ℋ ∧ C ∈ A ∧ B ∈ span ⁡ C → B ∈ A
12 11 3expia ⊢ A ∈ S ℋ ∧ C ∈ A → B ∈ span ⁡ C → B ∈ A
13 10 12 syl5 ⊢ A ∈ S ℋ ∧ C ∈ A → B ∈ ℋ ∧ C ≠ 0 ℎ ∧ C ∈ span ⁡ B → B ∈ A
14 13 exp4b ⊢ A ∈ S ℋ → C ∈ A → B ∈ ℋ ∧ C ≠ 0 ℎ → C ∈ span ⁡ B → B ∈ A
15 14 com24 ⊢ A ∈ S ℋ → C ∈ span ⁡ B → B ∈ ℋ ∧ C ≠ 0 ℎ → C ∈ A → B ∈ A
16 15 exp4a ⊢ A ∈ S ℋ → C ∈ span ⁡ B → B ∈ ℋ → C ≠ 0 ℎ → C ∈ A → B ∈ A
17 16 com23 ⊢ A ∈ S ℋ → B ∈ ℋ → C ∈ span ⁡ B → C ≠ 0 ℎ → C ∈ A → B ∈ A
18 17 imp43 ⊢ A ∈ S ℋ ∧ B ∈ ℋ ∧ C ∈ span ⁡ B ∧ C ≠ 0 ℎ → C ∈ A → B ∈ A
19 5 18 impbid ⊢ A ∈ S ℋ ∧ B ∈ ℋ ∧ C ∈ span ⁡ B ∧ C ≠ 0 ℎ → B ∈ A ↔ C ∈ A