Theorem drgextvsca

Description: The scalar multiplication operation 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	drgextvsca	$$⊢\phi \to {\cdot }_E={\cdot }_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		eqid	$$⊢{\mathrm{Base}}_E={\mathrm{Base}}_E$$
6	5	subrgss	$$⊢U\in \mathrm{SubRing}\left(E\right)\to U\subseteq {\mathrm{Base}}_E$$
7	3 6	syl	$$⊢\phi \to U\subseteq {\mathrm{Base}}_E$$
8	4 7	sravsca	$$⊢\phi \to {\cdot }_E={\cdot }_B$$