Metamath Proof Explorer

Theorem o2timesd

Description: An element of a ring-like structure plus itself is two times the element. "Two" in such a structure is the sum of the unity element with itself. This (formerly) part of the proof for ringcom depends on the (right) distributivity and the existence of a (left) multiplicative identity only. (Contributed by Gérard Lang, 4-Dec-2014) (Revised by AV, 1-Feb-2025)

Ref Expression
Hypotheses o2timesd.e ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) )
o2timesd.u ⊢ ( 𝜑 → 1 ∈ 𝐵 )
o2timesd.i ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ( 1 · 𝑥 ) = 𝑥 )
o2timesd.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
Assertion o2timesd ( 𝜑 → ( 𝑋 + 𝑋 ) = ( ( 1 + 1 ) · 𝑋 ) )

Proof

Step Hyp Ref Expression
1 o2timesd.e ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) )
2 o2timesd.u ⊢ ( 𝜑 → 1 ∈ 𝐵 )
3 o2timesd.i ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ( 1 · 𝑥 ) = 𝑥 )
4 o2timesd.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
5 oveq2 ⊢ ( 𝑥 = 𝑋 → ( 1 · 𝑥 ) = ( 1 · 𝑋 ) )
6 id ⊢ ( 𝑥 = 𝑋 → 𝑥 = 𝑋 )
7 5 6 eqeq12d ⊢ ( 𝑥 = 𝑋 → ( ( 1 · 𝑥 ) = 𝑥 ↔ ( 1 · 𝑋 ) = 𝑋 ) )
8 7 rspcva ⊢ ( ( 𝑋 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( 1 · 𝑥 ) = 𝑥 ) → ( 1 · 𝑋 ) = 𝑋 )
9 8 eqcomd ⊢ ( ( 𝑋 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( 1 · 𝑥 ) = 𝑥 ) → 𝑋 = ( 1 · 𝑋 ) )
10 4 3 9 syl2anc ⊢ ( 𝜑 → 𝑋 = ( 1 · 𝑋 ) )
11 10 10 oveq12d ⊢ ( 𝜑 → ( 𝑋 + 𝑋 ) = ( ( 1 · 𝑋 ) + ( 1 · 𝑋 ) ) )
12 2 2 4 3jca ⊢ ( 𝜑 → ( 1 ∈ 𝐵 ∧ 1 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) )
13 oveq1 ⊢ ( 𝑥 = 1 → ( 𝑥 + 𝑦 ) = ( 1 + 𝑦 ) )
14 13 oveq1d ⊢ ( 𝑥 = 1 → ( ( 𝑥 + 𝑦 ) · 𝑧 ) = ( ( 1 + 𝑦 ) · 𝑧 ) )
15 oveq1 ⊢ ( 𝑥 = 1 → ( 𝑥 · 𝑧 ) = ( 1 · 𝑧 ) )
16 15 oveq1d ⊢ ( 𝑥 = 1 → ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) = ( ( 1 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) )
17 14 16 eqeq12d ⊢ ( 𝑥 = 1 → ( ( ( 𝑥 + 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) ↔ ( ( 1 + 𝑦 ) · 𝑧 ) = ( ( 1 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) ) )
18 oveq2 ⊢ ( 𝑦 = 1 → ( 1 + 𝑦 ) = ( 1 + 1 ) )
19 18 oveq1d ⊢ ( 𝑦 = 1 → ( ( 1 + 𝑦 ) · 𝑧 ) = ( ( 1 + 1 ) · 𝑧 ) )
20 oveq1 ⊢ ( 𝑦 = 1 → ( 𝑦 · 𝑧 ) = ( 1 · 𝑧 ) )
21 20 oveq2d ⊢ ( 𝑦 = 1 → ( ( 1 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) = ( ( 1 · 𝑧 ) + ( 1 · 𝑧 ) ) )
22 19 21 eqeq12d ⊢ ( 𝑦 = 1 → ( ( ( 1 + 𝑦 ) · 𝑧 ) = ( ( 1 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) ↔ ( ( 1 + 1 ) · 𝑧 ) = ( ( 1 · 𝑧 ) + ( 1 · 𝑧 ) ) ) )
23 oveq2 ⊢ ( 𝑧 = 𝑋 → ( ( 1 + 1 ) · 𝑧 ) = ( ( 1 + 1 ) · 𝑋 ) )
24 oveq2 ⊢ ( 𝑧 = 𝑋 → ( 1 · 𝑧 ) = ( 1 · 𝑋 ) )
25 24 24 oveq12d ⊢ ( 𝑧 = 𝑋 → ( ( 1 · 𝑧 ) + ( 1 · 𝑧 ) ) = ( ( 1 · 𝑋 ) + ( 1 · 𝑋 ) ) )
26 23 25 eqeq12d ⊢ ( 𝑧 = 𝑋 → ( ( ( 1 + 1 ) · 𝑧 ) = ( ( 1 · 𝑧 ) + ( 1 · 𝑧 ) ) ↔ ( ( 1 + 1 ) · 𝑋 ) = ( ( 1 · 𝑋 ) + ( 1 · 𝑋 ) ) ) )
27 17 22 26 rspc3v ⊢ ( ( 1 ∈ 𝐵 ∧ 1 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) → ( ( 1 + 1 ) · 𝑋 ) = ( ( 1 · 𝑋 ) + ( 1 · 𝑋 ) ) ) )
28 12 1 27 sylc ⊢ ( 𝜑 → ( ( 1 + 1 ) · 𝑋 ) = ( ( 1 · 𝑋 ) + ( 1 · 𝑋 ) ) )
29 11 28 eqtr4d ⊢ ( 𝜑 → ( 𝑋 + 𝑋 ) = ( ( 1 + 1 ) · 𝑋 ) )