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 · ˙ = G
mulginvcom.i I = inv g G
Assertion mulginvcom G Grp N X B N · ˙ I X = I N · ˙ X

Proof

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