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 isdrngd for the characterization using right-inverses. (Contributed by NM, 2-Aug-2013)

	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.j	$⊢ (φ \land (x \in B \land x \neq \underset{˙}{0})) \to I \neq \underset{˙}{0}$
	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.j	$⊢ (φ \land (x \in B \land x \neq \underset{˙}{0})) \to I \neq \underset{˙}{0}$
10		isdrngd.k	$⊢ (φ \land (x \in B \land x \neq \underset{˙}{0})) \to I \underset{˙}{\cdot} x = \underset{˙}{1}$
11		difss	$⊢ B ∖ \{\underset{˙}{0}\} \subseteq B$
12	11 1	sseqtrid	$⊢ φ \to B ∖ \{\underset{˙}{0}\} \subseteq {Base}_{R}$
13		eqid	$⊢ {mulGrp}_{R} ↾_{𝑠} (B ∖ \{\underset{˙}{0}\}) = {mulGrp}_{R} ↾_{𝑠} (B ∖ \{\underset{˙}{0}\})$
14		eqid	$⊢ {mulGrp}_{R} = {mulGrp}_{R}$
15		eqid	$⊢ {Base}_{R} = {Base}_{R}$
16	14 15	mgpbas	$⊢ {Base}_{R} = {Base}_{{mulGrp}_{R}}$
17	13 16	ressbas2	$⊢ B ∖ \{\underset{˙}{0}\} \subseteq {Base}_{R} \to B ∖ \{\underset{˙}{0}\} = {Base}_{({mulGrp}_{R} ↾_{𝑠} (B ∖ \{\underset{˙}{0}\}))}$
18	12 17	syl	$⊢ φ \to B ∖ \{\underset{˙}{0}\} = {Base}_{({mulGrp}_{R} ↾_{𝑠} (B ∖ \{\underset{˙}{0}\}))}$
19		fvex	$⊢ {Base}_{R} \in V$
20	1 19	eqeltrdi	$⊢ φ \to B \in V$
21		difexg	$⊢ B \in V \to B ∖ \{\underset{˙}{0}\} \in V$
22		eqid	$⊢ \cdot_{R} = \cdot_{R}$
23	14 22	mgpplusg	$⊢ \cdot_{R} = +_{{mulGrp}_{R}}$
24	13 23	ressplusg	$⊢ B ∖ \{\underset{˙}{0}\} \in V \to \cdot_{R} = +_{({mulGrp}_{R} ↾_{𝑠} (B ∖ \{\underset{˙}{0}\}))}$
25	20 21 24	3syl	$⊢ φ \to \cdot_{R} = +_{({mulGrp}_{R} ↾_{𝑠} (B ∖ \{\underset{˙}{0}\}))}$
26	2 25	eqtrd	$⊢ φ \to \underset{˙}{\cdot} = +_{({mulGrp}_{R} ↾_{𝑠} (B ∖ \{\underset{˙}{0}\}))}$
27		eldifsn	$⊢ x \in (B ∖ \{\underset{˙}{0}\}) \leftrightarrow (x \in B \land x \neq \underset{˙}{0})$
28		eldifsn	$⊢ y \in (B ∖ \{\underset{˙}{0}\}) \leftrightarrow (y \in B \land y \neq \underset{˙}{0})$
29	15 22	ringcl	$⊢ (R \in Ring \land x \in {Base}_{R} \land y \in {Base}_{R}) \to x \cdot_{R} y \in {Base}_{R}$
30	5 29	syl3an1	$⊢ (φ \land x \in {Base}_{R} \land y \in {Base}_{R}) \to x \cdot_{R} y \in {Base}_{R}$
31	30	3expib	$⊢ φ \to ((x \in {Base}_{R} \land y \in {Base}_{R}) \to x \cdot_{R} y \in {Base}_{R})$
32	1	eleq2d	$⊢ φ \to (x \in B \leftrightarrow x \in {Base}_{R})$
33	1	eleq2d	$⊢ φ \to (y \in B \leftrightarrow y \in {Base}_{R})$
34	32 33	anbi12d	$⊢ φ \to ((x \in B \land y \in B) \leftrightarrow (x \in {Base}_{R} \land y \in {Base}_{R}))$
35	2	oveqd	$⊢ φ \to x \underset{˙}{\cdot} y = x \cdot_{R} y$
36	35 1	eleq12d	$⊢ φ \to (x \underset{˙}{\cdot} y \in B \leftrightarrow x \cdot_{R} y \in {Base}_{R})$
37	31 34 36	3imtr4d	$⊢ φ \to ((x \in B \land y \in B) \to x \underset{˙}{\cdot} y \in B)$
38	37	3impib	$⊢ (φ \land x \in B \land y \in B) \to x \underset{˙}{\cdot} y \in B$
39	38	3adant2r	$⊢ (φ \land (x \in B \land x \neq \underset{˙}{0}) \land y \in B) \to x \underset{˙}{\cdot} y \in B$
40	39	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$
41		eldifsn	$⊢ x \underset{˙}{\cdot} y \in (B ∖ \{\underset{˙}{0}\}) \leftrightarrow (x \underset{˙}{\cdot} y \in B \land x \underset{˙}{\cdot} y \neq \underset{˙}{0})$
42	40 6 41	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}\})$
43	28 42	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}\})$
44	27 43	syl3an2b	$⊢ (φ \land x \in (B ∖ \{\underset{˙}{0}\}) \land y \in (B ∖ \{\underset{˙}{0}\})) \to x \underset{˙}{\cdot} y \in (B ∖ \{\underset{˙}{0}\})$
45	15 22	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)$
46	45	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))$
47	5 46	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))$
48	1	eleq2d	$⊢ φ \to (z \in B \leftrightarrow z \in {Base}_{R})$
49	32 33 48	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}))$
50		eqidd	$⊢ φ \to z = z$
51	2 35 50	oveq123d	$⊢ φ \to (x \underset{˙}{\cdot} y) \underset{˙}{\cdot} z = (x \cdot_{R} y) \cdot_{R} z$
52		eqidd	$⊢ φ \to x = x$
53	2	oveqd	$⊢ φ \to y \underset{˙}{\cdot} z = y \cdot_{R} z$
54	2 52 53	oveq123d	$⊢ φ \to x \underset{˙}{\cdot} (y \underset{˙}{\cdot} z) = x \cdot_{R} (y \cdot_{R} z)$
55	51 54	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))$
56	47 49 55	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))$
57		eldifi	$⊢ x \in (B ∖ \{\underset{˙}{0}\}) \to x \in B$
58		eldifi	$⊢ y \in (B ∖ \{\underset{˙}{0}\}) \to y \in B$
59		eldifi	$⊢ z \in (B ∖ \{\underset{˙}{0}\}) \to z \in B$
60	57 58 59	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)$
61	56 60	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)$
62		eqid	$⊢ 1_{R} = 1_{R}$
63	15 62	ringidcl	$⊢ R \in Ring \to 1_{R} \in {Base}_{R}$
64	5 63	syl	$⊢ φ \to 1_{R} \in {Base}_{R}$
65	64 4 1	3eltr4d	$⊢ φ \to \underset{˙}{1} \in B$
66		eldifsn	$⊢ \underset{˙}{1} \in (B ∖ \{\underset{˙}{0}\}) \leftrightarrow (\underset{˙}{1} \in B \land \underset{˙}{1} \neq \underset{˙}{0})$
67	65 7 66	sylanbrc	$⊢ φ \to \underset{˙}{1} \in (B ∖ \{\underset{˙}{0}\})$
68	15 22 62	ringlidm	$⊢ (R \in Ring \land x \in {Base}_{R}) \to 1_{R} \cdot_{R} x = x$
69	68	ex	$⊢ R \in Ring \to (x \in {Base}_{R} \to 1_{R} \cdot_{R} x = x)$
70	5 69	syl	$⊢ φ \to (x \in {Base}_{R} \to 1_{R} \cdot_{R} x = x)$
71	2 4 52	oveq123d	$⊢ φ \to \underset{˙}{1} \underset{˙}{\cdot} x = 1_{R} \cdot_{R} x$
72	71	eqeq1d	$⊢ φ \to (\underset{˙}{1} \underset{˙}{\cdot} x = x \leftrightarrow 1_{R} \cdot_{R} x = x)$
73	70 32 72	3imtr4d	$⊢ φ \to (x \in B \to \underset{˙}{1} \underset{˙}{\cdot} x = x)$
74	73	imp	$⊢ (φ \land x \in B) \to \underset{˙}{1} \underset{˙}{\cdot} x = x$
75	74	adantrr	$⊢ (φ \land (x \in B \land x \neq \underset{˙}{0})) \to \underset{˙}{1} \underset{˙}{\cdot} x = x$
76	27 75	sylan2b	$⊢ (φ \land x \in (B ∖ \{\underset{˙}{0}\})) \to \underset{˙}{1} \underset{˙}{\cdot} x = x$
77		eldifsn	$⊢ I \in (B ∖ \{\underset{˙}{0}\}) \leftrightarrow (I \in B \land I \neq \underset{˙}{0})$
78	8 9 77	sylanbrc	$⊢ (φ \land (x \in B \land x \neq \underset{˙}{0})) \to I \in (B ∖ \{\underset{˙}{0}\})$
79	27 78	sylan2b	$⊢ (φ \land x \in (B ∖ \{\underset{˙}{0}\})) \to I \in (B ∖ \{\underset{˙}{0}\})$
80	27 10	sylan2b	$⊢ (φ \land x \in (B ∖ \{\underset{˙}{0}\})) \to I \underset{˙}{\cdot} x = \underset{˙}{1}$
81	18 26 44 61 67 76 79 80	isgrpd	$⊢ φ \to {mulGrp}_{R} ↾_{𝑠} (B ∖ \{\underset{˙}{0}\}) \in Grp$
82	3	sneqd	$⊢ φ \to \{\underset{˙}{0}\} = \{0_{R}\}$
83	1 82	difeq12d	$⊢ φ \to B ∖ \{\underset{˙}{0}\} = {Base}_{R} ∖ \{0_{R}\}$
84	83	oveq2d	$⊢ φ \to {mulGrp}_{R} ↾_{𝑠} (B ∖ \{\underset{˙}{0}\}) = {mulGrp}_{R} ↾_{𝑠} ({Base}_{R} ∖ \{0_{R}\})$
85	84	eleq1d	$⊢ φ \to ({mulGrp}_{R} ↾_{𝑠} (B ∖ \{\underset{˙}{0}\}) \in Grp \leftrightarrow {mulGrp}_{R} ↾_{𝑠} ({Base}_{R} ∖ \{0_{R}\}) \in Grp)$
86	85	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))$
87	5 81 86	mpbi2and	$⊢ φ \to (R \in Ring \land {mulGrp}_{R} ↾_{𝑠} ({Base}_{R} ∖ \{0_{R}\}) \in Grp)$
88		eqid	$⊢ 0_{R} = 0_{R}$
89		eqid	$⊢ {mulGrp}_{R} ↾_{𝑠} ({Base}_{R} ∖ \{0_{R}\}) = {mulGrp}_{R} ↾_{𝑠} ({Base}_{R} ∖ \{0_{R}\})$
90	15 88 89	isdrng2	$⊢ R \in DivRing \leftrightarrow (R \in Ring \land {mulGrp}_{R} ↾_{𝑠} ({Base}_{R} ∖ \{0_{R}\}) \in Grp)$
91	87 90	sylibr	$⊢ φ \to R \in DivRing$

Metamath Proof Explorer

Theorem isdrngd

Proof