Theorem islring

Description: The predicate "is a local ring". (Contributed by SN, 23-Feb-2025)

	Ref	Expression
Hypotheses	islring.b	$$⊢B={\mathrm{Base}}_R$$
	islring.a	$$⊢\underset{\dot{}}{+}={+}_R$$
	islring.1	$$⊢\underset{\dot{}}{1}=1_R$$
	islring.u	$$⊢U=\mathrm{Unit}\left(R\right)$$
Assertion	islring	$$⊢R\in \mathrm{LRing}\leftrightarrow \left(R\in \mathrm{NzRing}\wedge \forall x\in B\forall y\in B\left(x\underset{\dot{}}{+}y=\underset{\dot{}}{1}\to \left(x\in U\vee y\in U\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		islring.b	$$⊢B={\mathrm{Base}}_R$$
2		islring.a	$$⊢\underset{\dot{}}{+}={+}_R$$
3		islring.1	$$⊢\underset{\dot{}}{1}=1_R$$
4		islring.u	$$⊢U=\mathrm{Unit}\left(R\right)$$
5		fveq2	$$⊢r=R\to {\mathrm{Base}}_r={\mathrm{Base}}_R$$
6	5 1	eqtr4di	$$⊢r=R\to {\mathrm{Base}}_r=B$$
7		fveq2	$$⊢r=R\to {+}_r={+}_R$$
8	7 2	eqtr4di	$$⊢r=R\to {+}_r=\underset{\dot{}}{+}$$
9	8	oveqd	$$⊢r=R\to x{+}_{r}y=x\underset{\dot{}}{+}y$$
10		fveq2	$$⊢r=R\to 1_r=1_R$$
11	10 3	eqtr4di	$$⊢r=R\to 1_r=\underset{\dot{}}{1}$$
12	9 11	eqeq12d	$$⊢r=R\to \left(x{+}_{r}y=1_r\leftrightarrow x\underset{\dot{}}{+}y=\underset{\dot{}}{1}\right)$$
13		fveq2	$$⊢r=R\to \mathrm{Unit}\left(r\right)=\mathrm{Unit}\left(R\right)$$
14	13 4	eqtr4di	$$⊢r=R\to \mathrm{Unit}\left(r\right)=U$$
15	14	eleq2d	$$⊢r=R\to \left(x\in \mathrm{Unit}\left(r\right)\leftrightarrow x\in U\right)$$
16	14	eleq2d	$$⊢r=R\to \left(y\in \mathrm{Unit}\left(r\right)\leftrightarrow y\in U\right)$$
17	15 16	orbi12d	$$⊢r=R\to \left(\left(x\in \mathrm{Unit}\left(r\right)\vee y\in \mathrm{Unit}\left(r\right)\right)\leftrightarrow \left(x\in U\vee y\in U\right)\right)$$
18	12 17	imbi12d	$$⊢r=R\to \left(\left(x{+}_{r}y=1_r\to \left(x\in \mathrm{Unit}\left(r\right)\vee y\in \mathrm{Unit}\left(r\right)\right)\right)\leftrightarrow \left(x\underset{\dot{}}{+}y=\underset{\dot{}}{1}\to \left(x\in U\vee y\in U\right)\right)\right)$$
19	6 18	raleqbidv	$$⊢r=R\to \left(\forall y\in {\mathrm{Base}}_r\left(x{+}_{r}y=1_r\to \left(x\in \mathrm{Unit}\left(r\right)\vee y\in \mathrm{Unit}\left(r\right)\right)\right)\leftrightarrow \forall y\in B\left(x\underset{\dot{}}{+}y=\underset{\dot{}}{1}\to \left(x\in U\vee y\in U\right)\right)\right)$$
20	6 19	raleqbidv	$$⊢r=R\to \left(\forall x\in {\mathrm{Base}}_r\forall y\in {\mathrm{Base}}_r\left(x{+}_{r}y=1_r\to \left(x\in \mathrm{Unit}\left(r\right)\vee y\in \mathrm{Unit}\left(r\right)\right)\right)\leftrightarrow \forall x\in B\forall y\in B\left(x\underset{\dot{}}{+}y=\underset{\dot{}}{1}\to \left(x\in U\vee y\in U\right)\right)\right)$$
21		df-lring	$$⊢\mathrm{LRing}=\left\{r\in \mathrm{NzRing}|\forall x\in {\mathrm{Base}}_r\forall y\in {\mathrm{Base}}_r\left(x{+}_{r}y=1_r\to \left(x\in \mathrm{Unit}\left(r\right)\vee y\in \mathrm{Unit}\left(r\right)\right)\right)\right\}$$
22	20 21	elrab2	$$⊢R\in \mathrm{LRing}\leftrightarrow \left(R\in \mathrm{NzRing}\wedge \forall x\in B\forall y\in B\left(x\underset{\dot{}}{+}y=\underset{\dot{}}{1}\to \left(x\in U\vee y\in U\right)\right)\right)$$