Theorem rrgval

Description: Value of the set or left-regular elements in a ring. (Contributed by Stefan O'Rear, 22-Mar-2015)

	Ref	Expression
Hypotheses	rrgval.e	$$⊢E=\mathrm{RLReg}\left(R\right)$$
	rrgval.b	$$⊢B={\mathrm{Base}}_R$$
	rrgval.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	rrgval.z	$$⊢\underset{\dot{}}{0}=0_R$$
Assertion	rrgval	$$⊢E=\left\{x\in B|\forall y\in B\left(x\underset{\dot{}}{·}y=\underset{\dot{}}{0}\to y=\underset{\dot{}}{0}\right)\right\}$$

Proof

Step	Hyp	Ref	Expression
1		rrgval.e	$$⊢E=\mathrm{RLReg}\left(R\right)$$
2		rrgval.b	$$⊢B={\mathrm{Base}}_R$$
3		rrgval.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
4		rrgval.z	$$⊢\underset{\dot{}}{0}=0_R$$
5		fveq2	$$⊢r=R\to {\mathrm{Base}}_r={\mathrm{Base}}_R$$
6	5 2	eqtr4di	$$⊢r=R\to {\mathrm{Base}}_r=B$$
7		fveq2	$$⊢r=R\to {\cdot }_r={\cdot }_R$$
8	7 3	eqtr4di	$$⊢r=R\to {\cdot }_r=\underset{\dot{}}{·}$$
9	8	oveqd	$$⊢r=R\to x{\cdot }_{r}y=x\underset{\dot{}}{·}y$$
10		fveq2	$$⊢r=R\to 0_r=0_R$$
11	10 4	eqtr4di	$$⊢r=R\to 0_r=\underset{\dot{}}{0}$$
12	9 11	eqeq12d	$$⊢r=R\to \left(x{\cdot }_{r}y=0_r\leftrightarrow x\underset{\dot{}}{·}y=\underset{\dot{}}{0}\right)$$
13	11	eqeq2d	$$⊢r=R\to \left(y=0_r\leftrightarrow y=\underset{\dot{}}{0}\right)$$
14	12 13	imbi12d	$$⊢r=R\to \left(\left(x{\cdot }_{r}y=0_r\to y=0_r\right)\leftrightarrow \left(x\underset{\dot{}}{·}y=\underset{\dot{}}{0}\to y=\underset{\dot{}}{0}\right)\right)$$
15	6 14	raleqbidv	$$⊢r=R\to \left(\forall y\in {\mathrm{Base}}_r\left(x{\cdot }_{r}y=0_r\to y=0_r\right)\leftrightarrow \forall y\in B\left(x\underset{\dot{}}{·}y=\underset{\dot{}}{0}\to y=\underset{\dot{}}{0}\right)\right)$$
16	6 15	rabeqbidv	$$⊢r=R\to \left\{x\in {\mathrm{Base}}_r|\forall y\in {\mathrm{Base}}_r\left(x{\cdot }_{r}y=0_r\to y=0_r\right)\right\}=\left\{x\in B|\forall y\in B\left(x\underset{\dot{}}{·}y=\underset{\dot{}}{0}\to y=\underset{\dot{}}{0}\right)\right\}$$
17		df-rlreg	$$⊢\mathrm{RLReg}=\left(r\in \mathrm{V}⟼\left\{x\in {\mathrm{Base}}_r|\forall y\in {\mathrm{Base}}_r\left(x{\cdot }_{r}y=0_r\to y=0_r\right)\right\}\right)$$
18	2	fvexi	$$⊢B\in \mathrm{V}$$
19	18	rabex	$$⊢\left\{x\in B|\forall y\in B\left(x\underset{\dot{}}{·}y=\underset{\dot{}}{0}\to y=\underset{\dot{}}{0}\right)\right\}\in \mathrm{V}$$
20	16 17 19	fvmpt	$$⊢R\in \mathrm{V}\to \mathrm{RLReg}\left(R\right)=\left\{x\in B|\forall y\in B\left(x\underset{\dot{}}{·}y=\underset{\dot{}}{0}\to y=\underset{\dot{}}{0}\right)\right\}$$
21		fvprc	$$⊢\neg R\in \mathrm{V}\to \mathrm{RLReg}\left(R\right)=\varnothing$$
22		fvprc	$$⊢\neg R\in \mathrm{V}\to {\mathrm{Base}}_R=\varnothing$$
23	2 22	eqtrid	$$⊢\neg R\in \mathrm{V}\to B=\varnothing$$
24	23	rabeqdv	$$⊢\neg R\in \mathrm{V}\to \left\{x\in B|\forall y\in B\left(x\underset{\dot{}}{·}y=\underset{\dot{}}{0}\to y=\underset{\dot{}}{0}\right)\right\}=\left\{x\in \varnothing |\forall y\in B\left(x\underset{\dot{}}{·}y=\underset{\dot{}}{0}\to y=\underset{\dot{}}{0}\right)\right\}$$
25		rab0	$$⊢\left\{x\in \varnothing |\forall y\in B\left(x\underset{\dot{}}{·}y=\underset{\dot{}}{0}\to y=\underset{\dot{}}{0}\right)\right\}=\varnothing$$
26	24 25	eqtrdi	$$⊢\neg R\in \mathrm{V}\to \left\{x\in B|\forall y\in B\left(x\underset{\dot{}}{·}y=\underset{\dot{}}{0}\to y=\underset{\dot{}}{0}\right)\right\}=\varnothing$$
27	21 26	eqtr4d	$$⊢\neg R\in \mathrm{V}\to \mathrm{RLReg}\left(R\right)=\left\{x\in B|\forall y\in B\left(x\underset{\dot{}}{·}y=\underset{\dot{}}{0}\to y=\underset{\dot{}}{0}\right)\right\}$$
28	20 27	pm2.61i	$$⊢\mathrm{RLReg}\left(R\right)=\left\{x\in B|\forall y\in B\left(x\underset{\dot{}}{·}y=\underset{\dot{}}{0}\to y=\underset{\dot{}}{0}\right)\right\}$$
29	1 28	eqtri	$$⊢E=\left\{x\in B|\forall y\in B\left(x\underset{\dot{}}{·}y=\underset{\dot{}}{0}\to y=\underset{\dot{}}{0}\right)\right\}$$