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

Metamath Proof Explorer

Theorem ringo2times

Description: A ring element plus itself is two times the element. "Two" in an arbitrary unital ring is the sum of the unity element with itself. (Contributed by AV, 24-Aug-2021) Variant of o2timesd for rings. (Revised by AV, 5-Feb-2025)

		Ref	Expression
	Hypotheses	ringo2times.b	$⊢ B = {Base}_{R}$
		ringo2times.p	$⊢ \underset{˙}{+} = +_{R}$
		ringo2times.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
		ringo2times.u	$⊢ \underset{˙}{1} = 1_{R}$
	Assertion	ringo2times	$⊢ (R \in Ring \land A \in B) \to A \underset{˙}{+} A = (\underset{˙}{1} \underset{˙}{+} \underset{˙}{1}) \underset{˙}{\cdot} A$

Proof

Step	Hyp	Ref	Expression
1		ringo2times.b	$⊢ B = {Base}_{R}$
2		ringo2times.p	$⊢ \underset{˙}{+} = +_{R}$
3		ringo2times.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
4		ringo2times.u	$⊢ \underset{˙}{1} = 1_{R}$
5	1 2 3	ringdir	$⊢ (R \in Ring \land (x \in B \land y \in B \land z \in B)) \to (x \underset{˙}{+} y) \underset{˙}{\cdot} z = (x \underset{˙}{\cdot} z) \underset{˙}{+} (y \underset{˙}{\cdot} z)$
6	5	ralrimivvva	$⊢ R \in Ring \to \forall x \in B \forall y \in B \forall z \in B (x \underset{˙}{+} y) \underset{˙}{\cdot} z = (x \underset{˙}{\cdot} z) \underset{˙}{+} (y \underset{˙}{\cdot} z)$
7	6	adantr	$⊢ (R \in Ring \land A \in B) \to \forall x \in B \forall y \in B \forall z \in B (x \underset{˙}{+} y) \underset{˙}{\cdot} z = (x \underset{˙}{\cdot} z) \underset{˙}{+} (y \underset{˙}{\cdot} z)$
8	1 4	ringidcl	$⊢ R \in Ring \to \underset{˙}{1} \in B$
9	8	adantr	$⊢ (R \in Ring \land A \in B) \to \underset{˙}{1} \in B$
10	1 3 4	ringlidm	$⊢ (R \in Ring \land x \in B) \to \underset{˙}{1} \underset{˙}{\cdot} x = x$
11	10	ralrimiva	$⊢ R \in Ring \to \forall x \in B \underset{˙}{1} \underset{˙}{\cdot} x = x$
12	11	adantr	$⊢ (R \in Ring \land A \in B) \to \forall x \in B \underset{˙}{1} \underset{˙}{\cdot} x = x$
13		simpr	$⊢ (R \in Ring \land A \in B) \to A \in B$
14	7 9 12 13	o2timesd	$⊢ (R \in Ring \land A \in B) \to A \underset{˙}{+} A = (\underset{˙}{1} \underset{˙}{+} \underset{˙}{1}) \underset{˙}{\cdot} A$