Theorem grpcominv2

Description: If two elements commute, then they commute with each other's inverses (case of the second element commuting with the inverse of the first element). (Contributed by SN, 1-Feb-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	grpcominv2	$$⊢\phi \to Y\underset{\dot{}}{+}N\left(X\right)=N\left(X\right)\underset{\dot{}}{+}Y$$

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	7	eqcomd	$$⊢\phi \to Y\underset{\dot{}}{+}X=X\underset{\dot{}}{+}Y$$
9	1 2 3 4 6 5 8	grpcominv1	$$⊢\phi \to Y\underset{\dot{}}{+}N\left(X\right)=N\left(X\right)\underset{\dot{}}{+}Y$$