Metamath Proof Explorer


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 = Base G
grpcominv.p + ˙ = + G
grpcominv.n N = inv g G
grpcominv.g φ G Grp
grpcominv.x φ X B
grpcominv.y φ Y B
grpcominv.1 φ X + ˙ Y = Y + ˙ X
Assertion grpcominv2 φ Y + ˙ N X = N X + ˙ Y

Proof

Step Hyp Ref Expression
1 grpcominv.b B = Base G
2 grpcominv.p + ˙ = + G
3 grpcominv.n N = inv g G
4 grpcominv.g φ G Grp
5 grpcominv.x φ X B
6 grpcominv.y φ Y B
7 grpcominv.1 φ X + ˙ Y = Y + ˙ X
8 7 eqcomd φ Y + ˙ X = X + ˙ Y
9 1 2 3 4 6 5 8 grpcominv1 φ Y + ˙ N X = N X + ˙ Y