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 
|- ( ph -> W e. LVec )
lsatcmp.t 
|- ( ph -> T e. A )
lsatcmp.u 
|- ( ph -> U e. A )
Assertion lsatcmp 
|- ( ph -> ( T C_ U <-> T = U ) )

Proof

Step Hyp Ref Expression
1 lsatcmp.a 
 |-  A = ( LSAtoms ` W )
2 lsatcmp.w 
 |-  ( ph -> W e. LVec )
3 lsatcmp.t 
 |-  ( ph -> T e. A )
4 lsatcmp.u 
 |-  ( ph -> U e. A )
5 lveclmod 
 |-  ( W e. LVec -> W e. LMod )
6 2 5 syl 
 |-  ( ph -> W e. LMod )
7 eqid 
 |-  ( Base ` W ) = ( Base ` W )
8 eqid 
 |-  ( LSpan ` W ) = ( LSpan ` W )
9 eqid 
 |-  ( 0g ` W ) = ( 0g ` W )
10 7 8 9 1 islsat 
 |-  ( W e. LMod -> ( U e. A <-> E. v e. ( ( Base ` W ) \ { ( 0g ` W ) } ) U = ( ( LSpan ` W ) ` { v } ) ) )
11 6 10 syl 
 |-  ( ph -> ( U e. A <-> E. v e. ( ( Base ` W ) \ { ( 0g ` W ) } ) U = ( ( LSpan ` W ) ` { v } ) ) )
12 4 11 mpbid 
 |-  ( ph -> E. v e. ( ( Base ` W ) \ { ( 0g ` W ) } ) U = ( ( LSpan ` W ) ` { v } ) )
13 eldifsn 
 |-  ( v e. ( ( Base ` W ) \ { ( 0g ` W ) } ) <-> ( v e. ( Base ` W ) /\ v =/= ( 0g ` W ) ) )
14 9 1 6 3 lsatn0 
 |-  ( ph -> T =/= { ( 0g ` W ) } )
15 14 ad2antrr 
 |-  ( ( ( ph /\ ( v e. ( Base ` W ) /\ v =/= ( 0g ` W ) ) ) /\ T C_ ( ( LSpan ` W ) ` { v } ) ) -> T =/= { ( 0g ` W ) } )
16 2 ad2antrr 
 |-  ( ( ( ph /\ ( v e. ( Base ` W ) /\ v =/= ( 0g ` W ) ) ) /\ T C_ ( ( LSpan ` W ) ` { v } ) ) -> W e. LVec )
17 eqid 
 |-  ( LSubSp ` W ) = ( LSubSp ` W )
18 17 1 6 3 lsatlssel 
 |-  ( ph -> T e. ( LSubSp ` W ) )
19 18 ad2antrr 
 |-  ( ( ( ph /\ ( v e. ( Base ` W ) /\ v =/= ( 0g ` W ) ) ) /\ T C_ ( ( LSpan ` W ) ` { v } ) ) -> T e. ( LSubSp ` W ) )
20 simplrl 
 |-  ( ( ( ph /\ ( v e. ( Base ` W ) /\ v =/= ( 0g ` W ) ) ) /\ T C_ ( ( LSpan ` W ) ` { v } ) ) -> v e. ( Base ` W ) )
21 simpr 
 |-  ( ( ( ph /\ ( v e. ( Base ` W ) /\ v =/= ( 0g ` W ) ) ) /\ T C_ ( ( LSpan ` W ) ` { v } ) ) -> T C_ ( ( LSpan ` W ) ` { v } ) )
22 7 9 17 8 lspsnat 
 |-  ( ( ( W e. LVec /\ T e. ( LSubSp ` W ) /\ v e. ( Base ` W ) ) /\ T C_ ( ( LSpan ` W ) ` { v } ) ) -> ( T = ( ( LSpan ` W ) ` { v } ) \/ T = { ( 0g ` W ) } ) )
23 16 19 20 21 22 syl31anc 
 |-  ( ( ( ph /\ ( v e. ( Base ` W ) /\ v =/= ( 0g ` W ) ) ) /\ T C_ ( ( LSpan ` W ) ` { v } ) ) -> ( T = ( ( LSpan ` W ) ` { v } ) \/ T = { ( 0g ` W ) } ) )
24 23 ord 
 |-  ( ( ( ph /\ ( v e. ( Base ` W ) /\ v =/= ( 0g ` W ) ) ) /\ T C_ ( ( LSpan ` W ) ` { v } ) ) -> ( -. T = ( ( LSpan ` W ) ` { v } ) -> T = { ( 0g ` W ) } ) )
25 24 necon1ad 
 |-  ( ( ( ph /\ ( v e. ( Base ` W ) /\ v =/= ( 0g ` W ) ) ) /\ T C_ ( ( LSpan ` W ) ` { v } ) ) -> ( T =/= { ( 0g ` W ) } -> T = ( ( LSpan ` W ) ` { v } ) ) )
26 15 25 mpd 
 |-  ( ( ( ph /\ ( v e. ( Base ` W ) /\ v =/= ( 0g ` W ) ) ) /\ T C_ ( ( LSpan ` W ) ` { v } ) ) -> T = ( ( LSpan ` W ) ` { v } ) )
27 26 ex 
 |-  ( ( ph /\ ( v e. ( Base ` W ) /\ v =/= ( 0g ` W ) ) ) -> ( T C_ ( ( LSpan ` W ) ` { v } ) -> T = ( ( LSpan ` W ) ` { v } ) ) )
28 eqimss 
 |-  ( T = ( ( LSpan ` W ) ` { v } ) -> T C_ ( ( LSpan ` W ) ` { v } ) )
29 27 28 impbid1 
 |-  ( ( ph /\ ( v e. ( Base ` W ) /\ v =/= ( 0g ` W ) ) ) -> ( T C_ ( ( LSpan ` W ) ` { v } ) <-> T = ( ( LSpan ` W ) ` { v } ) ) )
30 29 ex 
 |-  ( ph -> ( ( v e. ( Base ` W ) /\ v =/= ( 0g ` W ) ) -> ( T C_ ( ( LSpan ` W ) ` { v } ) <-> T = ( ( LSpan ` W ) ` { v } ) ) ) )
31 13 30 syl5bi 
 |-  ( ph -> ( v e. ( ( Base ` W ) \ { ( 0g ` W ) } ) -> ( T C_ ( ( LSpan ` W ) ` { v } ) <-> T = ( ( LSpan ` W ) ` { v } ) ) ) )
32 sseq2 
 |-  ( U = ( ( LSpan ` W ) ` { v } ) -> ( T C_ U <-> T C_ ( ( LSpan ` W ) ` { v } ) ) )
33 eqeq2 
 |-  ( U = ( ( LSpan ` W ) ` { v } ) -> ( T = U <-> T = ( ( LSpan ` W ) ` { v } ) ) )
34 32 33 bibi12d 
 |-  ( U = ( ( LSpan ` W ) ` { v } ) -> ( ( T C_ U <-> T = U ) <-> ( T C_ ( ( LSpan ` W ) ` { v } ) <-> T = ( ( LSpan ` W ) ` { v } ) ) ) )
35 34 biimprcd 
 |-  ( ( T C_ ( ( LSpan ` W ) ` { v } ) <-> T = ( ( LSpan ` W ) ` { v } ) ) -> ( U = ( ( LSpan ` W ) ` { v } ) -> ( T C_ U <-> T = U ) ) )
36 31 35 syl6 
 |-  ( ph -> ( v e. ( ( Base ` W ) \ { ( 0g ` W ) } ) -> ( U = ( ( LSpan ` W ) ` { v } ) -> ( T C_ U <-> T = U ) ) ) )
37 36 rexlimdv 
 |-  ( ph -> ( E. v e. ( ( Base ` W ) \ { ( 0g ` W ) } ) U = ( ( LSpan ` W ) ` { v } ) -> ( T C_ U <-> T = U ) ) )
38 12 37 mpd 
 |-  ( ph -> ( T C_ U <-> T = U ) )