Theorem gsumsra

Description: The group sum in a subring algebra is the same as the ring's group sum. (Contributed by Thierry Arnoux, 28-May-2023)

	Ref	Expression
Hypotheses	gsumsra.1	⊢ 𝐴 = ( ( subringAlg ‘ 𝑅 ) ‘ 𝐵 )
	gsumsra.2	⊢ ( 𝜑 → 𝐹 ∈ 𝑈 )
	gsumsra.3	⊢ ( 𝜑 → 𝑅 ∈ 𝑉 )
	gsumsra.4	⊢ ( 𝜑 → 𝐴 ∈ 𝑊 )
	gsumsra.5	⊢ ( 𝜑 → 𝐵 ⊆ ( Base ‘ 𝑅 ) )
Assertion	gsumsra	⊢ ( 𝜑 → ( 𝑅 Σg 𝐹 ) = ( 𝐴 Σg 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		gsumsra.1	⊢ 𝐴 = ( ( subringAlg ‘ 𝑅 ) ‘ 𝐵 )
2		gsumsra.2	⊢ ( 𝜑 → 𝐹 ∈ 𝑈 )
3		gsumsra.3	⊢ ( 𝜑 → 𝑅 ∈ 𝑉 )
4		gsumsra.4	⊢ ( 𝜑 → 𝐴 ∈ 𝑊 )
5		gsumsra.5	⊢ ( 𝜑 → 𝐵 ⊆ ( Base ‘ 𝑅 ) )
6	1	a1i	⊢ ( 𝜑 → 𝐴 = ( ( subringAlg ‘ 𝑅 ) ‘ 𝐵 ) )
7	6 5	srabase	⊢ ( 𝜑 → ( Base ‘ 𝑅 ) = ( Base ‘ 𝐴 ) )
8	6 5	sraaddg	⊢ ( 𝜑 → ( +g ‘ 𝑅 ) = ( +g ‘ 𝐴 ) )
9	2 3 4 7 8	gsumpropd	⊢ ( 𝜑 → ( 𝑅 Σg 𝐹 ) = ( 𝐴 Σg 𝐹 ) )