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 ∈ SubGrp ⁡ G ∧ T ∈ SubGrp ⁡ G ∧ U ∈ SubGrp ⁡ G → S ⊆ U ∧ T ⊆ U ↔ S ⊕ ˙ T ⊆ U

Proof

Step Hyp Ref Expression
1 lsmub1.p ⊢ ⊕ ˙ = LSSum ⁡ G
2 simp3 ⊢ S ∈ SubGrp ⁡ G ∧ T ∈ SubGrp ⁡ G ∧ U ∈ SubGrp ⁡ G → U ∈ SubGrp ⁡ G
3 1 lsmless12 ⊢ U ∈ SubGrp ⁡ G ∧ U ∈ SubGrp ⁡ G ∧ S ⊆ U ∧ T ⊆ U → S ⊕ ˙ T ⊆ U ⊕ ˙ U
4 3 ex ⊢ U ∈ SubGrp ⁡ G ∧ U ∈ SubGrp ⁡ G → S ⊆ U ∧ T ⊆ U → S ⊕ ˙ T ⊆ U ⊕ ˙ U
5 2 2 4 syl2anc ⊢ S ∈ SubGrp ⁡ G ∧ T ∈ SubGrp ⁡ G ∧ U ∈ SubGrp ⁡ G → S ⊆ U ∧ T ⊆ U → S ⊕ ˙ T ⊆ U ⊕ ˙ U
6 1 lsmidm ⊢ U ∈ SubGrp ⁡ G → U ⊕ ˙ U = U
7 6 3ad2ant3 ⊢ S ∈ SubGrp ⁡ G ∧ T ∈ SubGrp ⁡ G ∧ U ∈ SubGrp ⁡ G → U ⊕ ˙ U = U
8 7 sseq2d ⊢ S ∈ SubGrp ⁡ G ∧ T ∈ SubGrp ⁡ G ∧ U ∈ SubGrp ⁡ G → S ⊕ ˙ T ⊆ U ⊕ ˙ U ↔ S ⊕ ˙ T ⊆ U
9 5 8 sylibd ⊢ S ∈ SubGrp ⁡ G ∧ T ∈ SubGrp ⁡ G ∧ U ∈ SubGrp ⁡ G → S ⊆ U ∧ T ⊆ U → S ⊕ ˙ T ⊆ U
10 1 lsmub1 ⊢ S ∈ SubGrp ⁡ G ∧ T ∈ SubGrp ⁡ G → S ⊆ S ⊕ ˙ T
11 10 3adant3 ⊢ S ∈ SubGrp ⁡ G ∧ T ∈ SubGrp ⁡ G ∧ U ∈ SubGrp ⁡ G → S ⊆ S ⊕ ˙ T
12 sstr2 ⊢ S ⊆ S ⊕ ˙ T → S ⊕ ˙ T ⊆ U → S ⊆ U
13 11 12 syl ⊢ S ∈ SubGrp ⁡ G ∧ T ∈ SubGrp ⁡ G ∧ U ∈ SubGrp ⁡ G → S ⊕ ˙ T ⊆ U → S ⊆ U
14 1 lsmub2 ⊢ S ∈ SubGrp ⁡ G ∧ T ∈ SubGrp ⁡ G → T ⊆ S ⊕ ˙ T
15 14 3adant3 ⊢ S ∈ SubGrp ⁡ G ∧ T ∈ SubGrp ⁡ G ∧ U ∈ SubGrp ⁡ G → T ⊆ S ⊕ ˙ T
16 sstr2 ⊢ T ⊆ S ⊕ ˙ T → S ⊕ ˙ T ⊆ U → T ⊆ U
17 15 16 syl ⊢ S ∈ SubGrp ⁡ G ∧ T ∈ SubGrp ⁡ G ∧ U ∈ SubGrp ⁡ G → S ⊕ ˙ T ⊆ U → T ⊆ U
18 13 17 jcad ⊢ S ∈ SubGrp ⁡ G ∧ T ∈ SubGrp ⁡ G ∧ U ∈ SubGrp ⁡ G → S ⊕ ˙ T ⊆ U → S ⊆ U ∧ T ⊆ U
19 9 18 impbid ⊢ S ∈ SubGrp ⁡ G ∧ T ∈ SubGrp ⁡ G ∧ U ∈ SubGrp ⁡ G → S ⊆ U ∧ T ⊆ U ↔ S ⊕ ˙ T ⊆ U