isdrngd

Description: Properties that characterize a division ring among rings: it should be nonzero, have no nonzero zero-divisors, and every nonzero element x should have a left-inverse I ( x ) . See isdrngrd for the characterization using right-inverses. (Contributed by NM, 2-Aug-2013) Remove hypothesis. (Revised by SN, 19-Feb-2025)

	Ref	Expression
Hypotheses	isdrngd.b	$⊢ φ \to B = {Base}_{R}$
	isdrngd.t	$⊢ φ \to \underset{˙}{\cdot} = \cdot_{R}$
	isdrngd.z	$⊢ φ \to \underset{˙}{0} = 0_{R}$
	isdrngd.u	$⊢ φ \to \underset{˙}{1} = 1_{R}$
	isdrngd.r	$⊢ φ \to R \in Ring$
	isdrngd.n	$⊢ (φ \land (x \in B \land x \neq \underset{˙}{0}) \land (y \in B \land y \neq \underset{˙}{0})) \to x \underset{˙}{\cdot} y \neq \underset{˙}{0}$
	isdrngd.o	$⊢ φ \to \underset{˙}{1} \neq \underset{˙}{0}$
	isdrngd.i	$⊢ (φ \land (x \in B \land x \neq \underset{˙}{0})) \to I \in B$
	isdrngd.k	$⊢ (φ \land (x \in B \land x \neq \underset{˙}{0})) \to I \underset{˙}{\cdot} x = \underset{˙}{1}$
Assertion	isdrngd	$⊢ φ \to R \in DivRing$

Proof

Step	Hyp	Ref	Expression
1		isdrngd.b	$⊢ φ \to B = {Base}_{R}$
2		isdrngd.t	$⊢ φ \to \underset{˙}{\cdot} = \cdot_{R}$
3		isdrngd.z	$⊢ φ \to \underset{˙}{0} = 0_{R}$
4		isdrngd.u	$⊢ φ \to \underset{˙}{1} = 1_{R}$
5		isdrngd.r	$⊢ φ \to R \in Ring$
6		isdrngd.n	$⊢ (φ \land (x \in B \land x \neq \underset{˙}{0}) \land (y \in B \land y \neq \underset{˙}{0})) \to x \underset{˙}{\cdot} y \neq \underset{˙}{0}$
7		isdrngd.o	$⊢ φ \to \underset{˙}{1} \neq \underset{˙}{0}$
8		isdrngd.i	$⊢ (φ \land (x \in B \land x \neq \underset{˙}{0})) \to I \in B$
9		isdrngd.k	$⊢ (φ \land (x \in B \land x \neq \underset{˙}{0})) \to I \underset{˙}{\cdot} x = \underset{˙}{1}$
10		difss	$⊢ B ∖ \{\underset{˙}{0}\} \subseteq B$
11	10 1	sseqtrid	$⊢ φ \to B ∖ \{\underset{˙}{0}\} \subseteq {Base}_{R}$
12		eqid	$⊢ {mulGrp}_{R} ↾_{𝑠} (B ∖ \{\underset{˙}{0}\}) = {mulGrp}_{R} ↾_{𝑠} (B ∖ \{\underset{˙}{0}\})$
13		eqid	$⊢ {mulGrp}_{R} = {mulGrp}_{R}$
14		eqid	$⊢ {Base}_{R} = {Base}_{R}$
15	13 14	mgpbas	$⊢ {Base}_{R} = {Base}_{{mulGrp}_{R}}$
16	12 15	ressbas2	$⊢ B ∖ \{\underset{˙}{0}\} \subseteq {Base}_{R} \to B ∖ \{\underset{˙}{0}\} = {Base}_{({mulGrp}_{R} ↾_{𝑠} (B ∖ \{\underset{˙}{0}\}))}$
17	11 16	syl	$⊢ φ \to B ∖ \{\underset{˙}{0}\} = {Base}_{({mulGrp}_{R} ↾_{𝑠} (B ∖ \{\underset{˙}{0}\}))}$
18		fvex	$⊢ {Base}_{R} \in V$
19	1 18	eqeltrdi	$⊢ φ \to B \in V$
20		difexg	$⊢ B \in V \to B ∖ \{\underset{˙}{0}\} \in V$
21		eqid	$⊢ \cdot_{R} = \cdot_{R}$
22	13 21	mgpplusg	$⊢ \cdot_{R} = +_{{mulGrp}_{R}}$
23	12 22	ressplusg	$⊢ B ∖ \{\underset{˙}{0}\} \in V \to \cdot_{R} = +_{({mulGrp}_{R} ↾_{𝑠} (B ∖ \{\underset{˙}{0}\}))}$
24	19 20 23	3syl	$⊢ φ \to \cdot_{R} = +_{({mulGrp}_{R} ↾_{𝑠} (B ∖ \{\underset{˙}{0}\}))}$
25	2 24	eqtrd	$⊢ φ \to \underset{˙}{\cdot} = +_{({mulGrp}_{R} ↾_{𝑠} (B ∖ \{\underset{˙}{0}\}))}$
26		eldifsn	$⊢ x \in (B ∖ \{\underset{˙}{0}\}) \leftrightarrow (x \in B \land x \neq \underset{˙}{0})$
27		eldifsn	$⊢ y \in (B ∖ \{\underset{˙}{0}\}) \leftrightarrow (y \in B \land y \neq \underset{˙}{0})$
28	14 21	ringcl	$⊢ (R \in Ring \land x \in {Base}_{R} \land y \in {Base}_{R}) \to x \cdot_{R} y \in {Base}_{R}$
29	5 28	syl3an1	$⊢ (φ \land x \in {Base}_{R} \land y \in {Base}_{R}) \to x \cdot_{R} y \in {Base}_{R}$
30	29	3expib	$⊢ φ \to ((x \in {Base}_{R} \land y \in {Base}_{R}) \to x \cdot_{R} y \in {Base}_{R})$
31	1	eleq2d	$⊢ φ \to (x \in B \leftrightarrow x \in {Base}_{R})$
32	1	eleq2d	$⊢ φ \to (y \in B \leftrightarrow y \in {Base}_{R})$
33	31 32	anbi12d	$⊢ φ \to ((x \in B \land y \in B) \leftrightarrow (x \in {Base}_{R} \land y \in {Base}_{R}))$
34	2	oveqd	$⊢ φ \to x \underset{˙}{\cdot} y = x \cdot_{R} y$
35	34 1	eleq12d	$⊢ φ \to (x \underset{˙}{\cdot} y \in B \leftrightarrow x \cdot_{R} y \in {Base}_{R})$
36	30 33 35	3imtr4d	$⊢ φ \to ((x \in B \land y \in B) \to x \underset{˙}{\cdot} y \in B)$
37	36	3impib	$⊢ (φ \land x \in B \land y \in B) \to x \underset{˙}{\cdot} y \in B$
38	37	3adant2r	$⊢ (φ \land (x \in B \land x \neq \underset{˙}{0}) \land y \in B) \to x \underset{˙}{\cdot} y \in B$
39	38	3adant3r	$⊢ (φ \land (x \in B \land x \neq \underset{˙}{0}) \land (y \in B \land y \neq \underset{˙}{0})) \to x \underset{˙}{\cdot} y \in B$
40		eldifsn	$⊢ x \underset{˙}{\cdot} y \in (B ∖ \{\underset{˙}{0}\}) \leftrightarrow (x \underset{˙}{\cdot} y \in B \land x \underset{˙}{\cdot} y \neq \underset{˙}{0})$
41	39 6 40	sylanbrc	$⊢ (φ \land (x \in B \land x \neq \underset{˙}{0}) \land (y \in B \land y \neq \underset{˙}{0})) \to x \underset{˙}{\cdot} y \in (B ∖ \{\underset{˙}{0}\})$
42	27 41	syl3an3b	$⊢ (φ \land (x \in B \land x \neq \underset{˙}{0}) \land y \in (B ∖ \{\underset{˙}{0}\})) \to x \underset{˙}{\cdot} y \in (B ∖ \{\underset{˙}{0}\})$
43	26 42	syl3an2b	$⊢ (φ \land x \in (B ∖ \{\underset{˙}{0}\}) \land y \in (B ∖ \{\underset{˙}{0}\})) \to x \underset{˙}{\cdot} y \in (B ∖ \{\underset{˙}{0}\})$
44	14 21	ringass	$⊢ (R \in Ring \land (x \in {Base}_{R} \land y \in {Base}_{R} \land z \in {Base}_{R})) \to (x \cdot_{R} y) \cdot_{R} z = x \cdot_{R} (y \cdot_{R} z)$
45	44	ex	$⊢ R \in Ring \to ((x \in {Base}_{R} \land y \in {Base}_{R} \land z \in {Base}_{R}) \to (x \cdot_{R} y) \cdot_{R} z = x \cdot_{R} (y \cdot_{R} z))$
46	5 45	syl	$⊢ φ \to ((x \in {Base}_{R} \land y \in {Base}_{R} \land z \in {Base}_{R}) \to (x \cdot_{R} y) \cdot_{R} z = x \cdot_{R} (y \cdot_{R} z))$
47	1	eleq2d	$⊢ φ \to (z \in B \leftrightarrow z \in {Base}_{R})$
48	31 32 47	3anbi123d	$⊢ φ \to ((x \in B \land y \in B \land z \in B) \leftrightarrow (x \in {Base}_{R} \land y \in {Base}_{R} \land z \in {Base}_{R}))$
49		eqidd	$⊢ φ \to z = z$
50	2 34 49	oveq123d	$⊢ φ \to (x \underset{˙}{\cdot} y) \underset{˙}{\cdot} z = (x \cdot_{R} y) \cdot_{R} z$
51		eqidd	$⊢ φ \to x = x$
52	2	oveqd	$⊢ φ \to y \underset{˙}{\cdot} z = y \cdot_{R} z$
53	2 51 52	oveq123d	$⊢ φ \to x \underset{˙}{\cdot} (y \underset{˙}{\cdot} z) = x \cdot_{R} (y \cdot_{R} z)$
54	50 53	eqeq12d	$⊢ φ \to ((x \underset{˙}{\cdot} y) \underset{˙}{\cdot} z = x \underset{˙}{\cdot} (y \underset{˙}{\cdot} z) \leftrightarrow (x \cdot_{R} y) \cdot_{R} z = x \cdot_{R} (y \cdot_{R} z))$
55	46 48 54	3imtr4d	$⊢ φ \to ((x \in B \land y \in B \land z \in B) \to (x \underset{˙}{\cdot} y) \underset{˙}{\cdot} z = x \underset{˙}{\cdot} (y \underset{˙}{\cdot} z))$
56		eldifi	$⊢ x \in (B ∖ \{\underset{˙}{0}\}) \to x \in B$
57		eldifi	$⊢ y \in (B ∖ \{\underset{˙}{0}\}) \to y \in B$
58		eldifi	$⊢ z \in (B ∖ \{\underset{˙}{0}\}) \to z \in B$
59	56 57 58	3anim123i	$⊢ (x \in (B ∖ \{\underset{˙}{0}\}) \land y \in (B ∖ \{\underset{˙}{0}\}) \land z \in (B ∖ \{\underset{˙}{0}\})) \to (x \in B \land y \in B \land z \in B)$
60	55 59	impel	$⊢ (φ \land (x \in (B ∖ \{\underset{˙}{0}\}) \land y \in (B ∖ \{\underset{˙}{0}\}) \land z \in (B ∖ \{\underset{˙}{0}\}))) \to (x \underset{˙}{\cdot} y) \underset{˙}{\cdot} z = x \underset{˙}{\cdot} (y \underset{˙}{\cdot} z)$
61		eqid	$⊢ 1_{R} = 1_{R}$
62	14 61	ringidcl	$⊢ R \in Ring \to 1_{R} \in {Base}_{R}$
63	5 62	syl	$⊢ φ \to 1_{R} \in {Base}_{R}$
64	63 4 1	3eltr4d	$⊢ φ \to \underset{˙}{1} \in B$
65		eldifsn	$⊢ \underset{˙}{1} \in (B ∖ \{\underset{˙}{0}\}) \leftrightarrow (\underset{˙}{1} \in B \land \underset{˙}{1} \neq \underset{˙}{0})$
66	64 7 65	sylanbrc	$⊢ φ \to \underset{˙}{1} \in (B ∖ \{\underset{˙}{0}\})$
67	14 21 61	ringlidm	$⊢ (R \in Ring \land x \in {Base}_{R}) \to 1_{R} \cdot_{R} x = x$
68	67	ex	$⊢ R \in Ring \to (x \in {Base}_{R} \to 1_{R} \cdot_{R} x = x)$
69	5 68	syl	$⊢ φ \to (x \in {Base}_{R} \to 1_{R} \cdot_{R} x = x)$
70	2 4 51	oveq123d	$⊢ φ \to \underset{˙}{1} \underset{˙}{\cdot} x = 1_{R} \cdot_{R} x$
71	70	eqeq1d	$⊢ φ \to (\underset{˙}{1} \underset{˙}{\cdot} x = x \leftrightarrow 1_{R} \cdot_{R} x = x)$
72	69 31 71	3imtr4d	$⊢ φ \to (x \in B \to \underset{˙}{1} \underset{˙}{\cdot} x = x)$
73	72	imp	$⊢ (φ \land x \in B) \to \underset{˙}{1} \underset{˙}{\cdot} x = x$
74	73	adantrr	$⊢ (φ \land (x \in B \land x \neq \underset{˙}{0})) \to \underset{˙}{1} \underset{˙}{\cdot} x = x$
75	26 74	sylan2b	$⊢ (φ \land x \in (B ∖ \{\underset{˙}{0}\})) \to \underset{˙}{1} \underset{˙}{\cdot} x = x$
76	7	adantr	$⊢ (φ \land (x \in B \land x \neq \underset{˙}{0})) \to \underset{˙}{1} \neq \underset{˙}{0}$
77		simpr	$⊢ ((φ \land (x \in B \land x \neq \underset{˙}{0})) \land I = \underset{˙}{0}) \to I = \underset{˙}{0}$
78	77	oveq1d	$⊢ ((φ \land (x \in B \land x \neq \underset{˙}{0})) \land I = \underset{˙}{0}) \to I \underset{˙}{\cdot} x = \underset{˙}{0} \underset{˙}{\cdot} x$
79	9	adantr	$⊢ ((φ \land (x \in B \land x \neq \underset{˙}{0})) \land I = \underset{˙}{0}) \to I \underset{˙}{\cdot} x = \underset{˙}{1}$
80	31	biimpa	$⊢ (φ \land x \in B) \to x \in {Base}_{R}$
81	80	adantrr	$⊢ (φ \land (x \in B \land x \neq \underset{˙}{0})) \to x \in {Base}_{R}$
82		eqid	$⊢ 0_{R} = 0_{R}$
83	14 21 82	ringlz	$⊢ (R \in Ring \land x \in {Base}_{R}) \to 0_{R} \cdot_{R} x = 0_{R}$
84	5 81 83	syl2an2r	$⊢ (φ \land (x \in B \land x \neq \underset{˙}{0})) \to 0_{R} \cdot_{R} x = 0_{R}$
85	2 3 51	oveq123d	$⊢ φ \to \underset{˙}{0} \underset{˙}{\cdot} x = 0_{R} \cdot_{R} x$
86	85	adantr	$⊢ (φ \land (x \in B \land x \neq \underset{˙}{0})) \to \underset{˙}{0} \underset{˙}{\cdot} x = 0_{R} \cdot_{R} x$
87	3	adantr	$⊢ (φ \land (x \in B \land x \neq \underset{˙}{0})) \to \underset{˙}{0} = 0_{R}$
88	84 86 87	3eqtr4d	$⊢ (φ \land (x \in B \land x \neq \underset{˙}{0})) \to \underset{˙}{0} \underset{˙}{\cdot} x = \underset{˙}{0}$
89	88	adantr	$⊢ ((φ \land (x \in B \land x \neq \underset{˙}{0})) \land I = \underset{˙}{0}) \to \underset{˙}{0} \underset{˙}{\cdot} x = \underset{˙}{0}$
90	78 79 89	3eqtr3d	$⊢ ((φ \land (x \in B \land x \neq \underset{˙}{0})) \land I = \underset{˙}{0}) \to \underset{˙}{1} = \underset{˙}{0}$
91	76 90	mteqand	$⊢ (φ \land (x \in B \land x \neq \underset{˙}{0})) \to I \neq \underset{˙}{0}$
92		eldifsn	$⊢ I \in (B ∖ \{\underset{˙}{0}\}) \leftrightarrow (I \in B \land I \neq \underset{˙}{0})$
93	8 91 92	sylanbrc	$⊢ (φ \land (x \in B \land x \neq \underset{˙}{0})) \to I \in (B ∖ \{\underset{˙}{0}\})$
94	26 93	sylan2b	$⊢ (φ \land x \in (B ∖ \{\underset{˙}{0}\})) \to I \in (B ∖ \{\underset{˙}{0}\})$
95	26 9	sylan2b	$⊢ (φ \land x \in (B ∖ \{\underset{˙}{0}\})) \to I \underset{˙}{\cdot} x = \underset{˙}{1}$
96	17 25 43 60 66 75 94 95	isgrpd	$⊢ φ \to {mulGrp}_{R} ↾_{𝑠} (B ∖ \{\underset{˙}{0}\}) \in Grp$
97	3	sneqd	$⊢ φ \to \{\underset{˙}{0}\} = \{0_{R}\}$
98	1 97	difeq12d	$⊢ φ \to B ∖ \{\underset{˙}{0}\} = {Base}_{R} ∖ \{0_{R}\}$
99	98	oveq2d	$⊢ φ \to {mulGrp}_{R} ↾_{𝑠} (B ∖ \{\underset{˙}{0}\}) = {mulGrp}_{R} ↾_{𝑠} ({Base}_{R} ∖ \{0_{R}\})$
100	99	eleq1d	$⊢ φ \to ({mulGrp}_{R} ↾_{𝑠} (B ∖ \{\underset{˙}{0}\}) \in Grp \leftrightarrow {mulGrp}_{R} ↾_{𝑠} ({Base}_{R} ∖ \{0_{R}\}) \in Grp)$
101	100	anbi2d	$⊢ φ \to ((R \in Ring \land {mulGrp}_{R} ↾_{𝑠} (B ∖ \{\underset{˙}{0}\}) \in Grp) \leftrightarrow (R \in Ring \land {mulGrp}_{R} ↾_{𝑠} ({Base}_{R} ∖ \{0_{R}\}) \in Grp))$
102	5 96 101	mpbi2and	$⊢ φ \to (R \in Ring \land {mulGrp}_{R} ↾_{𝑠} ({Base}_{R} ∖ \{0_{R}\}) \in Grp)$
103		eqid	$⊢ {mulGrp}_{R} ↾_{𝑠} ({Base}_{R} ∖ \{0_{R}\}) = {mulGrp}_{R} ↾_{𝑠} ({Base}_{R} ∖ \{0_{R}\})$
104	14 82 103	isdrng2	$⊢ R \in DivRing \leftrightarrow (R \in Ring \land {mulGrp}_{R} ↾_{𝑠} ({Base}_{R} ∖ \{0_{R}\}) \in Grp)$
105	102 104	sylibr	$⊢ φ \to R \in DivRing$

Metamath Proof Explorer

Theorem isdrngd

Proof