Theorem 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	|- ( ph -> E e. DivRing )
	drgext.2	|- ( ph -> U e. ( SubRing ` E ) )
	drgext.f	|- F = ( E |`s U )
	drgext.3	|- ( ph -> F e. DivRing )
	drgextgsum.1	|- ( ph -> X e. V )
Assertion	drgextgsum	|- ( ph -> ( E gsum ( i e. X |-> Y ) ) = ( B gsum ( i e. X |-> Y ) ) )

Proof

Step	Hyp	Ref	Expression
1		drgext.b	|- B = ( ( subringAlg ` E ) ` U )
2		drgext.1	|- ( ph -> E e. DivRing )
3		drgext.2	|- ( ph -> U e. ( SubRing ` E ) )
4		drgext.f	|- F = ( E |`s U )
5		drgext.3	|- ( ph -> F e. DivRing )
6		drgextgsum.1	|- ( ph -> X e. V )
7	6	mptexd	|- ( ph -> ( i e. X |-> Y ) e. _V )
8	1 4	sralvec	|- ( ( E e. DivRing /\ F e. DivRing /\ U e. ( SubRing ` E ) ) -> B e. LVec )
9	2 5 3 8	syl3anc	|- ( ph -> B e. LVec )
10		eqid	|- ( Base ` E ) = ( Base ` E )
11	10	subrgss	|- ( U e. ( SubRing ` E ) -> U C_ ( Base ` E ) )
12	3 11	syl	|- ( ph -> U C_ ( Base ` E ) )
13	1 7 2 9 12	gsumsra	|- ( ph -> ( E gsum ( i e. X |-> Y ) ) = ( B gsum ( i e. X |-> Y ) ) )