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 𝐹 ) )