Metamath Proof Explorer

Theorem lsmlub

Description: The least upper bound property of subgroup sum. (Contributed by NM, 6-Feb-2014) (Revised by Mario Carneiro, 21-Jun-2014)

Ref Expression
Hypothesis lsmub1.p 
|- .(+) = ( LSSum ` G )
Assertion lsmlub 
|- ( ( S e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) -> ( ( S C_ U /\ T C_ U ) <-> ( S .(+) T ) C_ U ) )

Proof

Step Hyp Ref Expression
1 lsmub1.p 
 |-  .(+) = ( LSSum ` G )
2 simp3 
 |-  ( ( S e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) -> U e. ( SubGrp ` G ) )
3 1 lsmless12 
 |-  ( ( ( U e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) /\ ( S C_ U /\ T C_ U ) ) -> ( S .(+) T ) C_ ( U .(+) U ) )
4 3 ex 
 |-  ( ( U e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) -> ( ( S C_ U /\ T C_ U ) -> ( S .(+) T ) C_ ( U .(+) U ) ) )
5 2 2 4 syl2anc 
 |-  ( ( S e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) -> ( ( S C_ U /\ T C_ U ) -> ( S .(+) T ) C_ ( U .(+) U ) ) )
6 1 lsmidm 
 |-  ( U e. ( SubGrp ` G ) -> ( U .(+) U ) = U )
7 6 3ad2ant3 
 |-  ( ( S e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) -> ( U .(+) U ) = U )
8 7 sseq2d 
 |-  ( ( S e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) -> ( ( S .(+) T ) C_ ( U .(+) U ) <-> ( S .(+) T ) C_ U ) )
9 5 8 sylibd 
 |-  ( ( S e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) -> ( ( S C_ U /\ T C_ U ) -> ( S .(+) T ) C_ U ) )
10 1 lsmub1 
 |-  ( ( S e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) ) -> S C_ ( S .(+) T ) )
11 10 3adant3 
 |-  ( ( S e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) -> S C_ ( S .(+) T ) )
12 sstr2 
 |-  ( S C_ ( S .(+) T ) -> ( ( S .(+) T ) C_ U -> S C_ U ) )
13 11 12 syl 
 |-  ( ( S e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) -> ( ( S .(+) T ) C_ U -> S C_ U ) )
14 1 lsmub2 
 |-  ( ( S e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) ) -> T C_ ( S .(+) T ) )
15 14 3adant3 
 |-  ( ( S e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) -> T C_ ( S .(+) T ) )
16 sstr2 
 |-  ( T C_ ( S .(+) T ) -> ( ( S .(+) T ) C_ U -> T C_ U ) )
17 15 16 syl 
 |-  ( ( S e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) -> ( ( S .(+) T ) C_ U -> T C_ U ) )
18 13 17 jcad 
 |-  ( ( S e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) -> ( ( S .(+) T ) C_ U -> ( S C_ U /\ T C_ U ) ) )
19 9 18 impbid 
 |-  ( ( S e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) -> ( ( S C_ U /\ T C_ U ) <-> ( S .(+) T ) C_ U ) )