Metamath Proof Explorer

Theorem elspansn5

Description: A vector belonging to both a subspace and the span of the singleton of a vector not in it must be zero. (Contributed by NM, 17-Dec-2004) (New usage is discouraged.)

Ref Expression
Assertion elspansn5 ⊢ A ∈ S ℋ → B ∈ ℋ ∧ ¬ B ∈ A ∧ C ∈ span ⁡ B ∧ C ∈ A → C = 0 ℎ

Proof

Step Hyp Ref Expression
1 elspansn4 ⊢ A ∈ S ℋ ∧ B ∈ ℋ ∧ C ∈ span ⁡ B ∧ C ≠ 0 ℎ → B ∈ A ↔ C ∈ A
2 1 biimprd ⊢ A ∈ S ℋ ∧ B ∈ ℋ ∧ C ∈ span ⁡ B ∧ C ≠ 0 ℎ → C ∈ A → B ∈ A
3 2 exp32 ⊢ A ∈ S ℋ ∧ B ∈ ℋ → C ∈ span ⁡ B → C ≠ 0 ℎ → C ∈ A → B ∈ A
4 3 com34 ⊢ A ∈ S ℋ ∧ B ∈ ℋ → C ∈ span ⁡ B → C ∈ A → C ≠ 0 ℎ → B ∈ A
5 4 imp32 ⊢ A ∈ S ℋ ∧ B ∈ ℋ ∧ C ∈ span ⁡ B ∧ C ∈ A → C ≠ 0 ℎ → B ∈ A
6 5 necon1bd ⊢ A ∈ S ℋ ∧ B ∈ ℋ ∧ C ∈ span ⁡ B ∧ C ∈ A → ¬ B ∈ A → C = 0 ℎ
7 6 exp31 ⊢ A ∈ S ℋ → B ∈ ℋ → C ∈ span ⁡ B ∧ C ∈ A → ¬ B ∈ A → C = 0 ℎ
8 7 com34 ⊢ A ∈ S ℋ → B ∈ ℋ → ¬ B ∈ A → C ∈ span ⁡ B ∧ C ∈ A → C = 0 ℎ
9 8 imp4c ⊢ A ∈ S ℋ → B ∈ ℋ ∧ ¬ B ∈ A ∧ C ∈ span ⁡ B ∧ C ∈ A → C = 0 ℎ