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

Theorem symggrplem 18695
Description: Lemma for symggrp 19183 and efmndsgrp 18697. Conditions for an operation to be associative. Formerly part of proof for symggrp 19183. (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 6218 . 2 ((𝑋𝑌) ∘ 𝑍) = (𝑋 ∘ (𝑌𝑍))
2 oveq1 7365 . . . . . 6 (𝑥 = 𝑋 → (𝑥 + 𝑦) = (𝑋 + 𝑦))
32eleq1d 2823 . . . . 5 (𝑥 = 𝑋 → ((𝑥 + 𝑦) ∈ 𝐵 ↔ (𝑋 + 𝑦) ∈ 𝐵))
4 oveq2 7366 . . . . . 6 (𝑦 = 𝑌 → (𝑋 + 𝑦) = (𝑋 + 𝑌))
54eleq1d 2823 . . . . 5 (𝑦 = 𝑌 → ((𝑋 + 𝑦) ∈ 𝐵 ↔ (𝑋 + 𝑌) ∈ 𝐵))
6 symggrplem.c . . . . 5 ((𝑥𝐵𝑦𝐵) → (𝑥 + 𝑦) ∈ 𝐵)
73, 5, 6vtocl2ga 3536 . . . 4 ((𝑋𝐵𝑌𝐵) → (𝑋 + 𝑌) ∈ 𝐵)
8 oveq1 7365 . . . . . 6 (𝑥 = (𝑋 + 𝑌) → (𝑥 + 𝑦) = ((𝑋 + 𝑌) + 𝑦))
9 coeq1 5814 . . . . . 6 (𝑥 = (𝑋 + 𝑌) → (𝑥𝑦) = ((𝑋 + 𝑌) ∘ 𝑦))
108, 9eqeq12d 2753 . . . . 5 (𝑥 = (𝑋 + 𝑌) → ((𝑥 + 𝑦) = (𝑥𝑦) ↔ ((𝑋 + 𝑌) + 𝑦) = ((𝑋 + 𝑌) ∘ 𝑦)))
11 oveq2 7366 . . . . . 6 (𝑦 = 𝑍 → ((𝑋 + 𝑌) + 𝑦) = ((𝑋 + 𝑌) + 𝑍))
12 coeq2 5815 . . . . . 6 (𝑦 = 𝑍 → ((𝑋 + 𝑌) ∘ 𝑦) = ((𝑋 + 𝑌) ∘ 𝑍))
1311, 12eqeq12d 2753 . . . . 5 (𝑦 = 𝑍 → (((𝑋 + 𝑌) + 𝑦) = ((𝑋 + 𝑌) ∘ 𝑦) ↔ ((𝑋 + 𝑌) + 𝑍) = ((𝑋 + 𝑌) ∘ 𝑍)))
14 symggrplem.p . . . . 5 ((𝑥𝐵𝑦𝐵) → (𝑥 + 𝑦) = (𝑥𝑦))
1510, 13, 14vtocl2ga 3536 . . . 4 (((𝑋 + 𝑌) ∈ 𝐵𝑍𝐵) → ((𝑋 + 𝑌) + 𝑍) = ((𝑋 + 𝑌) ∘ 𝑍))
167, 15stoic3 1779 . . 3 ((𝑋𝐵𝑌𝐵𝑍𝐵) → ((𝑋 + 𝑌) + 𝑍) = ((𝑋 + 𝑌) ∘ 𝑍))
17 coeq1 5814 . . . . . . 7 (𝑥 = 𝑋 → (𝑥𝑦) = (𝑋𝑦))
182, 17eqeq12d 2753 . . . . . 6 (𝑥 = 𝑋 → ((𝑥 + 𝑦) = (𝑥𝑦) ↔ (𝑋 + 𝑦) = (𝑋𝑦)))
19 coeq2 5815 . . . . . . 7 (𝑦 = 𝑌 → (𝑋𝑦) = (𝑋𝑌))
204, 19eqeq12d 2753 . . . . . 6 (𝑦 = 𝑌 → ((𝑋 + 𝑦) = (𝑋𝑦) ↔ (𝑋 + 𝑌) = (𝑋𝑌)))
2118, 20, 14vtocl2ga 3536 . . . . 5 ((𝑋𝐵𝑌𝐵) → (𝑋 + 𝑌) = (𝑋𝑌))
22213adant3 1133 . . . 4 ((𝑋𝐵𝑌𝐵𝑍𝐵) → (𝑋 + 𝑌) = (𝑋𝑌))
2322coeq1d 5818 . . 3 ((𝑋𝐵𝑌𝐵𝑍𝐵) → ((𝑋 + 𝑌) ∘ 𝑍) = ((𝑋𝑌) ∘ 𝑍))
2416, 23eqtrd 2777 . 2 ((𝑋𝐵𝑌𝐵𝑍𝐵) → ((𝑋 + 𝑌) + 𝑍) = ((𝑋𝑌) ∘ 𝑍))
25 simp1 1137 . . . 4 ((𝑋𝐵𝑌𝐵𝑍𝐵) → 𝑋𝐵)
26 oveq1 7365 . . . . . . 7 (𝑥 = 𝑌 → (𝑥 + 𝑦) = (𝑌 + 𝑦))
2726eleq1d 2823 . . . . . 6 (𝑥 = 𝑌 → ((𝑥 + 𝑦) ∈ 𝐵 ↔ (𝑌 + 𝑦) ∈ 𝐵))
28 oveq2 7366 . . . . . . 7 (𝑦 = 𝑍 → (𝑌 + 𝑦) = (𝑌 + 𝑍))
2928eleq1d 2823 . . . . . 6 (𝑦 = 𝑍 → ((𝑌 + 𝑦) ∈ 𝐵 ↔ (𝑌 + 𝑍) ∈ 𝐵))
3027, 29, 6vtocl2ga 3536 . . . . 5 ((𝑌𝐵𝑍𝐵) → (𝑌 + 𝑍) ∈ 𝐵)
31303adant1 1131 . . . 4 ((𝑋𝐵𝑌𝐵𝑍𝐵) → (𝑌 + 𝑍) ∈ 𝐵)
32 oveq2 7366 . . . . . 6 (𝑦 = (𝑌 + 𝑍) → (𝑋 + 𝑦) = (𝑋 + (𝑌 + 𝑍)))
33 coeq2 5815 . . . . . 6 (𝑦 = (𝑌 + 𝑍) → (𝑋𝑦) = (𝑋 ∘ (𝑌 + 𝑍)))
3432, 33eqeq12d 2753 . . . . 5 (𝑦 = (𝑌 + 𝑍) → ((𝑋 + 𝑦) = (𝑋𝑦) ↔ (𝑋 + (𝑌 + 𝑍)) = (𝑋 ∘ (𝑌 + 𝑍))))
3518, 34, 14vtocl2ga 3536 . . . 4 ((𝑋𝐵 ∧ (𝑌 + 𝑍) ∈ 𝐵) → (𝑋 + (𝑌 + 𝑍)) = (𝑋 ∘ (𝑌 + 𝑍)))
3625, 31, 35syl2anc 585 . . 3 ((𝑋𝐵𝑌𝐵𝑍𝐵) → (𝑋 + (𝑌 + 𝑍)) = (𝑋 ∘ (𝑌 + 𝑍)))
37 coeq1 5814 . . . . . . 7 (𝑥 = 𝑌 → (𝑥𝑦) = (𝑌𝑦))
3826, 37eqeq12d 2753 . . . . . 6 (𝑥 = 𝑌 → ((𝑥 + 𝑦) = (𝑥𝑦) ↔ (𝑌 + 𝑦) = (𝑌𝑦)))
39 coeq2 5815 . . . . . . 7 (𝑦 = 𝑍 → (𝑌𝑦) = (𝑌𝑍))
4028, 39eqeq12d 2753 . . . . . 6 (𝑦 = 𝑍 → ((𝑌 + 𝑦) = (𝑌𝑦) ↔ (𝑌 + 𝑍) = (𝑌𝑍)))
4138, 40, 14vtocl2ga 3536 . . . . 5 ((𝑌𝐵𝑍𝐵) → (𝑌 + 𝑍) = (𝑌𝑍))
42413adant1 1131 . . . 4 ((𝑋𝐵𝑌𝐵𝑍𝐵) → (𝑌 + 𝑍) = (𝑌𝑍))
4342coeq2d 5819 . . 3 ((𝑋𝐵𝑌𝐵𝑍𝐵) → (𝑋 ∘ (𝑌 + 𝑍)) = (𝑋 ∘ (𝑌𝑍)))
4436, 43eqtrd 2777 . 2 ((𝑋𝐵𝑌𝐵𝑍𝐵) → (𝑋 + (𝑌 + 𝑍)) = (𝑋 ∘ (𝑌𝑍)))
451, 24, 443eqtr4a 2803 1 ((𝑋𝐵𝑌𝐵𝑍𝐵) → ((𝑋 + 𝑌) + 𝑍) = (𝑋 + (𝑌 + 𝑍)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  w3a 1088   = wceq 1542  wcel 2107  ccom 5638  (class class class)co 7358
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-11 2155  ax-ext 2708  ax-sep 5257  ax-nul 5264  ax-pr 5385
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 2715  df-cleq 2729  df-clel 2815  df-rab 3409  df-v 3448  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-br 5107  df-opab 5169  df-xp 5640  df-rel 5641  df-co 5643  df-iota 6449  df-fv 6505  df-ov 7361
This theorem is referenced by:  efmndsgrp  18697  smndex1sgrp  18719  symggrp  19183
  Copyright terms: Public domain W3C validator