Theorem symggrplem 18919

Description: Lemma for symggrp 19442 and efmndsgrp 18921. Conditions for an operation to be associative. Formerly part of proof for symggrp 19442. (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 6296	. 2 ⊢ ((𝑋 ∘ 𝑌) ∘ 𝑍) = (𝑋 ∘ (𝑌 ∘ 𝑍))
2		oveq1 7455	. . . . . 6 ⊢ (𝑥 = 𝑋 → (𝑥 + 𝑦) = (𝑋 + 𝑦))
3	2	eleq1d 2829	. . . . 5 ⊢ (𝑥 = 𝑋 → ((𝑥 + 𝑦) ∈ 𝐵 ↔ (𝑋 + 𝑦) ∈ 𝐵))
4		oveq2 7456	. . . . . 6 ⊢ (𝑦 = 𝑌 → (𝑋 + 𝑦) = (𝑋 + 𝑌))
5	4	eleq1d 2829	. . . . 5 ⊢ (𝑦 = 𝑌 → ((𝑋 + 𝑦) ∈ 𝐵 ↔ (𝑋 + 𝑌) ∈ 𝐵))
6		symggrplem.c	. . . . 5 ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) ∈ 𝐵)
7	3, 5, 6	vtocl2ga 3590	. . . 4 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) ∈ 𝐵)
8		oveq1 7455	. . . . . 6 ⊢ (𝑥 = (𝑋 + 𝑌) → (𝑥 + 𝑦) = ((𝑋 + 𝑌) + 𝑦))
9		coeq1 5882	. . . . . 6 ⊢ (𝑥 = (𝑋 + 𝑌) → (𝑥 ∘ 𝑦) = ((𝑋 + 𝑌) ∘ 𝑦))
10	8, 9	eqeq12d 2756	. . . . 5 ⊢ (𝑥 = (𝑋 + 𝑌) → ((𝑥 + 𝑦) = (𝑥 ∘ 𝑦) ↔ ((𝑋 + 𝑌) + 𝑦) = ((𝑋 + 𝑌) ∘ 𝑦)))
11		oveq2 7456	. . . . . 6 ⊢ (𝑦 = 𝑍 → ((𝑋 + 𝑌) + 𝑦) = ((𝑋 + 𝑌) + 𝑍))
12		coeq2 5883	. . . . . 6 ⊢ (𝑦 = 𝑍 → ((𝑋 + 𝑌) ∘ 𝑦) = ((𝑋 + 𝑌) ∘ 𝑍))
13	11, 12	eqeq12d 2756	. . . . 5 ⊢ (𝑦 = 𝑍 → (((𝑋 + 𝑌) + 𝑦) = ((𝑋 + 𝑌) ∘ 𝑦) ↔ ((𝑋 + 𝑌) + 𝑍) = ((𝑋 + 𝑌) ∘ 𝑍)))
14		symggrplem.p	. . . . 5 ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) = (𝑥 ∘ 𝑦))
15	10, 13, 14	vtocl2ga 3590	. . . 4 ⊢ (((𝑋 + 𝑌) ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → ((𝑋 + 𝑌) + 𝑍) = ((𝑋 + 𝑌) ∘ 𝑍))
16	7, 15	stoic3 1774	. . 3 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → ((𝑋 + 𝑌) + 𝑍) = ((𝑋 + 𝑌) ∘ 𝑍))
17		coeq1 5882	. . . . . . 7 ⊢ (𝑥 = 𝑋 → (𝑥 ∘ 𝑦) = (𝑋 ∘ 𝑦))
18	2, 17	eqeq12d 2756	. . . . . 6 ⊢ (𝑥 = 𝑋 → ((𝑥 + 𝑦) = (𝑥 ∘ 𝑦) ↔ (𝑋 + 𝑦) = (𝑋 ∘ 𝑦)))
19		coeq2 5883	. . . . . . 7 ⊢ (𝑦 = 𝑌 → (𝑋 ∘ 𝑦) = (𝑋 ∘ 𝑌))
20	4, 19	eqeq12d 2756	. . . . . 6 ⊢ (𝑦 = 𝑌 → ((𝑋 + 𝑦) = (𝑋 ∘ 𝑦) ↔ (𝑋 + 𝑌) = (𝑋 ∘ 𝑌)))
21	18, 20, 14	vtocl2ga 3590	. . . . 5 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) = (𝑋 ∘ 𝑌))
22	21	3adant3 1132	. . . 4 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → (𝑋 + 𝑌) = (𝑋 ∘ 𝑌))
23	22	coeq1d 5886	. . 3 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → ((𝑋 + 𝑌) ∘ 𝑍) = ((𝑋 ∘ 𝑌) ∘ 𝑍))
24	16, 23	eqtrd 2780	. 2 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → ((𝑋 + 𝑌) + 𝑍) = ((𝑋 ∘ 𝑌) ∘ 𝑍))
25		simp1 1136	. . . 4 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → 𝑋 ∈ 𝐵)
26		oveq1 7455	. . . . . . 7 ⊢ (𝑥 = 𝑌 → (𝑥 + 𝑦) = (𝑌 + 𝑦))
27	26	eleq1d 2829	. . . . . 6 ⊢ (𝑥 = 𝑌 → ((𝑥 + 𝑦) ∈ 𝐵 ↔ (𝑌 + 𝑦) ∈ 𝐵))
28		oveq2 7456	. . . . . . 7 ⊢ (𝑦 = 𝑍 → (𝑌 + 𝑦) = (𝑌 + 𝑍))
29	28	eleq1d 2829	. . . . . 6 ⊢ (𝑦 = 𝑍 → ((𝑌 + 𝑦) ∈ 𝐵 ↔ (𝑌 + 𝑍) ∈ 𝐵))
30	27, 29, 6	vtocl2ga 3590	. . . . 5 ⊢ ((𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → (𝑌 + 𝑍) ∈ 𝐵)
31	30	3adant1 1130	. . . 4 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → (𝑌 + 𝑍) ∈ 𝐵)
32		oveq2 7456	. . . . . 6 ⊢ (𝑦 = (𝑌 + 𝑍) → (𝑋 + 𝑦) = (𝑋 + (𝑌 + 𝑍)))
33		coeq2 5883	. . . . . 6 ⊢ (𝑦 = (𝑌 + 𝑍) → (𝑋 ∘ 𝑦) = (𝑋 ∘ (𝑌 + 𝑍)))
34	32, 33	eqeq12d 2756	. . . . 5 ⊢ (𝑦 = (𝑌 + 𝑍) → ((𝑋 + 𝑦) = (𝑋 ∘ 𝑦) ↔ (𝑋 + (𝑌 + 𝑍)) = (𝑋 ∘ (𝑌 + 𝑍))))
35	18, 34, 14	vtocl2ga 3590	. . . 4 ⊢ ((𝑋 ∈ 𝐵 ∧ (𝑌 + 𝑍) ∈ 𝐵) → (𝑋 + (𝑌 + 𝑍)) = (𝑋 ∘ (𝑌 + 𝑍)))
36	25, 31, 35	syl2anc 583	. . 3 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → (𝑋 + (𝑌 + 𝑍)) = (𝑋 ∘ (𝑌 + 𝑍)))
37		coeq1 5882	. . . . . . 7 ⊢ (𝑥 = 𝑌 → (𝑥 ∘ 𝑦) = (𝑌 ∘ 𝑦))
38	26, 37	eqeq12d 2756	. . . . . 6 ⊢ (𝑥 = 𝑌 → ((𝑥 + 𝑦) = (𝑥 ∘ 𝑦) ↔ (𝑌 + 𝑦) = (𝑌 ∘ 𝑦)))
39		coeq2 5883	. . . . . . 7 ⊢ (𝑦 = 𝑍 → (𝑌 ∘ 𝑦) = (𝑌 ∘ 𝑍))
40	28, 39	eqeq12d 2756	. . . . . 6 ⊢ (𝑦 = 𝑍 → ((𝑌 + 𝑦) = (𝑌 ∘ 𝑦) ↔ (𝑌 + 𝑍) = (𝑌 ∘ 𝑍)))
41	38, 40, 14	vtocl2ga 3590	. . . . 5 ⊢ ((𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → (𝑌 + 𝑍) = (𝑌 ∘ 𝑍))
42	41	3adant1 1130	. . . 4 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → (𝑌 + 𝑍) = (𝑌 ∘ 𝑍))
43	42	coeq2d 5887	. . 3 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → (𝑋 ∘ (𝑌 + 𝑍)) = (𝑋 ∘ (𝑌 ∘ 𝑍)))
44	36, 43	eqtrd 2780	. 2 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → (𝑋 + (𝑌 + 𝑍)) = (𝑋 ∘ (𝑌 ∘ 𝑍)))
45	1, 24, 44	3eqtr4a 2806	1 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → ((𝑋 + 𝑌) + 𝑍) = (𝑋 + (𝑌 + 𝑍)))

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087   = wceq 1537   ∈ wcel 2108   ∘ ccom 5704  (class class class)co 7448

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-11 2158  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-opab 5229  df-xp 5706  df-rel 5707  df-co 5709  df-iota 6525  df-fv 6581  df-ov 7451

This theorem is referenced by:  efmndsgrp  18921  smndex1sgrp  18943  symggrp  19442