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 ` G )
grpcominv.n
|- N = ( invg ` G )
grpcominv.g
|- ( ph -> G e. Grp )
grpcominv.x
|- ( ph -> X e. B )
grpcominv.y
|- ( ph -> Y e. B )
grpcominv.1
|- ( ph -> ( X .+ Y ) = ( Y .+ X ) )
Assertion grpcominv1
|- ( ph -> ( X .+ ( N ` Y ) ) = ( ( N ` Y ) .+ X ) )

Proof

Step Hyp Ref Expression
1 grpcominv.b
 |-  B = ( Base ` G )
2 grpcominv.p
 |-  .+ = ( +g ` G )
3 grpcominv.n
 |-  N = ( invg ` G )
4 grpcominv.g
 |-  ( ph -> G e. Grp )
5 grpcominv.x
 |-  ( ph -> X e. B )
6 grpcominv.y
 |-  ( ph -> Y e. B )
7 grpcominv.1
 |-  ( ph -> ( X .+ Y ) = ( Y .+ X ) )
8 1 3 4 6 grpinvcld
 |-  ( ph -> ( N ` Y ) e. B )
9 1 2 4 8 6 5 grpassd
 |-  ( ph -> ( ( ( N ` Y ) .+ Y ) .+ X ) = ( ( N ` Y ) .+ ( Y .+ X ) ) )
10 eqid
 |-  ( 0g ` G ) = ( 0g ` G )
11 1 2 10 3 4 6 grplinvd
 |-  ( ph -> ( ( N ` Y ) .+ Y ) = ( 0g ` G ) )
12 11 oveq1d
 |-  ( ph -> ( ( ( N ` Y ) .+ Y ) .+ X ) = ( ( 0g ` G ) .+ X ) )
13 1 2 10 4 5 grplidd
 |-  ( ph -> ( ( 0g ` G ) .+ X ) = X )
14 12 13 eqtr2d
 |-  ( ph -> X = ( ( ( N ` Y ) .+ Y ) .+ X ) )
15 7 oveq2d
 |-  ( ph -> ( ( N ` Y ) .+ ( X .+ Y ) ) = ( ( N ` Y ) .+ ( Y .+ X ) ) )
16 9 14 15 3eqtr4rd
 |-  ( ph -> ( ( N ` Y ) .+ ( X .+ Y ) ) = X )
17 1 2 4 8 5 6 grpassd
 |-  ( ph -> ( ( ( N ` Y ) .+ X ) .+ Y ) = ( ( N ` Y ) .+ ( X .+ Y ) ) )
18 1 2 3 4 5 6 grpasscan2d
 |-  ( ph -> ( ( X .+ ( N ` Y ) ) .+ Y ) = X )
19 16 17 18 3eqtr4rd
 |-  ( ph -> ( ( X .+ ( N ` Y ) ) .+ Y ) = ( ( ( N ` Y ) .+ X ) .+ Y ) )
20 1 2 4 5 8 grpcld
 |-  ( ph -> ( X .+ ( N ` Y ) ) e. B )
21 1 2 4 8 5 grpcld
 |-  ( ph -> ( ( N ` Y ) .+ X ) e. B )
22 1 2 grprcan
 |-  ( ( G e. Grp /\ ( ( X .+ ( N ` Y ) ) e. B /\ ( ( N ` Y ) .+ X ) e. B /\ Y e. B ) ) -> ( ( ( X .+ ( N ` Y ) ) .+ Y ) = ( ( ( N ` Y ) .+ X ) .+ Y ) <-> ( X .+ ( N ` Y ) ) = ( ( N ` Y ) .+ X ) ) )
23 4 20 21 6 22 syl13anc
 |-  ( ph -> ( ( ( X .+ ( N ` Y ) ) .+ Y ) = ( ( ( N ` Y ) .+ X ) .+ Y ) <-> ( X .+ ( N ` Y ) ) = ( ( N ` Y ) .+ X ) ) )
24 19 23 mpbid
 |-  ( ph -> ( X .+ ( N ` Y ) ) = ( ( N ` Y ) .+ X ) )