Theorem grpasscan1

Description: An associative cancellation law for groups. (Contributed by Paul Chapman, 25-Feb-2008) (Revised by AV, 30-Aug-2021)

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

Proof

Step	Hyp	Ref	Expression
1		grplcan.b	$$⊢B={\mathrm{Base}}_G$$
2		grplcan.p	$$⊢\underset{\dot{}}{+}={+}_G$$
3		grpasscan1.n	$$⊢N={inv}_g\left(G\right)$$
4		eqid	$$⊢0_G=0_G$$
5	1 2 4 3	grprinv	$$⊢\left(G\in \mathrm{Grp}\wedge X\in B\right)\to X\underset{\dot{}}{+}N\left(X\right)=0_G$$
6	5	3adant3	$$⊢\left(G\in \mathrm{Grp}\wedge X\in B\wedge Y\in B\right)\to X\underset{\dot{}}{+}N\left(X\right)=0_G$$
7	6	oveq1d	$$⊢\left(G\in \mathrm{Grp}\wedge X\in B\wedge Y\in B\right)\to \left(X\underset{\dot{}}{+}N\left(X\right)\right)\underset{\dot{}}{+}Y=0_G\underset{\dot{}}{+}Y$$
8	1 3	grpinvcl	$$⊢\left(G\in \mathrm{Grp}\wedge X\in B\right)\to N\left(X\right)\in B$$
9	1 2	grpass	$$⊢\left(G\in \mathrm{Grp}\wedge \left(X\in B\wedge N\left(X\right)\in B\wedge Y\in B\right)\right)\to \left(X\underset{\dot{}}{+}N\left(X\right)\right)\underset{\dot{}}{+}Y=X\underset{\dot{}}{+}\left(N\left(X\right)\underset{\dot{}}{+}Y\right)$$
10	9	3exp2	$$⊢G\in \mathrm{Grp}\to \left(X\in B\to \left(N\left(X\right)\in B\to \left(Y\in B\to \left(X\underset{\dot{}}{+}N\left(X\right)\right)\underset{\dot{}}{+}Y=X\underset{\dot{}}{+}\left(N\left(X\right)\underset{\dot{}}{+}Y\right)\right)\right)\right)$$
11	10	imp	$$⊢\left(G\in \mathrm{Grp}\wedge X\in B\right)\to \left(N\left(X\right)\in B\to \left(Y\in B\to \left(X\underset{\dot{}}{+}N\left(X\right)\right)\underset{\dot{}}{+}Y=X\underset{\dot{}}{+}\left(N\left(X\right)\underset{\dot{}}{+}Y\right)\right)\right)$$
12	8 11	mpd	$$⊢\left(G\in \mathrm{Grp}\wedge X\in B\right)\to \left(Y\in B\to \left(X\underset{\dot{}}{+}N\left(X\right)\right)\underset{\dot{}}{+}Y=X\underset{\dot{}}{+}\left(N\left(X\right)\underset{\dot{}}{+}Y\right)\right)$$
13	12	3impia	$$⊢\left(G\in \mathrm{Grp}\wedge X\in B\wedge Y\in B\right)\to \left(X\underset{\dot{}}{+}N\left(X\right)\right)\underset{\dot{}}{+}Y=X\underset{\dot{}}{+}\left(N\left(X\right)\underset{\dot{}}{+}Y\right)$$
14	1 2 4	grplid	$$⊢\left(G\in \mathrm{Grp}\wedge Y\in B\right)\to 0_G\underset{\dot{}}{+}Y=Y$$
15	14	3adant2	$$⊢\left(G\in \mathrm{Grp}\wedge X\in B\wedge Y\in B\right)\to 0_G\underset{\dot{}}{+}Y=Y$$
16	7 13 15	3eqtr3d	$$⊢\left(G\in \mathrm{Grp}\wedge X\in B\wedge Y\in B\right)\to X\underset{\dot{}}{+}\left(N\left(X\right)\underset{\dot{}}{+}Y\right)=Y$$