MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rglcom4d Structured version   Visualization version   GIF version

Theorem rglcom4d 20034
Description: Restricted commutativity of the addition in a ring-like structure. This (formerly) part of the proof for ringcom 20097 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.)
Hypotheses
Ref Expression
o2timesd.e (πœ‘ β†’ βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐡 βˆ€π‘§ ∈ 𝐡 ((π‘₯ + 𝑦) Β· 𝑧) = ((π‘₯ Β· 𝑧) + (𝑦 Β· 𝑧)))
o2timesd.u (πœ‘ β†’ 1 ∈ 𝐡)
o2timesd.i (πœ‘ β†’ βˆ€π‘₯ ∈ 𝐡 ( 1 Β· π‘₯) = π‘₯)
o2timesd.x (πœ‘ β†’ 𝑋 ∈ 𝐡)
rglcom4d.a (πœ‘ β†’ βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐡 (π‘₯ + 𝑦) ∈ 𝐡)
rglcom4d.d (πœ‘ β†’ βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐡 βˆ€π‘§ ∈ 𝐡 (π‘₯ Β· (𝑦 + 𝑧)) = ((π‘₯ Β· 𝑦) + (π‘₯ Β· 𝑧)))
rglcom4d.y (πœ‘ β†’ π‘Œ ∈ 𝐡)
Assertion
Ref Expression
rglcom4d (πœ‘ β†’ ((𝑋 + 𝑋) + (π‘Œ + π‘Œ)) = ((𝑋 + π‘Œ) + (𝑋 + π‘Œ)))
Distinct variable groups:   π‘₯,𝐡,𝑦,𝑧   π‘₯,𝑋,𝑦,𝑧   π‘₯, 1 ,𝑦,𝑧   π‘₯, Β· ,𝑦,𝑧   π‘₯, + ,𝑦,𝑧   π‘₯,π‘Œ,𝑦,𝑧
Allowed substitution hints:   πœ‘(π‘₯,𝑦,𝑧)

Proof of Theorem rglcom4d
StepHypRef Expression
1 o2timesd.u . . . . . . 7 (πœ‘ β†’ 1 ∈ 𝐡)
21, 1jca 513 . . . . . 6 (πœ‘ β†’ ( 1 ∈ 𝐡 ∧ 1 ∈ 𝐡))
3 rglcom4d.a . . . . . 6 (πœ‘ β†’ βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐡 (π‘₯ + 𝑦) ∈ 𝐡)
4 oveq1 7416 . . . . . . . 8 (π‘₯ = 1 β†’ (π‘₯ + 𝑦) = ( 1 + 𝑦))
54eleq1d 2819 . . . . . . 7 (π‘₯ = 1 β†’ ((π‘₯ + 𝑦) ∈ 𝐡 ↔ ( 1 + 𝑦) ∈ 𝐡))
6 oveq2 7417 . . . . . . . 8 (𝑦 = 1 β†’ ( 1 + 𝑦) = ( 1 + 1 ))
76eleq1d 2819 . . . . . . 7 (𝑦 = 1 β†’ (( 1 + 𝑦) ∈ 𝐡 ↔ ( 1 + 1 ) ∈ 𝐡))
85, 7rspc2v 3623 . . . . . 6 (( 1 ∈ 𝐡 ∧ 1 ∈ 𝐡) β†’ (βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐡 (π‘₯ + 𝑦) ∈ 𝐡 β†’ ( 1 + 1 ) ∈ 𝐡))
92, 3, 8sylc 65 . . . . 5 (πœ‘ β†’ ( 1 + 1 ) ∈ 𝐡)
10 o2timesd.x . . . . 5 (πœ‘ β†’ 𝑋 ∈ 𝐡)
11 rglcom4d.y . . . . 5 (πœ‘ β†’ π‘Œ ∈ 𝐡)
129, 10, 113jca 1129 . . . 4 (πœ‘ β†’ (( 1 + 1 ) ∈ 𝐡 ∧ 𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡))
13 rglcom4d.d . . . 4 (πœ‘ β†’ βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐡 βˆ€π‘§ ∈ 𝐡 (π‘₯ Β· (𝑦 + 𝑧)) = ((π‘₯ Β· 𝑦) + (π‘₯ Β· 𝑧)))
14 oveq1 7416 . . . . . 6 (π‘₯ = ( 1 + 1 ) β†’ (π‘₯ Β· (𝑦 + 𝑧)) = (( 1 + 1 ) Β· (𝑦 + 𝑧)))
15 oveq1 7416 . . . . . . 7 (π‘₯ = ( 1 + 1 ) β†’ (π‘₯ Β· 𝑦) = (( 1 + 1 ) Β· 𝑦))
16 oveq1 7416 . . . . . . 7 (π‘₯ = ( 1 + 1 ) β†’ (π‘₯ Β· 𝑧) = (( 1 + 1 ) Β· 𝑧))
1715, 16oveq12d 7427 . . . . . 6 (π‘₯ = ( 1 + 1 ) β†’ ((π‘₯ Β· 𝑦) + (π‘₯ Β· 𝑧)) = ((( 1 + 1 ) Β· 𝑦) + (( 1 + 1 ) Β· 𝑧)))
1814, 17eqeq12d 2749 . . . . 5 (π‘₯ = ( 1 + 1 ) β†’ ((π‘₯ Β· (𝑦 + 𝑧)) = ((π‘₯ Β· 𝑦) + (π‘₯ Β· 𝑧)) ↔ (( 1 + 1 ) Β· (𝑦 + 𝑧)) = ((( 1 + 1 ) Β· 𝑦) + (( 1 + 1 ) Β· 𝑧))))
19 oveq1 7416 . . . . . . 7 (𝑦 = 𝑋 β†’ (𝑦 + 𝑧) = (𝑋 + 𝑧))
2019oveq2d 7425 . . . . . 6 (𝑦 = 𝑋 β†’ (( 1 + 1 ) Β· (𝑦 + 𝑧)) = (( 1 + 1 ) Β· (𝑋 + 𝑧)))
21 oveq2 7417 . . . . . . 7 (𝑦 = 𝑋 β†’ (( 1 + 1 ) Β· 𝑦) = (( 1 + 1 ) Β· 𝑋))
2221oveq1d 7424 . . . . . 6 (𝑦 = 𝑋 β†’ ((( 1 + 1 ) Β· 𝑦) + (( 1 + 1 ) Β· 𝑧)) = ((( 1 + 1 ) Β· 𝑋) + (( 1 + 1 ) Β· 𝑧)))
2320, 22eqeq12d 2749 . . . . 5 (𝑦 = 𝑋 β†’ ((( 1 + 1 ) Β· (𝑦 + 𝑧)) = ((( 1 + 1 ) Β· 𝑦) + (( 1 + 1 ) Β· 𝑧)) ↔ (( 1 + 1 ) Β· (𝑋 + 𝑧)) = ((( 1 + 1 ) Β· 𝑋) + (( 1 + 1 ) Β· 𝑧))))
24 oveq2 7417 . . . . . . 7 (𝑧 = π‘Œ β†’ (𝑋 + 𝑧) = (𝑋 + π‘Œ))
2524oveq2d 7425 . . . . . 6 (𝑧 = π‘Œ β†’ (( 1 + 1 ) Β· (𝑋 + 𝑧)) = (( 1 + 1 ) Β· (𝑋 + π‘Œ)))
26 oveq2 7417 . . . . . . 7 (𝑧 = π‘Œ β†’ (( 1 + 1 ) Β· 𝑧) = (( 1 + 1 ) Β· π‘Œ))
2726oveq2d 7425 . . . . . 6 (𝑧 = π‘Œ β†’ ((( 1 + 1 ) Β· 𝑋) + (( 1 + 1 ) Β· 𝑧)) = ((( 1 + 1 ) Β· 𝑋) + (( 1 + 1 ) Β· π‘Œ)))
2825, 27eqeq12d 2749 . . . . 5 (𝑧 = π‘Œ β†’ ((( 1 + 1 ) Β· (𝑋 + 𝑧)) = ((( 1 + 1 ) Β· 𝑋) + (( 1 + 1 ) Β· 𝑧)) ↔ (( 1 + 1 ) Β· (𝑋 + π‘Œ)) = ((( 1 + 1 ) Β· 𝑋) + (( 1 + 1 ) Β· π‘Œ))))
2918, 23, 28rspc3v 3628 . . . 4 ((( 1 + 1 ) ∈ 𝐡 ∧ 𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡) β†’ (βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐡 βˆ€π‘§ ∈ 𝐡 (π‘₯ Β· (𝑦 + 𝑧)) = ((π‘₯ Β· 𝑦) + (π‘₯ Β· 𝑧)) β†’ (( 1 + 1 ) Β· (𝑋 + π‘Œ)) = ((( 1 + 1 ) Β· 𝑋) + (( 1 + 1 ) Β· π‘Œ))))
3012, 13, 29sylc 65 . . 3 (πœ‘ β†’ (( 1 + 1 ) Β· (𝑋 + π‘Œ)) = ((( 1 + 1 ) Β· 𝑋) + (( 1 + 1 ) Β· π‘Œ)))
31 oveq1 7416 . . . . . . . 8 (π‘₯ = 𝑋 β†’ (π‘₯ + 𝑦) = (𝑋 + 𝑦))
3231eleq1d 2819 . . . . . . 7 (π‘₯ = 𝑋 β†’ ((π‘₯ + 𝑦) ∈ 𝐡 ↔ (𝑋 + 𝑦) ∈ 𝐡))
33 oveq2 7417 . . . . . . . 8 (𝑦 = π‘Œ β†’ (𝑋 + 𝑦) = (𝑋 + π‘Œ))
3433eleq1d 2819 . . . . . . 7 (𝑦 = π‘Œ β†’ ((𝑋 + 𝑦) ∈ 𝐡 ↔ (𝑋 + π‘Œ) ∈ 𝐡))
3532, 34rspc2va 3624 . . . . . 6 (((𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡) ∧ βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐡 (π‘₯ + 𝑦) ∈ 𝐡) β†’ (𝑋 + π‘Œ) ∈ 𝐡)
3610, 11, 3, 35syl21anc 837 . . . . 5 (πœ‘ β†’ (𝑋 + π‘Œ) ∈ 𝐡)
371, 1, 363jca 1129 . . . 4 (πœ‘ β†’ ( 1 ∈ 𝐡 ∧ 1 ∈ 𝐡 ∧ (𝑋 + π‘Œ) ∈ 𝐡))
38 o2timesd.e . . . 4 (πœ‘ β†’ βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐡 βˆ€π‘§ ∈ 𝐡 ((π‘₯ + 𝑦) Β· 𝑧) = ((π‘₯ Β· 𝑧) + (𝑦 Β· 𝑧)))
394oveq1d 7424 . . . . . 6 (π‘₯ = 1 β†’ ((π‘₯ + 𝑦) Β· 𝑧) = (( 1 + 𝑦) Β· 𝑧))
40 oveq1 7416 . . . . . . 7 (π‘₯ = 1 β†’ (π‘₯ Β· 𝑧) = ( 1 Β· 𝑧))
4140oveq1d 7424 . . . . . 6 (π‘₯ = 1 β†’ ((π‘₯ Β· 𝑧) + (𝑦 Β· 𝑧)) = (( 1 Β· 𝑧) + (𝑦 Β· 𝑧)))
4239, 41eqeq12d 2749 . . . . 5 (π‘₯ = 1 β†’ (((π‘₯ + 𝑦) Β· 𝑧) = ((π‘₯ Β· 𝑧) + (𝑦 Β· 𝑧)) ↔ (( 1 + 𝑦) Β· 𝑧) = (( 1 Β· 𝑧) + (𝑦 Β· 𝑧))))
436oveq1d 7424 . . . . . 6 (𝑦 = 1 β†’ (( 1 + 𝑦) Β· 𝑧) = (( 1 + 1 ) Β· 𝑧))
44 oveq1 7416 . . . . . . 7 (𝑦 = 1 β†’ (𝑦 Β· 𝑧) = ( 1 Β· 𝑧))
4544oveq2d 7425 . . . . . 6 (𝑦 = 1 β†’ (( 1 Β· 𝑧) + (𝑦 Β· 𝑧)) = (( 1 Β· 𝑧) + ( 1 Β· 𝑧)))
4643, 45eqeq12d 2749 . . . . 5 (𝑦 = 1 β†’ ((( 1 + 𝑦) Β· 𝑧) = (( 1 Β· 𝑧) + (𝑦 Β· 𝑧)) ↔ (( 1 + 1 ) Β· 𝑧) = (( 1 Β· 𝑧) + ( 1 Β· 𝑧))))
47 oveq2 7417 . . . . . 6 (𝑧 = (𝑋 + π‘Œ) β†’ (( 1 + 1 ) Β· 𝑧) = (( 1 + 1 ) Β· (𝑋 + π‘Œ)))
48 oveq2 7417 . . . . . . 7 (𝑧 = (𝑋 + π‘Œ) β†’ ( 1 Β· 𝑧) = ( 1 Β· (𝑋 + π‘Œ)))
4948, 48oveq12d 7427 . . . . . 6 (𝑧 = (𝑋 + π‘Œ) β†’ (( 1 Β· 𝑧) + ( 1 Β· 𝑧)) = (( 1 Β· (𝑋 + π‘Œ)) + ( 1 Β· (𝑋 + π‘Œ))))
5047, 49eqeq12d 2749 . . . . 5 (𝑧 = (𝑋 + π‘Œ) β†’ ((( 1 + 1 ) Β· 𝑧) = (( 1 Β· 𝑧) + ( 1 Β· 𝑧)) ↔ (( 1 + 1 ) Β· (𝑋 + π‘Œ)) = (( 1 Β· (𝑋 + π‘Œ)) + ( 1 Β· (𝑋 + π‘Œ)))))
5142, 46, 50rspc3v 3628 . . . 4 (( 1 ∈ 𝐡 ∧ 1 ∈ 𝐡 ∧ (𝑋 + π‘Œ) ∈ 𝐡) β†’ (βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐡 βˆ€π‘§ ∈ 𝐡 ((π‘₯ + 𝑦) Β· 𝑧) = ((π‘₯ Β· 𝑧) + (𝑦 Β· 𝑧)) β†’ (( 1 + 1 ) Β· (𝑋 + π‘Œ)) = (( 1 Β· (𝑋 + π‘Œ)) + ( 1 Β· (𝑋 + π‘Œ)))))
5237, 38, 51sylc 65 . . 3 (πœ‘ β†’ (( 1 + 1 ) Β· (𝑋 + π‘Œ)) = (( 1 Β· (𝑋 + π‘Œ)) + ( 1 Β· (𝑋 + π‘Œ))))
5330, 52eqtr3d 2775 . 2 (πœ‘ β†’ ((( 1 + 1 ) Β· 𝑋) + (( 1 + 1 ) Β· π‘Œ)) = (( 1 Β· (𝑋 + π‘Œ)) + ( 1 Β· (𝑋 + π‘Œ))))
54 o2timesd.i . . . . 5 (πœ‘ β†’ βˆ€π‘₯ ∈ 𝐡 ( 1 Β· π‘₯) = π‘₯)
5538, 1, 54, 10o2timesd 20033 . . . 4 (πœ‘ β†’ (𝑋 + 𝑋) = (( 1 + 1 ) Β· 𝑋))
5655eqcomd 2739 . . 3 (πœ‘ β†’ (( 1 + 1 ) Β· 𝑋) = (𝑋 + 𝑋))
5738, 1, 54, 11o2timesd 20033 . . . 4 (πœ‘ β†’ (π‘Œ + π‘Œ) = (( 1 + 1 ) Β· π‘Œ))
5857eqcomd 2739 . . 3 (πœ‘ β†’ (( 1 + 1 ) Β· π‘Œ) = (π‘Œ + π‘Œ))
5956, 58oveq12d 7427 . 2 (πœ‘ β†’ ((( 1 + 1 ) Β· 𝑋) + (( 1 + 1 ) Β· π‘Œ)) = ((𝑋 + 𝑋) + (π‘Œ + π‘Œ)))
60 oveq2 7417 . . . . . 6 (π‘₯ = (𝑋 + π‘Œ) β†’ ( 1 Β· π‘₯) = ( 1 Β· (𝑋 + π‘Œ)))
61 id 22 . . . . . 6 (π‘₯ = (𝑋 + π‘Œ) β†’ π‘₯ = (𝑋 + π‘Œ))
6260, 61eqeq12d 2749 . . . . 5 (π‘₯ = (𝑋 + π‘Œ) β†’ (( 1 Β· π‘₯) = π‘₯ ↔ ( 1 Β· (𝑋 + π‘Œ)) = (𝑋 + π‘Œ)))
6362rspcva 3611 . . . 4 (((𝑋 + π‘Œ) ∈ 𝐡 ∧ βˆ€π‘₯ ∈ 𝐡 ( 1 Β· π‘₯) = π‘₯) β†’ ( 1 Β· (𝑋 + π‘Œ)) = (𝑋 + π‘Œ))
6436, 54, 63syl2anc 585 . . 3 (πœ‘ β†’ ( 1 Β· (𝑋 + π‘Œ)) = (𝑋 + π‘Œ))
6564, 64oveq12d 7427 . 2 (πœ‘ β†’ (( 1 Β· (𝑋 + π‘Œ)) + ( 1 Β· (𝑋 + π‘Œ))) = ((𝑋 + π‘Œ) + (𝑋 + π‘Œ)))
6653, 59, 653eqtr3d 2781 1 (πœ‘ β†’ ((𝑋 + 𝑋) + (π‘Œ + π‘Œ)) = ((𝑋 + π‘Œ) + (𝑋 + π‘Œ)))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ∧ wa 397   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107  βˆ€wral 3062  (class class class)co 7409
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3063  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-iota 6496  df-fv 6552  df-ov 7412
This theorem is referenced by:  srgcom4lem  20036  ringcomlem  20096
  Copyright terms: Public domain W3C validator