Theorem drgext0gsca

Description: The additive neutral element of the scalar field 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	drgext0gsca	$$⊢\phi \to 0_B=0_{\mathrm{Scalar}\left(B\right)}$$

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		drngring	$$⊢E\in \mathrm{DivRing}\to E\in \mathrm{Ring}$$
5		ringmnd	$$⊢E\in \mathrm{Ring}\to E\in \mathrm{Mnd}$$
6	2 4 5	3syl	$$⊢\phi \to E\in \mathrm{Mnd}$$
7		subrgsubg	$$⊢U\in \mathrm{SubRing}\left(E\right)\to U\in \mathrm{SubGrp}\left(E\right)$$
8		eqid	$$⊢0_E=0_E$$
9	8	subg0cl	$$⊢U\in \mathrm{SubGrp}\left(E\right)\to 0_E\in U$$
10	3 7 9	3syl	$$⊢\phi \to 0_E\in U$$
11		eqid	$$⊢{\mathrm{Base}}_E={\mathrm{Base}}_E$$
12	11	subrgss	$$⊢U\in \mathrm{SubRing}\left(E\right)\to U\subseteq {\mathrm{Base}}_E$$
13	3 12	syl	$$⊢\phi \to U\subseteq {\mathrm{Base}}_E$$
14		eqid	$$⊢E{\upharpoonright }_{𝑠}U=E{\upharpoonright }_{𝑠}U$$
15	14 11 8	ress0g	$$⊢\left(E\in \mathrm{Mnd}\wedge 0_E\in U\wedge U\subseteq {\mathrm{Base}}_E\right)\to 0_E=0_{\left(E{\upharpoonright }_{𝑠}U\right)}$$
16	6 10 13 15	syl3anc	$$⊢\phi \to 0_E=0_{\left(E{\upharpoonright }_{𝑠}U\right)}$$
17	1 2 3	drgext0g	$$⊢\phi \to 0_E=0_B$$
18	1	a1i	$$⊢\phi \to B=\mathrm{subringAlg}\left(E\right)\left(U\right)$$
19	18 13	srasca	$$⊢\phi \to E{\upharpoonright }_{𝑠}U=\mathrm{Scalar}\left(B\right)$$
20	19	fveq2d	$$⊢\phi \to 0_{\left(E{\upharpoonright }_{𝑠}U\right)}=0_{\mathrm{Scalar}\left(B\right)}$$
21	16 17 20	3eqtr3d	$$⊢\phi \to 0_B=0_{\mathrm{Scalar}\left(B\right)}$$