Theorem grpasscan2d

Description: An associative cancellation law for groups. (Contributed by SN, 29-Jan-2025)

	Ref	Expression
Hypotheses	grpasscan2d.b	$$⊢B={\mathrm{Base}}_G$$
	grpasscan2d.p	$$⊢\underset{\dot{}}{+}={+}_G$$
	grpasscan2d.n	$$⊢N={inv}_g\left(G\right)$$
	grpasscan2d.g	$$⊢\phi \to G\in \mathrm{Grp}$$
	grpasscan2d.1	$$⊢\phi \to X\in B$$
	grpasscan2d.2	$$⊢\phi \to Y\in B$$
Assertion	grpasscan2d	$$⊢\phi \to \left(X\underset{\dot{}}{+}N\left(Y\right)\right)\underset{\dot{}}{+}Y=X$$

Proof

Step	Hyp	Ref	Expression
1		grpasscan2d.b	$$⊢B={\mathrm{Base}}_G$$
2		grpasscan2d.p	$$⊢\underset{\dot{}}{+}={+}_G$$
3		grpasscan2d.n	$$⊢N={inv}_g\left(G\right)$$
4		grpasscan2d.g	$$⊢\phi \to G\in \mathrm{Grp}$$
5		grpasscan2d.1	$$⊢\phi \to X\in B$$
6		grpasscan2d.2	$$⊢\phi \to Y\in B$$
7	1 2 3	grpasscan2	$$⊢\left(G\in \mathrm{Grp}\wedge X\in B\wedge Y\in B\right)\to \left(X\underset{\dot{}}{+}N\left(Y\right)\right)\underset{\dot{}}{+}Y=X$$
8	4 5 6 7	syl3anc	$$⊢\phi \to \left(X\underset{\dot{}}{+}N\left(Y\right)\right)\underset{\dot{}}{+}Y=X$$