Theorem sdrgdvcl

Description: A sub-division-ring is closed under the ring division operation. (Contributed by Thierry Arnoux, 15-Jan-2025)

	Ref	Expression
Hypotheses	sdrgdvcl.i	$$⊢\underset{\dot{}}{\times }={/}_r\left(R\right)$$
	sdrgdvcl.0	$$⊢\underset{\dot{}}{0}=0_R$$
	sdrgdvcl.a	$$⊢\phi \to A\in \mathrm{SubDRing}\left(R\right)$$
	sdrgdvcl.x	$$⊢\phi \to X\in A$$
	sdrgdvcl.y	$$⊢\phi \to Y\in A$$
	sdrgdvcl.1	$$⊢\phi \to Y\ne \underset{\dot{}}{0}$$
Assertion	sdrgdvcl	$$⊢\phi \to X\underset{\dot{}}{\times }Y\in A$$

Proof

Step	Hyp	Ref	Expression
1		sdrgdvcl.i	$$⊢\underset{\dot{}}{\times }={/}_r\left(R\right)$$
2		sdrgdvcl.0	$$⊢\underset{\dot{}}{0}=0_R$$
3		sdrgdvcl.a	$$⊢\phi \to A\in \mathrm{SubDRing}\left(R\right)$$
4		sdrgdvcl.x	$$⊢\phi \to X\in A$$
5		sdrgdvcl.y	$$⊢\phi \to Y\in A$$
6		sdrgdvcl.1	$$⊢\phi \to Y\ne \underset{\dot{}}{0}$$
7		issdrg	$$⊢A\in \mathrm{SubDRing}\left(R\right)\leftrightarrow \left(R\in \mathrm{DivRing}\wedge A\in \mathrm{SubRing}\left(R\right)\wedge R{\upharpoonright }_{𝑠}A\in \mathrm{DivRing}\right)$$
8	3 7	sylib	$$⊢\phi \to \left(R\in \mathrm{DivRing}\wedge A\in \mathrm{SubRing}\left(R\right)\wedge R{\upharpoonright }_{𝑠}A\in \mathrm{DivRing}\right)$$
9	8	simp3d	$$⊢\phi \to R{\upharpoonright }_{𝑠}A\in \mathrm{DivRing}$$
10	9	drngringd	$$⊢\phi \to R{\upharpoonright }_{𝑠}A\in \mathrm{Ring}$$
11	8	simp2d	$$⊢\phi \to A\in \mathrm{SubRing}\left(R\right)$$
12		eqid	$$⊢R{\upharpoonright }_{𝑠}A=R{\upharpoonright }_{𝑠}A$$
13	12	subrgbas	$$⊢A\in \mathrm{SubRing}\left(R\right)\to A={\mathrm{Base}}_{\left(R{\upharpoonright }_{𝑠}A\right)}$$
14	11 13	syl	$$⊢\phi \to A={\mathrm{Base}}_{\left(R{\upharpoonright }_{𝑠}A\right)}$$
15	4 14	eleqtrd	$$⊢\phi \to X\in {\mathrm{Base}}_{\left(R{\upharpoonright }_{𝑠}A\right)}$$
16	5 14	eleqtrd	$$⊢\phi \to Y\in {\mathrm{Base}}_{\left(R{\upharpoonright }_{𝑠}A\right)}$$
17	12 2	subrg0	$$⊢A\in \mathrm{SubRing}\left(R\right)\to \underset{\dot{}}{0}=0_{\left(R{\upharpoonright }_{𝑠}A\right)}$$
18	11 17	syl	$$⊢\phi \to \underset{\dot{}}{0}=0_{\left(R{\upharpoonright }_{𝑠}A\right)}$$
19	6 18	neeqtrd	$$⊢\phi \to Y\ne 0_{\left(R{\upharpoonright }_{𝑠}A\right)}$$
20		eqid	$$⊢{\mathrm{Base}}_{\left(R{\upharpoonright }_{𝑠}A\right)}={\mathrm{Base}}_{\left(R{\upharpoonright }_{𝑠}A\right)}$$
21		eqid	$$⊢\mathrm{Unit}\left(R{\upharpoonright }_{𝑠}A\right)=\mathrm{Unit}\left(R{\upharpoonright }_{𝑠}A\right)$$
22		eqid	$$⊢0_{\left(R{\upharpoonright }_{𝑠}A\right)}=0_{\left(R{\upharpoonright }_{𝑠}A\right)}$$
23	20 21 22	drngunit	$$⊢R{\upharpoonright }_{𝑠}A\in \mathrm{DivRing}\to \left(Y\in \mathrm{Unit}\left(R{\upharpoonright }_{𝑠}A\right)\leftrightarrow \left(Y\in {\mathrm{Base}}_{\left(R{\upharpoonright }_{𝑠}A\right)}\wedge Y\ne 0_{\left(R{\upharpoonright }_{𝑠}A\right)}\right)\right)$$
24	23	biimpar	$$⊢\left(R{\upharpoonright }_{𝑠}A\in \mathrm{DivRing}\wedge \left(Y\in {\mathrm{Base}}_{\left(R{\upharpoonright }_{𝑠}A\right)}\wedge Y\ne 0_{\left(R{\upharpoonright }_{𝑠}A\right)}\right)\right)\to Y\in \mathrm{Unit}\left(R{\upharpoonright }_{𝑠}A\right)$$
25	9 16 19 24	syl12anc	$$⊢\phi \to Y\in \mathrm{Unit}\left(R{\upharpoonright }_{𝑠}A\right)$$
26		eqid	$$⊢{/}_r\left(R{\upharpoonright }_{𝑠}A\right)={/}_r\left(R{\upharpoonright }_{𝑠}A\right)$$
27	20 21 26	dvrcl	$$⊢\left(R{\upharpoonright }_{𝑠}A\in \mathrm{Ring}\wedge X\in {\mathrm{Base}}_{\left(R{\upharpoonright }_{𝑠}A\right)}\wedge Y\in \mathrm{Unit}\left(R{\upharpoonright }_{𝑠}A\right)\right)\to X{/}_r\left(R{\upharpoonright }_{𝑠}A\right)Y\in {\mathrm{Base}}_{\left(R{\upharpoonright }_{𝑠}A\right)}$$
28	10 15 25 27	syl3anc	$$⊢\phi \to X{/}_r\left(R{\upharpoonright }_{𝑠}A\right)Y\in {\mathrm{Base}}_{\left(R{\upharpoonright }_{𝑠}A\right)}$$
29	12 1 21 26	subrgdv	$$⊢\left(A\in \mathrm{SubRing}\left(R\right)\wedge X\in A\wedge Y\in \mathrm{Unit}\left(R{\upharpoonright }_{𝑠}A\right)\right)\to X\underset{\dot{}}{\times }Y=X{/}_r\left(R{\upharpoonright }_{𝑠}A\right)Y$$
30	11 4 25 29	syl3anc	$$⊢\phi \to X\underset{\dot{}}{\times }Y=X{/}_r\left(R{\upharpoonright }_{𝑠}A\right)Y$$
31	28 30 14	3eltr4d	$$⊢\phi \to X\underset{\dot{}}{\times }Y\in A$$