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	⊢ 𝐵 = ( Base ‘ 𝑅 )
	ringadd2.p	⊢ + = ( +g ‘ 𝑅 )
	ringadd2.t	⊢ · = ( .r ‘ 𝑅 )
	rngo2times.u	⊢ 1 = ( 1r ‘ 𝑅 )
Assertion	rngo2times	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐴 ∈ 𝐵 ) → ( 𝐴 + 𝐴 ) = ( ( 1 + 1 ) · 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		ringadd2.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		ringadd2.p	⊢ + = ( +g ‘ 𝑅 )
3		ringadd2.t	⊢ · = ( .r ‘ 𝑅 )
4		rngo2times.u	⊢ 1 = ( 1r ‘ 𝑅 )
5	1 3 4	ringlidm	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐴 ∈ 𝐵 ) → ( 1 · 𝐴 ) = 𝐴 )
6	5	eqcomd	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐴 ∈ 𝐵 ) → 𝐴 = ( 1 · 𝐴 ) )
7	6 6	oveq12d	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐴 ∈ 𝐵 ) → ( 𝐴 + 𝐴 ) = ( ( 1 · 𝐴 ) + ( 1 · 𝐴 ) ) )
8		simpl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐴 ∈ 𝐵 ) → 𝑅 ∈ Ring )
9	1 4	ringidcl	⊢ ( 𝑅 ∈ Ring → 1 ∈ 𝐵 )
10	9	adantr	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐴 ∈ 𝐵 ) → 1 ∈ 𝐵 )
11		simpr	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐴 ∈ 𝐵 ) → 𝐴 ∈ 𝐵 )
12	1 2 3	ringdir	⊢ ( ( 𝑅 ∈ Ring ∧ ( 1 ∈ 𝐵 ∧ 1 ∈ 𝐵 ∧ 𝐴 ∈ 𝐵 ) ) → ( ( 1 + 1 ) · 𝐴 ) = ( ( 1 · 𝐴 ) + ( 1 · 𝐴 ) ) )
13	8 10 10 11 12	syl13anc	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐴 ∈ 𝐵 ) → ( ( 1 + 1 ) · 𝐴 ) = ( ( 1 · 𝐴 ) + ( 1 · 𝐴 ) ) )
14	7 13	eqtr4d	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐴 ∈ 𝐵 ) → ( 𝐴 + 𝐴 ) = ( ( 1 + 1 ) · 𝐴 ) )