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

Proof

Step	Hyp	Ref	Expression
1		ringo2times.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		ringo2times.p	⊢ + = ( +g ‘ 𝑅 )
3		ringo2times.t	⊢ · = ( .r ‘ 𝑅 )
4		ringo2times.u	⊢ 1 = ( 1r ‘ 𝑅 )
5	1 2 3	ringdir	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( ( 𝑥 + 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) )
6	5	ralrimivvva	⊢ ( 𝑅 ∈ Ring → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) )
7	6	adantr	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐴 ∈ 𝐵 ) → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) )
8	1 4	ringidcl	⊢ ( 𝑅 ∈ Ring → 1 ∈ 𝐵 )
9	8	adantr	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐴 ∈ 𝐵 ) → 1 ∈ 𝐵 )
10	1 3 4	ringlidm	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐵 ) → ( 1 · 𝑥 ) = 𝑥 )
11	10	ralrimiva	⊢ ( 𝑅 ∈ Ring → ∀ 𝑥 ∈ 𝐵 ( 1 · 𝑥 ) = 𝑥 )
12	11	adantr	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐴 ∈ 𝐵 ) → ∀ 𝑥 ∈ 𝐵 ( 1 · 𝑥 ) = 𝑥 )
13		simpr	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐴 ∈ 𝐵 ) → 𝐴 ∈ 𝐵 )
14	7 9 12 13	o2timesd	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐴 ∈ 𝐵 ) → ( 𝐴 + 𝐴 ) = ( ( 1 + 1 ) · 𝐴 ) )