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

Metamath Proof Explorer

Theorem lsmub2x

Description: Subgroup sum is an upper bound of its arguments. (Contributed by NM, 6-Feb-2014) (Revised by Mario Carneiro, 19-Apr-2016)

Ref Expression
Hypotheses lsmless2.v ⊢ 𝐵 = ( Base ‘ 𝐺 )
lsmless2.s ⊢ ⊕ = ( LSSum ‘ 𝐺 )
Assertion lsmub2x ( ( 𝑇 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑈 ⊆ 𝐵 ) → 𝑈 ⊆ ( 𝑇 ⊕ 𝑈 ) )

Proof

Step Hyp Ref Expression
1 lsmless2.v ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 lsmless2.s ⊢ ⊕ = ( LSSum ‘ 𝐺 )
3 submrcl ⊢ ( 𝑇 ∈ ( SubMnd ‘ 𝐺 ) → 𝐺 ∈ Mnd )
4 3 ad2antrr ⊢ ( ( ( 𝑇 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑈 ⊆ 𝐵 ) ∧ 𝑥 ∈ 𝑈 ) → 𝐺 ∈ Mnd )
5 simpr ⊢ ( ( 𝑇 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑈 ⊆ 𝐵 ) → 𝑈 ⊆ 𝐵 )
6 5 sselda ⊢ ( ( ( 𝑇 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑈 ⊆ 𝐵 ) ∧ 𝑥 ∈ 𝑈 ) → 𝑥 ∈ 𝐵 )
7 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
8 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
9 1 7 8 mndlid ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑥 ∈ 𝐵 ) → ( ( 0g ‘ 𝐺 ) ( +g ‘ 𝐺 ) 𝑥 ) = 𝑥 )
10 4 6 9 syl2anc ⊢ ( ( ( 𝑇 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑈 ⊆ 𝐵 ) ∧ 𝑥 ∈ 𝑈 ) → ( ( 0g ‘ 𝐺 ) ( +g ‘ 𝐺 ) 𝑥 ) = 𝑥 )
11 1 submss ⊢ ( 𝑇 ∈ ( SubMnd ‘ 𝐺 ) → 𝑇 ⊆ 𝐵 )
12 11 ad2antrr ⊢ ( ( ( 𝑇 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑈 ⊆ 𝐵 ) ∧ 𝑥 ∈ 𝑈 ) → 𝑇 ⊆ 𝐵 )
13 simplr ⊢ ( ( ( 𝑇 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑈 ⊆ 𝐵 ) ∧ 𝑥 ∈ 𝑈 ) → 𝑈 ⊆ 𝐵 )
14 8 subm0cl ⊢ ( 𝑇 ∈ ( SubMnd ‘ 𝐺 ) → ( 0g ‘ 𝐺 ) ∈ 𝑇 )
15 14 ad2antrr ⊢ ( ( ( 𝑇 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑈 ⊆ 𝐵 ) ∧ 𝑥 ∈ 𝑈 ) → ( 0g ‘ 𝐺 ) ∈ 𝑇 )
16 simpr ⊢ ( ( ( 𝑇 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑈 ⊆ 𝐵 ) ∧ 𝑥 ∈ 𝑈 ) → 𝑥 ∈ 𝑈 )
17 1 7 2 lsmelvalix ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵 ) ∧ ( ( 0g ‘ 𝐺 ) ∈ 𝑇 ∧ 𝑥 ∈ 𝑈 ) ) → ( ( 0g ‘ 𝐺 ) ( +g ‘ 𝐺 ) 𝑥 ) ∈ ( 𝑇 ⊕ 𝑈 ) )
18 4 12 13 15 16 17 syl32anc ⊢ ( ( ( 𝑇 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑈 ⊆ 𝐵 ) ∧ 𝑥 ∈ 𝑈 ) → ( ( 0g ‘ 𝐺 ) ( +g ‘ 𝐺 ) 𝑥 ) ∈ ( 𝑇 ⊕ 𝑈 ) )
19 10 18 eqeltrrd ⊢ ( ( ( 𝑇 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑈 ⊆ 𝐵 ) ∧ 𝑥 ∈ 𝑈 ) → 𝑥 ∈ ( 𝑇 ⊕ 𝑈 ) )
20 19 ex ⊢ ( ( 𝑇 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑈 ⊆ 𝐵 ) → ( 𝑥 ∈ 𝑈 → 𝑥 ∈ ( 𝑇 ⊕ 𝑈 ) ) )
21 20 ssrdv ⊢ ( ( 𝑇 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑈 ⊆ 𝐵 ) → 𝑈 ⊆ ( 𝑇 ⊕ 𝑈 ) )