Metamath Proof Explorer

Theorem lsatcmp

Description: If two atoms are comparable, they are equal. ( atsseq analog.) TODO: can lspsncmp shorten this? (Contributed by NM, 25-Aug-2014)

Ref Expression
Hypotheses lsatcmp.a ⊢ A = LSAtoms ⁡ W
lsatcmp.w ⊢ φ → W ∈ LVec
lsatcmp.t ⊢ φ → T ∈ A
lsatcmp.u ⊢ φ → U ∈ A
Assertion lsatcmp ⊢ φ → T ⊆ U ↔ T = U

Proof

Step Hyp Ref Expression
1 lsatcmp.a ⊢ A = LSAtoms ⁡ W
2 lsatcmp.w ⊢ φ → W ∈ LVec
3 lsatcmp.t ⊢ φ → T ∈ A
4 lsatcmp.u ⊢ φ → U ∈ A
5 lveclmod ⊢ W ∈ LVec → W ∈ LMod
6 2 5 syl ⊢ φ → W ∈ LMod
7 eqid ⊢ Base W = Base W
8 eqid ⊢ LSpan ⁡ W = LSpan ⁡ W
9 eqid ⊢ 0 W = 0 W
10 7 8 9 1 islsat ⊢ W ∈ LMod → U ∈ A ↔ ∃ v ∈ Base W ∖ 0 W U = LSpan ⁡ W ⁡ v
11 6 10 syl ⊢ φ → U ∈ A ↔ ∃ v ∈ Base W ∖ 0 W U = LSpan ⁡ W ⁡ v
12 4 11 mpbid ⊢ φ → ∃ v ∈ Base W ∖ 0 W U = LSpan ⁡ W ⁡ v
13 eldifsn ⊢ v ∈ Base W ∖ 0 W ↔ v ∈ Base W ∧ v ≠ 0 W
14 9 1 6 3 lsatn0 ⊢ φ → T ≠ 0 W
15 14 ad2antrr ⊢ φ ∧ v ∈ Base W ∧ v ≠ 0 W ∧ T ⊆ LSpan ⁡ W ⁡ v → T ≠ 0 W
16 2 ad2antrr ⊢ φ ∧ v ∈ Base W ∧ v ≠ 0 W ∧ T ⊆ LSpan ⁡ W ⁡ v → W ∈ LVec
17 eqid ⊢ LSubSp ⁡ W = LSubSp ⁡ W
18 17 1 6 3 lsatlssel ⊢ φ → T ∈ LSubSp ⁡ W
19 18 ad2antrr ⊢ φ ∧ v ∈ Base W ∧ v ≠ 0 W ∧ T ⊆ LSpan ⁡ W ⁡ v → T ∈ LSubSp ⁡ W
20 simplrl ⊢ φ ∧ v ∈ Base W ∧ v ≠ 0 W ∧ T ⊆ LSpan ⁡ W ⁡ v → v ∈ Base W
21 simpr ⊢ φ ∧ v ∈ Base W ∧ v ≠ 0 W ∧ T ⊆ LSpan ⁡ W ⁡ v → T ⊆ LSpan ⁡ W ⁡ v
22 7 9 17 8 lspsnat ⊢ W ∈ LVec ∧ T ∈ LSubSp ⁡ W ∧ v ∈ Base W ∧ T ⊆ LSpan ⁡ W ⁡ v → T = LSpan ⁡ W ⁡ v ∨ T = 0 W
23 16 19 20 21 22 syl31anc ⊢ φ ∧ v ∈ Base W ∧ v ≠ 0 W ∧ T ⊆ LSpan ⁡ W ⁡ v → T = LSpan ⁡ W ⁡ v ∨ T = 0 W
24 23 ord ⊢ φ ∧ v ∈ Base W ∧ v ≠ 0 W ∧ T ⊆ LSpan ⁡ W ⁡ v → ¬ T = LSpan ⁡ W ⁡ v → T = 0 W
25 24 necon1ad ⊢ φ ∧ v ∈ Base W ∧ v ≠ 0 W ∧ T ⊆ LSpan ⁡ W ⁡ v → T ≠ 0 W → T = LSpan ⁡ W ⁡ v
26 15 25 mpd ⊢ φ ∧ v ∈ Base W ∧ v ≠ 0 W ∧ T ⊆ LSpan ⁡ W ⁡ v → T = LSpan ⁡ W ⁡ v
27 26 ex ⊢ φ ∧ v ∈ Base W ∧ v ≠ 0 W → T ⊆ LSpan ⁡ W ⁡ v → T = LSpan ⁡ W ⁡ v
28 eqimss ⊢ T = LSpan ⁡ W ⁡ v → T ⊆ LSpan ⁡ W ⁡ v
29 27 28 impbid1 ⊢ φ ∧ v ∈ Base W ∧ v ≠ 0 W → T ⊆ LSpan ⁡ W ⁡ v ↔ T = LSpan ⁡ W ⁡ v
30 29 ex ⊢ φ → v ∈ Base W ∧ v ≠ 0 W → T ⊆ LSpan ⁡ W ⁡ v ↔ T = LSpan ⁡ W ⁡ v
31 13 30 syl5bi ⊢ φ → v ∈ Base W ∖ 0 W → T ⊆ LSpan ⁡ W ⁡ v ↔ T = LSpan ⁡ W ⁡ v
32 sseq2 ⊢ U = LSpan ⁡ W ⁡ v → T ⊆ U ↔ T ⊆ LSpan ⁡ W ⁡ v
33 eqeq2 ⊢ U = LSpan ⁡ W ⁡ v → T = U ↔ T = LSpan ⁡ W ⁡ v
34 32 33 bibi12d ⊢ U = LSpan ⁡ W ⁡ v → T ⊆ U ↔ T = U ↔ T ⊆ LSpan ⁡ W ⁡ v ↔ T = LSpan ⁡ W ⁡ v
35 34 biimprcd ⊢ T ⊆ LSpan ⁡ W ⁡ v ↔ T = LSpan ⁡ W ⁡ v → U = LSpan ⁡ W ⁡ v → T ⊆ U ↔ T = U
36 31 35 syl6 ⊢ φ → v ∈ Base W ∖ 0 W → U = LSpan ⁡ W ⁡ v → T ⊆ U ↔ T = U
37 36 rexlimdv ⊢ φ → ∃ v ∈ Base W ∖ 0 W U = LSpan ⁡ W ⁡ v → T ⊆ U ↔ T = U
38 12 37 mpd ⊢ φ → T ⊆ U ↔ T = U