Metamath Proof Explorer

Theorem ringadd2

Description: A ring element plus itself is two times the element. (Contributed by Steve Rodriguez, 9-Sep-2007) (Revised by Mario Carneiro, 22-Dec-2013) (Revised by AV, 24-Aug-2021) (Proof shortened by AV, 1-Feb-2025)

		Ref	Expression
	Hypotheses	ringadd2.b	$⊢ B = {Base}_{R}$
		ringadd2.p	$⊢ \underset{˙}{+} = +_{R}$
		ringadd2.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	Assertion	ringadd2	$⊢ (R \in Ring \land X \in B) \to \exists x \in B X \underset{˙}{+} X = (x \underset{˙}{+} x) \underset{˙}{\cdot} X$

Proof

Step	Hyp	Ref	Expression
1		ringadd2.b	$⊢ B = {Base}_{R}$
2		ringadd2.p	$⊢ \underset{˙}{+} = +_{R}$
3		ringadd2.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
4		eqid	$⊢ 1_{R} = 1_{R}$
5	1 4	ringidcl	$⊢ R \in Ring \to 1_{R} \in B$
6	5	adantr	$⊢ (R \in Ring \land X \in B) \to 1_{R} \in B$
7		simpr	$⊢ ((R \in Ring \land X \in B) \land x = 1_{R}) \to x = 1_{R}$
8	7 7	oveq12d	$⊢ ((R \in Ring \land X \in B) \land x = 1_{R}) \to x \underset{˙}{+} x = 1_{R} \underset{˙}{+} 1_{R}$
9	8	oveq1d	$⊢ ((R \in Ring \land X \in B) \land x = 1_{R}) \to (x \underset{˙}{+} x) \underset{˙}{\cdot} X = (1_{R} \underset{˙}{+} 1_{R}) \underset{˙}{\cdot} X$
10	9	eqeq2d	$⊢ ((R \in Ring \land X \in B) \land x = 1_{R}) \to (X \underset{˙}{+} X = (x \underset{˙}{+} x) \underset{˙}{\cdot} X \leftrightarrow X \underset{˙}{+} X = (1_{R} \underset{˙}{+} 1_{R}) \underset{˙}{\cdot} X)$
11	1 2 3 4	ringo2times	$⊢ (R \in Ring \land X \in B) \to X \underset{˙}{+} X = (1_{R} \underset{˙}{+} 1_{R}) \underset{˙}{\cdot} X$
12	6 10 11	rspcedvd	$⊢ (R \in Ring \land X \in B) \to \exists x \in B X \underset{˙}{+} X = (x \underset{˙}{+} x) \underset{˙}{\cdot} X$