Theorem symggrplem 18847

Description: Lemma for symggrp 19370 and efmndsgrp 18849. Conditions for an operation to be associative. Formerly part of proof for symggrp 19370. (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 6221	. 2 ⊢ ((𝑋 ∘ 𝑌) ∘ 𝑍) = (𝑋 ∘ (𝑌 ∘ 𝑍))
2		oveq1 7367	. . . . . 6 ⊢ (𝑥 = 𝑋 → (𝑥 + 𝑦) = (𝑋 + 𝑦))
3	2	eleq1d 2826	. . . . 5 ⊢ (𝑥 = 𝑋 → ((𝑥 + 𝑦) ∈ 𝐵 ↔ (𝑋 + 𝑦) ∈ 𝐵))
4		oveq2 7368	. . . . . 6 ⊢ (𝑦 = 𝑌 → (𝑋 + 𝑦) = (𝑋 + 𝑌))
5	4	eleq1d 2826	. . . . 5 ⊢ (𝑦 = 𝑌 → ((𝑋 + 𝑦) ∈ 𝐵 ↔ (𝑋 + 𝑌) ∈ 𝐵))
6		symggrplem.c	. . . . 5 ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) ∈ 𝐵)
7	3, 5, 6	vtocl2ga 3523	. . . 4 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) ∈ 𝐵)
8		oveq1 7367	. . . . . 6 ⊢ (𝑥 = (𝑋 + 𝑌) → (𝑥 + 𝑦) = ((𝑋 + 𝑌) + 𝑦))
9		coeq1 5802	. . . . . 6 ⊢ (𝑥 = (𝑋 + 𝑌) → (𝑥 ∘ 𝑦) = ((𝑋 + 𝑌) ∘ 𝑦))
10	8, 9	eqeq12d 2757	. . . . 5 ⊢ (𝑥 = (𝑋 + 𝑌) → ((𝑥 + 𝑦) = (𝑥 ∘ 𝑦) ↔ ((𝑋 + 𝑌) + 𝑦) = ((𝑋 + 𝑌) ∘ 𝑦)))
11		oveq2 7368	. . . . . 6 ⊢ (𝑦 = 𝑍 → ((𝑋 + 𝑌) + 𝑦) = ((𝑋 + 𝑌) + 𝑍))
12		coeq2 5803	. . . . . 6 ⊢ (𝑦 = 𝑍 → ((𝑋 + 𝑌) ∘ 𝑦) = ((𝑋 + 𝑌) ∘ 𝑍))
13	11, 12	eqeq12d 2757	. . . . 5 ⊢ (𝑦 = 𝑍 → (((𝑋 + 𝑌) + 𝑦) = ((𝑋 + 𝑌) ∘ 𝑦) ↔ ((𝑋 + 𝑌) + 𝑍) = ((𝑋 + 𝑌) ∘ 𝑍)))
14		symggrplem.p	. . . . 5 ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) = (𝑥 ∘ 𝑦))
15	10, 13, 14	vtocl2ga 3523	. . . 4 ⊢ (((𝑋 + 𝑌) ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → ((𝑋 + 𝑌) + 𝑍) = ((𝑋 + 𝑌) ∘ 𝑍))
16	7, 15	stoic3 1784	. . 3 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → ((𝑋 + 𝑌) + 𝑍) = ((𝑋 + 𝑌) ∘ 𝑍))
17		coeq1 5802	. . . . . . 7 ⊢ (𝑥 = 𝑋 → (𝑥 ∘ 𝑦) = (𝑋 ∘ 𝑦))
18	2, 17	eqeq12d 2757	. . . . . 6 ⊢ (𝑥 = 𝑋 → ((𝑥 + 𝑦) = (𝑥 ∘ 𝑦) ↔ (𝑋 + 𝑦) = (𝑋 ∘ 𝑦)))
19		coeq2 5803	. . . . . . 7 ⊢ (𝑦 = 𝑌 → (𝑋 ∘ 𝑦) = (𝑋 ∘ 𝑌))
20	4, 19	eqeq12d 2757	. . . . . 6 ⊢ (𝑦 = 𝑌 → ((𝑋 + 𝑦) = (𝑋 ∘ 𝑦) ↔ (𝑋 + 𝑌) = (𝑋 ∘ 𝑌)))
21	18, 20, 14	vtocl2ga 3523	. . . . 5 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) = (𝑋 ∘ 𝑌))
22	21	3adant3 1139	. . . 4 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → (𝑋 + 𝑌) = (𝑋 ∘ 𝑌))
23	22	coeq1d 5806	. . 3 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → ((𝑋 + 𝑌) ∘ 𝑍) = ((𝑋 ∘ 𝑌) ∘ 𝑍))
24	16, 23	eqtrd 2776	. 2 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → ((𝑋 + 𝑌) + 𝑍) = ((𝑋 ∘ 𝑌) ∘ 𝑍))
25		simp1 1143	. . . 4 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → 𝑋 ∈ 𝐵)
26		oveq1 7367	. . . . . . 7 ⊢ (𝑥 = 𝑌 → (𝑥 + 𝑦) = (𝑌 + 𝑦))
27	26	eleq1d 2826	. . . . . 6 ⊢ (𝑥 = 𝑌 → ((𝑥 + 𝑦) ∈ 𝐵 ↔ (𝑌 + 𝑦) ∈ 𝐵))
28		oveq2 7368	. . . . . . 7 ⊢ (𝑦 = 𝑍 → (𝑌 + 𝑦) = (𝑌 + 𝑍))
29	28	eleq1d 2826	. . . . . 6 ⊢ (𝑦 = 𝑍 → ((𝑌 + 𝑦) ∈ 𝐵 ↔ (𝑌 + 𝑍) ∈ 𝐵))
30	27, 29, 6	vtocl2ga 3523	. . . . 5 ⊢ ((𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → (𝑌 + 𝑍) ∈ 𝐵)
31	30	3adant1 1137	. . . 4 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → (𝑌 + 𝑍) ∈ 𝐵)
32		oveq2 7368	. . . . . 6 ⊢ (𝑦 = (𝑌 + 𝑍) → (𝑋 + 𝑦) = (𝑋 + (𝑌 + 𝑍)))
33		coeq2 5803	. . . . . 6 ⊢ (𝑦 = (𝑌 + 𝑍) → (𝑋 ∘ 𝑦) = (𝑋 ∘ (𝑌 + 𝑍)))
34	32, 33	eqeq12d 2757	. . . . 5 ⊢ (𝑦 = (𝑌 + 𝑍) → ((𝑋 + 𝑦) = (𝑋 ∘ 𝑦) ↔ (𝑋 + (𝑌 + 𝑍)) = (𝑋 ∘ (𝑌 + 𝑍))))
35	18, 34, 14	vtocl2ga 3523	. . . 4 ⊢ ((𝑋 ∈ 𝐵 ∧ (𝑌 + 𝑍) ∈ 𝐵) → (𝑋 + (𝑌 + 𝑍)) = (𝑋 ∘ (𝑌 + 𝑍)))
36	25, 31, 35	syl2anc 591	. . 3 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → (𝑋 + (𝑌 + 𝑍)) = (𝑋 ∘ (𝑌 + 𝑍)))
37		coeq1 5802	. . . . . . 7 ⊢ (𝑥 = 𝑌 → (𝑥 ∘ 𝑦) = (𝑌 ∘ 𝑦))
38	26, 37	eqeq12d 2757	. . . . . 6 ⊢ (𝑥 = 𝑌 → ((𝑥 + 𝑦) = (𝑥 ∘ 𝑦) ↔ (𝑌 + 𝑦) = (𝑌 ∘ 𝑦)))
39		coeq2 5803	. . . . . . 7 ⊢ (𝑦 = 𝑍 → (𝑌 ∘ 𝑦) = (𝑌 ∘ 𝑍))
40	28, 39	eqeq12d 2757	. . . . . 6 ⊢ (𝑦 = 𝑍 → ((𝑌 + 𝑦) = (𝑌 ∘ 𝑦) ↔ (𝑌 + 𝑍) = (𝑌 ∘ 𝑍)))
41	38, 40, 14	vtocl2ga 3523	. . . . 5 ⊢ ((𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → (𝑌 + 𝑍) = (𝑌 ∘ 𝑍))
42	41	3adant1 1137	. . . 4 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → (𝑌 + 𝑍) = (𝑌 ∘ 𝑍))
43	42	coeq2d 5807	. . 3 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → (𝑋 ∘ (𝑌 + 𝑍)) = (𝑋 ∘ (𝑌 ∘ 𝑍)))
44	36, 43	eqtrd 2776	. 2 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → (𝑋 + (𝑌 + 𝑍)) = (𝑋 ∘ (𝑌 ∘ 𝑍)))
45	1, 24, 44	3eqtr4a 2802	1 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → ((𝑋 + 𝑌) + 𝑍) = (𝑋 + (𝑌 + 𝑍)))

Syntax hints:   → wi 4   ∧ wa 397   ∧ w3a 1093   = wceq 1548   ∈ wcel 2121   ∘ ccom 5625  (class class class)co 7360

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-11 2170  ax-ext 2713  ax-sep 5221  ax-pr 5365

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-rab 3394  df-v 3435  df-dif 3888  df-un 3890  df-in 3892  df-ss 3902  df-nul 4265  df-if 4458  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4842  df-br 5076  df-opab 5138  df-xp 5627  df-rel 5628  df-co 5630  df-iota 6445  df-fv 6497  df-ov 7363

This theorem is referenced by:  efmndsgrp  18849  smndex1sgrp  18874  symggrp  19370