This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) )