Theorem symggrplem 18438

Description: Lemma for symggrp 18923 and efmndsgrp 18440. Conditions for an operation to be associative. Formerly part of proof for symggrp 18923. (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

Step	Hyp	Ref	Expression
1		coass 6158	. 2 ⊢ ((𝑋 ∘ 𝑌) ∘ 𝑍) = (𝑋 ∘ (𝑌 ∘ 𝑍))
2		oveq1 7262	. . . . . 6 ⊢ (𝑥 = 𝑋 → (𝑥 + 𝑦) = (𝑋 + 𝑦))
3	2	eleq1d 2823	. . . . 5 ⊢ (𝑥 = 𝑋 → ((𝑥 + 𝑦) ∈ 𝐵 ↔ (𝑋 + 𝑦) ∈ 𝐵))
4		oveq2 7263	. . . . . 6 ⊢ (𝑦 = 𝑌 → (𝑋 + 𝑦) = (𝑋 + 𝑌))
5	4	eleq1d 2823	. . . . 5 ⊢ (𝑦 = 𝑌 → ((𝑋 + 𝑦) ∈ 𝐵 ↔ (𝑋 + 𝑌) ∈ 𝐵))
6		symggrplem.c	. . . . 5 ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) ∈ 𝐵)
7	3, 5, 6	vtocl2ga 3504	. . . 4 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) ∈ 𝐵)
8		oveq1 7262	. . . . . 6 ⊢ (𝑥 = (𝑋 + 𝑌) → (𝑥 + 𝑦) = ((𝑋 + 𝑌) + 𝑦))
9		coeq1 5755	. . . . . 6 ⊢ (𝑥 = (𝑋 + 𝑌) → (𝑥 ∘ 𝑦) = ((𝑋 + 𝑌) ∘ 𝑦))
10	8, 9	eqeq12d 2754	. . . . 5 ⊢ (𝑥 = (𝑋 + 𝑌) → ((𝑥 + 𝑦) = (𝑥 ∘ 𝑦) ↔ ((𝑋 + 𝑌) + 𝑦) = ((𝑋 + 𝑌) ∘ 𝑦)))
11		oveq2 7263	. . . . . 6 ⊢ (𝑦 = 𝑍 → ((𝑋 + 𝑌) + 𝑦) = ((𝑋 + 𝑌) + 𝑍))
12		coeq2 5756	. . . . . 6 ⊢ (𝑦 = 𝑍 → ((𝑋 + 𝑌) ∘ 𝑦) = ((𝑋 + 𝑌) ∘ 𝑍))
13	11, 12	eqeq12d 2754	. . . . 5 ⊢ (𝑦 = 𝑍 → (((𝑋 + 𝑌) + 𝑦) = ((𝑋 + 𝑌) ∘ 𝑦) ↔ ((𝑋 + 𝑌) + 𝑍) = ((𝑋 + 𝑌) ∘ 𝑍)))
14		symggrplem.p	. . . . 5 ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) = (𝑥 ∘ 𝑦))
15	10, 13, 14	vtocl2ga 3504	. . . 4 ⊢ (((𝑋 + 𝑌) ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → ((𝑋 + 𝑌) + 𝑍) = ((𝑋 + 𝑌) ∘ 𝑍))
16	7, 15	stoic3 1780	. . 3 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → ((𝑋 + 𝑌) + 𝑍) = ((𝑋 + 𝑌) ∘ 𝑍))
17		coeq1 5755	. . . . . . 7 ⊢ (𝑥 = 𝑋 → (𝑥 ∘ 𝑦) = (𝑋 ∘ 𝑦))
18	2, 17	eqeq12d 2754	. . . . . 6 ⊢ (𝑥 = 𝑋 → ((𝑥 + 𝑦) = (𝑥 ∘ 𝑦) ↔ (𝑋 + 𝑦) = (𝑋 ∘ 𝑦)))
19		coeq2 5756	. . . . . . 7 ⊢ (𝑦 = 𝑌 → (𝑋 ∘ 𝑦) = (𝑋 ∘ 𝑌))
20	4, 19	eqeq12d 2754	. . . . . 6 ⊢ (𝑦 = 𝑌 → ((𝑋 + 𝑦) = (𝑋 ∘ 𝑦) ↔ (𝑋 + 𝑌) = (𝑋 ∘ 𝑌)))
21	18, 20, 14	vtocl2ga 3504	. . . . 5 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) = (𝑋 ∘ 𝑌))
22	21	3adant3 1130	. . . 4 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → (𝑋 + 𝑌) = (𝑋 ∘ 𝑌))
23	22	coeq1d 5759	. . 3 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → ((𝑋 + 𝑌) ∘ 𝑍) = ((𝑋 ∘ 𝑌) ∘ 𝑍))
24	16, 23	eqtrd 2778	. 2 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → ((𝑋 + 𝑌) + 𝑍) = ((𝑋 ∘ 𝑌) ∘ 𝑍))
25		simp1 1134	. . . 4 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → 𝑋 ∈ 𝐵)
26		oveq1 7262	. . . . . . 7 ⊢ (𝑥 = 𝑌 → (𝑥 + 𝑦) = (𝑌 + 𝑦))
27	26	eleq1d 2823	. . . . . 6 ⊢ (𝑥 = 𝑌 → ((𝑥 + 𝑦) ∈ 𝐵 ↔ (𝑌 + 𝑦) ∈ 𝐵))
28		oveq2 7263	. . . . . . 7 ⊢ (𝑦 = 𝑍 → (𝑌 + 𝑦) = (𝑌 + 𝑍))
29	28	eleq1d 2823	. . . . . 6 ⊢ (𝑦 = 𝑍 → ((𝑌 + 𝑦) ∈ 𝐵 ↔ (𝑌 + 𝑍) ∈ 𝐵))
30	27, 29, 6	vtocl2ga 3504	. . . . 5 ⊢ ((𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → (𝑌 + 𝑍) ∈ 𝐵)
31	30	3adant1 1128	. . . 4 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → (𝑌 + 𝑍) ∈ 𝐵)
32		oveq2 7263	. . . . . 6 ⊢ (𝑦 = (𝑌 + 𝑍) → (𝑋 + 𝑦) = (𝑋 + (𝑌 + 𝑍)))
33		coeq2 5756	. . . . . 6 ⊢ (𝑦 = (𝑌 + 𝑍) → (𝑋 ∘ 𝑦) = (𝑋 ∘ (𝑌 + 𝑍)))
34	32, 33	eqeq12d 2754	. . . . 5 ⊢ (𝑦 = (𝑌 + 𝑍) → ((𝑋 + 𝑦) = (𝑋 ∘ 𝑦) ↔ (𝑋 + (𝑌 + 𝑍)) = (𝑋 ∘ (𝑌 + 𝑍))))
35	18, 34, 14	vtocl2ga 3504	. . . 4 ⊢ ((𝑋 ∈ 𝐵 ∧ (𝑌 + 𝑍) ∈ 𝐵) → (𝑋 + (𝑌 + 𝑍)) = (𝑋 ∘ (𝑌 + 𝑍)))
36	25, 31, 35	syl2anc 583	. . 3 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → (𝑋 + (𝑌 + 𝑍)) = (𝑋 ∘ (𝑌 + 𝑍)))
37		coeq1 5755	. . . . . . 7 ⊢ (𝑥 = 𝑌 → (𝑥 ∘ 𝑦) = (𝑌 ∘ 𝑦))
38	26, 37	eqeq12d 2754	. . . . . 6 ⊢ (𝑥 = 𝑌 → ((𝑥 + 𝑦) = (𝑥 ∘ 𝑦) ↔ (𝑌 + 𝑦) = (𝑌 ∘ 𝑦)))
39		coeq2 5756	. . . . . . 7 ⊢ (𝑦 = 𝑍 → (𝑌 ∘ 𝑦) = (𝑌 ∘ 𝑍))
40	28, 39	eqeq12d 2754	. . . . . 6 ⊢ (𝑦 = 𝑍 → ((𝑌 + 𝑦) = (𝑌 ∘ 𝑦) ↔ (𝑌 + 𝑍) = (𝑌 ∘ 𝑍)))
41	38, 40, 14	vtocl2ga 3504	. . . . 5 ⊢ ((𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → (𝑌 + 𝑍) = (𝑌 ∘ 𝑍))
42	41	3adant1 1128	. . . 4 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → (𝑌 + 𝑍) = (𝑌 ∘ 𝑍))
43	42	coeq2d 5760	. . 3 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → (𝑋 ∘ (𝑌 + 𝑍)) = (𝑋 ∘ (𝑌 ∘ 𝑍)))
44	36, 43	eqtrd 2778	. 2 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → (𝑋 + (𝑌 + 𝑍)) = (𝑋 ∘ (𝑌 ∘ 𝑍)))
45	1, 24, 44	3eqtr4a 2805	1 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → ((𝑋 + 𝑌) + 𝑍) = (𝑋 + (𝑌 + 𝑍)))

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1085   = wceq 1539   ∈ wcel 2108   ∘ ccom 5584  (class class class)co 7255

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-xp 5586  df-rel 5587  df-co 5589  df-iota 6376  df-fv 6426  df-ov 7258

This theorem is referenced by:  efmndsgrp  18440  smndex1sgrp  18462  symggrp  18923