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 ) ) )