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=\mathrm{subringAlg}\left(E\right)\left(U\right)$$
	drgext.1	$$⊢\phi \to E\in \mathrm{DivRing}$$
	drgext.2	$$⊢\phi \to U\in \mathrm{SubRing}\left(E\right)$$
Assertion	drgext0g	$$⊢\phi \to 0_E=0_B$$

Proof

Step	Hyp	Ref	Expression
1		drgext.b	$$⊢B=\mathrm{subringAlg}\left(E\right)\left(U\right)$$
2		drgext.1	$$⊢\phi \to E\in \mathrm{DivRing}$$
3		drgext.2	$$⊢\phi \to U\in \mathrm{SubRing}\left(E\right)$$
4	1	a1i	$$⊢\phi \to B=\mathrm{subringAlg}\left(E\right)\left(U\right)$$
5		eqidd	$$⊢\phi \to 0_E=0_E$$
6		eqid	$$⊢{\mathrm{Base}}_E={\mathrm{Base}}_E$$
7	6	subrgss	$$⊢U\in \mathrm{SubRing}\left(E\right)\to U\subseteq {\mathrm{Base}}_E$$
8	3 7	syl	$$⊢\phi \to U\subseteq {\mathrm{Base}}_E$$
9	4 5 8	sralmod0	$$⊢\phi \to 0_E=0_B$$