ringlz

Description: The zero of a unital ring is a left-absorbing element. (Contributed by FL, 31-Aug-2009)

	Ref	Expression
Hypotheses	rngz.b	$⊢ B = {Base}_{R}$
	rngz.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	rngz.z	$⊢ \underset{˙}{0} = 0_{R}$
Assertion	ringlz	$⊢ (R \in Ring \land X \in B) \to \underset{˙}{0} \underset{˙}{\cdot} X = \underset{˙}{0}$

Proof

Step	Hyp	Ref	Expression
1		rngz.b	$⊢ B = {Base}_{R}$
2		rngz.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
3		rngz.z	$⊢ \underset{˙}{0} = 0_{R}$
4		ringgrp	$⊢ R \in Ring \to R \in Grp$
5	1 3	grpidcl	$⊢ R \in Grp \to \underset{˙}{0} \in B$
6		eqid	$⊢ +_{R} = +_{R}$
7	1 6 3	grplid	$⊢ (R \in Grp \land \underset{˙}{0} \in B) \to \underset{˙}{0} +_{R} \underset{˙}{0} = \underset{˙}{0}$
8	4 5 7	syl2anc2	$⊢ R \in Ring \to \underset{˙}{0} +_{R} \underset{˙}{0} = \underset{˙}{0}$
9	8	adantr	$⊢ (R \in Ring \land X \in B) \to \underset{˙}{0} +_{R} \underset{˙}{0} = \underset{˙}{0}$
10	9	oveq1d	$⊢ (R \in Ring \land X \in B) \to (\underset{˙}{0} +_{R} \underset{˙}{0}) \underset{˙}{\cdot} X = \underset{˙}{0} \underset{˙}{\cdot} X$
11	4 5	syl	$⊢ R \in Ring \to \underset{˙}{0} \in B$
12	11	adantr	$⊢ (R \in Ring \land X \in B) \to \underset{˙}{0} \in B$
13		simpr	$⊢ (R \in Ring \land X \in B) \to X \in B$
14	12 12 13	3jca	$⊢ (R \in Ring \land X \in B) \to (\underset{˙}{0} \in B \land \underset{˙}{0} \in B \land X \in B)$
15	1 6 2	ringdir	$⊢ (R \in Ring \land (\underset{˙}{0} \in B \land \underset{˙}{0} \in B \land X \in B)) \to (\underset{˙}{0} +_{R} \underset{˙}{0}) \underset{˙}{\cdot} X = (\underset{˙}{0} \underset{˙}{\cdot} X) +_{R} (\underset{˙}{0} \underset{˙}{\cdot} X)$
16	14 15	syldan	$⊢ (R \in Ring \land X \in B) \to (\underset{˙}{0} +_{R} \underset{˙}{0}) \underset{˙}{\cdot} X = (\underset{˙}{0} \underset{˙}{\cdot} X) +_{R} (\underset{˙}{0} \underset{˙}{\cdot} X)$
17	4	adantr	$⊢ (R \in Ring \land X \in B) \to R \in Grp$
18		simpl	$⊢ (R \in Ring \land X \in B) \to R \in Ring$
19	1 2	ringcl	$⊢ (R \in Ring \land \underset{˙}{0} \in B \land X \in B) \to \underset{˙}{0} \underset{˙}{\cdot} X \in B$
20	18 12 13 19	syl3anc	$⊢ (R \in Ring \land X \in B) \to \underset{˙}{0} \underset{˙}{\cdot} X \in B$
21	1 6 3	grprid	$⊢ (R \in Grp \land \underset{˙}{0} \underset{˙}{\cdot} X \in B) \to (\underset{˙}{0} \underset{˙}{\cdot} X) +_{R} \underset{˙}{0} = \underset{˙}{0} \underset{˙}{\cdot} X$
22	21	eqcomd	$⊢ (R \in Grp \land \underset{˙}{0} \underset{˙}{\cdot} X \in B) \to \underset{˙}{0} \underset{˙}{\cdot} X = (\underset{˙}{0} \underset{˙}{\cdot} X) +_{R} \underset{˙}{0}$
23	17 20 22	syl2anc	$⊢ (R \in Ring \land X \in B) \to \underset{˙}{0} \underset{˙}{\cdot} X = (\underset{˙}{0} \underset{˙}{\cdot} X) +_{R} \underset{˙}{0}$
24	10 16 23	3eqtr3d	$⊢ (R \in Ring \land X \in B) \to (\underset{˙}{0} \underset{˙}{\cdot} X) +_{R} (\underset{˙}{0} \underset{˙}{\cdot} X) = (\underset{˙}{0} \underset{˙}{\cdot} X) +_{R} \underset{˙}{0}$
25	1 6	grplcan	$⊢ (R \in Grp \land (\underset{˙}{0} \underset{˙}{\cdot} X \in B \land \underset{˙}{0} \in B \land \underset{˙}{0} \underset{˙}{\cdot} X \in B)) \to ((\underset{˙}{0} \underset{˙}{\cdot} X) +_{R} (\underset{˙}{0} \underset{˙}{\cdot} X) = (\underset{˙}{0} \underset{˙}{\cdot} X) +_{R} \underset{˙}{0} \leftrightarrow \underset{˙}{0} \underset{˙}{\cdot} X = \underset{˙}{0})$
26	17 20 12 20 25	syl13anc	$⊢ (R \in Ring \land X \in B) \to ((\underset{˙}{0} \underset{˙}{\cdot} X) +_{R} (\underset{˙}{0} \underset{˙}{\cdot} X) = (\underset{˙}{0} \underset{˙}{\cdot} X) +_{R} \underset{˙}{0} \leftrightarrow \underset{˙}{0} \underset{˙}{\cdot} X = \underset{˙}{0})$
27	24 26	mpbid	$⊢ (R \in Ring \land X \in B) \to \underset{˙}{0} \underset{˙}{\cdot} X = \underset{˙}{0}$

Metamath Proof Explorer

Theorem ringlz

Proof