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{˙}{\times} = /_{r} (R)$
	sdrgdvcl.0	$⊢ \underset{˙}{0} = 0_{R}$
	sdrgdvcl.a	$⊢ φ \to A \in SubDRing (R)$
	sdrgdvcl.x	$⊢ φ \to X \in A$
	sdrgdvcl.y	$⊢ φ \to Y \in A$
	sdrgdvcl.1	$⊢ φ \to Y \neq \underset{˙}{0}$
Assertion	sdrgdvcl	$⊢ φ \to X \underset{˙}{\times} Y \in A$

Proof

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

Metamath Proof Explorer

Theorem sdrgdvcl

Proof