Theorem symggrplem 19106

Description: Lemma for symggrp 19641 and efmndsgrp 19108. Conditions for an operation to be associative. Formerly part of proof for symggrp 19641. (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 6281	. 2 ⊢ ((𝑋 ∘ 𝑌) ∘ 𝑍) = (𝑋 ∘ (𝑌 ∘ 𝑍))
2		oveq1 7447	. . . . . 6 ⊢ (𝑥 = 𝑋 → (𝑥 + 𝑦) = (𝑋 + 𝑦))
3	2	eleq1d 2849	. . . . 5 ⊢ (𝑥 = 𝑋 → ((𝑥 + 𝑦) ∈ 𝐵 ↔ (𝑋 + 𝑦) ∈ 𝐵))
4		oveq2 7448	. . . . . 6 ⊢ (𝑦 = 𝑌 → (𝑋 + 𝑦) = (𝑋 + 𝑌))
5	4	eleq1d 2849	. . . . 5 ⊢ (𝑦 = 𝑌 → ((𝑋 + 𝑦) ∈ 𝐵 ↔ (𝑋 + 𝑌) ∈ 𝐵))
6		symggrplem.c	. . . . 5 ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) ∈ 𝐵)
7	3, 5, 6	vtocl2ga 3541	. . . 4 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) ∈ 𝐵)
8		oveq1 7447	. . . . . 6 ⊢ (𝑥 = (𝑋 + 𝑌) → (𝑥 + 𝑦) = ((𝑋 + 𝑌) + 𝑦))
9		coeq1 5840	. . . . . 6 ⊢ (𝑥 = (𝑋 + 𝑌) → (𝑥 ∘ 𝑦) = ((𝑋 + 𝑌) ∘ 𝑦))
10	8, 9	eqeq12d 2779	. . . . 5 ⊢ (𝑥 = (𝑋 + 𝑌) → ((𝑥 + 𝑦) = (𝑥 ∘ 𝑦) ↔ ((𝑋 + 𝑌) + 𝑦) = ((𝑋 + 𝑌) ∘ 𝑦)))
11		oveq2 7448	. . . . . 6 ⊢ (𝑦 = 𝑍 → ((𝑋 + 𝑌) + 𝑦) = ((𝑋 + 𝑌) + 𝑍))
12		coeq2 5841	. . . . . 6 ⊢ (𝑦 = 𝑍 → ((𝑋 + 𝑌) ∘ 𝑦) = ((𝑋 + 𝑌) ∘ 𝑍))
13	11, 12	eqeq12d 2779	. . . . 5 ⊢ (𝑦 = 𝑍 → (((𝑋 + 𝑌) + 𝑦) = ((𝑋 + 𝑌) ∘ 𝑦) ↔ ((𝑋 + 𝑌) + 𝑍) = ((𝑋 + 𝑌) ∘ 𝑍)))
14		symggrplem.p	. . . . 5 ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) = (𝑥 ∘ 𝑦))
15	10, 13, 14	vtocl2ga 3541	. . . 4 ⊢ (((𝑋 + 𝑌) ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → ((𝑋 + 𝑌) + 𝑍) = ((𝑋 + 𝑌) ∘ 𝑍))
16	7, 15	stoic3 1809	. . 3 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → ((𝑋 + 𝑌) + 𝑍) = ((𝑋 + 𝑌) ∘ 𝑍))
17		coeq1 5840	. . . . . . 7 ⊢ (𝑥 = 𝑋 → (𝑥 ∘ 𝑦) = (𝑋 ∘ 𝑦))
18	2, 17	eqeq12d 2779	. . . . . 6 ⊢ (𝑥 = 𝑋 → ((𝑥 + 𝑦) = (𝑥 ∘ 𝑦) ↔ (𝑋 + 𝑦) = (𝑋 ∘ 𝑦)))
19		coeq2 5841	. . . . . . 7 ⊢ (𝑦 = 𝑌 → (𝑋 ∘ 𝑦) = (𝑋 ∘ 𝑌))
20	4, 19	eqeq12d 2779	. . . . . 6 ⊢ (𝑦 = 𝑌 → ((𝑋 + 𝑦) = (𝑋 ∘ 𝑦) ↔ (𝑋 + 𝑌) = (𝑋 ∘ 𝑌)))
21	18, 20, 14	vtocl2ga 3541	. . . . 5 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) = (𝑋 ∘ 𝑌))
22	21	3adant3 1150	. . . 4 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → (𝑋 + 𝑌) = (𝑋 ∘ 𝑌))
23	22	coeq1d 5844	. . 3 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → ((𝑋 + 𝑌) ∘ 𝑍) = ((𝑋 ∘ 𝑌) ∘ 𝑍))
24	16, 23	eqtrd 2798	. 2 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → ((𝑋 + 𝑌) + 𝑍) = ((𝑋 ∘ 𝑌) ∘ 𝑍))
25		simp1 1154	. . . 4 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → 𝑋 ∈ 𝐵)
26		oveq1 7447	. . . . . . 7 ⊢ (𝑥 = 𝑌 → (𝑥 + 𝑦) = (𝑌 + 𝑦))
27	26	eleq1d 2849	. . . . . 6 ⊢ (𝑥 = 𝑌 → ((𝑥 + 𝑦) ∈ 𝐵 ↔ (𝑌 + 𝑦) ∈ 𝐵))
28		oveq2 7448	. . . . . . 7 ⊢ (𝑦 = 𝑍 → (𝑌 + 𝑦) = (𝑌 + 𝑍))
29	28	eleq1d 2849	. . . . . 6 ⊢ (𝑦 = 𝑍 → ((𝑌 + 𝑦) ∈ 𝐵 ↔ (𝑌 + 𝑍) ∈ 𝐵))
30	27, 29, 6	vtocl2ga 3541	. . . . 5 ⊢ ((𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → (𝑌 + 𝑍) ∈ 𝐵)
31	30	3adant1 1148	. . . 4 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → (𝑌 + 𝑍) ∈ 𝐵)
32		oveq2 7448	. . . . . 6 ⊢ (𝑦 = (𝑌 + 𝑍) → (𝑋 + 𝑦) = (𝑋 + (𝑌 + 𝑍)))
33		coeq2 5841	. . . . . 6 ⊢ (𝑦 = (𝑌 + 𝑍) → (𝑋 ∘ 𝑦) = (𝑋 ∘ (𝑌 + 𝑍)))
34	32, 33	eqeq12d 2779	. . . . 5 ⊢ (𝑦 = (𝑌 + 𝑍) → ((𝑋 + 𝑦) = (𝑋 ∘ 𝑦) ↔ (𝑋 + (𝑌 + 𝑍)) = (𝑋 ∘ (𝑌 + 𝑍))))
35	18, 34, 14	vtocl2ga 3541	. . . 4 ⊢ ((𝑋 ∈ 𝐵 ∧ (𝑌 + 𝑍) ∈ 𝐵) → (𝑋 + (𝑌 + 𝑍)) = (𝑋 ∘ (𝑌 + 𝑍)))
36	25, 31, 35	syl2anc 596	. . 3 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → (𝑋 + (𝑌 + 𝑍)) = (𝑋 ∘ (𝑌 + 𝑍)))
37		coeq1 5840	. . . . . . 7 ⊢ (𝑥 = 𝑌 → (𝑥 ∘ 𝑦) = (𝑌 ∘ 𝑦))
38	26, 37	eqeq12d 2779	. . . . . 6 ⊢ (𝑥 = 𝑌 → ((𝑥 + 𝑦) = (𝑥 ∘ 𝑦) ↔ (𝑌 + 𝑦) = (𝑌 ∘ 𝑦)))
39		coeq2 5841	. . . . . . 7 ⊢ (𝑦 = 𝑍 → (𝑌 ∘ 𝑦) = (𝑌 ∘ 𝑍))
40	28, 39	eqeq12d 2779	. . . . . 6 ⊢ (𝑦 = 𝑍 → ((𝑌 + 𝑦) = (𝑌 ∘ 𝑦) ↔ (𝑌 + 𝑍) = (𝑌 ∘ 𝑍)))
41	38, 40, 14	vtocl2ga 3541	. . . . 5 ⊢ ((𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → (𝑌 + 𝑍) = (𝑌 ∘ 𝑍))
42	41	3adant1 1148	. . . 4 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → (𝑌 + 𝑍) = (𝑌 ∘ 𝑍))
43	42	coeq2d 5845	. . 3 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → (𝑋 ∘ (𝑌 + 𝑍)) = (𝑋 ∘ (𝑌 ∘ 𝑍)))
44	36, 43	eqtrd 2798	. 2 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → (𝑋 + (𝑌 + 𝑍)) = (𝑋 ∘ (𝑌 ∘ 𝑍)))
45	1, 24, 44	3eqtr4a 2824	1 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → ((𝑋 + 𝑌) + 𝑍) = (𝑋 + (𝑌 + 𝑍)))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103   = wceq 1570   ∈ wcel 2147   ∘ ccom 5659  (class class class)co 7440

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5252  ax-pr 5395

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5171  df-xp 5661  df-rel 5662  df-co 5664  df-iota 6509  df-fv 6563  df-ov 7443

This theorem is used by:  efmndsgrp  19108  smndex1sgrp  19133  symggrp  19641