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=\mathrm{subringAlg}\left(R\right)\left(B\right)$$
	gsumsra.2	$$⊢\phi \to F\in U$$
	gsumsra.3	$$⊢\phi \to R\in V$$
	gsumsra.4	$$⊢\phi \to A\in W$$
	gsumsra.5	$$⊢\phi \to B\subseteq {\mathrm{Base}}_R$$
Assertion	gsumsra	$$⊢\phi \to {\sum }_{R}F={\sum }_{A}F$$

Proof

Step	Hyp	Ref	Expression
1		gsumsra.1	$$⊢A=\mathrm{subringAlg}\left(R\right)\left(B\right)$$
2		gsumsra.2	$$⊢\phi \to F\in U$$
3		gsumsra.3	$$⊢\phi \to R\in V$$
4		gsumsra.4	$$⊢\phi \to A\in W$$
5		gsumsra.5	$$⊢\phi \to B\subseteq {\mathrm{Base}}_R$$
6	1	a1i	$$⊢\phi \to A=\mathrm{subringAlg}\left(R\right)\left(B\right)$$
7	6 5	srabase	$$⊢\phi \to {\mathrm{Base}}_R={\mathrm{Base}}_A$$
8	6 5	sraaddg	$$⊢\phi \to {+}_R={+}_A$$
9	2 3 4 7 8	gsumpropd	$$⊢\phi \to {\sum }_{R}F={\sum }_{A}F$$