Theorem symggrplem 18887

Description: Lemma for symggrp 19410 and efmndsgrp 18889. Conditions for an operation to be associative. Formerly part of proof for symggrp 19410. (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 6279	. 2 ⊢ ((𝑋 ∘ 𝑌) ∘ 𝑍) = (𝑋 ∘ (𝑌 ∘ 𝑍))
2		oveq1 7434	. . . . . 6 ⊢ (𝑥 = 𝑋 → (𝑥 + 𝑦) = (𝑋 + 𝑦))
3	2	eleq1d 2814	. . . . 5 ⊢ (𝑥 = 𝑋 → ((𝑥 + 𝑦) ∈ 𝐵 ↔ (𝑋 + 𝑦) ∈ 𝐵))
4		oveq2 7435	. . . . . 6 ⊢ (𝑦 = 𝑌 → (𝑋 + 𝑦) = (𝑋 + 𝑌))
5	4	eleq1d 2814	. . . . 5 ⊢ (𝑦 = 𝑌 → ((𝑋 + 𝑦) ∈ 𝐵 ↔ (𝑋 + 𝑌) ∈ 𝐵))
6		symggrplem.c	. . . . 5 ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) ∈ 𝐵)
7	3, 5, 6	vtocl2ga 3575	. . . 4 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) ∈ 𝐵)
8		oveq1 7434	. . . . . 6 ⊢ (𝑥 = (𝑋 + 𝑌) → (𝑥 + 𝑦) = ((𝑋 + 𝑌) + 𝑦))
9		coeq1 5866	. . . . . 6 ⊢ (𝑥 = (𝑋 + 𝑌) → (𝑥 ∘ 𝑦) = ((𝑋 + 𝑌) ∘ 𝑦))
10	8, 9	eqeq12d 2745	. . . . 5 ⊢ (𝑥 = (𝑋 + 𝑌) → ((𝑥 + 𝑦) = (𝑥 ∘ 𝑦) ↔ ((𝑋 + 𝑌) + 𝑦) = ((𝑋 + 𝑌) ∘ 𝑦)))
11		oveq2 7435	. . . . . 6 ⊢ (𝑦 = 𝑍 → ((𝑋 + 𝑌) + 𝑦) = ((𝑋 + 𝑌) + 𝑍))
12		coeq2 5867	. . . . . 6 ⊢ (𝑦 = 𝑍 → ((𝑋 + 𝑌) ∘ 𝑦) = ((𝑋 + 𝑌) ∘ 𝑍))
13	11, 12	eqeq12d 2745	. . . . 5 ⊢ (𝑦 = 𝑍 → (((𝑋 + 𝑌) + 𝑦) = ((𝑋 + 𝑌) ∘ 𝑦) ↔ ((𝑋 + 𝑌) + 𝑍) = ((𝑋 + 𝑌) ∘ 𝑍)))
14		symggrplem.p	. . . . 5 ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) = (𝑥 ∘ 𝑦))
15	10, 13, 14	vtocl2ga 3575	. . . 4 ⊢ (((𝑋 + 𝑌) ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → ((𝑋 + 𝑌) + 𝑍) = ((𝑋 + 𝑌) ∘ 𝑍))
16	7, 15	stoic3 1771	. . 3 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → ((𝑋 + 𝑌) + 𝑍) = ((𝑋 + 𝑌) ∘ 𝑍))
17		coeq1 5866	. . . . . . 7 ⊢ (𝑥 = 𝑋 → (𝑥 ∘ 𝑦) = (𝑋 ∘ 𝑦))
18	2, 17	eqeq12d 2745	. . . . . 6 ⊢ (𝑥 = 𝑋 → ((𝑥 + 𝑦) = (𝑥 ∘ 𝑦) ↔ (𝑋 + 𝑦) = (𝑋 ∘ 𝑦)))
19		coeq2 5867	. . . . . . 7 ⊢ (𝑦 = 𝑌 → (𝑋 ∘ 𝑦) = (𝑋 ∘ 𝑌))
20	4, 19	eqeq12d 2745	. . . . . 6 ⊢ (𝑦 = 𝑌 → ((𝑋 + 𝑦) = (𝑋 ∘ 𝑦) ↔ (𝑋 + 𝑌) = (𝑋 ∘ 𝑌)))
21	18, 20, 14	vtocl2ga 3575	. . . . 5 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) = (𝑋 ∘ 𝑌))
22	21	3adant3 1129	. . . 4 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → (𝑋 + 𝑌) = (𝑋 ∘ 𝑌))
23	22	coeq1d 5870	. . 3 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → ((𝑋 + 𝑌) ∘ 𝑍) = ((𝑋 ∘ 𝑌) ∘ 𝑍))
24	16, 23	eqtrd 2769	. 2 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → ((𝑋 + 𝑌) + 𝑍) = ((𝑋 ∘ 𝑌) ∘ 𝑍))
25		simp1 1133	. . . 4 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → 𝑋 ∈ 𝐵)
26		oveq1 7434	. . . . . . 7 ⊢ (𝑥 = 𝑌 → (𝑥 + 𝑦) = (𝑌 + 𝑦))
27	26	eleq1d 2814	. . . . . 6 ⊢ (𝑥 = 𝑌 → ((𝑥 + 𝑦) ∈ 𝐵 ↔ (𝑌 + 𝑦) ∈ 𝐵))
28		oveq2 7435	. . . . . . 7 ⊢ (𝑦 = 𝑍 → (𝑌 + 𝑦) = (𝑌 + 𝑍))
29	28	eleq1d 2814	. . . . . 6 ⊢ (𝑦 = 𝑍 → ((𝑌 + 𝑦) ∈ 𝐵 ↔ (𝑌 + 𝑍) ∈ 𝐵))
30	27, 29, 6	vtocl2ga 3575	. . . . 5 ⊢ ((𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → (𝑌 + 𝑍) ∈ 𝐵)
31	30	3adant1 1127	. . . 4 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → (𝑌 + 𝑍) ∈ 𝐵)
32		oveq2 7435	. . . . . 6 ⊢ (𝑦 = (𝑌 + 𝑍) → (𝑋 + 𝑦) = (𝑋 + (𝑌 + 𝑍)))
33		coeq2 5867	. . . . . 6 ⊢ (𝑦 = (𝑌 + 𝑍) → (𝑋 ∘ 𝑦) = (𝑋 ∘ (𝑌 + 𝑍)))
34	32, 33	eqeq12d 2745	. . . . 5 ⊢ (𝑦 = (𝑌 + 𝑍) → ((𝑋 + 𝑦) = (𝑋 ∘ 𝑦) ↔ (𝑋 + (𝑌 + 𝑍)) = (𝑋 ∘ (𝑌 + 𝑍))))
35	18, 34, 14	vtocl2ga 3575	. . . 4 ⊢ ((𝑋 ∈ 𝐵 ∧ (𝑌 + 𝑍) ∈ 𝐵) → (𝑋 + (𝑌 + 𝑍)) = (𝑋 ∘ (𝑌 + 𝑍)))
36	25, 31, 35	syl2anc 582	. . 3 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → (𝑋 + (𝑌 + 𝑍)) = (𝑋 ∘ (𝑌 + 𝑍)))
37		coeq1 5866	. . . . . . 7 ⊢ (𝑥 = 𝑌 → (𝑥 ∘ 𝑦) = (𝑌 ∘ 𝑦))
38	26, 37	eqeq12d 2745	. . . . . 6 ⊢ (𝑥 = 𝑌 → ((𝑥 + 𝑦) = (𝑥 ∘ 𝑦) ↔ (𝑌 + 𝑦) = (𝑌 ∘ 𝑦)))
39		coeq2 5867	. . . . . . 7 ⊢ (𝑦 = 𝑍 → (𝑌 ∘ 𝑦) = (𝑌 ∘ 𝑍))
40	28, 39	eqeq12d 2745	. . . . . 6 ⊢ (𝑦 = 𝑍 → ((𝑌 + 𝑦) = (𝑌 ∘ 𝑦) ↔ (𝑌 + 𝑍) = (𝑌 ∘ 𝑍)))
41	38, 40, 14	vtocl2ga 3575	. . . . 5 ⊢ ((𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → (𝑌 + 𝑍) = (𝑌 ∘ 𝑍))
42	41	3adant1 1127	. . . 4 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → (𝑌 + 𝑍) = (𝑌 ∘ 𝑍))
43	42	coeq2d 5871	. . 3 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → (𝑋 ∘ (𝑌 + 𝑍)) = (𝑋 ∘ (𝑌 ∘ 𝑍)))
44	36, 43	eqtrd 2769	. 2 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → (𝑋 + (𝑌 + 𝑍)) = (𝑋 ∘ (𝑌 ∘ 𝑍)))
45	1, 24, 44	3eqtr4a 2795	1 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → ((𝑋 + 𝑌) + 𝑍) = (𝑋 + (𝑌 + 𝑍)))

Syntax hints:   → wi 4   ∧ wa 394   ∧ w3a 1084   = wceq 1534   ∈ wcel 2100   ∘ ccom 5688  (class class class)co 7427

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2102  ax-9 2110  ax-11 2150  ax-ext 2700  ax-sep 5305  ax-nul 5312  ax-pr 5435

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2062  df-clab 2707  df-cleq 2721  df-clel 2806  df-rab 3429  df-v 3474  df-dif 3961  df-un 3963  df-ss 3975  df-nul 4334  df-if 4535  df-sn 4635  df-pr 4637  df-op 4641  df-uni 4917  df-br 5155  df-opab 5217  df-xp 5690  df-rel 5691  df-co 5693  df-iota 6508  df-fv 6564  df-ov 7430

This theorem is referenced by:  efmndsgrp  18889  smndex1sgrp  18911  symggrp  19410