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 φ E DivRing
drgext.2 φ U SubRing E
drgext.f F = E 𝑠 U
drgext.3 φ F DivRing
drgextgsum.1 φ X V
Assertion drgextgsum φ E i X Y = B i X Y

Proof

Step Hyp Ref Expression
1 drgext.b B = subringAlg E U
2 drgext.1 φ E DivRing
3 drgext.2 φ U SubRing E
4 drgext.f F = E 𝑠 U
5 drgext.3 φ F DivRing
6 drgextgsum.1 φ X V
7 6 mptexd φ i X Y V
8 1 4 sralvec E DivRing F DivRing U SubRing E B LVec
9 2 5 3 8 syl3anc φ B LVec
10 eqid Base E = Base E
11 10 subrgss U SubRing E U Base E
12 3 11 syl φ U Base E
13 1 7 2 9 12 gsumsra φ E i X Y = B i X Y