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

Metamath Proof Explorer

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ℎ ) ) → ( 𝐵 ∈ 𝐴 ↔ 𝐶 ∈ 𝐴 ) )