Metamath Proof Explorer

Theorem rngo2times

Description: A ring element plus itself is two times the element. "Two" in an arbitrary unital ring is the sum of the unit with itself. (Contributed by AV, 24-Aug-2021)

		Ref	Expression
	Hypotheses	ringadd2.b	$⊢ B = {Base}_{R}$
		ringadd2.p	$⊢ \underset{˙}{+} = +_{R}$
		ringadd2.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
		rngo2times.u	$⊢ \underset{˙}{1} = 1_{R}$
	Assertion	rngo2times	$⊢ (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		ringadd2.b	$⊢ B = {Base}_{R}$
2		ringadd2.p	$⊢ \underset{˙}{+} = +_{R}$
3		ringadd2.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
4		rngo2times.u	$⊢ \underset{˙}{1} = 1_{R}$
5	1 3 4	ringlidm	$⊢ (R \in Ring \land A \in B) \to \underset{˙}{1} \underset{˙}{\cdot} A = A$
6	5	eqcomd	$⊢ (R \in Ring \land A \in B) \to A = \underset{˙}{1} \underset{˙}{\cdot} A$
7	6 6	oveq12d	$⊢ (R \in Ring \land A \in B) \to A \underset{˙}{+} A = (\underset{˙}{1} \underset{˙}{\cdot} A) \underset{˙}{+} (\underset{˙}{1} \underset{˙}{\cdot} A)$
8		simpl	$⊢ (R \in Ring \land A \in B) \to R \in Ring$
9	1 4	ringidcl	$⊢ R \in Ring \to \underset{˙}{1} \in B$
10	9	adantr	$⊢ (R \in Ring \land A \in B) \to \underset{˙}{1} \in B$
11		simpr	$⊢ (R \in Ring \land A \in B) \to A \in B$
12	1 2 3	ringdir	$⊢ (R \in Ring \land (\underset{˙}{1} \in B \land \underset{˙}{1} \in B \land A \in B)) \to (\underset{˙}{1} \underset{˙}{+} \underset{˙}{1}) \underset{˙}{\cdot} A = (\underset{˙}{1} \underset{˙}{\cdot} A) \underset{˙}{+} (\underset{˙}{1} \underset{˙}{\cdot} A)$
13	8 10 10 11 12	syl13anc	$⊢ (R \in Ring \land A \in B) \to (\underset{˙}{1} \underset{˙}{+} \underset{˙}{1}) \underset{˙}{\cdot} A = (\underset{˙}{1} \underset{˙}{\cdot} A) \underset{˙}{+} (\underset{˙}{1} \underset{˙}{\cdot} A)$
14	7 13	eqtr4d	$⊢ (R \in Ring \land A \in B) \to A \underset{˙}{+} A = (\underset{˙}{1} \underset{˙}{+} \underset{˙}{1}) \underset{˙}{\cdot} A$