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 ˙=LSSumG
Assertion lsmlub SSubGrpGTSubGrpGUSubGrpGSUTUS˙TU

Proof

Step Hyp Ref Expression
1 lsmub1.p ˙=LSSumG
2 simp3 SSubGrpGTSubGrpGUSubGrpGUSubGrpG
3 1 lsmless12 USubGrpGUSubGrpGSUTUS˙TU˙U
4 3 ex USubGrpGUSubGrpGSUTUS˙TU˙U
5 2 2 4 syl2anc SSubGrpGTSubGrpGUSubGrpGSUTUS˙TU˙U
6 1 lsmidm USubGrpGU˙U=U
7 6 3ad2ant3 SSubGrpGTSubGrpGUSubGrpGU˙U=U
8 7 sseq2d SSubGrpGTSubGrpGUSubGrpGS˙TU˙US˙TU
9 5 8 sylibd SSubGrpGTSubGrpGUSubGrpGSUTUS˙TU
10 1 lsmub1 SSubGrpGTSubGrpGSS˙T
11 10 3adant3 SSubGrpGTSubGrpGUSubGrpGSS˙T
12 sstr2 SS˙TS˙TUSU
13 11 12 syl SSubGrpGTSubGrpGUSubGrpGS˙TUSU
14 1 lsmub2 SSubGrpGTSubGrpGTS˙T
15 14 3adant3 SSubGrpGTSubGrpGUSubGrpGTS˙T
16 sstr2 TS˙TS˙TUTU
17 15 16 syl SSubGrpGTSubGrpGUSubGrpGS˙TUTU
18 13 17 jcad SSubGrpGTSubGrpGUSubGrpGS˙TUSUTU
19 9 18 impbid SSubGrpGTSubGrpGUSubGrpGSUTUS˙TU