Theorem lsmval

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

	Ref	Expression
Hypotheses	lsmval.v	⊢ 𝐵 = ( Base ‘ 𝐺 )
	lsmval.a	⊢ + = ( +g ‘ 𝐺 )
	lsmval.p	⊢ ⊕ = ( LSSum ‘ 𝐺 )
Assertion	lsmval	⊢ ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) → ( 𝑇 ⊕ 𝑈 ) = ran ( 𝑥 ∈ 𝑇 , 𝑦 ∈ 𝑈 ↦ ( 𝑥 + 𝑦 ) ) )

Proof

Step	Hyp	Ref	Expression
1		lsmval.v	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		lsmval.a	⊢ + = ( +g ‘ 𝐺 )
3		lsmval.p	⊢ ⊕ = ( LSSum ‘ 𝐺 )
4		subgrcl	⊢ ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) → 𝐺 ∈ Grp )
5	1	subgss	⊢ ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) → 𝑇 ⊆ 𝐵 )
6	1	subgss	⊢ ( 𝑈 ∈ ( SubGrp ‘ 𝐺 ) → 𝑈 ⊆ 𝐵 )
7	1 2 3	lsmvalx	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵 ) → ( 𝑇 ⊕ 𝑈 ) = ran ( 𝑥 ∈ 𝑇 , 𝑦 ∈ 𝑈 ↦ ( 𝑥 + 𝑦 ) ) )
8	4 5 6 7	syl2an3an	⊢ ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) → ( 𝑇 ⊕ 𝑈 ) = ran ( 𝑥 ∈ 𝑇 , 𝑦 ∈ 𝑈 ↦ ( 𝑥 + 𝑦 ) ) )