Metamath Proof Explorer


Theorem drgext0g

Description: The additive neutral element of a division ring extension. (Contributed by Thierry Arnoux, 17-Jul-2023)

Ref Expression
Hypotheses drgext.b B=subringAlgEU
drgext.1 φEDivRing
drgext.2 φUSubRingE
Assertion drgext0g φ0E=0B

Proof

Step Hyp Ref Expression
1 drgext.b B=subringAlgEU
2 drgext.1 φEDivRing
3 drgext.2 φUSubRingE
4 1 a1i φB=subringAlgEU
5 eqidd φ0E=0E
6 eqid BaseE=BaseE
7 6 subrgss USubRingEUBaseE
8 3 7 syl φUBaseE
9 4 5 8 sralmod0 φ0E=0B