ringrz

Description: The zero of a unital ring is a right-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	ringrz	$⊢ (R \in Ring \land X \in B) \to X \underset{˙}{\cdot} \underset{˙}{0} = \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	oveq2d	$⊢ (R \in Ring \land X \in B) \to X \underset{˙}{\cdot} (\underset{˙}{0} +_{R} \underset{˙}{0}) = X \underset{˙}{\cdot} \underset{˙}{0}$
11		simpr	$⊢ (R \in Ring \land X \in B) \to X \in B$
12	4 5	syl	$⊢ R \in Ring \to \underset{˙}{0} \in B$
13	12	adantr	$⊢ (R \in Ring \land X \in B) \to \underset{˙}{0} \in B$
14	11 13 13	3jca	$⊢ (R \in Ring \land X \in B) \to (X \in B \land \underset{˙}{0} \in B \land \underset{˙}{0} \in B)$
15	1 6 2	ringdi	$⊢ (R \in Ring \land (X \in B \land \underset{˙}{0} \in B \land \underset{˙}{0} \in B)) \to X \underset{˙}{\cdot} (\underset{˙}{0} +_{R} \underset{˙}{0}) = (X \underset{˙}{\cdot} \underset{˙}{0}) +_{R} (X \underset{˙}{\cdot} \underset{˙}{0})$
16	14 15	syldan	$⊢ (R \in Ring \land X \in B) \to X \underset{˙}{\cdot} (\underset{˙}{0} +_{R} \underset{˙}{0}) = (X \underset{˙}{\cdot} \underset{˙}{0}) +_{R} (X \underset{˙}{\cdot} \underset{˙}{0})$
17	4	adantr	$⊢ (R \in Ring \land X \in B) \to R \in Grp$
18	1 2	ringcl	$⊢ (R \in Ring \land X \in B \land \underset{˙}{0} \in B) \to X \underset{˙}{\cdot} \underset{˙}{0} \in B$
19	13 18	mpd3an3	$⊢ (R \in Ring \land X \in B) \to X \underset{˙}{\cdot} \underset{˙}{0} \in B$
20	1 6 3	grplid	$⊢ (R \in Grp \land X \underset{˙}{\cdot} \underset{˙}{0} \in B) \to \underset{˙}{0} +_{R} (X \underset{˙}{\cdot} \underset{˙}{0}) = X \underset{˙}{\cdot} \underset{˙}{0}$
21	20	eqcomd	$⊢ (R \in Grp \land X \underset{˙}{\cdot} \underset{˙}{0} \in B) \to X \underset{˙}{\cdot} \underset{˙}{0} = \underset{˙}{0} +_{R} (X \underset{˙}{\cdot} \underset{˙}{0})$
22	17 19 21	syl2anc	$⊢ (R \in Ring \land X \in B) \to X \underset{˙}{\cdot} \underset{˙}{0} = \underset{˙}{0} +_{R} (X \underset{˙}{\cdot} \underset{˙}{0})$
23	10 16 22	3eqtr3d	$⊢ (R \in Ring \land X \in B) \to (X \underset{˙}{\cdot} \underset{˙}{0}) +_{R} (X \underset{˙}{\cdot} \underset{˙}{0}) = \underset{˙}{0} +_{R} (X \underset{˙}{\cdot} \underset{˙}{0})$
24	1 6	grprcan	$⊢ (R \in Grp \land (X \underset{˙}{\cdot} \underset{˙}{0} \in B \land \underset{˙}{0} \in B \land X \underset{˙}{\cdot} \underset{˙}{0} \in B)) \to ((X \underset{˙}{\cdot} \underset{˙}{0}) +_{R} (X \underset{˙}{\cdot} \underset{˙}{0}) = \underset{˙}{0} +_{R} (X \underset{˙}{\cdot} \underset{˙}{0}) \leftrightarrow X \underset{˙}{\cdot} \underset{˙}{0} = \underset{˙}{0})$
25	17 19 13 19 24	syl13anc	$⊢ (R \in Ring \land X \in B) \to ((X \underset{˙}{\cdot} \underset{˙}{0}) +_{R} (X \underset{˙}{\cdot} \underset{˙}{0}) = \underset{˙}{0} +_{R} (X \underset{˙}{\cdot} \underset{˙}{0}) \leftrightarrow X \underset{˙}{\cdot} \underset{˙}{0} = \underset{˙}{0})$
26	23 25	mpbid	$⊢ (R \in Ring \land X \in B) \to X \underset{˙}{\cdot} \underset{˙}{0} = \underset{˙}{0}$

Metamath Proof Explorer

Theorem ringrz

Proof