rrgeq0i

Description: Property of a left-regular element. (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	rrgeq0i	$⊢ (X \in E \land Y \in B) \to (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	1 2 3 4	isrrg	$⊢ X \in E \leftrightarrow (X \in B \land \forall y \in B (X \underset{˙}{\cdot} y = \underset{˙}{0} \to y = \underset{˙}{0}))$
6	5	simprbi	$⊢ X \in E \to \forall y \in B (X \underset{˙}{\cdot} y = \underset{˙}{0} \to y = \underset{˙}{0})$
7		oveq2	$⊢ y = Y \to X \underset{˙}{\cdot} y = X \underset{˙}{\cdot} Y$
8	7	eqeq1d	$⊢ y = Y \to (X \underset{˙}{\cdot} y = \underset{˙}{0} \leftrightarrow X \underset{˙}{\cdot} Y = \underset{˙}{0})$
9		eqeq1	$⊢ y = Y \to (y = \underset{˙}{0} \leftrightarrow Y = \underset{˙}{0})$
10	8 9	imbi12d	$⊢ y = Y \to ((X \underset{˙}{\cdot} y = \underset{˙}{0} \to y = \underset{˙}{0}) \leftrightarrow (X \underset{˙}{\cdot} Y = \underset{˙}{0} \to Y = \underset{˙}{0}))$
11	10	rspcv	$⊢ Y \in B \to (\forall y \in B (X \underset{˙}{\cdot} y = \underset{˙}{0} \to y = \underset{˙}{0}) \to (X \underset{˙}{\cdot} Y = \underset{˙}{0} \to Y = \underset{˙}{0}))$
12	6 11	mpan9	$⊢ (X \in E \land Y \in B) \to (X \underset{˙}{\cdot} Y = \underset{˙}{0} \to Y = \underset{˙}{0})$

Metamath Proof Explorer