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

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. = ( 0g ` W )
lsatcmp2.a 
|- A = ( LSAtoms ` W )
lsatcmp2.w 
|- ( ph -> W e. LVec )
lsatcmp2.t 
|- ( ph -> T e. A )
lsatcmp2.u 
|- ( ph -> ( U e. A \/ U = { .0. } ) )
Assertion lsatcmp2 
|- ( ph -> ( T C_ U <-> T = U ) )

Proof

Step Hyp Ref Expression
1 lsatcmp2.o 
 |-  .0. = ( 0g ` W )
2 lsatcmp2.a 
 |-  A = ( LSAtoms ` W )
3 lsatcmp2.w 
 |-  ( ph -> W e. LVec )
4 lsatcmp2.t 
 |-  ( ph -> T e. A )
5 lsatcmp2.u 
 |-  ( ph -> ( U e. A \/ U = { .0. } ) )
6 simpr 
 |-  ( ( ph /\ T C_ U ) -> T C_ U )
7 3 adantr 
 |-  ( ( ph /\ T C_ U ) -> W e. LVec )
8 4 adantr 
 |-  ( ( ph /\ T C_ U ) -> T e. A )
9 lveclmod 
 |-  ( W e. LVec -> W e. LMod )
10 3 9 syl 
 |-  ( ph -> W e. LMod )
11 10 adantr 
 |-  ( ( ph /\ T C_ U ) -> W e. LMod )
12 1 2 11 8 6 lsatssn0 
 |-  ( ( ph /\ T C_ U ) -> U =/= { .0. } )
13 5 ord 
 |-  ( ph -> ( -. U e. A -> U = { .0. } ) )
14 13 necon1ad 
 |-  ( ph -> ( U =/= { .0. } -> U e. A ) )
15 14 adantr 
 |-  ( ( ph /\ T C_ U ) -> ( U =/= { .0. } -> U e. A ) )
16 12 15 mpd 
 |-  ( ( ph /\ T C_ U ) -> U e. A )
17 2 7 8 16 lsatcmp 
 |-  ( ( ph /\ T C_ U ) -> ( T C_ U <-> T = U ) )
18 6 17 mpbid 
 |-  ( ( ph /\ T C_ U ) -> T = U )
19 18 ex 
 |-  ( ph -> ( T C_ U -> T = U ) )
20 eqimss 
 |-  ( T = U -> T C_ U )
21 19 20 impbid1 
 |-  ( ph -> ( T C_ U <-> T = U ) )