Theorem lsmelvali

Description: Subgroup sum membership (for a left module or left vector space). (Contributed by NM, 4-Feb-2014) (Revised by Mario Carneiro, 19-Apr-2016)

	Ref	Expression
Hypotheses	lsmelval.a	⊢ + = ( +g ‘ 𝐺 )
	lsmelval.p	⊢ ⊕ = ( LSSum ‘ 𝐺 )
Assertion	lsmelvali	⊢ ( ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( 𝑋 ∈ 𝑇 ∧ 𝑌 ∈ 𝑈 ) ) → ( 𝑋 + 𝑌 ) ∈ ( 𝑇 ⊕ 𝑈 ) )

Proof

Step	Hyp	Ref	Expression
1		lsmelval.a	⊢ + = ( +g ‘ 𝐺 )
2		lsmelval.p	⊢ ⊕ = ( LSSum ‘ 𝐺 )
3		subgrcl	⊢ ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) → 𝐺 ∈ Grp )
4	3	adantr	⊢ ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) → 𝐺 ∈ Grp )
5		eqid	⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
6	5	subgss	⊢ ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) → 𝑇 ⊆ ( Base ‘ 𝐺 ) )
7	6	adantr	⊢ ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) → 𝑇 ⊆ ( Base ‘ 𝐺 ) )
8	5	subgss	⊢ ( 𝑈 ∈ ( SubGrp ‘ 𝐺 ) → 𝑈 ⊆ ( Base ‘ 𝐺 ) )
9	8	adantl	⊢ ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) → 𝑈 ⊆ ( Base ‘ 𝐺 ) )
10	4 7 9	3jca	⊢ ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) → ( 𝐺 ∈ Grp ∧ 𝑇 ⊆ ( Base ‘ 𝐺 ) ∧ 𝑈 ⊆ ( Base ‘ 𝐺 ) ) )
11	5 1 2	lsmelvalix	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑇 ⊆ ( Base ‘ 𝐺 ) ∧ 𝑈 ⊆ ( Base ‘ 𝐺 ) ) ∧ ( 𝑋 ∈ 𝑇 ∧ 𝑌 ∈ 𝑈 ) ) → ( 𝑋 + 𝑌 ) ∈ ( 𝑇 ⊕ 𝑈 ) )
12	10 11	sylan	⊢ ( ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( 𝑋 ∈ 𝑇 ∧ 𝑌 ∈ 𝑈 ) ) → ( 𝑋 + 𝑌 ) ∈ ( 𝑇 ⊕ 𝑈 ) )