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

Theorem symggrplem 18049
Description: Lemma for symggrp 18528 and efmndsgrp 18051. Conditions for an operation to be associative. Formerly part of proof for symggrp 18528. (Contributed by AV, 28-Jan-2024.)
Hypotheses
Ref Expression
symggrplem.c ((𝑥𝐵𝑦𝐵) → (𝑥 + 𝑦) ∈ 𝐵)
symggrplem.p ((𝑥𝐵𝑦𝐵) → (𝑥 + 𝑦) = (𝑥𝑦))
Assertion
Ref Expression
symggrplem ((𝑋𝐵𝑌𝐵𝑍𝐵) → ((𝑋 + 𝑌) + 𝑍) = (𝑋 + (𝑌 + 𝑍)))
Distinct variable groups:   𝑥,𝐵,𝑦   𝑥,𝑋,𝑦   𝑥,𝑌,𝑦   𝑦,𝑍   𝑥, + ,𝑦
Allowed substitution hint:   𝑍(𝑥)

Proof of Theorem symggrplem
StepHypRef Expression
1 coass 6105 . 2 ((𝑋𝑌) ∘ 𝑍) = (𝑋 ∘ (𝑌𝑍))
2 oveq1 7156 . . . . . 6 (𝑥 = 𝑋 → (𝑥 + 𝑦) = (𝑋 + 𝑦))
32eleq1d 2900 . . . . 5 (𝑥 = 𝑋 → ((𝑥 + 𝑦) ∈ 𝐵 ↔ (𝑋 + 𝑦) ∈ 𝐵))
4 oveq2 7157 . . . . . 6 (𝑦 = 𝑌 → (𝑋 + 𝑦) = (𝑋 + 𝑌))
54eleq1d 2900 . . . . 5 (𝑦 = 𝑌 → ((𝑋 + 𝑦) ∈ 𝐵 ↔ (𝑋 + 𝑌) ∈ 𝐵))
6 symggrplem.c . . . . 5 ((𝑥𝐵𝑦𝐵) → (𝑥 + 𝑦) ∈ 𝐵)
73, 5, 6vtocl2ga 3561 . . . 4 ((𝑋𝐵𝑌𝐵) → (𝑋 + 𝑌) ∈ 𝐵)
8 oveq1 7156 . . . . . 6 (𝑥 = (𝑋 + 𝑌) → (𝑥 + 𝑦) = ((𝑋 + 𝑌) + 𝑦))
9 coeq1 5715 . . . . . 6 (𝑥 = (𝑋 + 𝑌) → (𝑥𝑦) = ((𝑋 + 𝑌) ∘ 𝑦))
108, 9eqeq12d 2840 . . . . 5 (𝑥 = (𝑋 + 𝑌) → ((𝑥 + 𝑦) = (𝑥𝑦) ↔ ((𝑋 + 𝑌) + 𝑦) = ((𝑋 + 𝑌) ∘ 𝑦)))
11 oveq2 7157 . . . . . 6 (𝑦 = 𝑍 → ((𝑋 + 𝑌) + 𝑦) = ((𝑋 + 𝑌) + 𝑍))
12 coeq2 5716 . . . . . 6 (𝑦 = 𝑍 → ((𝑋 + 𝑌) ∘ 𝑦) = ((𝑋 + 𝑌) ∘ 𝑍))
1311, 12eqeq12d 2840 . . . . 5 (𝑦 = 𝑍 → (((𝑋 + 𝑌) + 𝑦) = ((𝑋 + 𝑌) ∘ 𝑦) ↔ ((𝑋 + 𝑌) + 𝑍) = ((𝑋 + 𝑌) ∘ 𝑍)))
14 symggrplem.p . . . . 5 ((𝑥𝐵𝑦𝐵) → (𝑥 + 𝑦) = (𝑥𝑦))
1510, 13, 14vtocl2ga 3561 . . . 4 (((𝑋 + 𝑌) ∈ 𝐵𝑍𝐵) → ((𝑋 + 𝑌) + 𝑍) = ((𝑋 + 𝑌) ∘ 𝑍))
167, 15stoic3 1778 . . 3 ((𝑋𝐵𝑌𝐵𝑍𝐵) → ((𝑋 + 𝑌) + 𝑍) = ((𝑋 + 𝑌) ∘ 𝑍))
17 coeq1 5715 . . . . . . 7 (𝑥 = 𝑋 → (𝑥𝑦) = (𝑋𝑦))
182, 17eqeq12d 2840 . . . . . 6 (𝑥 = 𝑋 → ((𝑥 + 𝑦) = (𝑥𝑦) ↔ (𝑋 + 𝑦) = (𝑋𝑦)))
19 coeq2 5716 . . . . . . 7 (𝑦 = 𝑌 → (𝑋𝑦) = (𝑋𝑌))
204, 19eqeq12d 2840 . . . . . 6 (𝑦 = 𝑌 → ((𝑋 + 𝑦) = (𝑋𝑦) ↔ (𝑋 + 𝑌) = (𝑋𝑌)))
2118, 20, 14vtocl2ga 3561 . . . . 5 ((𝑋𝐵𝑌𝐵) → (𝑋 + 𝑌) = (𝑋𝑌))
22213adant3 1129 . . . 4 ((𝑋𝐵𝑌𝐵𝑍𝐵) → (𝑋 + 𝑌) = (𝑋𝑌))
2322coeq1d 5719 . . 3 ((𝑋𝐵𝑌𝐵𝑍𝐵) → ((𝑋 + 𝑌) ∘ 𝑍) = ((𝑋𝑌) ∘ 𝑍))
2416, 23eqtrd 2859 . 2 ((𝑋𝐵𝑌𝐵𝑍𝐵) → ((𝑋 + 𝑌) + 𝑍) = ((𝑋𝑌) ∘ 𝑍))
25 simp1 1133 . . . 4 ((𝑋𝐵𝑌𝐵𝑍𝐵) → 𝑋𝐵)
26 oveq1 7156 . . . . . . 7 (𝑥 = 𝑌 → (𝑥 + 𝑦) = (𝑌 + 𝑦))
2726eleq1d 2900 . . . . . 6 (𝑥 = 𝑌 → ((𝑥 + 𝑦) ∈ 𝐵 ↔ (𝑌 + 𝑦) ∈ 𝐵))
28 oveq2 7157 . . . . . . 7 (𝑦 = 𝑍 → (𝑌 + 𝑦) = (𝑌 + 𝑍))
2928eleq1d 2900 . . . . . 6 (𝑦 = 𝑍 → ((𝑌 + 𝑦) ∈ 𝐵 ↔ (𝑌 + 𝑍) ∈ 𝐵))
3027, 29, 6vtocl2ga 3561 . . . . 5 ((𝑌𝐵𝑍𝐵) → (𝑌 + 𝑍) ∈ 𝐵)
31303adant1 1127 . . . 4 ((𝑋𝐵𝑌𝐵𝑍𝐵) → (𝑌 + 𝑍) ∈ 𝐵)
32 oveq2 7157 . . . . . 6 (𝑦 = (𝑌 + 𝑍) → (𝑋 + 𝑦) = (𝑋 + (𝑌 + 𝑍)))
33 coeq2 5716 . . . . . 6 (𝑦 = (𝑌 + 𝑍) → (𝑋𝑦) = (𝑋 ∘ (𝑌 + 𝑍)))
3432, 33eqeq12d 2840 . . . . 5 (𝑦 = (𝑌 + 𝑍) → ((𝑋 + 𝑦) = (𝑋𝑦) ↔ (𝑋 + (𝑌 + 𝑍)) = (𝑋 ∘ (𝑌 + 𝑍))))
3518, 34, 14vtocl2ga 3561 . . . 4 ((𝑋𝐵 ∧ (𝑌 + 𝑍) ∈ 𝐵) → (𝑋 + (𝑌 + 𝑍)) = (𝑋 ∘ (𝑌 + 𝑍)))
3625, 31, 35syl2anc 587 . . 3 ((𝑋𝐵𝑌𝐵𝑍𝐵) → (𝑋 + (𝑌 + 𝑍)) = (𝑋 ∘ (𝑌 + 𝑍)))
37 coeq1 5715 . . . . . . 7 (𝑥 = 𝑌 → (𝑥𝑦) = (𝑌𝑦))
3826, 37eqeq12d 2840 . . . . . 6 (𝑥 = 𝑌 → ((𝑥 + 𝑦) = (𝑥𝑦) ↔ (𝑌 + 𝑦) = (𝑌𝑦)))
39 coeq2 5716 . . . . . . 7 (𝑦 = 𝑍 → (𝑌𝑦) = (𝑌𝑍))
4028, 39eqeq12d 2840 . . . . . 6 (𝑦 = 𝑍 → ((𝑌 + 𝑦) = (𝑌𝑦) ↔ (𝑌 + 𝑍) = (𝑌𝑍)))
4138, 40, 14vtocl2ga 3561 . . . . 5 ((𝑌𝐵𝑍𝐵) → (𝑌 + 𝑍) = (𝑌𝑍))
42413adant1 1127 . . . 4 ((𝑋𝐵𝑌𝐵𝑍𝐵) → (𝑌 + 𝑍) = (𝑌𝑍))
4342coeq2d 5720 . . 3 ((𝑋𝐵𝑌𝐵𝑍𝐵) → (𝑋 ∘ (𝑌 + 𝑍)) = (𝑋 ∘ (𝑌𝑍)))
4436, 43eqtrd 2859 . 2 ((𝑋𝐵𝑌𝐵𝑍𝐵) → (𝑋 + (𝑌 + 𝑍)) = (𝑋 ∘ (𝑌𝑍)))
451, 24, 443eqtr4a 2885 1 ((𝑋𝐵𝑌𝐵𝑍𝐵) → ((𝑋 + 𝑌) + 𝑍) = (𝑋 + (𝑌 + 𝑍)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  w3a 1084   = wceq 1538  wcel 2115  ccom 5546  (class class class)co 7149
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 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-sep 5189  ax-nul 5196  ax-pr 5317
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-v 3482  df-dif 3922  df-un 3924  df-in 3926  df-ss 3936  df-nul 4277  df-if 4451  df-sn 4551  df-pr 4553  df-op 4557  df-uni 4825  df-br 5053  df-opab 5115  df-xp 5548  df-rel 5549  df-co 5551  df-iota 6302  df-fv 6351  df-ov 7152
This theorem is referenced by:  efmndsgrp  18051  smndex1sgrp  18073  symggrp  18528
  Copyright terms: Public domain W3C validator