Metamath Proof Explorer


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