Theorem symggrplem

Description: Lemma for symggrp and efmndsgrp . Conditions for an operation to be associative. Formerly part of proof for symggrp . (Contributed by AV, 28-Jan-2024)

	Ref	Expression
Hypotheses	symggrplem.c	$$⊢\left(x\in B\wedge y\in B\right)\to x\underset{\dot{}}{+}y\in B$$
	symggrplem.p	$$⊢\left(x\in B\wedge y\in B\right)\to x\underset{\dot{}}{+}y=x\circ y$$
Assertion	symggrplem	$$⊢\left(X\in B\wedge Y\in B\wedge Z\in B\right)\to \left(X\underset{\dot{}}{+}Y\right)\underset{\dot{}}{+}Z=X\underset{\dot{}}{+}\left(Y\underset{\dot{}}{+}Z\right)$$

Proof

Step	Hyp	Ref	Expression
1		symggrplem.c	$$⊢\left(x\in B\wedge y\in B\right)\to x\underset{\dot{}}{+}y\in B$$
2		symggrplem.p	$$⊢\left(x\in B\wedge y\in B\right)\to x\underset{\dot{}}{+}y=x\circ y$$
3		coass	$$⊢\left(X\circ Y\right)\circ Z=X\circ \left(Y\circ Z\right)$$
4		oveq1	$$⊢x=X\to x\underset{\dot{}}{+}y=X\underset{\dot{}}{+}y$$
5	4	eleq1d	$$⊢x=X\to \left(x\underset{\dot{}}{+}y\in B\leftrightarrow X\underset{\dot{}}{+}y\in B\right)$$
6		oveq2	$$⊢y=Y\to X\underset{\dot{}}{+}y=X\underset{\dot{}}{+}Y$$
7	6	eleq1d	$$⊢y=Y\to \left(X\underset{\dot{}}{+}y\in B\leftrightarrow X\underset{\dot{}}{+}Y\in B\right)$$
8	5 7 1	vtocl2ga	$$⊢\left(X\in B\wedge Y\in B\right)\to X\underset{\dot{}}{+}Y\in B$$
9		oveq1	$$⊢x=X\underset{\dot{}}{+}Y\to x\underset{\dot{}}{+}y=\left(X\underset{\dot{}}{+}Y\right)\underset{\dot{}}{+}y$$
10		coeq1	$$⊢x=X\underset{\dot{}}{+}Y\to x\circ y=\left(X\underset{\dot{}}{+}Y\right)\circ y$$
11	9 10	eqeq12d	$$⊢x=X\underset{\dot{}}{+}Y\to \left(x\underset{\dot{}}{+}y=x\circ y\leftrightarrow \left(X\underset{\dot{}}{+}Y\right)\underset{\dot{}}{+}y=\left(X\underset{\dot{}}{+}Y\right)\circ y\right)$$
12		oveq2	$$⊢y=Z\to \left(X\underset{\dot{}}{+}Y\right)\underset{\dot{}}{+}y=\left(X\underset{\dot{}}{+}Y\right)\underset{\dot{}}{+}Z$$
13		coeq2	$$⊢y=Z\to \left(X\underset{\dot{}}{+}Y\right)\circ y=\left(X\underset{\dot{}}{+}Y\right)\circ Z$$
14	12 13	eqeq12d	$$⊢y=Z\to \left(\left(X\underset{\dot{}}{+}Y\right)\underset{\dot{}}{+}y=\left(X\underset{\dot{}}{+}Y\right)\circ y\leftrightarrow \left(X\underset{\dot{}}{+}Y\right)\underset{\dot{}}{+}Z=\left(X\underset{\dot{}}{+}Y\right)\circ Z\right)$$
15	11 14 2	vtocl2ga	$$⊢\left(X\underset{\dot{}}{+}Y\in B\wedge Z\in B\right)\to \left(X\underset{\dot{}}{+}Y\right)\underset{\dot{}}{+}Z=\left(X\underset{\dot{}}{+}Y\right)\circ Z$$
16	8 15	stoic3	$$⊢\left(X\in B\wedge Y\in B\wedge Z\in B\right)\to \left(X\underset{\dot{}}{+}Y\right)\underset{\dot{}}{+}Z=\left(X\underset{\dot{}}{+}Y\right)\circ Z$$
17		coeq1	$$⊢x=X\to x\circ y=X\circ y$$
18	4 17	eqeq12d	$$⊢x=X\to \left(x\underset{\dot{}}{+}y=x\circ y\leftrightarrow X\underset{\dot{}}{+}y=X\circ y\right)$$
19		coeq2	$$⊢y=Y\to X\circ y=X\circ Y$$
20	6 19	eqeq12d	$$⊢y=Y\to \left(X\underset{\dot{}}{+}y=X\circ y\leftrightarrow X\underset{\dot{}}{+}Y=X\circ Y\right)$$
21	18 20 2	vtocl2ga	$$⊢\left(X\in B\wedge Y\in B\right)\to X\underset{\dot{}}{+}Y=X\circ Y$$
22	21	3adant3	$$⊢\left(X\in B\wedge Y\in B\wedge Z\in B\right)\to X\underset{\dot{}}{+}Y=X\circ Y$$
23	22	coeq1d	$$⊢\left(X\in B\wedge Y\in B\wedge Z\in B\right)\to \left(X\underset{\dot{}}{+}Y\right)\circ Z=\left(X\circ Y\right)\circ Z$$
24	16 23	eqtrd	$$⊢\left(X\in B\wedge Y\in B\wedge Z\in B\right)\to \left(X\underset{\dot{}}{+}Y\right)\underset{\dot{}}{+}Z=\left(X\circ Y\right)\circ Z$$
25		simp1	$$⊢\left(X\in B\wedge Y\in B\wedge Z\in B\right)\to X\in B$$
26		oveq1	$$⊢x=Y\to x\underset{\dot{}}{+}y=Y\underset{\dot{}}{+}y$$
27	26	eleq1d	$$⊢x=Y\to \left(x\underset{\dot{}}{+}y\in B\leftrightarrow Y\underset{\dot{}}{+}y\in B\right)$$
28		oveq2	$$⊢y=Z\to Y\underset{\dot{}}{+}y=Y\underset{\dot{}}{+}Z$$
29	28	eleq1d	$$⊢y=Z\to \left(Y\underset{\dot{}}{+}y\in B\leftrightarrow Y\underset{\dot{}}{+}Z\in B\right)$$
30	27 29 1	vtocl2ga	$$⊢\left(Y\in B\wedge Z\in B\right)\to Y\underset{\dot{}}{+}Z\in B$$
31	30	3adant1	$$⊢\left(X\in B\wedge Y\in B\wedge Z\in B\right)\to Y\underset{\dot{}}{+}Z\in B$$
32		oveq2	$$⊢y=Y\underset{\dot{}}{+}Z\to X\underset{\dot{}}{+}y=X\underset{\dot{}}{+}\left(Y\underset{\dot{}}{+}Z\right)$$
33		coeq2	$$⊢y=Y\underset{\dot{}}{+}Z\to X\circ y=X\circ \left(Y\underset{\dot{}}{+}Z\right)$$
34	32 33	eqeq12d	$$⊢y=Y\underset{\dot{}}{+}Z\to \left(X\underset{\dot{}}{+}y=X\circ y\leftrightarrow X\underset{\dot{}}{+}\left(Y\underset{\dot{}}{+}Z\right)=X\circ \left(Y\underset{\dot{}}{+}Z\right)\right)$$
35	18 34 2	vtocl2ga	$$⊢\left(X\in B\wedge Y\underset{\dot{}}{+}Z\in B\right)\to X\underset{\dot{}}{+}\left(Y\underset{\dot{}}{+}Z\right)=X\circ \left(Y\underset{\dot{}}{+}Z\right)$$
36	25 31 35	syl2anc	$$⊢\left(X\in B\wedge Y\in B\wedge Z\in B\right)\to X\underset{\dot{}}{+}\left(Y\underset{\dot{}}{+}Z\right)=X\circ \left(Y\underset{\dot{}}{+}Z\right)$$
37		coeq1	$$⊢x=Y\to x\circ y=Y\circ y$$
38	26 37	eqeq12d	$$⊢x=Y\to \left(x\underset{\dot{}}{+}y=x\circ y\leftrightarrow Y\underset{\dot{}}{+}y=Y\circ y\right)$$
39		coeq2	$$⊢y=Z\to Y\circ y=Y\circ Z$$
40	28 39	eqeq12d	$$⊢y=Z\to \left(Y\underset{\dot{}}{+}y=Y\circ y\leftrightarrow Y\underset{\dot{}}{+}Z=Y\circ Z\right)$$
41	38 40 2	vtocl2ga	$$⊢\left(Y\in B\wedge Z\in B\right)\to Y\underset{\dot{}}{+}Z=Y\circ Z$$
42	41	3adant1	$$⊢\left(X\in B\wedge Y\in B\wedge Z\in B\right)\to Y\underset{\dot{}}{+}Z=Y\circ Z$$
43	42	coeq2d	$$⊢\left(X\in B\wedge Y\in B\wedge Z\in B\right)\to X\circ \left(Y\underset{\dot{}}{+}Z\right)=X\circ \left(Y\circ Z\right)$$
44	36 43	eqtrd	$$⊢\left(X\in B\wedge Y\in B\wedge Z\in B\right)\to X\underset{\dot{}}{+}\left(Y\underset{\dot{}}{+}Z\right)=X\circ \left(Y\circ Z\right)$$
45	3 24 44	3eqtr4a	$$⊢\left(X\in B\wedge Y\in B\wedge Z\in B\right)\to \left(X\underset{\dot{}}{+}Y\right)\underset{\dot{}}{+}Z=X\underset{\dot{}}{+}\left(Y\underset{\dot{}}{+}Z\right)$$