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

Proof

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