This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rrgeq0

Description: Left-multiplication by a left regular element does not change zeroness. (Contributed by Stefan O'Rear, 28-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	rrgeq0	$⊢ (R \in Ring \land X \in E \land Y \in B) \to (X \underset{˙}{\cdot} Y = \underset{˙}{0} \leftrightarrow Y = \underset{˙}{0})$

Proof

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	rrgeq0i	$⊢ (X \in E \land Y \in B) \to (X \underset{˙}{\cdot} Y = \underset{˙}{0} \to Y = \underset{˙}{0})$
6	5	3adant1	$⊢ (R \in Ring \land X \in E \land Y \in B) \to (X \underset{˙}{\cdot} Y = \underset{˙}{0} \to Y = \underset{˙}{0})$
7		simp1	$⊢ (R \in Ring \land X \in E \land Y \in B) \to R \in Ring$
8	1 2 3 4	rrgval	$⊢ E = \{x \in B \| \forall y \in B (x \underset{˙}{\cdot} y = \underset{˙}{0} \to y = \underset{˙}{0})\}$
9	8	ssrab3	$⊢ E \subseteq B$
10		simp2	$⊢ (R \in Ring \land X \in E \land Y \in B) \to X \in E$
11	9 10	sselid	$⊢ (R \in Ring \land X \in E \land Y \in B) \to X \in B$
12	2 3 4	ringrz	$⊢ (R \in Ring \land X \in B) \to X \underset{˙}{\cdot} \underset{˙}{0} = \underset{˙}{0}$
13	7 11 12	syl2anc	$⊢ (R \in Ring \land X \in E \land Y \in B) \to X \underset{˙}{\cdot} \underset{˙}{0} = \underset{˙}{0}$
14		oveq2	$⊢ Y = \underset{˙}{0} \to X \underset{˙}{\cdot} Y = X \underset{˙}{\cdot} \underset{˙}{0}$
15	14	eqeq1d	$⊢ Y = \underset{˙}{0} \to (X \underset{˙}{\cdot} Y = \underset{˙}{0} \leftrightarrow X \underset{˙}{\cdot} \underset{˙}{0} = \underset{˙}{0})$
16	13 15	syl5ibrcom	$⊢ (R \in Ring \land X \in E \land Y \in B) \to (Y = \underset{˙}{0} \to X \underset{˙}{\cdot} Y = \underset{˙}{0})$
17	6 16	impbid	$⊢ (R \in Ring \land X \in E \land Y \in B) \to (X \underset{˙}{\cdot} Y = \underset{˙}{0} \leftrightarrow Y = \underset{˙}{0})$