This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) · 𝐴 ) )