drgextgsum

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

	Ref	Expression
Hypotheses	drgext.b	$⊢ B = subringAlg (E) (U)$
	drgext.1	$⊢ φ \to E \in DivRing$
	drgext.2	$⊢ φ \to U \in SubRing (E)$
	drgext.f	$⊢ F = E ↾_{𝑠} U$
	drgext.3	$⊢ φ \to F \in DivRing$
	drgextgsum.1	$⊢ φ \to X \in V$
Assertion	drgextgsum	$⊢ φ \to \underset{i \in X}{\sum_{E}} Y = \underset{i \in X}{\sum_{B}} Y$

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

Metamath Proof Explorer