Theorem isdrng3lem1

Description: Lemma for isdrng3 (for the left to right 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={\mathrm{Base}}_R$$
	isdrng3.0	$$⊢\underset{\dot{}}{0}=0_R$$
	isdrng3.1	$$⊢\underset{\dot{}}{1}=1_R$$
	isdrng3.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
Assertion	isdrng3lem1	$$⊢\left(R\in \mathrm{Ring}\wedge {\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\in \mathrm{Grp}\right)\to \forall x\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\exists y\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)y\underset{\dot{}}{·}x=\underset{\dot{}}{1}$$

Proof

Step	Hyp	Ref	Expression
1		isdrng3.b	$$⊢B={\mathrm{Base}}_R$$
2		isdrng3.0	$$⊢\underset{\dot{}}{0}=0_R$$
3		isdrng3.1	$$⊢\underset{\dot{}}{1}=1_R$$
4		isdrng3.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
5	1	isdrng3lem0	$$⊢{\mathrm{Base}}_{\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)}=B\setminus \left\{\underset{\dot{}}{0}\right\}$$
6	5	eqcomi	$$⊢B\setminus \left\{\underset{\dot{}}{0}\right\}={\mathrm{Base}}_{\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)}$$
7	6	eleq2i	$$⊢x\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\leftrightarrow x\in {\mathrm{Base}}_{\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)}$$
8		oveq1	$$⊢y={inv}_g\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\left(x\right)\to y{+}_{\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)}x={inv}_g\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\left(x\right){+}_{\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)}x$$
9	8	eqeq1d	$$⊢y={inv}_g\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\left(x\right)\to \left(y{+}_{\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)}x=\underset{\dot{}}{1}\leftrightarrow {inv}_g\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\left(x\right){+}_{\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)}x=\underset{\dot{}}{1}\right)$$
10		eqid	$$⊢{\mathrm{Base}}_{\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)}={\mathrm{Base}}_{\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)}$$
11		eqid	$$⊢{inv}_g\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)={inv}_g\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)$$
12	10 11	grpinvcl	$$⊢\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\in \mathrm{Grp}\wedge x\in {\mathrm{Base}}_{\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)}\right)\to {inv}_g\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\left(x\right)\in {\mathrm{Base}}_{\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)}$$
13	12	adantll	$$⊢\left(\left(R\in \mathrm{Ring}\wedge {\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\in \mathrm{Grp}\right)\wedge x\in {\mathrm{Base}}_{\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)}\right)\to {inv}_g\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\left(x\right)\in {\mathrm{Base}}_{\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)}$$
14		eqid	$$⊢{+}_{\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)}={+}_{\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)}$$
15		eqid	$$⊢0_{\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)}=0_{\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)}$$
16	10 14 15 11	grplinv	$$⊢\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\in \mathrm{Grp}\wedge x\in {\mathrm{Base}}_{\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)}\right)\to {inv}_g\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\left(x\right){+}_{\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)}x=0_{\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)}$$
17	16	adantll	$$⊢\left(\left(R\in \mathrm{Ring}\wedge {\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\in \mathrm{Grp}\right)\wedge x\in {\mathrm{Base}}_{\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)}\right)\to {inv}_g\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\left(x\right){+}_{\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)}x=0_{\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)}$$
18		eqid	$$⊢{\mathrm{mulGrp}}_R={\mathrm{mulGrp}}_R$$
19	18	ringmgp	$$⊢R\in \mathrm{Ring}\to {\mathrm{mulGrp}}_R\in \mathrm{Mnd}$$
20	19	adantr	$$⊢\left(R\in \mathrm{Ring}\wedge {\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\in \mathrm{Grp}\right)\to {\mathrm{mulGrp}}_R\in \mathrm{Mnd}$$
21	1 3	ringidcl	$$⊢R\in \mathrm{Ring}\to \underset{\dot{}}{1}\in B$$
22	21	adantr	$$⊢\left(R\in \mathrm{Ring}\wedge {\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\in \mathrm{Grp}\right)\to \underset{\dot{}}{1}\in B$$
23		eqid	$$⊢{\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)={\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
24	1 2 23	isdrng2	$$⊢R\in \mathrm{DivRing}\leftrightarrow \left(R\in \mathrm{Ring}\wedge {\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\in \mathrm{Grp}\right)$$
25	2 3	drngunz	$$⊢R\in \mathrm{DivRing}\to \underset{\dot{}}{1}\ne \underset{\dot{}}{0}$$
26	24 25	sylbir	$$⊢\left(R\in \mathrm{Ring}\wedge {\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\in \mathrm{Grp}\right)\to \underset{\dot{}}{1}\ne \underset{\dot{}}{0}$$
27	22 26	eldifsnd	$$⊢\left(R\in \mathrm{Ring}\wedge {\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\in \mathrm{Grp}\right)\to \underset{\dot{}}{1}\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
28		difssd	$$⊢\left(R\in \mathrm{Ring}\wedge {\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\in \mathrm{Grp}\right)\to B\setminus \left\{\underset{\dot{}}{0}\right\}\subseteq B$$
29	18 1	mgpbas	$$⊢B={\mathrm{Base}}_{{\mathrm{mulGrp}}_R}$$
30	18 3	ringidval	$$⊢\underset{\dot{}}{1}=0_{{\mathrm{mulGrp}}_R}$$
31	23 29 30	ress0g	$$⊢\left({\mathrm{mulGrp}}_R\in \mathrm{Mnd}\wedge \underset{\dot{}}{1}\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\wedge B\setminus \left\{\underset{\dot{}}{0}\right\}\subseteq B\right)\to \underset{\dot{}}{1}=0_{\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)}$$
32	31	eqcomd	$$⊢\left({\mathrm{mulGrp}}_R\in \mathrm{Mnd}\wedge \underset{\dot{}}{1}\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\wedge B\setminus \left\{\underset{\dot{}}{0}\right\}\subseteq B\right)\to 0_{\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)}=\underset{\dot{}}{1}$$
33	20 27 28 32	syl3anc	$$⊢\left(R\in \mathrm{Ring}\wedge {\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\in \mathrm{Grp}\right)\to 0_{\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)}=\underset{\dot{}}{1}$$
34	33	adantr	$$⊢\left(\left(R\in \mathrm{Ring}\wedge {\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\in \mathrm{Grp}\right)\wedge x\in {\mathrm{Base}}_{\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)}\right)\to 0_{\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)}=\underset{\dot{}}{1}$$
35	17 34	eqtrd	$$⊢\left(\left(R\in \mathrm{Ring}\wedge {\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\in \mathrm{Grp}\right)\wedge x\in {\mathrm{Base}}_{\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)}\right)\to {inv}_g\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\left(x\right){+}_{\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)}x=\underset{\dot{}}{1}$$
36	9 13 35	rspcedvdw	$$⊢\left(\left(R\in \mathrm{Ring}\wedge {\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\in \mathrm{Grp}\right)\wedge x\in {\mathrm{Base}}_{\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)}\right)\to \exists y\in {\mathrm{Base}}_{\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)}y{+}_{\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)}x=\underset{\dot{}}{1}$$
37	7 36	sylan2b	$$⊢\left(\left(R\in \mathrm{Ring}\wedge {\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\in \mathrm{Grp}\right)\wedge x\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\to \exists y\in {\mathrm{Base}}_{\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)}y{+}_{\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)}x=\underset{\dot{}}{1}$$
38	5	a1i	$$⊢\left(\left(R\in \mathrm{Ring}\wedge {\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\in \mathrm{Grp}\right)\wedge x\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\to {\mathrm{Base}}_{\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)}=B\setminus \left\{\underset{\dot{}}{0}\right\}$$
39	38	rexeqdv	$$⊢\left(\left(R\in \mathrm{Ring}\wedge {\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\in \mathrm{Grp}\right)\wedge x\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\to \left(\exists y\in {\mathrm{Base}}_{\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)}y{+}_{\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)}x=\underset{\dot{}}{1}\leftrightarrow \exists y\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)y{+}_{\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)}x=\underset{\dot{}}{1}\right)$$
40	18 4	mgpplusg	$$⊢\underset{\dot{}}{·}={+}_{{\mathrm{mulGrp}}_R}$$
41	1	fvexi	$$⊢B\in \mathrm{V}$$
42	41	difexi	$$⊢B\setminus \left\{\underset{\dot{}}{0}\right\}\in \mathrm{V}$$
43		eqid	$$⊢{+}_{{\mathrm{mulGrp}}_R}={+}_{{\mathrm{mulGrp}}_R}$$
44	23 43	ressplusg	$$⊢B\setminus \left\{\underset{\dot{}}{0}\right\}\in \mathrm{V}\to {+}_{{\mathrm{mulGrp}}_R}={+}_{\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)}$$
45	42 44	ax-mp	$$⊢{+}_{{\mathrm{mulGrp}}_R}={+}_{\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)}$$
46	40 45	eqtr2i	$$⊢{+}_{\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)}=\underset{\dot{}}{·}$$
47	46	oveqi	$$⊢y{+}_{\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)}x=y\underset{\dot{}}{·}x$$
48	47	eqeq1i	$$⊢y{+}_{\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)}x=\underset{\dot{}}{1}\leftrightarrow y\underset{\dot{}}{·}x=\underset{\dot{}}{1}$$
49	48	rexbii	$$⊢\exists y\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)y{+}_{\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)}x=\underset{\dot{}}{1}\leftrightarrow \exists y\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)y\underset{\dot{}}{·}x=\underset{\dot{}}{1}$$
50	39 49	bitrdi	$$⊢\left(\left(R\in \mathrm{Ring}\wedge {\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\in \mathrm{Grp}\right)\wedge x\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\to \left(\exists y\in {\mathrm{Base}}_{\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)}y{+}_{\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)}x=\underset{\dot{}}{1}\leftrightarrow \exists y\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)y\underset{\dot{}}{·}x=\underset{\dot{}}{1}\right)$$
51	37 50	mpbid	$$⊢\left(\left(R\in \mathrm{Ring}\wedge {\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\in \mathrm{Grp}\right)\wedge x\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\to \exists y\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)y\underset{\dot{}}{·}x=\underset{\dot{}}{1}$$
52	51	ralrimiva	$$⊢\left(R\in \mathrm{Ring}\wedge {\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\in \mathrm{Grp}\right)\to \forall x\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\exists y\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)y\underset{\dot{}}{·}x=\underset{\dot{}}{1}$$