This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lsmless12

Description: Subset implies subgroup sum subset. (Contributed by NM, 14-Jan-2015) (Revised by Mario Carneiro, 19-Apr-2016)

Ref Expression
Hypothesis lsmub1.p ⊢ ⊕ = ( LSSum ‘ 𝐺 )
Assertion lsmless12 ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( 𝑅 ⊆ 𝑆 ∧ 𝑇 ⊆ 𝑈 ) ) → ( 𝑅 ⊕ 𝑇 ) ⊆ ( 𝑆 ⊕ 𝑈 ) )

Proof

Step Hyp Ref Expression
1 lsmub1.p ⊢ ⊕ = ( LSSum ‘ 𝐺 )
2 subgrcl ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝐺 ∈ Grp )
3 2 ad2antrr ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( 𝑅 ⊆ 𝑆 ∧ 𝑇 ⊆ 𝑈 ) ) → 𝐺 ∈ Grp )
4 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
5 4 subgss ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝑆 ⊆ ( Base ‘ 𝐺 ) )
6 5 ad2antrr ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( 𝑅 ⊆ 𝑆 ∧ 𝑇 ⊆ 𝑈 ) ) → 𝑆 ⊆ ( Base ‘ 𝐺 ) )
7 simprr ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( 𝑅 ⊆ 𝑆 ∧ 𝑇 ⊆ 𝑈 ) ) → 𝑇 ⊆ 𝑈 )
8 4 subgss ⊢ ( 𝑈 ∈ ( SubGrp ‘ 𝐺 ) → 𝑈 ⊆ ( Base ‘ 𝐺 ) )
9 8 ad2antlr ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( 𝑅 ⊆ 𝑆 ∧ 𝑇 ⊆ 𝑈 ) ) → 𝑈 ⊆ ( Base ‘ 𝐺 ) )
10 7 9 sstrd ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( 𝑅 ⊆ 𝑆 ∧ 𝑇 ⊆ 𝑈 ) ) → 𝑇 ⊆ ( Base ‘ 𝐺 ) )
11 simprl ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( 𝑅 ⊆ 𝑆 ∧ 𝑇 ⊆ 𝑈 ) ) → 𝑅 ⊆ 𝑆 )
12 4 1 lsmless1x ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑆 ⊆ ( Base ‘ 𝐺 ) ∧ 𝑇 ⊆ ( Base ‘ 𝐺 ) ) ∧ 𝑅 ⊆ 𝑆 ) → ( 𝑅 ⊕ 𝑇 ) ⊆ ( 𝑆 ⊕ 𝑇 ) )
13 3 6 10 11 12 syl31anc ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( 𝑅 ⊆ 𝑆 ∧ 𝑇 ⊆ 𝑈 ) ) → ( 𝑅 ⊕ 𝑇 ) ⊆ ( 𝑆 ⊕ 𝑇 ) )
14 simpll ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( 𝑅 ⊆ 𝑆 ∧ 𝑇 ⊆ 𝑈 ) ) → 𝑆 ∈ ( SubGrp ‘ 𝐺 ) )
15 simplr ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( 𝑅 ⊆ 𝑆 ∧ 𝑇 ⊆ 𝑈 ) ) → 𝑈 ∈ ( SubGrp ‘ 𝐺 ) )
16 1 lsmless2 ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ⊆ 𝑈 ) → ( 𝑆 ⊕ 𝑇 ) ⊆ ( 𝑆 ⊕ 𝑈 ) )
17 14 15 7 16 syl3anc ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( 𝑅 ⊆ 𝑆 ∧ 𝑇 ⊆ 𝑈 ) ) → ( 𝑆 ⊕ 𝑇 ) ⊆ ( 𝑆 ⊕ 𝑈 ) )
18 13 17 sstrd ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( 𝑅 ⊆ 𝑆 ∧ 𝑇 ⊆ 𝑈 ) ) → ( 𝑅 ⊕ 𝑇 ) ⊆ ( 𝑆 ⊕ 𝑈 ) )