Theorem isrrg

Description: Membership in the set of left-regular elements. (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	isrrg	$$⊢X\in E\leftrightarrow \left(X\in B\wedge \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		oveq1	$$⊢x=X\to x\underset{\dot{}}{·}y=X\underset{\dot{}}{·}y$$
6	5	eqeq1d	$$⊢x=X\to \left(x\underset{\dot{}}{·}y=\underset{\dot{}}{0}\leftrightarrow X\underset{\dot{}}{·}y=\underset{\dot{}}{0}\right)$$
7	6	imbi1d	$$⊢x=X\to \left(\left(x\underset{\dot{}}{·}y=\underset{\dot{}}{0}\to y=\underset{\dot{}}{0}\right)\leftrightarrow \left(X\underset{\dot{}}{·}y=\underset{\dot{}}{0}\to y=\underset{\dot{}}{0}\right)\right)$$
8	7	ralbidv	$$⊢x=X\to \left(\forall y\in B\left(x\underset{\dot{}}{·}y=\underset{\dot{}}{0}\to y=\underset{\dot{}}{0}\right)\leftrightarrow \forall y\in B\left(X\underset{\dot{}}{·}y=\underset{\dot{}}{0}\to y=\underset{\dot{}}{0}\right)\right)$$
9	1 2 3 4	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\}$$
10	8 9	elrab2	$$⊢X\in E\leftrightarrow \left(X\in B\wedge \forall y\in B\left(X\underset{\dot{}}{·}y=\underset{\dot{}}{0}\to y=\underset{\dot{}}{0}\right)\right)$$