Metamath Proof Explorer


Theorem lsatcmp2

Description: If an atom is included in at-most an atom, they are equal. More general version of lsatcmp . TODO: can lspsncmp shorten this? (Contributed by NM, 3-Feb-2015)

Ref Expression
Hypotheses lsatcmp2.o 0 ˙ = 0 W
lsatcmp2.a A = LSAtoms W
lsatcmp2.w φ W LVec
lsatcmp2.t φ T A
lsatcmp2.u φ U A U = 0 ˙
Assertion lsatcmp2 φ T U T = U

Proof

Step Hyp Ref Expression
1 lsatcmp2.o 0 ˙ = 0 W
2 lsatcmp2.a A = LSAtoms W
3 lsatcmp2.w φ W LVec
4 lsatcmp2.t φ T A
5 lsatcmp2.u φ U A U = 0 ˙
6 simpr φ T U T U
7 3 adantr φ T U W LVec
8 4 adantr φ T U T A
9 lveclmod W LVec W LMod
10 3 9 syl φ W LMod
11 10 adantr φ T U W LMod
12 1 2 11 8 6 lsatssn0 φ T U U 0 ˙
13 5 ord φ ¬ U A U = 0 ˙
14 13 necon1ad φ U 0 ˙ U A
15 14 adantr φ T U U 0 ˙ U A
16 12 15 mpd φ T U U A
17 2 7 8 16 lsatcmp φ T U T U T = U
18 6 17 mpbid φ T U T = U
19 18 ex φ T U T = U
20 eqimss T = U T U
21 19 20 impbid1 φ T U T = U