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

Metamath Proof Explorer

Theorem lssnle

Description: Equivalent expressions for "not less than". ( chnlei analog.) (Contributed by NM, 10-Jan-2015) (Revised by Mario Carneiro, 19-Apr-2016)

Ref Expression
Hypotheses lssnle.p 
|- .(+) = ( LSSum ` G )
lssnle.t 
|- ( ph -> T e. ( SubGrp ` G ) )
lssnle.u 
|- ( ph -> U e. ( SubGrp ` G ) )
Assertion lssnle 
|- ( ph -> ( -. U C_ T <-> T C. ( T .(+) U ) ) )

Proof

Step Hyp Ref Expression
1 lssnle.p 
 |-  .(+) = ( LSSum ` G )
2 lssnle.t 
 |-  ( ph -> T e. ( SubGrp ` G ) )
3 lssnle.u 
 |-  ( ph -> U e. ( SubGrp ` G ) )
4 1 lsmss2b 
 |-  ( ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) -> ( U C_ T <-> ( T .(+) U ) = T ) )
5 2 3 4 syl2anc 
 |-  ( ph -> ( U C_ T <-> ( T .(+) U ) = T ) )
6 eqcom 
 |-  ( ( T .(+) U ) = T <-> T = ( T .(+) U ) )
7 5 6 bitrdi 
 |-  ( ph -> ( U C_ T <-> T = ( T .(+) U ) ) )
8 7 necon3bbid 
 |-  ( ph -> ( -. U C_ T <-> T =/= ( T .(+) U ) ) )
9 1 lsmub1 
 |-  ( ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) -> T C_ ( T .(+) U ) )
10 2 3 9 syl2anc 
 |-  ( ph -> T C_ ( T .(+) U ) )
11 df-pss 
 |-  ( T C. ( T .(+) U ) <-> ( T C_ ( T .(+) U ) /\ T =/= ( T .(+) U ) ) )
12 11 baib 
 |-  ( T C_ ( T .(+) U ) -> ( T C. ( T .(+) U ) <-> T =/= ( T .(+) U ) ) )
13 10 12 syl 
 |-  ( ph -> ( T C. ( T .(+) U ) <-> T =/= ( T .(+) U ) ) )
14 8 13 bitr4d 
 |-  ( ph -> ( -. U C_ T <-> T C. ( T .(+) U ) ) )