isdrng3lem2

Description: Lemma for isdrng3 (for the right to left implication). Formerly part of proof for isdrng3 . (Contributed by Jeff Madsen, 8-Jun-2010) (Revised by AV, 22-Jul-2026)

	Ref	Expression
Hypotheses	isdrng3.b	$⊢ B = {Base}_{R}$
	isdrng3.0	$⊢ \underset{˙}{0} = 0_{R}$
	isdrng3.1	$⊢ \underset{˙}{1} = 1_{R}$
	isdrng3.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
Assertion	isdrng3lem2	$⊢ (R \in Ring \land \underset{˙}{1} \neq \underset{˙}{0} \land \forall x \in (B ∖ \{\underset{˙}{0}\}) \exists y \in (B ∖ \{\underset{˙}{0}\}) y \underset{˙}{\cdot} x = \underset{˙}{1}) \to {mulGrp}_{R} ↾_{𝑠} (B ∖ \{\underset{˙}{0}\}) \in Grp$

Proof

Step	Hyp	Ref	Expression
1		isdrng3.b	$⊢ B = {Base}_{R}$
2		isdrng3.0	$⊢ \underset{˙}{0} = 0_{R}$
3		isdrng3.1	$⊢ \underset{˙}{1} = 1_{R}$
4		isdrng3.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
5	1	isdrng3lem0	$⊢ {Base}_{({mulGrp}_{R} ↾_{𝑠} (B ∖ \{\underset{˙}{0}\}))} = B ∖ \{\underset{˙}{0}\}$
6	5	eqcomi	$⊢ B ∖ \{\underset{˙}{0}\} = {Base}_{({mulGrp}_{R} ↾_{𝑠} (B ∖ \{\underset{˙}{0}\}))}$
7	6	a1i	$⊢ (R \in Ring \land \underset{˙}{1} \neq \underset{˙}{0} \land \forall x \in (B ∖ \{\underset{˙}{0}\}) \exists y \in (B ∖ \{\underset{˙}{0}\}) y \underset{˙}{\cdot} x = \underset{˙}{1}) \to B ∖ \{\underset{˙}{0}\} = {Base}_{({mulGrp}_{R} ↾_{𝑠} (B ∖ \{\underset{˙}{0}\}))}$
8	1	fvexi	$⊢ B \in V$
9	8	a1i	$⊢ (R \in Ring \land \underset{˙}{1} \neq \underset{˙}{0} \land \forall x \in (B ∖ \{\underset{˙}{0}\}) \exists y \in (B ∖ \{\underset{˙}{0}\}) y \underset{˙}{\cdot} x = \underset{˙}{1}) \to B \in V$
10	9	difexd	$⊢ (R \in Ring \land \underset{˙}{1} \neq \underset{˙}{0} \land \forall x \in (B ∖ \{\underset{˙}{0}\}) \exists y \in (B ∖ \{\underset{˙}{0}\}) y \underset{˙}{\cdot} x = \underset{˙}{1}) \to B ∖ \{\underset{˙}{0}\} \in V$
11		eqid	$⊢ {mulGrp}_{R} ↾_{𝑠} (B ∖ \{\underset{˙}{0}\}) = {mulGrp}_{R} ↾_{𝑠} (B ∖ \{\underset{˙}{0}\})$
12		eqid	$⊢ {mulGrp}_{R} = {mulGrp}_{R}$
13	12 4	mgpplusg	$⊢ \underset{˙}{\cdot} = +_{{mulGrp}_{R}}$
14	11 13	ressplusg	$⊢ B ∖ \{\underset{˙}{0}\} \in V \to \underset{˙}{\cdot} = +_{({mulGrp}_{R} ↾_{𝑠} (B ∖ \{\underset{˙}{0}\}))}$
15	10 14	syl	$⊢ (R \in Ring \land \underset{˙}{1} \neq \underset{˙}{0} \land \forall x \in (B ∖ \{\underset{˙}{0}\}) \exists y \in (B ∖ \{\underset{˙}{0}\}) y \underset{˙}{\cdot} x = \underset{˙}{1}) \to \underset{˙}{\cdot} = +_{({mulGrp}_{R} ↾_{𝑠} (B ∖ \{\underset{˙}{0}\}))}$
16		simp1	$⊢ (R \in Ring \land \underset{˙}{1} \neq \underset{˙}{0} \land \forall x \in (B ∖ \{\underset{˙}{0}\}) \exists y \in (B ∖ \{\underset{˙}{0}\}) y \underset{˙}{\cdot} x = \underset{˙}{1}) \to R \in Ring$
17		eldifi	$⊢ a \in (B ∖ \{\underset{˙}{0}\}) \to a \in B$
18		eldifi	$⊢ b \in (B ∖ \{\underset{˙}{0}\}) \to b \in B$
19	1 4	ringcl	$⊢ (R \in Ring \land a \in B \land b \in B) \to a \underset{˙}{\cdot} b \in B$
20	16 17 18 19	syl3an	$⊢ ((R \in Ring \land \underset{˙}{1} \neq \underset{˙}{0} \land \forall x \in (B ∖ \{\underset{˙}{0}\}) \exists y \in (B ∖ \{\underset{˙}{0}\}) y \underset{˙}{\cdot} x = \underset{˙}{1}) \land a \in (B ∖ \{\underset{˙}{0}\}) \land b \in (B ∖ \{\underset{˙}{0}\})) \to a \underset{˙}{\cdot} b \in B$
21		oveq2	$⊢ x = a \to y \underset{˙}{\cdot} x = y \underset{˙}{\cdot} a$
22	21	eqeq1d	$⊢ x = a \to (y \underset{˙}{\cdot} x = \underset{˙}{1} \leftrightarrow y \underset{˙}{\cdot} a = \underset{˙}{1})$
23	22	rexbidv	$⊢ x = a \to (\exists y \in (B ∖ \{\underset{˙}{0}\}) y \underset{˙}{\cdot} x = \underset{˙}{1} \leftrightarrow \exists y \in (B ∖ \{\underset{˙}{0}\}) y \underset{˙}{\cdot} a = \underset{˙}{1})$
24	23	rspcv	$⊢ a \in (B ∖ \{\underset{˙}{0}\}) \to (\forall x \in (B ∖ \{\underset{˙}{0}\}) \exists y \in (B ∖ \{\underset{˙}{0}\}) y \underset{˙}{\cdot} x = \underset{˙}{1} \to \exists y \in (B ∖ \{\underset{˙}{0}\}) y \underset{˙}{\cdot} a = \underset{˙}{1})$
25	24	imdistanri	$⊢ (\forall x \in (B ∖ \{\underset{˙}{0}\}) \exists y \in (B ∖ \{\underset{˙}{0}\}) y \underset{˙}{\cdot} x = \underset{˙}{1} \land a \in (B ∖ \{\underset{˙}{0}\})) \to (\exists y \in (B ∖ \{\underset{˙}{0}\}) y \underset{˙}{\cdot} a = \underset{˙}{1} \land a \in (B ∖ \{\underset{˙}{0}\}))$
26		eldifsn	$⊢ b \in (B ∖ \{\underset{˙}{0}\}) \leftrightarrow (b \in B \land b \neq \underset{˙}{0})$
27		simp1	$⊢ (R \in Ring \land a \in B \land \exists y \in (B ∖ \{\underset{˙}{0}\}) y \underset{˙}{\cdot} a = \underset{˙}{1}) \to R \in Ring$
28	27	adantr	$⊢ ((R \in Ring \land a \in B \land \exists y \in (B ∖ \{\underset{˙}{0}\}) y \underset{˙}{\cdot} a = \underset{˙}{1}) \land b \in B) \to R \in Ring$
29		simpl2	$⊢ ((R \in Ring \land a \in B \land \exists y \in (B ∖ \{\underset{˙}{0}\}) y \underset{˙}{\cdot} a = \underset{˙}{1}) \land b \in B) \to a \in B$
30		difss	$⊢ B ∖ \{\underset{˙}{0}\} \subseteq B$
31		ssrexv	$⊢ B ∖ \{\underset{˙}{0}\} \subseteq B \to (\exists y \in (B ∖ \{\underset{˙}{0}\}) y \underset{˙}{\cdot} a = \underset{˙}{1} \to \exists y \in B y \underset{˙}{\cdot} a = \underset{˙}{1})$
32	30 31	ax-mp	$⊢ \exists y \in (B ∖ \{\underset{˙}{0}\}) y \underset{˙}{\cdot} a = \underset{˙}{1} \to \exists y \in B y \underset{˙}{\cdot} a = \underset{˙}{1}$
33		oveq1	$⊢ y = c \to y \underset{˙}{\cdot} a = c \underset{˙}{\cdot} a$
34	33	eqeq1d	$⊢ y = c \to (y \underset{˙}{\cdot} a = \underset{˙}{1} \leftrightarrow c \underset{˙}{\cdot} a = \underset{˙}{1})$
35	34	cbvrexvw	$⊢ \exists y \in B y \underset{˙}{\cdot} a = \underset{˙}{1} \leftrightarrow \exists c \in B c \underset{˙}{\cdot} a = \underset{˙}{1}$
36	32 35	sylib	$⊢ \exists y \in (B ∖ \{\underset{˙}{0}\}) y \underset{˙}{\cdot} a = \underset{˙}{1} \to \exists c \in B c \underset{˙}{\cdot} a = \underset{˙}{1}$
37	36	3ad2ant3	$⊢ (R \in Ring \land a \in B \land \exists y \in (B ∖ \{\underset{˙}{0}\}) y \underset{˙}{\cdot} a = \underset{˙}{1}) \to \exists c \in B c \underset{˙}{\cdot} a = \underset{˙}{1}$
38	37	adantr	$⊢ ((R \in Ring \land a \in B \land \exists y \in (B ∖ \{\underset{˙}{0}\}) y \underset{˙}{\cdot} a = \underset{˙}{1}) \land b \in B) \to \exists c \in B c \underset{˙}{\cdot} a = \underset{˙}{1}$
39		simpr	$⊢ ((R \in Ring \land a \in B \land \exists y \in (B ∖ \{\underset{˙}{0}\}) y \underset{˙}{\cdot} a = \underset{˙}{1}) \land b \in B) \to b \in B$
40	1 4 3 2 28 29 38 39	ringinvnzdiv	$⊢ ((R \in Ring \land a \in B \land \exists y \in (B ∖ \{\underset{˙}{0}\}) y \underset{˙}{\cdot} a = \underset{˙}{1}) \land b \in B) \to (a \underset{˙}{\cdot} b = \underset{˙}{0} \leftrightarrow b = \underset{˙}{0})$
41	40	biimpd	$⊢ ((R \in Ring \land a \in B \land \exists y \in (B ∖ \{\underset{˙}{0}\}) y \underset{˙}{\cdot} a = \underset{˙}{1}) \land b \in B) \to (a \underset{˙}{\cdot} b = \underset{˙}{0} \to b = \underset{˙}{0})$
42	41	ex	$⊢ (R \in Ring \land a \in B \land \exists y \in (B ∖ \{\underset{˙}{0}\}) y \underset{˙}{\cdot} a = \underset{˙}{1}) \to (b \in B \to (a \underset{˙}{\cdot} b = \underset{˙}{0} \to b = \underset{˙}{0}))$
43	17 42	syl3an2	$⊢ (R \in Ring \land a \in (B ∖ \{\underset{˙}{0}\}) \land \exists y \in (B ∖ \{\underset{˙}{0}\}) y \underset{˙}{\cdot} a = \underset{˙}{1}) \to (b \in B \to (a \underset{˙}{\cdot} b = \underset{˙}{0} \to b = \underset{˙}{0}))$
44	43	3expb	$⊢ (R \in Ring \land (a \in (B ∖ \{\underset{˙}{0}\}) \land \exists y \in (B ∖ \{\underset{˙}{0}\}) y \underset{˙}{\cdot} a = \underset{˙}{1})) \to (b \in B \to (a \underset{˙}{\cdot} b = \underset{˙}{0} \to b = \underset{˙}{0}))$
45	44	imp	$⊢ ((R \in Ring \land (a \in (B ∖ \{\underset{˙}{0}\}) \land \exists y \in (B ∖ \{\underset{˙}{0}\}) y \underset{˙}{\cdot} a = \underset{˙}{1})) \land b \in B) \to (a \underset{˙}{\cdot} b = \underset{˙}{0} \to b = \underset{˙}{0})$
46	45	necon3d	$⊢ ((R \in Ring \land (a \in (B ∖ \{\underset{˙}{0}\}) \land \exists y \in (B ∖ \{\underset{˙}{0}\}) y \underset{˙}{\cdot} a = \underset{˙}{1})) \land b \in B) \to (b \neq \underset{˙}{0} \to a \underset{˙}{\cdot} b \neq \underset{˙}{0})$
47	46	impr	$⊢ ((R \in Ring \land (a \in (B ∖ \{\underset{˙}{0}\}) \land \exists y \in (B ∖ \{\underset{˙}{0}\}) y \underset{˙}{\cdot} a = \underset{˙}{1})) \land (b \in B \land b \neq \underset{˙}{0})) \to a \underset{˙}{\cdot} b \neq \underset{˙}{0}$
48	26 47	sylan2b	$⊢ ((R \in Ring \land (a \in (B ∖ \{\underset{˙}{0}\}) \land \exists y \in (B ∖ \{\underset{˙}{0}\}) y \underset{˙}{\cdot} a = \underset{˙}{1})) \land b \in (B ∖ \{\underset{˙}{0}\})) \to a \underset{˙}{\cdot} b \neq \underset{˙}{0}$
49	48	an32s	$⊢ ((R \in Ring \land b \in (B ∖ \{\underset{˙}{0}\})) \land (a \in (B ∖ \{\underset{˙}{0}\}) \land \exists y \in (B ∖ \{\underset{˙}{0}\}) y \underset{˙}{\cdot} a = \underset{˙}{1})) \to a \underset{˙}{\cdot} b \neq \underset{˙}{0}$
50	49	ancom2s	$⊢ ((R \in Ring \land b \in (B ∖ \{\underset{˙}{0}\})) \land (\exists y \in (B ∖ \{\underset{˙}{0}\}) y \underset{˙}{\cdot} a = \underset{˙}{1} \land a \in (B ∖ \{\underset{˙}{0}\}))) \to a \underset{˙}{\cdot} b \neq \underset{˙}{0}$
51	25 50	sylan2	$⊢ ((R \in Ring \land b \in (B ∖ \{\underset{˙}{0}\})) \land (\forall x \in (B ∖ \{\underset{˙}{0}\}) \exists y \in (B ∖ \{\underset{˙}{0}\}) y \underset{˙}{\cdot} x = \underset{˙}{1} \land a \in (B ∖ \{\underset{˙}{0}\}))) \to a \underset{˙}{\cdot} b \neq \underset{˙}{0}$
52	51	an42s	$⊢ ((R \in Ring \land \forall x \in (B ∖ \{\underset{˙}{0}\}) \exists y \in (B ∖ \{\underset{˙}{0}\}) y \underset{˙}{\cdot} x = \underset{˙}{1}) \land (a \in (B ∖ \{\underset{˙}{0}\}) \land b \in (B ∖ \{\underset{˙}{0}\}))) \to a \underset{˙}{\cdot} b \neq \underset{˙}{0}$
53	52	exp32	$⊢ (R \in Ring \land \forall x \in (B ∖ \{\underset{˙}{0}\}) \exists y \in (B ∖ \{\underset{˙}{0}\}) y \underset{˙}{\cdot} x = \underset{˙}{1}) \to (a \in (B ∖ \{\underset{˙}{0}\}) \to (b \in (B ∖ \{\underset{˙}{0}\}) \to a \underset{˙}{\cdot} b \neq \underset{˙}{0}))$
54	53	3adant2	$⊢ (R \in Ring \land \underset{˙}{1} \neq \underset{˙}{0} \land \forall x \in (B ∖ \{\underset{˙}{0}\}) \exists y \in (B ∖ \{\underset{˙}{0}\}) y \underset{˙}{\cdot} x = \underset{˙}{1}) \to (a \in (B ∖ \{\underset{˙}{0}\}) \to (b \in (B ∖ \{\underset{˙}{0}\}) \to a \underset{˙}{\cdot} b \neq \underset{˙}{0}))$
55	54	3imp	$⊢ ((R \in Ring \land \underset{˙}{1} \neq \underset{˙}{0} \land \forall x \in (B ∖ \{\underset{˙}{0}\}) \exists y \in (B ∖ \{\underset{˙}{0}\}) y \underset{˙}{\cdot} x = \underset{˙}{1}) \land a \in (B ∖ \{\underset{˙}{0}\}) \land b \in (B ∖ \{\underset{˙}{0}\})) \to a \underset{˙}{\cdot} b \neq \underset{˙}{0}$
56	20 55	eldifsnd	$⊢ ((R \in Ring \land \underset{˙}{1} \neq \underset{˙}{0} \land \forall x \in (B ∖ \{\underset{˙}{0}\}) \exists y \in (B ∖ \{\underset{˙}{0}\}) y \underset{˙}{\cdot} x = \underset{˙}{1}) \land a \in (B ∖ \{\underset{˙}{0}\}) \land b \in (B ∖ \{\underset{˙}{0}\})) \to a \underset{˙}{\cdot} b \in (B ∖ \{\underset{˙}{0}\})$
57		eldifi	$⊢ c \in (B ∖ \{\underset{˙}{0}\}) \to c \in B$
58	17 18 57	3anim123i	$⊢ (a \in (B ∖ \{\underset{˙}{0}\}) \land b \in (B ∖ \{\underset{˙}{0}\}) \land c \in (B ∖ \{\underset{˙}{0}\})) \to (a \in B \land b \in B \land c \in B)$
59	1 4	ringass	$⊢ (R \in Ring \land (a \in B \land b \in B \land c \in B)) \to (a \underset{˙}{\cdot} b) \underset{˙}{\cdot} c = a \underset{˙}{\cdot} (b \underset{˙}{\cdot} c)$
60	16 58 59	syl2an	$⊢ ((R \in Ring \land \underset{˙}{1} \neq \underset{˙}{0} \land \forall x \in (B ∖ \{\underset{˙}{0}\}) \exists y \in (B ∖ \{\underset{˙}{0}\}) y \underset{˙}{\cdot} x = \underset{˙}{1}) \land (a \in (B ∖ \{\underset{˙}{0}\}) \land b \in (B ∖ \{\underset{˙}{0}\}) \land c \in (B ∖ \{\underset{˙}{0}\}))) \to (a \underset{˙}{\cdot} b) \underset{˙}{\cdot} c = a \underset{˙}{\cdot} (b \underset{˙}{\cdot} c)$
61	1 3	ringidcl	$⊢ R \in Ring \to \underset{˙}{1} \in B$
62		nelsn	$⊢ \underset{˙}{1} \neq \underset{˙}{0} \to \neg \underset{˙}{1} \in \{\underset{˙}{0}\}$
63	61 62	anim12i	$⊢ (R \in Ring \land \underset{˙}{1} \neq \underset{˙}{0}) \to (\underset{˙}{1} \in B \land \neg \underset{˙}{1} \in \{\underset{˙}{0}\})$
64		eldif	$⊢ \underset{˙}{1} \in (B ∖ \{\underset{˙}{0}\}) \leftrightarrow (\underset{˙}{1} \in B \land \neg \underset{˙}{1} \in \{\underset{˙}{0}\})$
65	63 64	sylibr	$⊢ (R \in Ring \land \underset{˙}{1} \neq \underset{˙}{0}) \to \underset{˙}{1} \in (B ∖ \{\underset{˙}{0}\})$
66	65	3adant3	$⊢ (R \in Ring \land \underset{˙}{1} \neq \underset{˙}{0} \land \forall x \in (B ∖ \{\underset{˙}{0}\}) \exists y \in (B ∖ \{\underset{˙}{0}\}) y \underset{˙}{\cdot} x = \underset{˙}{1}) \to \underset{˙}{1} \in (B ∖ \{\underset{˙}{0}\})$
67	1 4 3	ringlidm	$⊢ (R \in Ring \land a \in B) \to \underset{˙}{1} \underset{˙}{\cdot} a = a$
68	16 17 67	syl2an	$⊢ ((R \in Ring \land \underset{˙}{1} \neq \underset{˙}{0} \land \forall x \in (B ∖ \{\underset{˙}{0}\}) \exists y \in (B ∖ \{\underset{˙}{0}\}) y \underset{˙}{\cdot} x = \underset{˙}{1}) \land a \in (B ∖ \{\underset{˙}{0}\})) \to \underset{˙}{1} \underset{˙}{\cdot} a = a$
69		oveq1	$⊢ y = b \to y \underset{˙}{\cdot} a = b \underset{˙}{\cdot} a$
70	69	eqeq1d	$⊢ y = b \to (y \underset{˙}{\cdot} a = \underset{˙}{1} \leftrightarrow b \underset{˙}{\cdot} a = \underset{˙}{1})$
71	70	cbvrexvw	$⊢ \exists y \in (B ∖ \{\underset{˙}{0}\}) y \underset{˙}{\cdot} a = \underset{˙}{1} \leftrightarrow \exists b \in (B ∖ \{\underset{˙}{0}\}) b \underset{˙}{\cdot} a = \underset{˙}{1}$
72	23 71	bitrdi	$⊢ x = a \to (\exists y \in (B ∖ \{\underset{˙}{0}\}) y \underset{˙}{\cdot} x = \underset{˙}{1} \leftrightarrow \exists b \in (B ∖ \{\underset{˙}{0}\}) b \underset{˙}{\cdot} a = \underset{˙}{1})$
73	72	rspccv	$⊢ \forall x \in (B ∖ \{\underset{˙}{0}\}) \exists y \in (B ∖ \{\underset{˙}{0}\}) y \underset{˙}{\cdot} x = \underset{˙}{1} \to (a \in (B ∖ \{\underset{˙}{0}\}) \to \exists b \in (B ∖ \{\underset{˙}{0}\}) b \underset{˙}{\cdot} a = \underset{˙}{1})$
74	73	3ad2ant3	$⊢ (R \in Ring \land \underset{˙}{1} \neq \underset{˙}{0} \land \forall x \in (B ∖ \{\underset{˙}{0}\}) \exists y \in (B ∖ \{\underset{˙}{0}\}) y \underset{˙}{\cdot} x = \underset{˙}{1}) \to (a \in (B ∖ \{\underset{˙}{0}\}) \to \exists b \in (B ∖ \{\underset{˙}{0}\}) b \underset{˙}{\cdot} a = \underset{˙}{1})$
75	74	imp	$⊢ ((R \in Ring \land \underset{˙}{1} \neq \underset{˙}{0} \land \forall x \in (B ∖ \{\underset{˙}{0}\}) \exists y \in (B ∖ \{\underset{˙}{0}\}) y \underset{˙}{\cdot} x = \underset{˙}{1}) \land a \in (B ∖ \{\underset{˙}{0}\})) \to \exists b \in (B ∖ \{\underset{˙}{0}\}) b \underset{˙}{\cdot} a = \underset{˙}{1}$
76	7 15 56 60 66 68 75	isgrpde	$⊢ (R \in Ring \land \underset{˙}{1} \neq \underset{˙}{0} \land \forall x \in (B ∖ \{\underset{˙}{0}\}) \exists y \in (B ∖ \{\underset{˙}{0}\}) y \underset{˙}{\cdot} x = \underset{˙}{1}) \to {mulGrp}_{R} ↾_{𝑠} (B ∖ \{\underset{˙}{0}\}) \in Grp$

Metamath Proof Explorer

Theorem isdrng3lem2

Proof