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 ⊒ ( πœ‘ β†’ ( ( 𝑋 + 𝑋 ) + ( π‘Œ + π‘Œ ) ) = ( ( 𝑋 + π‘Œ ) + ( 𝑋 + π‘Œ ) ) )