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 ‘ 𝐺 )
Assertion lsmlub ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) → ( ( 𝑆𝑈𝑇𝑈 ) ↔ ( 𝑆 𝑇 ) ⊆ 𝑈 ) )

Proof

Step Hyp Ref Expression
1 lsmub1.p = ( LSSum ‘ 𝐺 )
2 simp3 ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) → 𝑈 ∈ ( SubGrp ‘ 𝐺 ) )
3 1 lsmless12 ( ( ( 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( 𝑆𝑈𝑇𝑈 ) ) → ( 𝑆 𝑇 ) ⊆ ( 𝑈 𝑈 ) )
4 3 ex ( ( 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) → ( ( 𝑆𝑈𝑇𝑈 ) → ( 𝑆 𝑇 ) ⊆ ( 𝑈 𝑈 ) ) )
5 2 2 4 syl2anc ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) → ( ( 𝑆𝑈𝑇𝑈 ) → ( 𝑆 𝑇 ) ⊆ ( 𝑈 𝑈 ) ) )
6 1 lsmidm ( 𝑈 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝑈 𝑈 ) = 𝑈 )
7 6 3ad2ant3 ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) → ( 𝑈 𝑈 ) = 𝑈 )
8 7 sseq2d ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) → ( ( 𝑆 𝑇 ) ⊆ ( 𝑈 𝑈 ) ↔ ( 𝑆 𝑇 ) ⊆ 𝑈 ) )
9 5 8 sylibd ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) → ( ( 𝑆𝑈𝑇𝑈 ) → ( 𝑆 𝑇 ) ⊆ 𝑈 ) )
10 1 lsmub1 ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ) → 𝑆 ⊆ ( 𝑆 𝑇 ) )
11 10 3adant3 ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) → 𝑆 ⊆ ( 𝑆 𝑇 ) )
12 sstr2 ( 𝑆 ⊆ ( 𝑆 𝑇 ) → ( ( 𝑆 𝑇 ) ⊆ 𝑈𝑆𝑈 ) )
13 11 12 syl ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) → ( ( 𝑆 𝑇 ) ⊆ 𝑈𝑆𝑈 ) )
14 1 lsmub2 ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ) → 𝑇 ⊆ ( 𝑆 𝑇 ) )
15 14 3adant3 ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) → 𝑇 ⊆ ( 𝑆 𝑇 ) )
16 sstr2 ( 𝑇 ⊆ ( 𝑆 𝑇 ) → ( ( 𝑆 𝑇 ) ⊆ 𝑈𝑇𝑈 ) )
17 15 16 syl ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) → ( ( 𝑆 𝑇 ) ⊆ 𝑈𝑇𝑈 ) )
18 13 17 jcad ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) → ( ( 𝑆 𝑇 ) ⊆ 𝑈 → ( 𝑆𝑈𝑇𝑈 ) ) )
19 9 18 impbid ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) → ( ( 𝑆𝑈𝑇𝑈 ) ↔ ( 𝑆 𝑇 ) ⊆ 𝑈 ) )