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