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ℎ ) )