This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ) )