Theorem drgextgsum

Description: Group sum in a division ring extension. (Contributed by Thierry Arnoux, 17-Jul-2023)

	Ref	Expression
Hypotheses	drgext.b	$$⊢B=\mathrm{subringAlg}\left(E\right)\left(U\right)$$
	drgext.1	$$⊢\phi \to E\in \mathrm{DivRing}$$
	drgext.2	$$⊢\phi \to U\in \mathrm{SubRing}\left(E\right)$$
	drgext.f	$$⊢F=E{\upharpoonright }_{𝑠}U$$
	drgext.3	$$⊢\phi \to F\in \mathrm{DivRing}$$
	drgextgsum.1	$$⊢\phi \to X\in V$$
Assertion	drgextgsum	$$⊢\phi \to \underset{i\in X}{{\sum }_E}Y=\underset{i\in X}{{\sum }_B}Y$$

Proof

Step	Hyp	Ref	Expression
1		drgext.b	$$⊢B=\mathrm{subringAlg}\left(E\right)\left(U\right)$$
2		drgext.1	$$⊢\phi \to E\in \mathrm{DivRing}$$
3		drgext.2	$$⊢\phi \to U\in \mathrm{SubRing}\left(E\right)$$
4		drgext.f	$$⊢F=E{\upharpoonright }_{𝑠}U$$
5		drgext.3	$$⊢\phi \to F\in \mathrm{DivRing}$$
6		drgextgsum.1	$$⊢\phi \to X\in V$$
7	6	mptexd	$$⊢\phi \to \left(i\in X⟼Y\right)\in \mathrm{V}$$
8	1 4	sralvec	$$⊢\left(E\in \mathrm{DivRing}\wedge F\in \mathrm{DivRing}\wedge U\in \mathrm{SubRing}\left(E\right)\right)\to B\in \mathrm{LVec}$$
9	2 5 3 8	syl3anc	$$⊢\phi \to B\in \mathrm{LVec}$$
10		eqid	$$⊢{\mathrm{Base}}_E={\mathrm{Base}}_E$$
11	10	subrgss	$$⊢U\in \mathrm{SubRing}\left(E\right)\to U\subseteq {\mathrm{Base}}_E$$
12	3 11	syl	$$⊢\phi \to U\subseteq {\mathrm{Base}}_E$$
13	1 7 2 9 12	gsumsra	$$⊢\phi \to \underset{i\in X}{{\sum }_E}Y=\underset{i\in X}{{\sum }_B}Y$$