Metamath Proof Explorer


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 = 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 grpcominv1 φ X + ˙ N Y = N Y + ˙ X

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 1 3 4 6 grpinvcld φ N Y B
9 1 2 4 8 6 5 grpassd φ N Y + ˙ Y + ˙ X = N Y + ˙ Y + ˙ X
10 eqid 0 G = 0 G
11 1 2 10 3 4 6 grplinvd φ N Y + ˙ Y = 0 G
12 11 oveq1d φ N Y + ˙ Y + ˙ X = 0 G + ˙ X
13 1 2 10 4 5 grplidd φ 0 G + ˙ X = X
14 12 13 eqtr2d φ X = N Y + ˙ Y + ˙ X
15 7 oveq2d φ N Y + ˙ X + ˙ Y = N Y + ˙ Y + ˙ X
16 9 14 15 3eqtr4rd φ N Y + ˙ X + ˙ Y = X
17 1 2 4 8 5 6 grpassd φ N Y + ˙ X + ˙ Y = N Y + ˙ X + ˙ Y
18 1 2 3 4 5 6 grpasscan2d φ X + ˙ N Y + ˙ Y = X
19 16 17 18 3eqtr4rd φ X + ˙ N Y + ˙ Y = N Y + ˙ X + ˙ Y
20 1 2 4 5 8 grpcld φ X + ˙ N Y B
21 1 2 4 8 5 grpcld φ N Y + ˙ X B
22 1 2 grprcan G Grp X + ˙ N Y B N Y + ˙ X B Y B X + ˙ N Y + ˙ Y = N Y + ˙ X + ˙ Y X + ˙ N Y = N Y + ˙ X
23 4 20 21 6 22 syl13anc φ X + ˙ N Y + ˙ Y = N Y + ˙ X + ˙ Y X + ˙ N Y = N Y + ˙ X
24 19 23 mpbid φ X + ˙ N Y = N Y + ˙ X