Theorem grpassd

Description: A group operation is associative. (Contributed by SN, 29-Jan-2025)

	Ref	Expression
Hypotheses	grpassd.b	$$⊢B={\mathrm{Base}}_G$$
	grpassd.p	$$⊢\underset{\dot{}}{+}={+}_G$$
	grpassd.g	$$⊢\phi \to G\in \mathrm{Grp}$$
	grpassd.1	$$⊢\phi \to X\in B$$
	grpassd.2	$$⊢\phi \to Y\in B$$
	grpassd.3	$$⊢\phi \to Z\in B$$
Assertion	grpassd	$$⊢\phi \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		grpassd.b	$$⊢B={\mathrm{Base}}_G$$
2		grpassd.p	$$⊢\underset{\dot{}}{+}={+}_G$$
3		grpassd.g	$$⊢\phi \to G\in \mathrm{Grp}$$
4		grpassd.1	$$⊢\phi \to X\in B$$
5		grpassd.2	$$⊢\phi \to Y\in B$$
6		grpassd.3	$$⊢\phi \to Z\in B$$
7	1 2	grpass	$$⊢\left(G\in \mathrm{Grp}\wedge \left(X\in B\wedge Y\in B\wedge Z\in B\right)\right)\to \left(X\underset{\dot{}}{+}Y\right)\underset{\dot{}}{+}Z=X\underset{\dot{}}{+}\left(Y\underset{\dot{}}{+}Z\right)$$
8	3 4 5 6 7	syl13anc	$$⊢\phi \to \left(X\underset{\dot{}}{+}Y\right)\underset{\dot{}}{+}Z=X\underset{\dot{}}{+}\left(Y\underset{\dot{}}{+}Z\right)$$