Metamath Proof Explorer


Theorem gicabl

Description: Being Abelian is a group invariant.MOVABLE (Contributed by Stefan O'Rear, 8-Jul-2015)

Ref Expression
Assertion gicabl G 𝑔 H G Abel H Abel

Proof

Step Hyp Ref Expression
1 brgic G 𝑔 H G GrpIso H
2 n0 G GrpIso H x x G GrpIso H
3 gimghm x G GrpIso H x G GrpHom H
4 ghmgrp1 x G GrpHom H G Grp
5 3 4 syl x G GrpIso H G Grp
6 ghmgrp2 x G GrpHom H H Grp
7 3 6 syl x G GrpIso H H Grp
8 5 7 2thd x G GrpIso H G Grp H Grp
9 5 grpmndd x G GrpIso H G Mnd
10 7 grpmndd x G GrpIso H H Mnd
11 9 10 2thd x G GrpIso H G Mnd H Mnd
12 eqid Base G = Base G
13 eqid Base H = Base H
14 12 13 gimf1o x G GrpIso H x : Base G 1-1 onto Base H
15 f1of1 x : Base G 1-1 onto Base H x : Base G 1-1 Base H
16 14 15 syl x G GrpIso H x : Base G 1-1 Base H
17 16 adantr x G GrpIso H y Base G z Base G x : Base G 1-1 Base H
18 5 adantr x G GrpIso H y Base G z Base G G Grp
19 simprl x G GrpIso H y Base G z Base G y Base G
20 simprr x G GrpIso H y Base G z Base G z Base G
21 eqid + G = + G
22 12 21 grpcl G Grp y Base G z Base G y + G z Base G
23 18 19 20 22 syl3anc x G GrpIso H y Base G z Base G y + G z Base G
24 12 21 grpcl G Grp z Base G y Base G z + G y Base G
25 18 20 19 24 syl3anc x G GrpIso H y Base G z Base G z + G y Base G
26 f1fveq x : Base G 1-1 Base H y + G z Base G z + G y Base G x y + G z = x z + G y y + G z = z + G y
27 17 23 25 26 syl12anc x G GrpIso H y Base G z Base G x y + G z = x z + G y y + G z = z + G y
28 3 adantr x G GrpIso H y Base G z Base G x G GrpHom H
29 eqid + H = + H
30 12 21 29 ghmlin x G GrpHom H y Base G z Base G x y + G z = x y + H x z
31 28 19 20 30 syl3anc x G GrpIso H y Base G z Base G x y + G z = x y + H x z
32 12 21 29 ghmlin x G GrpHom H z Base G y Base G x z + G y = x z + H x y
33 28 20 19 32 syl3anc x G GrpIso H y Base G z Base G x z + G y = x z + H x y
34 31 33 eqeq12d x G GrpIso H y Base G z Base G x y + G z = x z + G y x y + H x z = x z + H x y
35 27 34 bitr3d x G GrpIso H y Base G z Base G y + G z = z + G y x y + H x z = x z + H x y
36 35 2ralbidva x G GrpIso H y Base G z Base G y + G z = z + G y y Base G z Base G x y + H x z = x z + H x y
37 f1ofo x : Base G 1-1 onto Base H x : Base G onto Base H
38 foima x : Base G onto Base H x Base G = Base H
39 37 38 syl x : Base G 1-1 onto Base H x Base G = Base H
40 14 39 syl x G GrpIso H x Base G = Base H
41 40 raleqdv x G GrpIso H v x Base G x y + H v = v + H x y v Base H x y + H v = v + H x y
42 f1ofn x : Base G 1-1 onto Base H x Fn Base G
43 14 42 syl x G GrpIso H x Fn Base G
44 ssid Base G Base G
45 oveq2 v = x z x y + H v = x y + H x z
46 oveq1 v = x z v + H x y = x z + H x y
47 45 46 eqeq12d v = x z x y + H v = v + H x y x y + H x z = x z + H x y
48 47 ralima x Fn Base G Base G Base G v x Base G x y + H v = v + H x y z Base G x y + H x z = x z + H x y
49 43 44 48 sylancl x G GrpIso H v x Base G x y + H v = v + H x y z Base G x y + H x z = x z + H x y
50 41 49 bitr3d x G GrpIso H v Base H x y + H v = v + H x y z Base G x y + H x z = x z + H x y
51 50 ralbidv x G GrpIso H y Base G v Base H x y + H v = v + H x y y Base G z Base G x y + H x z = x z + H x y
52 36 51 bitr4d x G GrpIso H y Base G z Base G y + G z = z + G y y Base G v Base H x y + H v = v + H x y
53 40 raleqdv x G GrpIso H w x Base G v Base H w + H v = v + H w w Base H v Base H w + H v = v + H w
54 oveq1 w = x y w + H v = x y + H v
55 oveq2 w = x y v + H w = v + H x y
56 54 55 eqeq12d w = x y w + H v = v + H w x y + H v = v + H x y
57 56 ralbidv w = x y v Base H w + H v = v + H w v Base H x y + H v = v + H x y
58 57 ralima x Fn Base G Base G Base G w x Base G v Base H w + H v = v + H w y Base G v Base H x y + H v = v + H x y
59 43 44 58 sylancl x G GrpIso H w x Base G v Base H w + H v = v + H w y Base G v Base H x y + H v = v + H x y
60 53 59 bitr3d x G GrpIso H w Base H v Base H w + H v = v + H w y Base G v Base H x y + H v = v + H x y
61 52 60 bitr4d x G GrpIso H y Base G z Base G y + G z = z + G y w Base H v Base H w + H v = v + H w
62 11 61 anbi12d x G GrpIso H G Mnd y Base G z Base G y + G z = z + G y H Mnd w Base H v Base H w + H v = v + H w
63 12 21 iscmn G CMnd G Mnd y Base G z Base G y + G z = z + G y
64 13 29 iscmn H CMnd H Mnd w Base H v Base H w + H v = v + H w
65 62 63 64 3bitr4g x G GrpIso H G CMnd H CMnd
66 8 65 anbi12d x G GrpIso H G Grp G CMnd H Grp H CMnd
67 isabl G Abel G Grp G CMnd
68 isabl H Abel H Grp H CMnd
69 66 67 68 3bitr4g x G GrpIso H G Abel H Abel
70 69 exlimiv x x G GrpIso H G Abel H Abel
71 2 70 sylbi G GrpIso H G Abel H Abel
72 1 71 sylbi G 𝑔 H G Abel H Abel