This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝐴 ∈ Sℋ → ( ( ( 𝐵 ∈ ℋ ∧ ¬ 𝐵 ∈ 𝐴 ) ∧ ( 𝐶 ∈ ( span ‘ { 𝐵 } ) ∧ 𝐶 ∈ 𝐴 ) ) → 𝐶 = 0ℎ ) )

Proof

Step Hyp Ref Expression
1 elspansn4 ⊢ ( ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ( span ‘ { 𝐵 } ) ∧ 𝐶 ≠ 0ℎ ) ) → ( 𝐵 ∈ 𝐴 ↔ 𝐶 ∈ 𝐴 ) )
2 1 biimprd ⊢ ( ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ( span ‘ { 𝐵 } ) ∧ 𝐶 ≠ 0ℎ ) ) → ( 𝐶 ∈ 𝐴 → 𝐵 ∈ 𝐴 ) )
3 2 exp32 ⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ ℋ ) → ( 𝐶 ∈ ( span ‘ { 𝐵 } ) → ( 𝐶 ≠ 0ℎ → ( 𝐶 ∈ 𝐴 → 𝐵 ∈ 𝐴 ) ) ) )
4 3 com34 ⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ ℋ ) → ( 𝐶 ∈ ( span ‘ { 𝐵 } ) → ( 𝐶 ∈ 𝐴 → ( 𝐶 ≠ 0ℎ → 𝐵 ∈ 𝐴 ) ) ) )
5 4 imp32 ⊢ ( ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ( span ‘ { 𝐵 } ) ∧ 𝐶 ∈ 𝐴 ) ) → ( 𝐶 ≠ 0ℎ → 𝐵 ∈ 𝐴 ) )
6 5 necon1bd ⊢ ( ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ( span ‘ { 𝐵 } ) ∧ 𝐶 ∈ 𝐴 ) ) → ( ¬ 𝐵 ∈ 𝐴 → 𝐶 = 0ℎ ) )
7 6 exp31 ⊢ ( 𝐴 ∈ Sℋ → ( 𝐵 ∈ ℋ → ( ( 𝐶 ∈ ( span ‘ { 𝐵 } ) ∧ 𝐶 ∈ 𝐴 ) → ( ¬ 𝐵 ∈ 𝐴 → 𝐶 = 0ℎ ) ) ) )
8 7 com34 ⊢ ( 𝐴 ∈ Sℋ → ( 𝐵 ∈ ℋ → ( ¬ 𝐵 ∈ 𝐴 → ( ( 𝐶 ∈ ( span ‘ { 𝐵 } ) ∧ 𝐶 ∈ 𝐴 ) → 𝐶 = 0ℎ ) ) ) )
9 8 imp4c ⊢ ( 𝐴 ∈ Sℋ → ( ( ( 𝐵 ∈ ℋ ∧ ¬ 𝐵 ∈ 𝐴 ) ∧ ( 𝐶 ∈ ( span ‘ { 𝐵 } ) ∧ 𝐶 ∈ 𝐴 ) ) → 𝐶 = 0ℎ ) )