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

Theorem rglcom4d 19994
Description: Restricted commutativity of the addition in a ring-like structure. This (formerly) part of the proof for ringcom 20056 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 512 . . . . . 6 (𝜑 → ( 1𝐵1𝐵))
3 rglcom4d.a . . . . . 6 (𝜑 → ∀𝑥𝐵𝑦𝐵 (𝑥 + 𝑦) ∈ 𝐵)
4 oveq1 7401 . . . . . . . 8 (𝑥 = 1 → (𝑥 + 𝑦) = ( 1 + 𝑦))
54eleq1d 2818 . . . . . . 7 (𝑥 = 1 → ((𝑥 + 𝑦) ∈ 𝐵 ↔ ( 1 + 𝑦) ∈ 𝐵))
6 oveq2 7402 . . . . . . . 8 (𝑦 = 1 → ( 1 + 𝑦) = ( 1 + 1 ))
76eleq1d 2818 . . . . . . 7 (𝑦 = 1 → (( 1 + 𝑦) ∈ 𝐵 ↔ ( 1 + 1 ) ∈ 𝐵))
85, 7rspc2v 3619 . . . . . 6 (( 1𝐵1𝐵) → (∀𝑥𝐵𝑦𝐵 (𝑥 + 𝑦) ∈ 𝐵 → ( 1 + 1 ) ∈ 𝐵))
92, 3, 8sylc 65 . . . . 5 (𝜑 → ( 1 + 1 ) ∈ 𝐵)
10 o2timesd.x . . . . 5 (𝜑𝑋𝐵)
11 rglcom4d.y . . . . 5 (𝜑𝑌𝐵)
129, 10, 113jca 1128 . . . 4 (𝜑 → (( 1 + 1 ) ∈ 𝐵𝑋𝐵𝑌𝐵))
13 rglcom4d.d . . . 4 (𝜑 → ∀𝑥𝐵𝑦𝐵𝑧𝐵 (𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)))
14 oveq1 7401 . . . . . 6 (𝑥 = ( 1 + 1 ) → (𝑥 · (𝑦 + 𝑧)) = (( 1 + 1 ) · (𝑦 + 𝑧)))
15 oveq1 7401 . . . . . . 7 (𝑥 = ( 1 + 1 ) → (𝑥 · 𝑦) = (( 1 + 1 ) · 𝑦))
16 oveq1 7401 . . . . . . 7 (𝑥 = ( 1 + 1 ) → (𝑥 · 𝑧) = (( 1 + 1 ) · 𝑧))
1715, 16oveq12d 7412 . . . . . 6 (𝑥 = ( 1 + 1 ) → ((𝑥 · 𝑦) + (𝑥 · 𝑧)) = ((( 1 + 1 ) · 𝑦) + (( 1 + 1 ) · 𝑧)))
1814, 17eqeq12d 2748 . . . . 5 (𝑥 = ( 1 + 1 ) → ((𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ↔ (( 1 + 1 ) · (𝑦 + 𝑧)) = ((( 1 + 1 ) · 𝑦) + (( 1 + 1 ) · 𝑧))))
19 oveq1 7401 . . . . . . 7 (𝑦 = 𝑋 → (𝑦 + 𝑧) = (𝑋 + 𝑧))
2019oveq2d 7410 . . . . . 6 (𝑦 = 𝑋 → (( 1 + 1 ) · (𝑦 + 𝑧)) = (( 1 + 1 ) · (𝑋 + 𝑧)))
21 oveq2 7402 . . . . . . 7 (𝑦 = 𝑋 → (( 1 + 1 ) · 𝑦) = (( 1 + 1 ) · 𝑋))
2221oveq1d 7409 . . . . . 6 (𝑦 = 𝑋 → ((( 1 + 1 ) · 𝑦) + (( 1 + 1 ) · 𝑧)) = ((( 1 + 1 ) · 𝑋) + (( 1 + 1 ) · 𝑧)))
2320, 22eqeq12d 2748 . . . . 5 (𝑦 = 𝑋 → ((( 1 + 1 ) · (𝑦 + 𝑧)) = ((( 1 + 1 ) · 𝑦) + (( 1 + 1 ) · 𝑧)) ↔ (( 1 + 1 ) · (𝑋 + 𝑧)) = ((( 1 + 1 ) · 𝑋) + (( 1 + 1 ) · 𝑧))))
24 oveq2 7402 . . . . . . 7 (𝑧 = 𝑌 → (𝑋 + 𝑧) = (𝑋 + 𝑌))
2524oveq2d 7410 . . . . . 6 (𝑧 = 𝑌 → (( 1 + 1 ) · (𝑋 + 𝑧)) = (( 1 + 1 ) · (𝑋 + 𝑌)))
26 oveq2 7402 . . . . . . 7 (𝑧 = 𝑌 → (( 1 + 1 ) · 𝑧) = (( 1 + 1 ) · 𝑌))
2726oveq2d 7410 . . . . . 6 (𝑧 = 𝑌 → ((( 1 + 1 ) · 𝑋) + (( 1 + 1 ) · 𝑧)) = ((( 1 + 1 ) · 𝑋) + (( 1 + 1 ) · 𝑌)))
2825, 27eqeq12d 2748 . . . . 5 (𝑧 = 𝑌 → ((( 1 + 1 ) · (𝑋 + 𝑧)) = ((( 1 + 1 ) · 𝑋) + (( 1 + 1 ) · 𝑧)) ↔ (( 1 + 1 ) · (𝑋 + 𝑌)) = ((( 1 + 1 ) · 𝑋) + (( 1 + 1 ) · 𝑌))))
2918, 23, 28rspc3v 3624 . . . 4 ((( 1 + 1 ) ∈ 𝐵𝑋𝐵𝑌𝐵) → (∀𝑥𝐵𝑦𝐵𝑧𝐵 (𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) → (( 1 + 1 ) · (𝑋 + 𝑌)) = ((( 1 + 1 ) · 𝑋) + (( 1 + 1 ) · 𝑌))))
3012, 13, 29sylc 65 . . 3 (𝜑 → (( 1 + 1 ) · (𝑋 + 𝑌)) = ((( 1 + 1 ) · 𝑋) + (( 1 + 1 ) · 𝑌)))
31 oveq1 7401 . . . . . . . 8 (𝑥 = 𝑋 → (𝑥 + 𝑦) = (𝑋 + 𝑦))
3231eleq1d 2818 . . . . . . 7 (𝑥 = 𝑋 → ((𝑥 + 𝑦) ∈ 𝐵 ↔ (𝑋 + 𝑦) ∈ 𝐵))
33 oveq2 7402 . . . . . . . 8 (𝑦 = 𝑌 → (𝑋 + 𝑦) = (𝑋 + 𝑌))
3433eleq1d 2818 . . . . . . 7 (𝑦 = 𝑌 → ((𝑋 + 𝑦) ∈ 𝐵 ↔ (𝑋 + 𝑌) ∈ 𝐵))
3532, 34rspc2va 3620 . . . . . 6 (((𝑋𝐵𝑌𝐵) ∧ ∀𝑥𝐵𝑦𝐵 (𝑥 + 𝑦) ∈ 𝐵) → (𝑋 + 𝑌) ∈ 𝐵)
3610, 11, 3, 35syl21anc 836 . . . . 5 (𝜑 → (𝑋 + 𝑌) ∈ 𝐵)
371, 1, 363jca 1128 . . . 4 (𝜑 → ( 1𝐵1𝐵 ∧ (𝑋 + 𝑌) ∈ 𝐵))
38 o2timesd.e . . . 4 (𝜑 → ∀𝑥𝐵𝑦𝐵𝑧𝐵 ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧)))
394oveq1d 7409 . . . . . 6 (𝑥 = 1 → ((𝑥 + 𝑦) · 𝑧) = (( 1 + 𝑦) · 𝑧))
40 oveq1 7401 . . . . . . 7 (𝑥 = 1 → (𝑥 · 𝑧) = ( 1 · 𝑧))
4140oveq1d 7409 . . . . . 6 (𝑥 = 1 → ((𝑥 · 𝑧) + (𝑦 · 𝑧)) = (( 1 · 𝑧) + (𝑦 · 𝑧)))
4239, 41eqeq12d 2748 . . . . 5 (𝑥 = 1 → (((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧)) ↔ (( 1 + 𝑦) · 𝑧) = (( 1 · 𝑧) + (𝑦 · 𝑧))))
436oveq1d 7409 . . . . . 6 (𝑦 = 1 → (( 1 + 𝑦) · 𝑧) = (( 1 + 1 ) · 𝑧))
44 oveq1 7401 . . . . . . 7 (𝑦 = 1 → (𝑦 · 𝑧) = ( 1 · 𝑧))
4544oveq2d 7410 . . . . . 6 (𝑦 = 1 → (( 1 · 𝑧) + (𝑦 · 𝑧)) = (( 1 · 𝑧) + ( 1 · 𝑧)))
4643, 45eqeq12d 2748 . . . . 5 (𝑦 = 1 → ((( 1 + 𝑦) · 𝑧) = (( 1 · 𝑧) + (𝑦 · 𝑧)) ↔ (( 1 + 1 ) · 𝑧) = (( 1 · 𝑧) + ( 1 · 𝑧))))
47 oveq2 7402 . . . . . 6 (𝑧 = (𝑋 + 𝑌) → (( 1 + 1 ) · 𝑧) = (( 1 + 1 ) · (𝑋 + 𝑌)))
48 oveq2 7402 . . . . . . 7 (𝑧 = (𝑋 + 𝑌) → ( 1 · 𝑧) = ( 1 · (𝑋 + 𝑌)))
4948, 48oveq12d 7412 . . . . . 6 (𝑧 = (𝑋 + 𝑌) → (( 1 · 𝑧) + ( 1 · 𝑧)) = (( 1 · (𝑋 + 𝑌)) + ( 1 · (𝑋 + 𝑌))))
5047, 49eqeq12d 2748 . . . . 5 (𝑧 = (𝑋 + 𝑌) → ((( 1 + 1 ) · 𝑧) = (( 1 · 𝑧) + ( 1 · 𝑧)) ↔ (( 1 + 1 ) · (𝑋 + 𝑌)) = (( 1 · (𝑋 + 𝑌)) + ( 1 · (𝑋 + 𝑌)))))
5142, 46, 50rspc3v 3624 . . . 4 (( 1𝐵1𝐵 ∧ (𝑋 + 𝑌) ∈ 𝐵) → (∀𝑥𝐵𝑦𝐵𝑧𝐵 ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧)) → (( 1 + 1 ) · (𝑋 + 𝑌)) = (( 1 · (𝑋 + 𝑌)) + ( 1 · (𝑋 + 𝑌)))))
5237, 38, 51sylc 65 . . 3 (𝜑 → (( 1 + 1 ) · (𝑋 + 𝑌)) = (( 1 · (𝑋 + 𝑌)) + ( 1 · (𝑋 + 𝑌))))
5330, 52eqtr3d 2774 . 2 (𝜑 → ((( 1 + 1 ) · 𝑋) + (( 1 + 1 ) · 𝑌)) = (( 1 · (𝑋 + 𝑌)) + ( 1 · (𝑋 + 𝑌))))
54 o2timesd.i . . . . 5 (𝜑 → ∀𝑥𝐵 ( 1 · 𝑥) = 𝑥)
5538, 1, 54, 10o2timesd 19993 . . . 4 (𝜑 → (𝑋 + 𝑋) = (( 1 + 1 ) · 𝑋))
5655eqcomd 2738 . . 3 (𝜑 → (( 1 + 1 ) · 𝑋) = (𝑋 + 𝑋))
5738, 1, 54, 11o2timesd 19993 . . . 4 (𝜑 → (𝑌 + 𝑌) = (( 1 + 1 ) · 𝑌))
5857eqcomd 2738 . . 3 (𝜑 → (( 1 + 1 ) · 𝑌) = (𝑌 + 𝑌))
5956, 58oveq12d 7412 . 2 (𝜑 → ((( 1 + 1 ) · 𝑋) + (( 1 + 1 ) · 𝑌)) = ((𝑋 + 𝑋) + (𝑌 + 𝑌)))
60 oveq2 7402 . . . . . 6 (𝑥 = (𝑋 + 𝑌) → ( 1 · 𝑥) = ( 1 · (𝑋 + 𝑌)))
61 id 22 . . . . . 6 (𝑥 = (𝑋 + 𝑌) → 𝑥 = (𝑋 + 𝑌))
6260, 61eqeq12d 2748 . . . . 5 (𝑥 = (𝑋 + 𝑌) → (( 1 · 𝑥) = 𝑥 ↔ ( 1 · (𝑋 + 𝑌)) = (𝑋 + 𝑌)))
6362rspcva 3608 . . . 4 (((𝑋 + 𝑌) ∈ 𝐵 ∧ ∀𝑥𝐵 ( 1 · 𝑥) = 𝑥) → ( 1 · (𝑋 + 𝑌)) = (𝑋 + 𝑌))
6436, 54, 63syl2anc 584 . . 3 (𝜑 → ( 1 · (𝑋 + 𝑌)) = (𝑋 + 𝑌))
6564, 64oveq12d 7412 . 2 (𝜑 → (( 1 · (𝑋 + 𝑌)) + ( 1 · (𝑋 + 𝑌))) = ((𝑋 + 𝑌) + (𝑋 + 𝑌)))
6653, 59, 653eqtr3d 2780 1 (𝜑 → ((𝑋 + 𝑋) + (𝑌 + 𝑌)) = ((𝑋 + 𝑌) + (𝑋 + 𝑌)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1087   = wceq 1541  wcel 2106  wral 3061  (class class class)co 7394
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ral 3062  df-rab 3433  df-v 3476  df-dif 3948  df-un 3950  df-in 3952  df-ss 3962  df-nul 4320  df-if 4524  df-sn 4624  df-pr 4626  df-op 4630  df-uni 4903  df-br 5143  df-iota 6485  df-fv 6541  df-ov 7397
This theorem is referenced by:  srgcom4lem  19996  ringcomlem  20055
  Copyright terms: Public domain W3C validator