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

Metamath Proof Explorer

Theorem lsmless1

Description: Subset implies subgroup sum subset. (Contributed by NM, 6-Feb-2014) (Revised by Mario Carneiro, 19-Apr-2016)

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

Proof

Step Hyp Ref Expression
1 lsmub1.p ⊢ ⊕ = ( LSSum ‘ 𝐺 )
2 subgrcl ⊢ ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) → 𝐺 ∈ Grp )
3 2 3ad2ant1 ⊢ ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 ⊆ 𝑇 ) → 𝐺 ∈ Grp )
4 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
5 4 subgss ⊢ ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) → 𝑇 ⊆ ( Base ‘ 𝐺 ) )
6 5 3ad2ant1 ⊢ ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 ⊆ 𝑇 ) → 𝑇 ⊆ ( Base ‘ 𝐺 ) )
7 4 subgss ⊢ ( 𝑈 ∈ ( SubGrp ‘ 𝐺 ) → 𝑈 ⊆ ( Base ‘ 𝐺 ) )
8 7 3ad2ant2 ⊢ ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 ⊆ 𝑇 ) → 𝑈 ⊆ ( Base ‘ 𝐺 ) )
9 simp3 ⊢ ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 ⊆ 𝑇 ) → 𝑆 ⊆ 𝑇 )
10 4 1 lsmless1x ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑇 ⊆ ( Base ‘ 𝐺 ) ∧ 𝑈 ⊆ ( Base ‘ 𝐺 ) ) ∧ 𝑆 ⊆ 𝑇 ) → ( 𝑆 ⊕ 𝑈 ) ⊆ ( 𝑇 ⊕ 𝑈 ) )
11 3 6 8 9 10 syl31anc ⊢ ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 ⊆ 𝑇 ) → ( 𝑆 ⊕ 𝑈 ) ⊆ ( 𝑇 ⊕ 𝑈 ) )