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	|- A = ( ( subringAlg ` R ) ` B )
	gsumsra.2	|- ( ph -> F e. U )
	gsumsra.3	|- ( ph -> R e. V )
	gsumsra.4	|- ( ph -> A e. W )
	gsumsra.5	|- ( ph -> B C_ ( Base ` R ) )
Assertion	gsumsra	|- ( ph -> ( R gsum F ) = ( A gsum F ) )

Proof

Step	Hyp	Ref	Expression
1		gsumsra.1	|- A = ( ( subringAlg ` R ) ` B )
2		gsumsra.2	|- ( ph -> F e. U )
3		gsumsra.3	|- ( ph -> R e. V )
4		gsumsra.4	|- ( ph -> A e. W )
5		gsumsra.5	|- ( ph -> B C_ ( Base ` R ) )
6	1	a1i	|- ( ph -> A = ( ( subringAlg ` R ) ` B ) )
7	6 5	srabase	|- ( ph -> ( Base ` R ) = ( Base ` A ) )
8	6 5	sraaddg	|- ( ph -> ( +g ` R ) = ( +g ` A ) )
9	2 3 4 7 8	gsumpropd	|- ( ph -> ( R gsum F ) = ( A gsum F ) )