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 ⊢A∈Sℋ∧B∈ℋ∧C∈span⁡B∧C≠0ℎ→B∈A↔C∈A

Proof

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