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 = ( RLReg ` R )
	rrgval.b	|- B = ( Base ` R )
	rrgval.t	|- .x. = ( .r ` R )
	rrgval.z	|- .0. = ( 0g ` R )
Assertion	isrrg	|- ( X e. E <-> ( X e. B /\ A. y e. B ( ( X .x. y ) = .0. -> y = .0. ) ) )

Proof

Step	Hyp	Ref	Expression
1		rrgval.e	|- E = ( RLReg ` R )
2		rrgval.b	|- B = ( Base ` R )
3		rrgval.t	|- .x. = ( .r ` R )
4		rrgval.z	|- .0. = ( 0g ` R )
5		oveq1	|- ( x = X -> ( x .x. y ) = ( X .x. y ) )
6	5	eqeq1d	|- ( x = X -> ( ( x .x. y ) = .0. <-> ( X .x. y ) = .0. ) )
7	6	imbi1d	|- ( x = X -> ( ( ( x .x. y ) = .0. -> y = .0. ) <-> ( ( X .x. y ) = .0. -> y = .0. ) ) )
8	7	ralbidv	|- ( x = X -> ( A. y e. B ( ( x .x. y ) = .0. -> y = .0. ) <-> A. y e. B ( ( X .x. y ) = .0. -> y = .0. ) ) )
9	1 2 3 4	rrgval	|- E = { x e. B | A. y e. B ( ( x .x. y ) = .0. -> y = .0. ) }
10	8 9	elrab2	|- ( X e. E <-> ( X e. B /\ A. y e. B ( ( X .x. y ) = .0. -> y = .0. ) ) )