Theorem grpcominv1

Description: If two elements commute, then they commute with each other's inverses (case of the first element commuting with the inverse of the second element). (Contributed by SN, 29-Jan-2025)

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

Proof

Step	Hyp	Ref	Expression
1		grpcominv.b	$$⊢B={\mathrm{Base}}_G$$
2		grpcominv.p	$$⊢\underset{\dot{}}{+}={+}_G$$
3		grpcominv.n	$$⊢N={inv}_g\left(G\right)$$
4		grpcominv.g	$$⊢\phi \to G\in \mathrm{Grp}$$
5		grpcominv.x	$$⊢\phi \to X\in B$$
6		grpcominv.y	$$⊢\phi \to Y\in B$$
7		grpcominv.1	$$⊢\phi \to X\underset{\dot{}}{+}Y=Y\underset{\dot{}}{+}X$$
8	1 3 4 6	grpinvcld	$$⊢\phi \to N\left(Y\right)\in B$$
9	1 2 4 8 6 5	grpassd	$$⊢\phi \to \left(N\left(Y\right)\underset{\dot{}}{+}Y\right)\underset{\dot{}}{+}X=N\left(Y\right)\underset{\dot{}}{+}\left(Y\underset{\dot{}}{+}X\right)$$
10		eqid	$$⊢0_G=0_G$$
11	1 2 10 3 4 6	grplinvd	$$⊢\phi \to N\left(Y\right)\underset{\dot{}}{+}Y=0_G$$
12	11	oveq1d	$$⊢\phi \to \left(N\left(Y\right)\underset{\dot{}}{+}Y\right)\underset{\dot{}}{+}X=0_G\underset{\dot{}}{+}X$$
13	1 2 10 4 5	grplidd	$$⊢\phi \to 0_G\underset{\dot{}}{+}X=X$$
14	12 13	eqtr2d	$$⊢\phi \to X=\left(N\left(Y\right)\underset{\dot{}}{+}Y\right)\underset{\dot{}}{+}X$$
15	7	oveq2d	$$⊢\phi \to N\left(Y\right)\underset{\dot{}}{+}\left(X\underset{\dot{}}{+}Y\right)=N\left(Y\right)\underset{\dot{}}{+}\left(Y\underset{\dot{}}{+}X\right)$$
16	9 14 15	3eqtr4rd	$$⊢\phi \to N\left(Y\right)\underset{\dot{}}{+}\left(X\underset{\dot{}}{+}Y\right)=X$$
17	1 2 4 8 5 6	grpassd	$$⊢\phi \to \left(N\left(Y\right)\underset{\dot{}}{+}X\right)\underset{\dot{}}{+}Y=N\left(Y\right)\underset{\dot{}}{+}\left(X\underset{\dot{}}{+}Y\right)$$
18	1 2 3 4 5 6	grpasscan2d	$$⊢\phi \to \left(X\underset{\dot{}}{+}N\left(Y\right)\right)\underset{\dot{}}{+}Y=X$$
19	16 17 18	3eqtr4rd	$$⊢\phi \to \left(X\underset{\dot{}}{+}N\left(Y\right)\right)\underset{\dot{}}{+}Y=\left(N\left(Y\right)\underset{\dot{}}{+}X\right)\underset{\dot{}}{+}Y$$
20	1 2 4 5 8	grpcld	$$⊢\phi \to X\underset{\dot{}}{+}N\left(Y\right)\in B$$
21	1 2 4 8 5	grpcld	$$⊢\phi \to N\left(Y\right)\underset{\dot{}}{+}X\in B$$
22	1 2	grprcan	$$⊢\left(G\in \mathrm{Grp}\wedge \left(X\underset{\dot{}}{+}N\left(Y\right)\in B\wedge N\left(Y\right)\underset{\dot{}}{+}X\in B\wedge Y\in B\right)\right)\to \left(\left(X\underset{\dot{}}{+}N\left(Y\right)\right)\underset{\dot{}}{+}Y=\left(N\left(Y\right)\underset{\dot{}}{+}X\right)\underset{\dot{}}{+}Y\leftrightarrow X\underset{\dot{}}{+}N\left(Y\right)=N\left(Y\right)\underset{\dot{}}{+}X\right)$$
23	4 20 21 6 22	syl13anc	$$⊢\phi \to \left(\left(X\underset{\dot{}}{+}N\left(Y\right)\right)\underset{\dot{}}{+}Y=\left(N\left(Y\right)\underset{\dot{}}{+}X\right)\underset{\dot{}}{+}Y\leftrightarrow X\underset{\dot{}}{+}N\left(Y\right)=N\left(Y\right)\underset{\dot{}}{+}X\right)$$
24	19 23	mpbid	$$⊢\phi \to X\underset{\dot{}}{+}N\left(Y\right)=N\left(Y\right)\underset{\dot{}}{+}X$$