Theorem srgo2times

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

	Ref	Expression
Hypotheses	srgo2times.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	srgo2times.p	⊢ + = ( +g ‘ 𝑅 )
	srgo2times.t	⊢ · = ( .r ‘ 𝑅 )
	srgo2times.u	⊢ 1 = ( 1r ‘ 𝑅 )
Assertion	srgo2times	⊢ ( ( 𝑅 ∈ SRing ∧ 𝐴 ∈ 𝐵 ) → ( 𝐴 + 𝐴 ) = ( ( 1 + 1 ) · 𝐴 ) )

Proof

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