Metamath Proof Explorer

Theorem mulginvcom

Description: The group multiple operator commutes with the group inverse function. (Contributed by Paul Chapman, 17-Apr-2009) (Revised by AV, 31-Aug-2021)

Ref Expression
Hypotheses mulginvcom.b 
|- B = ( Base ` G )
mulginvcom.t 
|- .x. = ( .g ` G )
mulginvcom.i 
|- I = ( invg ` G )
Assertion mulginvcom 
|- ( ( G e. Grp /\ N e. ZZ /\ X e. B ) -> ( N .x. ( I ` X ) ) = ( I ` ( N .x. X ) ) )

Proof

Step Hyp Ref Expression
1 mulginvcom.b 
 |-  B = ( Base ` G )
2 mulginvcom.t 
 |-  .x. = ( .g ` G )
3 mulginvcom.i 
 |-  I = ( invg ` G )
4 oveq1 
 |-  ( x = 0 -> ( x .x. ( I ` X ) ) = ( 0 .x. ( I ` X ) ) )
5 fvoveq1 
 |-  ( x = 0 -> ( I ` ( x .x. X ) ) = ( I ` ( 0 .x. X ) ) )
6 4 5 eqeq12d 
 |-  ( x = 0 -> ( ( x .x. ( I ` X ) ) = ( I ` ( x .x. X ) ) <-> ( 0 .x. ( I ` X ) ) = ( I ` ( 0 .x. X ) ) ) )
7 oveq1 
 |-  ( x = y -> ( x .x. ( I ` X ) ) = ( y .x. ( I ` X ) ) )
8 fvoveq1 
 |-  ( x = y -> ( I ` ( x .x. X ) ) = ( I ` ( y .x. X ) ) )
9 7 8 eqeq12d 
 |-  ( x = y -> ( ( x .x. ( I ` X ) ) = ( I ` ( x .x. X ) ) <-> ( y .x. ( I ` X ) ) = ( I ` ( y .x. X ) ) ) )
10 oveq1 
 |-  ( x = ( y + 1 ) -> ( x .x. ( I ` X ) ) = ( ( y + 1 ) .x. ( I ` X ) ) )
11 fvoveq1 
 |-  ( x = ( y + 1 ) -> ( I ` ( x .x. X ) ) = ( I ` ( ( y + 1 ) .x. X ) ) )
12 10 11 eqeq12d 
 |-  ( x = ( y + 1 ) -> ( ( x .x. ( I ` X ) ) = ( I ` ( x .x. X ) ) <-> ( ( y + 1 ) .x. ( I ` X ) ) = ( I ` ( ( y + 1 ) .x. X ) ) ) )
13 oveq1 
 |-  ( x = -u y -> ( x .x. ( I ` X ) ) = ( -u y .x. ( I ` X ) ) )
14 fvoveq1 
 |-  ( x = -u y -> ( I ` ( x .x. X ) ) = ( I ` ( -u y .x. X ) ) )
15 13 14 eqeq12d 
 |-  ( x = -u y -> ( ( x .x. ( I ` X ) ) = ( I ` ( x .x. X ) ) <-> ( -u y .x. ( I ` X ) ) = ( I ` ( -u y .x. X ) ) ) )
16 oveq1 
 |-  ( x = N -> ( x .x. ( I ` X ) ) = ( N .x. ( I ` X ) ) )
17 fvoveq1 
 |-  ( x = N -> ( I ` ( x .x. X ) ) = ( I ` ( N .x. X ) ) )
18 16 17 eqeq12d 
 |-  ( x = N -> ( ( x .x. ( I ` X ) ) = ( I ` ( x .x. X ) ) <-> ( N .x. ( I ` X ) ) = ( I ` ( N .x. X ) ) ) )
19 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
20 19 3 grpinvid 
 |-  ( G e. Grp -> ( I ` ( 0g ` G ) ) = ( 0g ` G ) )
21 20 eqcomd 
 |-  ( G e. Grp -> ( 0g ` G ) = ( I ` ( 0g ` G ) ) )
22 21 adantr 
 |-  ( ( G e. Grp /\ X e. B ) -> ( 0g ` G ) = ( I ` ( 0g ` G ) ) )
23 1 3 grpinvcl 
 |-  ( ( G e. Grp /\ X e. B ) -> ( I ` X ) e. B )
24 1 19 2 mulg0 
 |-  ( ( I ` X ) e. B -> ( 0 .x. ( I ` X ) ) = ( 0g ` G ) )
25 23 24 syl 
 |-  ( ( G e. Grp /\ X e. B ) -> ( 0 .x. ( I ` X ) ) = ( 0g ` G ) )
26 1 19 2 mulg0 
 |-  ( X e. B -> ( 0 .x. X ) = ( 0g ` G ) )
27 26 adantl 
 |-  ( ( G e. Grp /\ X e. B ) -> ( 0 .x. X ) = ( 0g ` G ) )
28 27 fveq2d 
 |-  ( ( G e. Grp /\ X e. B ) -> ( I ` ( 0 .x. X ) ) = ( I ` ( 0g ` G ) ) )
29 22 25 28 3eqtr4d 
 |-  ( ( G e. Grp /\ X e. B ) -> ( 0 .x. ( I ` X ) ) = ( I ` ( 0 .x. X ) ) )
30 oveq2 
 |-  ( ( y .x. ( I ` X ) ) = ( I ` ( y .x. X ) ) -> ( ( I ` X ) ( +g ` G ) ( y .x. ( I ` X ) ) ) = ( ( I ` X ) ( +g ` G ) ( I ` ( y .x. X ) ) ) )
31 30 adantl 
 |-  ( ( ( G e. Grp /\ y e. NN0 /\ X e. B ) /\ ( y .x. ( I ` X ) ) = ( I ` ( y .x. X ) ) ) -> ( ( I ` X ) ( +g ` G ) ( y .x. ( I ` X ) ) ) = ( ( I ` X ) ( +g ` G ) ( I ` ( y .x. X ) ) ) )
32 grpmnd 
 |-  ( G e. Grp -> G e. Mnd )
33 32 3ad2ant1 
 |-  ( ( G e. Grp /\ y e. NN0 /\ X e. B ) -> G e. Mnd )
34 simp2 
 |-  ( ( G e. Grp /\ y e. NN0 /\ X e. B ) -> y e. NN0 )
35 23 3adant2 
 |-  ( ( G e. Grp /\ y e. NN0 /\ X e. B ) -> ( I ` X ) e. B )
36 eqid 
 |-  ( +g ` G ) = ( +g ` G )
37 1 2 36 mulgnn0p1 
 |-  ( ( G e. Mnd /\ y e. NN0 /\ ( I ` X ) e. B ) -> ( ( y + 1 ) .x. ( I ` X ) ) = ( ( y .x. ( I ` X ) ) ( +g ` G ) ( I ` X ) ) )
38 33 34 35 37 syl3anc 
 |-  ( ( G e. Grp /\ y e. NN0 /\ X e. B ) -> ( ( y + 1 ) .x. ( I ` X ) ) = ( ( y .x. ( I ` X ) ) ( +g ` G ) ( I ` X ) ) )
39 simp1 
 |-  ( ( G e. Grp /\ y e. NN0 /\ X e. B ) -> G e. Grp )
40 nn0z 
 |-  ( y e. NN0 -> y e. ZZ )
41 40 3ad2ant2 
 |-  ( ( G e. Grp /\ y e. NN0 /\ X e. B ) -> y e. ZZ )
42 1 2 36 mulgaddcom 
 |-  ( ( G e. Grp /\ y e. ZZ /\ ( I ` X ) e. B ) -> ( ( y .x. ( I ` X ) ) ( +g ` G ) ( I ` X ) ) = ( ( I ` X ) ( +g ` G ) ( y .x. ( I ` X ) ) ) )
43 39 41 35 42 syl3anc 
 |-  ( ( G e. Grp /\ y e. NN0 /\ X e. B ) -> ( ( y .x. ( I ` X ) ) ( +g ` G ) ( I ` X ) ) = ( ( I ` X ) ( +g ` G ) ( y .x. ( I ` X ) ) ) )
44 38 43 eqtrd 
 |-  ( ( G e. Grp /\ y e. NN0 /\ X e. B ) -> ( ( y + 1 ) .x. ( I ` X ) ) = ( ( I ` X ) ( +g ` G ) ( y .x. ( I ` X ) ) ) )
45 44 adantr 
 |-  ( ( ( G e. Grp /\ y e. NN0 /\ X e. B ) /\ ( y .x. ( I ` X ) ) = ( I ` ( y .x. X ) ) ) -> ( ( y + 1 ) .x. ( I ` X ) ) = ( ( I ` X ) ( +g ` G ) ( y .x. ( I ` X ) ) ) )
46 1 2 36 mulgnn0p1 
 |-  ( ( G e. Mnd /\ y e. NN0 /\ X e. B ) -> ( ( y + 1 ) .x. X ) = ( ( y .x. X ) ( +g ` G ) X ) )
47 32 46 syl3an1 
 |-  ( ( G e. Grp /\ y e. NN0 /\ X e. B ) -> ( ( y + 1 ) .x. X ) = ( ( y .x. X ) ( +g ` G ) X ) )
48 47 fveq2d 
 |-  ( ( G e. Grp /\ y e. NN0 /\ X e. B ) -> ( I ` ( ( y + 1 ) .x. X ) ) = ( I ` ( ( y .x. X ) ( +g ` G ) X ) ) )
49 1 2 mulgcl 
 |-  ( ( G e. Grp /\ y e. ZZ /\ X e. B ) -> ( y .x. X ) e. B )
50 40 49 syl3an2 
 |-  ( ( G e. Grp /\ y e. NN0 /\ X e. B ) -> ( y .x. X ) e. B )
51 1 36 3 grpinvadd 
 |-  ( ( G e. Grp /\ ( y .x. X ) e. B /\ X e. B ) -> ( I ` ( ( y .x. X ) ( +g ` G ) X ) ) = ( ( I ` X ) ( +g ` G ) ( I ` ( y .x. X ) ) ) )
52 50 51 syld3an2 
 |-  ( ( G e. Grp /\ y e. NN0 /\ X e. B ) -> ( I ` ( ( y .x. X ) ( +g ` G ) X ) ) = ( ( I ` X ) ( +g ` G ) ( I ` ( y .x. X ) ) ) )
53 48 52 eqtrd 
 |-  ( ( G e. Grp /\ y e. NN0 /\ X e. B ) -> ( I ` ( ( y + 1 ) .x. X ) ) = ( ( I ` X ) ( +g ` G ) ( I ` ( y .x. X ) ) ) )
54 53 adantr 
 |-  ( ( ( G e. Grp /\ y e. NN0 /\ X e. B ) /\ ( y .x. ( I ` X ) ) = ( I ` ( y .x. X ) ) ) -> ( I ` ( ( y + 1 ) .x. X ) ) = ( ( I ` X ) ( +g ` G ) ( I ` ( y .x. X ) ) ) )
55 31 45 54 3eqtr4d 
 |-  ( ( ( G e. Grp /\ y e. NN0 /\ X e. B ) /\ ( y .x. ( I ` X ) ) = ( I ` ( y .x. X ) ) ) -> ( ( y + 1 ) .x. ( I ` X ) ) = ( I ` ( ( y + 1 ) .x. X ) ) )
56 55 3exp1 
 |-  ( G e. Grp -> ( y e. NN0 -> ( X e. B -> ( ( y .x. ( I ` X ) ) = ( I ` ( y .x. X ) ) -> ( ( y + 1 ) .x. ( I ` X ) ) = ( I ` ( ( y + 1 ) .x. X ) ) ) ) ) )
57 56 com23 
 |-  ( G e. Grp -> ( X e. B -> ( y e. NN0 -> ( ( y .x. ( I ` X ) ) = ( I ` ( y .x. X ) ) -> ( ( y + 1 ) .x. ( I ` X ) ) = ( I ` ( ( y + 1 ) .x. X ) ) ) ) ) )
58 57 imp 
 |-  ( ( G e. Grp /\ X e. B ) -> ( y e. NN0 -> ( ( y .x. ( I ` X ) ) = ( I ` ( y .x. X ) ) -> ( ( y + 1 ) .x. ( I ` X ) ) = ( I ` ( ( y + 1 ) .x. X ) ) ) ) )
59 nnz 
 |-  ( y e. NN -> y e. ZZ )
60 23 3adant2 
 |-  ( ( G e. Grp /\ y e. ZZ /\ X e. B ) -> ( I ` X ) e. B )
61 1 2 3 mulgneg 
 |-  ( ( G e. Grp /\ y e. ZZ /\ ( I ` X ) e. B ) -> ( -u y .x. ( I ` X ) ) = ( I ` ( y .x. ( I ` X ) ) ) )
62 60 61 syld3an3 
 |-  ( ( G e. Grp /\ y e. ZZ /\ X e. B ) -> ( -u y .x. ( I ` X ) ) = ( I ` ( y .x. ( I ` X ) ) ) )
63 62 adantr 
 |-  ( ( ( G e. Grp /\ y e. ZZ /\ X e. B ) /\ ( y .x. ( I ` X ) ) = ( I ` ( y .x. X ) ) ) -> ( -u y .x. ( I ` X ) ) = ( I ` ( y .x. ( I ` X ) ) ) )
64 1 2 3 mulgneg 
 |-  ( ( G e. Grp /\ y e. ZZ /\ X e. B ) -> ( -u y .x. X ) = ( I ` ( y .x. X ) ) )
65 64 adantr 
 |-  ( ( ( G e. Grp /\ y e. ZZ /\ X e. B ) /\ ( y .x. ( I ` X ) ) = ( I ` ( y .x. X ) ) ) -> ( -u y .x. X ) = ( I ` ( y .x. X ) ) )
66 simpr 
 |-  ( ( ( G e. Grp /\ y e. ZZ /\ X e. B ) /\ ( y .x. ( I ` X ) ) = ( I ` ( y .x. X ) ) ) -> ( y .x. ( I ` X ) ) = ( I ` ( y .x. X ) ) )
67 65 66 eqtr4d 
 |-  ( ( ( G e. Grp /\ y e. ZZ /\ X e. B ) /\ ( y .x. ( I ` X ) ) = ( I ` ( y .x. X ) ) ) -> ( -u y .x. X ) = ( y .x. ( I ` X ) ) )
68 67 fveq2d 
 |-  ( ( ( G e. Grp /\ y e. ZZ /\ X e. B ) /\ ( y .x. ( I ` X ) ) = ( I ` ( y .x. X ) ) ) -> ( I ` ( -u y .x. X ) ) = ( I ` ( y .x. ( I ` X ) ) ) )
69 63 68 eqtr4d 
 |-  ( ( ( G e. Grp /\ y e. ZZ /\ X e. B ) /\ ( y .x. ( I ` X ) ) = ( I ` ( y .x. X ) ) ) -> ( -u y .x. ( I ` X ) ) = ( I ` ( -u y .x. X ) ) )
70 69 3exp1 
 |-  ( G e. Grp -> ( y e. ZZ -> ( X e. B -> ( ( y .x. ( I ` X ) ) = ( I ` ( y .x. X ) ) -> ( -u y .x. ( I ` X ) ) = ( I ` ( -u y .x. X ) ) ) ) ) )
71 70 com23 
 |-  ( G e. Grp -> ( X e. B -> ( y e. ZZ -> ( ( y .x. ( I ` X ) ) = ( I ` ( y .x. X ) ) -> ( -u y .x. ( I ` X ) ) = ( I ` ( -u y .x. X ) ) ) ) ) )
72 71 imp 
 |-  ( ( G e. Grp /\ X e. B ) -> ( y e. ZZ -> ( ( y .x. ( I ` X ) ) = ( I ` ( y .x. X ) ) -> ( -u y .x. ( I ` X ) ) = ( I ` ( -u y .x. X ) ) ) ) )
73 59 72 syl5 
 |-  ( ( G e. Grp /\ X e. B ) -> ( y e. NN -> ( ( y .x. ( I ` X ) ) = ( I ` ( y .x. X ) ) -> ( -u y .x. ( I ` X ) ) = ( I ` ( -u y .x. X ) ) ) ) )
74 6 9 12 15 18 29 58 73 zindd 
 |-  ( ( G e. Grp /\ X e. B ) -> ( N e. ZZ -> ( N .x. ( I ` X ) ) = ( I ` ( N .x. X ) ) ) )
75 74 ex 
 |-  ( G e. Grp -> ( X e. B -> ( N e. ZZ -> ( N .x. ( I ` X ) ) = ( I ` ( N .x. X ) ) ) ) )
76 75 com23 
 |-  ( G e. Grp -> ( N e. ZZ -> ( X e. B -> ( N .x. ( I ` X ) ) = ( I ` ( N .x. X ) ) ) ) )
77 76 3imp 
 |-  ( ( G e. Grp /\ N e. ZZ /\ X e. B ) -> ( N .x. ( I ` X ) ) = ( I ` ( N .x. X ) ) )