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	Could not format assertion : No typesetting found for |- ( R e. LRing <-> ( R e. NzRing /\ A. x e. B A. y e. B ( ( x .+ y ) = .1. -> ( x e. U \/ y e. U ) ) ) ) with typecode |-

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	Could not format LRing = { r e. NzRing | A. x e. ( Base ` r ) A. y e. ( Base ` r ) ( ( x ( +g ` r ) y ) = ( 1r ` r ) -> ( x e. ( Unit ` r ) \/ y e. ( Unit ` r ) ) ) } : No typesetting found for |- LRing = { r e. NzRing | A. x e. ( Base ` r ) A. y e. ( Base ` r ) ( ( x ( +g ` r ) y ) = ( 1r ` r ) -> ( x e. ( Unit ` r ) \/ y e. ( Unit ` r ) ) ) } with typecode |-
22	20 21	elrab2	Could not format ( R e. LRing <-> ( R e. NzRing /\ A. x e. B A. y e. B ( ( x .+ y ) = .1. -> ( x e. U \/ y e. U ) ) ) ) : No typesetting found for |- ( R e. LRing <-> ( R e. NzRing /\ A. x e. B A. y e. B ( ( x .+ y ) = .1. -> ( x e. U \/ y e. U ) ) ) ) with typecode |-