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 ‘ 𝐺 ) ) → ( ( 𝑆 ⊆ 𝑈 ∧ 𝑇 ⊆ 𝑈 ) ↔ ( 𝑆 ⊕ 𝑇 ) ⊆ 𝑈 ) )