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ℎ