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