Metamath Proof Explorer


Theorem gsumsubg

Description: The group sum in a subgroup is the same as the group sum. (Contributed by Thierry Arnoux, 28-May-2023)

Ref Expression
Hypotheses gsumsubg.1 𝐻 = ( 𝐺s 𝐵 )
gsumsubg.a ( 𝜑𝐴𝑉 )
gsumsubg.f ( 𝜑𝐹 : 𝐴𝐵 )
gsumsubg.b ( 𝜑𝐵 ∈ ( SubGrp ‘ 𝐺 ) )
Assertion gsumsubg ( 𝜑 → ( 𝐺 Σg 𝐹 ) = ( 𝐻 Σg 𝐹 ) )

Proof

Step Hyp Ref Expression
1 gsumsubg.1 𝐻 = ( 𝐺s 𝐵 )
2 gsumsubg.a ( 𝜑𝐴𝑉 )
3 gsumsubg.f ( 𝜑𝐹 : 𝐴𝐵 )
4 gsumsubg.b ( 𝜑𝐵 ∈ ( SubGrp ‘ 𝐺 ) )
5 eqid ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
6 eqid ( +g𝐺 ) = ( +g𝐺 )
7 4 elfvexd ( 𝜑𝐺 ∈ V )
8 5 subgss ( 𝐵 ∈ ( SubGrp ‘ 𝐺 ) → 𝐵 ⊆ ( Base ‘ 𝐺 ) )
9 4 8 syl ( 𝜑𝐵 ⊆ ( Base ‘ 𝐺 ) )
10 eqid ( 0g𝐺 ) = ( 0g𝐺 )
11 10 subg0cl ( 𝐵 ∈ ( SubGrp ‘ 𝐺 ) → ( 0g𝐺 ) ∈ 𝐵 )
12 4 11 syl ( 𝜑 → ( 0g𝐺 ) ∈ 𝐵 )
13 subgrcl ( 𝐵 ∈ ( SubGrp ‘ 𝐺 ) → 𝐺 ∈ Grp )
14 4 13 syl ( 𝜑𝐺 ∈ Grp )
15 5 6 10 grplid ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) → ( ( 0g𝐺 ) ( +g𝐺 ) 𝑥 ) = 𝑥 )
16 5 6 10 grprid ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) → ( 𝑥 ( +g𝐺 ) ( 0g𝐺 ) ) = 𝑥 )
17 15 16 jca ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) → ( ( ( 0g𝐺 ) ( +g𝐺 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g𝐺 ) ( 0g𝐺 ) ) = 𝑥 ) )
18 14 17 sylan ( ( 𝜑𝑥 ∈ ( Base ‘ 𝐺 ) ) → ( ( ( 0g𝐺 ) ( +g𝐺 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g𝐺 ) ( 0g𝐺 ) ) = 𝑥 ) )
19 5 6 1 7 2 9 3 12 18 gsumress ( 𝜑 → ( 𝐺 Σg 𝐹 ) = ( 𝐻 Σg 𝐹 ) )