Metamath Proof Explorer


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 ( 𝑥𝑇 , 𝑦𝑈 ↦ ( 𝑥 + 𝑦 ) ) )