Metamath Proof Explorer

Theorem rglcom4d

Description: Restricted commutativity of the addition in a ring-like structure. This (formerly) part of the proof for ringcom depends on the closure of the addition, the (left and 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 ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
rglcom4d.a ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 + 𝑦 ) ∈ 𝐵 )
rglcom4d.d ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( 𝑥 · ( 𝑦 + 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) )
rglcom4d.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
Assertion rglcom4d ( 𝜑 → ( ( 𝑋 + 𝑋 ) + ( 𝑌 + 𝑌 ) ) = ( ( 𝑋 + 𝑌 ) + ( 𝑋 + 𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 o2timesd.e ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) )
2 o2timesd.u ⊢ ( 𝜑 → 1 ∈ 𝐵 )
3 o2timesd.i ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ( 1 · 𝑥 ) = 𝑥 )
4 o2timesd.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
5 rglcom4d.a ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 + 𝑦 ) ∈ 𝐵 )
6 rglcom4d.d ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( 𝑥 · ( 𝑦 + 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) )
7 rglcom4d.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
8 2 2 jca ⊢ ( 𝜑 → ( 1 ∈ 𝐵 ∧ 1 ∈ 𝐵 ) )
9 oveq1 ⊢ ( 𝑥 = 1 → ( 𝑥 + 𝑦 ) = ( 1 + 𝑦 ) )
10 9 eleq1d ⊢ ( 𝑥 = 1 → ( ( 𝑥 + 𝑦 ) ∈ 𝐵 ↔ ( 1 + 𝑦 ) ∈ 𝐵 ) )
11 oveq2 ⊢ ( 𝑦 = 1 → ( 1 + 𝑦 ) = ( 1 + 1 ) )
12 11 eleq1d ⊢ ( 𝑦 = 1 → ( ( 1 + 𝑦 ) ∈ 𝐵 ↔ ( 1 + 1 ) ∈ 𝐵 ) )
13 10 12 rspc2v ⊢ ( ( 1 ∈ 𝐵 ∧ 1 ∈ 𝐵 ) → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 + 𝑦 ) ∈ 𝐵 → ( 1 + 1 ) ∈ 𝐵 ) )
14 8 5 13 sylc ⊢ ( 𝜑 → ( 1 + 1 ) ∈ 𝐵 )
15 14 4 7 3jca ⊢ ( 𝜑 → ( ( 1 + 1 ) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) )
16 oveq1 ⊢ ( 𝑥 = ( 1 + 1 ) → ( 𝑥 · ( 𝑦 + 𝑧 ) ) = ( ( 1 + 1 ) · ( 𝑦 + 𝑧 ) ) )
17 oveq1 ⊢ ( 𝑥 = ( 1 + 1 ) → ( 𝑥 · 𝑦 ) = ( ( 1 + 1 ) · 𝑦 ) )
18 oveq1 ⊢ ( 𝑥 = ( 1 + 1 ) → ( 𝑥 · 𝑧 ) = ( ( 1 + 1 ) · 𝑧 ) )
19 17 18 oveq12d ⊢ ( 𝑥 = ( 1 + 1 ) → ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) = ( ( ( 1 + 1 ) · 𝑦 ) + ( ( 1 + 1 ) · 𝑧 ) ) )
20 16 19 eqeq12d ⊢ ( 𝑥 = ( 1 + 1 ) → ( ( 𝑥 · ( 𝑦 + 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) ↔ ( ( 1 + 1 ) · ( 𝑦 + 𝑧 ) ) = ( ( ( 1 + 1 ) · 𝑦 ) + ( ( 1 + 1 ) · 𝑧 ) ) ) )
21 oveq1 ⊢ ( 𝑦 = 𝑋 → ( 𝑦 + 𝑧 ) = ( 𝑋 + 𝑧 ) )
22 21 oveq2d ⊢ ( 𝑦 = 𝑋 → ( ( 1 + 1 ) · ( 𝑦 + 𝑧 ) ) = ( ( 1 + 1 ) · ( 𝑋 + 𝑧 ) ) )
23 oveq2 ⊢ ( 𝑦 = 𝑋 → ( ( 1 + 1 ) · 𝑦 ) = ( ( 1 + 1 ) · 𝑋 ) )
24 23 oveq1d ⊢ ( 𝑦 = 𝑋 → ( ( ( 1 + 1 ) · 𝑦 ) + ( ( 1 + 1 ) · 𝑧 ) ) = ( ( ( 1 + 1 ) · 𝑋 ) + ( ( 1 + 1 ) · 𝑧 ) ) )
25 22 24 eqeq12d ⊢ ( 𝑦 = 𝑋 → ( ( ( 1 + 1 ) · ( 𝑦 + 𝑧 ) ) = ( ( ( 1 + 1 ) · 𝑦 ) + ( ( 1 + 1 ) · 𝑧 ) ) ↔ ( ( 1 + 1 ) · ( 𝑋 + 𝑧 ) ) = ( ( ( 1 + 1 ) · 𝑋 ) + ( ( 1 + 1 ) · 𝑧 ) ) ) )
26 oveq2 ⊢ ( 𝑧 = 𝑌 → ( 𝑋 + 𝑧 ) = ( 𝑋 + 𝑌 ) )
27 26 oveq2d ⊢ ( 𝑧 = 𝑌 → ( ( 1 + 1 ) · ( 𝑋 + 𝑧 ) ) = ( ( 1 + 1 ) · ( 𝑋 + 𝑌 ) ) )
28 oveq2 ⊢ ( 𝑧 = 𝑌 → ( ( 1 + 1 ) · 𝑧 ) = ( ( 1 + 1 ) · 𝑌 ) )
29 28 oveq2d ⊢ ( 𝑧 = 𝑌 → ( ( ( 1 + 1 ) · 𝑋 ) + ( ( 1 + 1 ) · 𝑧 ) ) = ( ( ( 1 + 1 ) · 𝑋 ) + ( ( 1 + 1 ) · 𝑌 ) ) )
30 27 29 eqeq12d ⊢ ( 𝑧 = 𝑌 → ( ( ( 1 + 1 ) · ( 𝑋 + 𝑧 ) ) = ( ( ( 1 + 1 ) · 𝑋 ) + ( ( 1 + 1 ) · 𝑧 ) ) ↔ ( ( 1 + 1 ) · ( 𝑋 + 𝑌 ) ) = ( ( ( 1 + 1 ) · 𝑋 ) + ( ( 1 + 1 ) · 𝑌 ) ) ) )
31 20 25 30 rspc3v ⊢ ( ( ( 1 + 1 ) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( 𝑥 · ( 𝑦 + 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) → ( ( 1 + 1 ) · ( 𝑋 + 𝑌 ) ) = ( ( ( 1 + 1 ) · 𝑋 ) + ( ( 1 + 1 ) · 𝑌 ) ) ) )
32 15 6 31 sylc ⊢ ( 𝜑 → ( ( 1 + 1 ) · ( 𝑋 + 𝑌 ) ) = ( ( ( 1 + 1 ) · 𝑋 ) + ( ( 1 + 1 ) · 𝑌 ) ) )
33 oveq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 + 𝑦 ) = ( 𝑋 + 𝑦 ) )
34 33 eleq1d ⊢ ( 𝑥 = 𝑋 → ( ( 𝑥 + 𝑦 ) ∈ 𝐵 ↔ ( 𝑋 + 𝑦 ) ∈ 𝐵 ) )
35 oveq2 ⊢ ( 𝑦 = 𝑌 → ( 𝑋 + 𝑦 ) = ( 𝑋 + 𝑌 ) )
36 35 eleq1d ⊢ ( 𝑦 = 𝑌 → ( ( 𝑋 + 𝑦 ) ∈ 𝐵 ↔ ( 𝑋 + 𝑌 ) ∈ 𝐵 ) )
37 34 36 rspc2va ⊢ ( ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 + 𝑦 ) ∈ 𝐵 ) → ( 𝑋 + 𝑌 ) ∈ 𝐵 )
38 4 7 5 37 syl21anc ⊢ ( 𝜑 → ( 𝑋 + 𝑌 ) ∈ 𝐵 )
39 2 2 38 3jca ⊢ ( 𝜑 → ( 1 ∈ 𝐵 ∧ 1 ∈ 𝐵 ∧ ( 𝑋 + 𝑌 ) ∈ 𝐵 ) )
40 9 oveq1d ⊢ ( 𝑥 = 1 → ( ( 𝑥 + 𝑦 ) · 𝑧 ) = ( ( 1 + 𝑦 ) · 𝑧 ) )
41 oveq1 ⊢ ( 𝑥 = 1 → ( 𝑥 · 𝑧 ) = ( 1 · 𝑧 ) )
42 41 oveq1d ⊢ ( 𝑥 = 1 → ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) = ( ( 1 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) )
43 40 42 eqeq12d ⊢ ( 𝑥 = 1 → ( ( ( 𝑥 + 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) ↔ ( ( 1 + 𝑦 ) · 𝑧 ) = ( ( 1 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) ) )
44 11 oveq1d ⊢ ( 𝑦 = 1 → ( ( 1 + 𝑦 ) · 𝑧 ) = ( ( 1 + 1 ) · 𝑧 ) )
45 oveq1 ⊢ ( 𝑦 = 1 → ( 𝑦 · 𝑧 ) = ( 1 · 𝑧 ) )
46 45 oveq2d ⊢ ( 𝑦 = 1 → ( ( 1 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) = ( ( 1 · 𝑧 ) + ( 1 · 𝑧 ) ) )
47 44 46 eqeq12d ⊢ ( 𝑦 = 1 → ( ( ( 1 + 𝑦 ) · 𝑧 ) = ( ( 1 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) ↔ ( ( 1 + 1 ) · 𝑧 ) = ( ( 1 · 𝑧 ) + ( 1 · 𝑧 ) ) ) )
48 oveq2 ⊢ ( 𝑧 = ( 𝑋 + 𝑌 ) → ( ( 1 + 1 ) · 𝑧 ) = ( ( 1 + 1 ) · ( 𝑋 + 𝑌 ) ) )
49 oveq2 ⊢ ( 𝑧 = ( 𝑋 + 𝑌 ) → ( 1 · 𝑧 ) = ( 1 · ( 𝑋 + 𝑌 ) ) )
50 49 49 oveq12d ⊢ ( 𝑧 = ( 𝑋 + 𝑌 ) → ( ( 1 · 𝑧 ) + ( 1 · 𝑧 ) ) = ( ( 1 · ( 𝑋 + 𝑌 ) ) + ( 1 · ( 𝑋 + 𝑌 ) ) ) )
51 48 50 eqeq12d ⊢ ( 𝑧 = ( 𝑋 + 𝑌 ) → ( ( ( 1 + 1 ) · 𝑧 ) = ( ( 1 · 𝑧 ) + ( 1 · 𝑧 ) ) ↔ ( ( 1 + 1 ) · ( 𝑋 + 𝑌 ) ) = ( ( 1 · ( 𝑋 + 𝑌 ) ) + ( 1 · ( 𝑋 + 𝑌 ) ) ) ) )
52 43 47 51 rspc3v ⊢ ( ( 1 ∈ 𝐵 ∧ 1 ∈ 𝐵 ∧ ( 𝑋 + 𝑌 ) ∈ 𝐵 ) → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) → ( ( 1 + 1 ) · ( 𝑋 + 𝑌 ) ) = ( ( 1 · ( 𝑋 + 𝑌 ) ) + ( 1 · ( 𝑋 + 𝑌 ) ) ) ) )
53 39 1 52 sylc ⊢ ( 𝜑 → ( ( 1 + 1 ) · ( 𝑋 + 𝑌 ) ) = ( ( 1 · ( 𝑋 + 𝑌 ) ) + ( 1 · ( 𝑋 + 𝑌 ) ) ) )
54 32 53 eqtr3d ⊢ ( 𝜑 → ( ( ( 1 + 1 ) · 𝑋 ) + ( ( 1 + 1 ) · 𝑌 ) ) = ( ( 1 · ( 𝑋 + 𝑌 ) ) + ( 1 · ( 𝑋 + 𝑌 ) ) ) )
55 1 2 3 4 o2timesd ⊢ ( 𝜑 → ( 𝑋 + 𝑋 ) = ( ( 1 + 1 ) · 𝑋 ) )
56 55 eqcomd ⊢ ( 𝜑 → ( ( 1 + 1 ) · 𝑋 ) = ( 𝑋 + 𝑋 ) )
57 1 2 3 7 o2timesd ⊢ ( 𝜑 → ( 𝑌 + 𝑌 ) = ( ( 1 + 1 ) · 𝑌 ) )
58 57 eqcomd ⊢ ( 𝜑 → ( ( 1 + 1 ) · 𝑌 ) = ( 𝑌 + 𝑌 ) )
59 56 58 oveq12d ⊢ ( 𝜑 → ( ( ( 1 + 1 ) · 𝑋 ) + ( ( 1 + 1 ) · 𝑌 ) ) = ( ( 𝑋 + 𝑋 ) + ( 𝑌 + 𝑌 ) ) )
60 oveq2 ⊢ ( 𝑥 = ( 𝑋 + 𝑌 ) → ( 1 · 𝑥 ) = ( 1 · ( 𝑋 + 𝑌 ) ) )
61 id ⊢ ( 𝑥 = ( 𝑋 + 𝑌 ) → 𝑥 = ( 𝑋 + 𝑌 ) )
62 60 61 eqeq12d ⊢ ( 𝑥 = ( 𝑋 + 𝑌 ) → ( ( 1 · 𝑥 ) = 𝑥 ↔ ( 1 · ( 𝑋 + 𝑌 ) ) = ( 𝑋 + 𝑌 ) ) )
63 62 rspcva ⊢ ( ( ( 𝑋 + 𝑌 ) ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( 1 · 𝑥 ) = 𝑥 ) → ( 1 · ( 𝑋 + 𝑌 ) ) = ( 𝑋 + 𝑌 ) )
64 38 3 63 syl2anc ⊢ ( 𝜑 → ( 1 · ( 𝑋 + 𝑌 ) ) = ( 𝑋 + 𝑌 ) )
65 64 64 oveq12d ⊢ ( 𝜑 → ( ( 1 · ( 𝑋 + 𝑌 ) ) + ( 1 · ( 𝑋 + 𝑌 ) ) ) = ( ( 𝑋 + 𝑌 ) + ( 𝑋 + 𝑌 ) ) )
66 54 59 65 3eqtr3d ⊢ ( 𝜑 → ( ( 𝑋 + 𝑋 ) + ( 𝑌 + 𝑌 ) ) = ( ( 𝑋 + 𝑌 ) + ( 𝑋 + 𝑌 ) ) )