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	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	rrgval.z	$⊢ \underset{˙}{0} = 0_{R}$
Assertion	isrrg	$⊢ X \in E \leftrightarrow (X \in B \land \forall y \in B (X \underset{˙}{\cdot} y = \underset{˙}{0} \to y = \underset{˙}{0}))$

Step	Hyp	Ref	Expression
1		rrgval.e	$⊢ E = RLReg (R)$
2		rrgval.b	$⊢ B = {Base}_{R}$
3		rrgval.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
4		rrgval.z	$⊢ \underset{˙}{0} = 0_{R}$
5		oveq1	$⊢ x = X \to x \underset{˙}{\cdot} y = X \underset{˙}{\cdot} y$
6	5	eqeq1d	$⊢ x = X \to (x \underset{˙}{\cdot} y = \underset{˙}{0} \leftrightarrow X \underset{˙}{\cdot} y = \underset{˙}{0})$
7	6	imbi1d	$⊢ x = X \to ((x \underset{˙}{\cdot} y = \underset{˙}{0} \to y = \underset{˙}{0}) \leftrightarrow (X \underset{˙}{\cdot} y = \underset{˙}{0} \to y = \underset{˙}{0}))$
8	7	ralbidv	$⊢ x = X \to (\forall y \in B (x \underset{˙}{\cdot} y = \underset{˙}{0} \to y = \underset{˙}{0}) \leftrightarrow \forall y \in B (X \underset{˙}{\cdot} y = \underset{˙}{0} \to y = \underset{˙}{0}))$
9	1 2 3 4	rrgval	$⊢ E = \{x \in B \| \forall y \in B (x \underset{˙}{\cdot} y = \underset{˙}{0} \to y = \underset{˙}{0})\}$
10	8 9	elrab2	$⊢ X \in E \leftrightarrow (X \in B \land \forall y \in B (X \underset{˙}{\cdot} y = \underset{˙}{0} \to y = \underset{˙}{0}))$

Metamath Proof Explorer