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 ( 𝐺 ≃𝑔 𝐻 → ( 𝐺 ∈ Abel ↔ 𝐻 ∈ Abel ) )

Proof

Step Hyp Ref Expression
1 brgic ⊢ ( 𝐺 ≃𝑔 𝐻 ↔ ( 𝐺 GrpIso 𝐻 ) ≠ ∅ )
2 n0 ⊢ ( ( 𝐺 GrpIso 𝐻 ) ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ ( 𝐺 GrpIso 𝐻 ) )
3 gimghm ⊢ ( 𝑥 ∈ ( 𝐺 GrpIso 𝐻 ) → 𝑥 ∈ ( 𝐺 GrpHom 𝐻 ) )
4 ghmgrp1 ⊢ ( 𝑥 ∈ ( 𝐺 GrpHom 𝐻 ) → 𝐺 ∈ Grp )
5 3 4 syl ⊢ ( 𝑥 ∈ ( 𝐺 GrpIso 𝐻 ) → 𝐺 ∈ Grp )
6 ghmgrp2 ⊢ ( 𝑥 ∈ ( 𝐺 GrpHom 𝐻 ) → 𝐻 ∈ Grp )
7 3 6 syl ⊢ ( 𝑥 ∈ ( 𝐺 GrpIso 𝐻 ) → 𝐻 ∈ Grp )
8 5 7 2thd ⊢ ( 𝑥 ∈ ( 𝐺 GrpIso 𝐻 ) → ( 𝐺 ∈ Grp ↔ 𝐻 ∈ Grp ) )
9 grpmnd ⊢ ( 𝐺 ∈ Grp → 𝐺 ∈ Mnd )
10 5 9 syl ⊢ ( 𝑥 ∈ ( 𝐺 GrpIso 𝐻 ) → 𝐺 ∈ Mnd )
11 grpmnd ⊢ ( 𝐻 ∈ Grp → 𝐻 ∈ Mnd )
12 7 11 syl ⊢ ( 𝑥 ∈ ( 𝐺 GrpIso 𝐻 ) → 𝐻 ∈ Mnd )
13 10 12 2thd ⊢ ( 𝑥 ∈ ( 𝐺 GrpIso 𝐻 ) → ( 𝐺 ∈ Mnd ↔ 𝐻 ∈ Mnd ) )
14 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
15 eqid ⊢ ( Base ‘ 𝐻 ) = ( Base ‘ 𝐻 )
16 14 15 gimf1o ⊢ ( 𝑥 ∈ ( 𝐺 GrpIso 𝐻 ) → 𝑥 : ( Base ‘ 𝐺 ) –1-1-onto→ ( Base ‘ 𝐻 ) )
17 f1of1 ⊢ ( 𝑥 : ( Base ‘ 𝐺 ) –1-1-onto→ ( Base ‘ 𝐻 ) → 𝑥 : ( Base ‘ 𝐺 ) –1-1→ ( Base ‘ 𝐻 ) )
18 16 17 syl ⊢ ( 𝑥 ∈ ( 𝐺 GrpIso 𝐻 ) → 𝑥 : ( Base ‘ 𝐺 ) –1-1→ ( Base ‘ 𝐻 ) )
19 18 adantr ⊢ ( ( 𝑥 ∈ ( 𝐺 GrpIso 𝐻 ) ∧ ( 𝑦 ∈ ( Base ‘ 𝐺 ) ∧ 𝑧 ∈ ( Base ‘ 𝐺 ) ) ) → 𝑥 : ( Base ‘ 𝐺 ) –1-1→ ( Base ‘ 𝐻 ) )
20 5 adantr ⊢ ( ( 𝑥 ∈ ( 𝐺 GrpIso 𝐻 ) ∧ ( 𝑦 ∈ ( Base ‘ 𝐺 ) ∧ 𝑧 ∈ ( Base ‘ 𝐺 ) ) ) → 𝐺 ∈ Grp )
21 simprl ⊢ ( ( 𝑥 ∈ ( 𝐺 GrpIso 𝐻 ) ∧ ( 𝑦 ∈ ( Base ‘ 𝐺 ) ∧ 𝑧 ∈ ( Base ‘ 𝐺 ) ) ) → 𝑦 ∈ ( Base ‘ 𝐺 ) )
22 simprr ⊢ ( ( 𝑥 ∈ ( 𝐺 GrpIso 𝐻 ) ∧ ( 𝑦 ∈ ( Base ‘ 𝐺 ) ∧ 𝑧 ∈ ( Base ‘ 𝐺 ) ) ) → 𝑧 ∈ ( Base ‘ 𝐺 ) )
23 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
24 14 23 grpcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ∧ 𝑧 ∈ ( Base ‘ 𝐺 ) ) → ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ ( Base ‘ 𝐺 ) )
25 20 21 22 24 syl3anc ⊢ ( ( 𝑥 ∈ ( 𝐺 GrpIso 𝐻 ) ∧ ( 𝑦 ∈ ( Base ‘ 𝐺 ) ∧ 𝑧 ∈ ( Base ‘ 𝐺 ) ) ) → ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ ( Base ‘ 𝐺 ) )
26 14 23 grpcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) → ( 𝑧 ( +g ‘ 𝐺 ) 𝑦 ) ∈ ( Base ‘ 𝐺 ) )
27 20 22 21 26 syl3anc ⊢ ( ( 𝑥 ∈ ( 𝐺 GrpIso 𝐻 ) ∧ ( 𝑦 ∈ ( Base ‘ 𝐺 ) ∧ 𝑧 ∈ ( Base ‘ 𝐺 ) ) ) → ( 𝑧 ( +g ‘ 𝐺 ) 𝑦 ) ∈ ( Base ‘ 𝐺 ) )
28 f1fveq ⊢ ( ( 𝑥 : ( Base ‘ 𝐺 ) –1-1→ ( Base ‘ 𝐻 ) ∧ ( ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ ( Base ‘ 𝐺 ) ∧ ( 𝑧 ( +g ‘ 𝐺 ) 𝑦 ) ∈ ( Base ‘ 𝐺 ) ) ) → ( ( 𝑥 ‘ ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ) = ( 𝑥 ‘ ( 𝑧 ( +g ‘ 𝐺 ) 𝑦 ) ) ↔ ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) = ( 𝑧 ( +g ‘ 𝐺 ) 𝑦 ) ) )
29 19 25 27 28 syl12anc ⊢ ( ( 𝑥 ∈ ( 𝐺 GrpIso 𝐻 ) ∧ ( 𝑦 ∈ ( Base ‘ 𝐺 ) ∧ 𝑧 ∈ ( Base ‘ 𝐺 ) ) ) → ( ( 𝑥 ‘ ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ) = ( 𝑥 ‘ ( 𝑧 ( +g ‘ 𝐺 ) 𝑦 ) ) ↔ ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) = ( 𝑧 ( +g ‘ 𝐺 ) 𝑦 ) ) )
30 3 adantr ⊢ ( ( 𝑥 ∈ ( 𝐺 GrpIso 𝐻 ) ∧ ( 𝑦 ∈ ( Base ‘ 𝐺 ) ∧ 𝑧 ∈ ( Base ‘ 𝐺 ) ) ) → 𝑥 ∈ ( 𝐺 GrpHom 𝐻 ) )
31 eqid ⊢ ( +g ‘ 𝐻 ) = ( +g ‘ 𝐻 )
32 14 23 31 ghmlin ⊢ ( ( 𝑥 ∈ ( 𝐺 GrpHom 𝐻 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ∧ 𝑧 ∈ ( Base ‘ 𝐺 ) ) → ( 𝑥 ‘ ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ) = ( ( 𝑥 ‘ 𝑦 ) ( +g ‘ 𝐻 ) ( 𝑥 ‘ 𝑧 ) ) )
33 30 21 22 32 syl3anc ⊢ ( ( 𝑥 ∈ ( 𝐺 GrpIso 𝐻 ) ∧ ( 𝑦 ∈ ( Base ‘ 𝐺 ) ∧ 𝑧 ∈ ( Base ‘ 𝐺 ) ) ) → ( 𝑥 ‘ ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ) = ( ( 𝑥 ‘ 𝑦 ) ( +g ‘ 𝐻 ) ( 𝑥 ‘ 𝑧 ) ) )
34 14 23 31 ghmlin ⊢ ( ( 𝑥 ∈ ( 𝐺 GrpHom 𝐻 ) ∧ 𝑧 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) → ( 𝑥 ‘ ( 𝑧 ( +g ‘ 𝐺 ) 𝑦 ) ) = ( ( 𝑥 ‘ 𝑧 ) ( +g ‘ 𝐻 ) ( 𝑥 ‘ 𝑦 ) ) )
35 30 22 21 34 syl3anc ⊢ ( ( 𝑥 ∈ ( 𝐺 GrpIso 𝐻 ) ∧ ( 𝑦 ∈ ( Base ‘ 𝐺 ) ∧ 𝑧 ∈ ( Base ‘ 𝐺 ) ) ) → ( 𝑥 ‘ ( 𝑧 ( +g ‘ 𝐺 ) 𝑦 ) ) = ( ( 𝑥 ‘ 𝑧 ) ( +g ‘ 𝐻 ) ( 𝑥 ‘ 𝑦 ) ) )
36 33 35 eqeq12d ⊢ ( ( 𝑥 ∈ ( 𝐺 GrpIso 𝐻 ) ∧ ( 𝑦 ∈ ( Base ‘ 𝐺 ) ∧ 𝑧 ∈ ( Base ‘ 𝐺 ) ) ) → ( ( 𝑥 ‘ ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ) = ( 𝑥 ‘ ( 𝑧 ( +g ‘ 𝐺 ) 𝑦 ) ) ↔ ( ( 𝑥 ‘ 𝑦 ) ( +g ‘ 𝐻 ) ( 𝑥 ‘ 𝑧 ) ) = ( ( 𝑥 ‘ 𝑧 ) ( +g ‘ 𝐻 ) ( 𝑥 ‘ 𝑦 ) ) ) )
37 29 36 bitr3d ⊢ ( ( 𝑥 ∈ ( 𝐺 GrpIso 𝐻 ) ∧ ( 𝑦 ∈ ( Base ‘ 𝐺 ) ∧ 𝑧 ∈ ( Base ‘ 𝐺 ) ) ) → ( ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) = ( 𝑧 ( +g ‘ 𝐺 ) 𝑦 ) ↔ ( ( 𝑥 ‘ 𝑦 ) ( +g ‘ 𝐻 ) ( 𝑥 ‘ 𝑧 ) ) = ( ( 𝑥 ‘ 𝑧 ) ( +g ‘ 𝐻 ) ( 𝑥 ‘ 𝑦 ) ) ) )
38 37 2ralbidva ⊢ ( 𝑥 ∈ ( 𝐺 GrpIso 𝐻 ) → ( ∀ 𝑦 ∈ ( Base ‘ 𝐺 ) ∀ 𝑧 ∈ ( Base ‘ 𝐺 ) ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) = ( 𝑧 ( +g ‘ 𝐺 ) 𝑦 ) ↔ ∀ 𝑦 ∈ ( Base ‘ 𝐺 ) ∀ 𝑧 ∈ ( Base ‘ 𝐺 ) ( ( 𝑥 ‘ 𝑦 ) ( +g ‘ 𝐻 ) ( 𝑥 ‘ 𝑧 ) ) = ( ( 𝑥 ‘ 𝑧 ) ( +g ‘ 𝐻 ) ( 𝑥 ‘ 𝑦 ) ) ) )
39 f1ofo ⊢ ( 𝑥 : ( Base ‘ 𝐺 ) –1-1-onto→ ( Base ‘ 𝐻 ) → 𝑥 : ( Base ‘ 𝐺 ) –onto→ ( Base ‘ 𝐻 ) )
40 foima ⊢ ( 𝑥 : ( Base ‘ 𝐺 ) –onto→ ( Base ‘ 𝐻 ) → ( 𝑥 “ ( Base ‘ 𝐺 ) ) = ( Base ‘ 𝐻 ) )
41 39 40 syl ⊢ ( 𝑥 : ( Base ‘ 𝐺 ) –1-1-onto→ ( Base ‘ 𝐻 ) → ( 𝑥 “ ( Base ‘ 𝐺 ) ) = ( Base ‘ 𝐻 ) )
42 16 41 syl ⊢ ( 𝑥 ∈ ( 𝐺 GrpIso 𝐻 ) → ( 𝑥 “ ( Base ‘ 𝐺 ) ) = ( Base ‘ 𝐻 ) )
43 42 raleqdv ⊢ ( 𝑥 ∈ ( 𝐺 GrpIso 𝐻 ) → ( ∀ 𝑣 ∈ ( 𝑥 “ ( Base ‘ 𝐺 ) ) ( ( 𝑥 ‘ 𝑦 ) ( +g ‘ 𝐻 ) 𝑣 ) = ( 𝑣 ( +g ‘ 𝐻 ) ( 𝑥 ‘ 𝑦 ) ) ↔ ∀ 𝑣 ∈ ( Base ‘ 𝐻 ) ( ( 𝑥 ‘ 𝑦 ) ( +g ‘ 𝐻 ) 𝑣 ) = ( 𝑣 ( +g ‘ 𝐻 ) ( 𝑥 ‘ 𝑦 ) ) ) )
44 f1ofn ⊢ ( 𝑥 : ( Base ‘ 𝐺 ) –1-1-onto→ ( Base ‘ 𝐻 ) → 𝑥 Fn ( Base ‘ 𝐺 ) )
45 16 44 syl ⊢ ( 𝑥 ∈ ( 𝐺 GrpIso 𝐻 ) → 𝑥 Fn ( Base ‘ 𝐺 ) )
46 ssid ⊢ ( Base ‘ 𝐺 ) ⊆ ( Base ‘ 𝐺 )
47 oveq2 ⊢ ( 𝑣 = ( 𝑥 ‘ 𝑧 ) → ( ( 𝑥 ‘ 𝑦 ) ( +g ‘ 𝐻 ) 𝑣 ) = ( ( 𝑥 ‘ 𝑦 ) ( +g ‘ 𝐻 ) ( 𝑥 ‘ 𝑧 ) ) )
48 oveq1 ⊢ ( 𝑣 = ( 𝑥 ‘ 𝑧 ) → ( 𝑣 ( +g ‘ 𝐻 ) ( 𝑥 ‘ 𝑦 ) ) = ( ( 𝑥 ‘ 𝑧 ) ( +g ‘ 𝐻 ) ( 𝑥 ‘ 𝑦 ) ) )
49 47 48 eqeq12d ⊢ ( 𝑣 = ( 𝑥 ‘ 𝑧 ) → ( ( ( 𝑥 ‘ 𝑦 ) ( +g ‘ 𝐻 ) 𝑣 ) = ( 𝑣 ( +g ‘ 𝐻 ) ( 𝑥 ‘ 𝑦 ) ) ↔ ( ( 𝑥 ‘ 𝑦 ) ( +g ‘ 𝐻 ) ( 𝑥 ‘ 𝑧 ) ) = ( ( 𝑥 ‘ 𝑧 ) ( +g ‘ 𝐻 ) ( 𝑥 ‘ 𝑦 ) ) ) )
50 49 ralima ⊢ ( ( 𝑥 Fn ( Base ‘ 𝐺 ) ∧ ( Base ‘ 𝐺 ) ⊆ ( Base ‘ 𝐺 ) ) → ( ∀ 𝑣 ∈ ( 𝑥 “ ( Base ‘ 𝐺 ) ) ( ( 𝑥 ‘ 𝑦 ) ( +g ‘ 𝐻 ) 𝑣 ) = ( 𝑣 ( +g ‘ 𝐻 ) ( 𝑥 ‘ 𝑦 ) ) ↔ ∀ 𝑧 ∈ ( Base ‘ 𝐺 ) ( ( 𝑥 ‘ 𝑦 ) ( +g ‘ 𝐻 ) ( 𝑥 ‘ 𝑧 ) ) = ( ( 𝑥 ‘ 𝑧 ) ( +g ‘ 𝐻 ) ( 𝑥 ‘ 𝑦 ) ) ) )
51 45 46 50 sylancl ⊢ ( 𝑥 ∈ ( 𝐺 GrpIso 𝐻 ) → ( ∀ 𝑣 ∈ ( 𝑥 “ ( Base ‘ 𝐺 ) ) ( ( 𝑥 ‘ 𝑦 ) ( +g ‘ 𝐻 ) 𝑣 ) = ( 𝑣 ( +g ‘ 𝐻 ) ( 𝑥 ‘ 𝑦 ) ) ↔ ∀ 𝑧 ∈ ( Base ‘ 𝐺 ) ( ( 𝑥 ‘ 𝑦 ) ( +g ‘ 𝐻 ) ( 𝑥 ‘ 𝑧 ) ) = ( ( 𝑥 ‘ 𝑧 ) ( +g ‘ 𝐻 ) ( 𝑥 ‘ 𝑦 ) ) ) )
52 43 51 bitr3d ⊢ ( 𝑥 ∈ ( 𝐺 GrpIso 𝐻 ) → ( ∀ 𝑣 ∈ ( Base ‘ 𝐻 ) ( ( 𝑥 ‘ 𝑦 ) ( +g ‘ 𝐻 ) 𝑣 ) = ( 𝑣 ( +g ‘ 𝐻 ) ( 𝑥 ‘ 𝑦 ) ) ↔ ∀ 𝑧 ∈ ( Base ‘ 𝐺 ) ( ( 𝑥 ‘ 𝑦 ) ( +g ‘ 𝐻 ) ( 𝑥 ‘ 𝑧 ) ) = ( ( 𝑥 ‘ 𝑧 ) ( +g ‘ 𝐻 ) ( 𝑥 ‘ 𝑦 ) ) ) )
53 52 ralbidv ⊢ ( 𝑥 ∈ ( 𝐺 GrpIso 𝐻 ) → ( ∀ 𝑦 ∈ ( Base ‘ 𝐺 ) ∀ 𝑣 ∈ ( Base ‘ 𝐻 ) ( ( 𝑥 ‘ 𝑦 ) ( +g ‘ 𝐻 ) 𝑣 ) = ( 𝑣 ( +g ‘ 𝐻 ) ( 𝑥 ‘ 𝑦 ) ) ↔ ∀ 𝑦 ∈ ( Base ‘ 𝐺 ) ∀ 𝑧 ∈ ( Base ‘ 𝐺 ) ( ( 𝑥 ‘ 𝑦 ) ( +g ‘ 𝐻 ) ( 𝑥 ‘ 𝑧 ) ) = ( ( 𝑥 ‘ 𝑧 ) ( +g ‘ 𝐻 ) ( 𝑥 ‘ 𝑦 ) ) ) )
54 38 53 bitr4d ⊢ ( 𝑥 ∈ ( 𝐺 GrpIso 𝐻 ) → ( ∀ 𝑦 ∈ ( Base ‘ 𝐺 ) ∀ 𝑧 ∈ ( Base ‘ 𝐺 ) ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) = ( 𝑧 ( +g ‘ 𝐺 ) 𝑦 ) ↔ ∀ 𝑦 ∈ ( Base ‘ 𝐺 ) ∀ 𝑣 ∈ ( Base ‘ 𝐻 ) ( ( 𝑥 ‘ 𝑦 ) ( +g ‘ 𝐻 ) 𝑣 ) = ( 𝑣 ( +g ‘ 𝐻 ) ( 𝑥 ‘ 𝑦 ) ) ) )
55 42 raleqdv ⊢ ( 𝑥 ∈ ( 𝐺 GrpIso 𝐻 ) → ( ∀ 𝑤 ∈ ( 𝑥 “ ( Base ‘ 𝐺 ) ) ∀ 𝑣 ∈ ( Base ‘ 𝐻 ) ( 𝑤 ( +g ‘ 𝐻 ) 𝑣 ) = ( 𝑣 ( +g ‘ 𝐻 ) 𝑤 ) ↔ ∀ 𝑤 ∈ ( Base ‘ 𝐻 ) ∀ 𝑣 ∈ ( Base ‘ 𝐻 ) ( 𝑤 ( +g ‘ 𝐻 ) 𝑣 ) = ( 𝑣 ( +g ‘ 𝐻 ) 𝑤 ) ) )
56 oveq1 ⊢ ( 𝑤 = ( 𝑥 ‘ 𝑦 ) → ( 𝑤 ( +g ‘ 𝐻 ) 𝑣 ) = ( ( 𝑥 ‘ 𝑦 ) ( +g ‘ 𝐻 ) 𝑣 ) )
57 oveq2 ⊢ ( 𝑤 = ( 𝑥 ‘ 𝑦 ) → ( 𝑣 ( +g ‘ 𝐻 ) 𝑤 ) = ( 𝑣 ( +g ‘ 𝐻 ) ( 𝑥 ‘ 𝑦 ) ) )
58 56 57 eqeq12d ⊢ ( 𝑤 = ( 𝑥 ‘ 𝑦 ) → ( ( 𝑤 ( +g ‘ 𝐻 ) 𝑣 ) = ( 𝑣 ( +g ‘ 𝐻 ) 𝑤 ) ↔ ( ( 𝑥 ‘ 𝑦 ) ( +g ‘ 𝐻 ) 𝑣 ) = ( 𝑣 ( +g ‘ 𝐻 ) ( 𝑥 ‘ 𝑦 ) ) ) )
59 58 ralbidv ⊢ ( 𝑤 = ( 𝑥 ‘ 𝑦 ) → ( ∀ 𝑣 ∈ ( Base ‘ 𝐻 ) ( 𝑤 ( +g ‘ 𝐻 ) 𝑣 ) = ( 𝑣 ( +g ‘ 𝐻 ) 𝑤 ) ↔ ∀ 𝑣 ∈ ( Base ‘ 𝐻 ) ( ( 𝑥 ‘ 𝑦 ) ( +g ‘ 𝐻 ) 𝑣 ) = ( 𝑣 ( +g ‘ 𝐻 ) ( 𝑥 ‘ 𝑦 ) ) ) )
60 59 ralima ⊢ ( ( 𝑥 Fn ( Base ‘ 𝐺 ) ∧ ( Base ‘ 𝐺 ) ⊆ ( Base ‘ 𝐺 ) ) → ( ∀ 𝑤 ∈ ( 𝑥 “ ( Base ‘ 𝐺 ) ) ∀ 𝑣 ∈ ( Base ‘ 𝐻 ) ( 𝑤 ( +g ‘ 𝐻 ) 𝑣 ) = ( 𝑣 ( +g ‘ 𝐻 ) 𝑤 ) ↔ ∀ 𝑦 ∈ ( Base ‘ 𝐺 ) ∀ 𝑣 ∈ ( Base ‘ 𝐻 ) ( ( 𝑥 ‘ 𝑦 ) ( +g ‘ 𝐻 ) 𝑣 ) = ( 𝑣 ( +g ‘ 𝐻 ) ( 𝑥 ‘ 𝑦 ) ) ) )
61 45 46 60 sylancl ⊢ ( 𝑥 ∈ ( 𝐺 GrpIso 𝐻 ) → ( ∀ 𝑤 ∈ ( 𝑥 “ ( Base ‘ 𝐺 ) ) ∀ 𝑣 ∈ ( Base ‘ 𝐻 ) ( 𝑤 ( +g ‘ 𝐻 ) 𝑣 ) = ( 𝑣 ( +g ‘ 𝐻 ) 𝑤 ) ↔ ∀ 𝑦 ∈ ( Base ‘ 𝐺 ) ∀ 𝑣 ∈ ( Base ‘ 𝐻 ) ( ( 𝑥 ‘ 𝑦 ) ( +g ‘ 𝐻 ) 𝑣 ) = ( 𝑣 ( +g ‘ 𝐻 ) ( 𝑥 ‘ 𝑦 ) ) ) )
62 55 61 bitr3d ⊢ ( 𝑥 ∈ ( 𝐺 GrpIso 𝐻 ) → ( ∀ 𝑤 ∈ ( Base ‘ 𝐻 ) ∀ 𝑣 ∈ ( Base ‘ 𝐻 ) ( 𝑤 ( +g ‘ 𝐻 ) 𝑣 ) = ( 𝑣 ( +g ‘ 𝐻 ) 𝑤 ) ↔ ∀ 𝑦 ∈ ( Base ‘ 𝐺 ) ∀ 𝑣 ∈ ( Base ‘ 𝐻 ) ( ( 𝑥 ‘ 𝑦 ) ( +g ‘ 𝐻 ) 𝑣 ) = ( 𝑣 ( +g ‘ 𝐻 ) ( 𝑥 ‘ 𝑦 ) ) ) )
63 54 62 bitr4d ⊢ ( 𝑥 ∈ ( 𝐺 GrpIso 𝐻 ) → ( ∀ 𝑦 ∈ ( Base ‘ 𝐺 ) ∀ 𝑧 ∈ ( Base ‘ 𝐺 ) ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) = ( 𝑧 ( +g ‘ 𝐺 ) 𝑦 ) ↔ ∀ 𝑤 ∈ ( Base ‘ 𝐻 ) ∀ 𝑣 ∈ ( Base ‘ 𝐻 ) ( 𝑤 ( +g ‘ 𝐻 ) 𝑣 ) = ( 𝑣 ( +g ‘ 𝐻 ) 𝑤 ) ) )
64 13 63 anbi12d ⊢ ( 𝑥 ∈ ( 𝐺 GrpIso 𝐻 ) → ( ( 𝐺 ∈ Mnd ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐺 ) ∀ 𝑧 ∈ ( Base ‘ 𝐺 ) ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) = ( 𝑧 ( +g ‘ 𝐺 ) 𝑦 ) ) ↔ ( 𝐻 ∈ Mnd ∧ ∀ 𝑤 ∈ ( Base ‘ 𝐻 ) ∀ 𝑣 ∈ ( Base ‘ 𝐻 ) ( 𝑤 ( +g ‘ 𝐻 ) 𝑣 ) = ( 𝑣 ( +g ‘ 𝐻 ) 𝑤 ) ) ) )
65 14 23 iscmn ⊢ ( 𝐺 ∈ CMnd ↔ ( 𝐺 ∈ Mnd ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐺 ) ∀ 𝑧 ∈ ( Base ‘ 𝐺 ) ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) = ( 𝑧 ( +g ‘ 𝐺 ) 𝑦 ) ) )
66 15 31 iscmn ⊢ ( 𝐻 ∈ CMnd ↔ ( 𝐻 ∈ Mnd ∧ ∀ 𝑤 ∈ ( Base ‘ 𝐻 ) ∀ 𝑣 ∈ ( Base ‘ 𝐻 ) ( 𝑤 ( +g ‘ 𝐻 ) 𝑣 ) = ( 𝑣 ( +g ‘ 𝐻 ) 𝑤 ) ) )
67 64 65 66 3bitr4g ⊢ ( 𝑥 ∈ ( 𝐺 GrpIso 𝐻 ) → ( 𝐺 ∈ CMnd ↔ 𝐻 ∈ CMnd ) )
68 8 67 anbi12d ⊢ ( 𝑥 ∈ ( 𝐺 GrpIso 𝐻 ) → ( ( 𝐺 ∈ Grp ∧ 𝐺 ∈ CMnd ) ↔ ( 𝐻 ∈ Grp ∧ 𝐻 ∈ CMnd ) ) )
69 isabl ⊢ ( 𝐺 ∈ Abel ↔ ( 𝐺 ∈ Grp ∧ 𝐺 ∈ CMnd ) )
70 isabl ⊢ ( 𝐻 ∈ Abel ↔ ( 𝐻 ∈ Grp ∧ 𝐻 ∈ CMnd ) )
71 68 69 70 3bitr4g ⊢ ( 𝑥 ∈ ( 𝐺 GrpIso 𝐻 ) → ( 𝐺 ∈ Abel ↔ 𝐻 ∈ Abel ) )
72 71 exlimiv ⊢ ( ∃ 𝑥 𝑥 ∈ ( 𝐺 GrpIso 𝐻 ) → ( 𝐺 ∈ Abel ↔ 𝐻 ∈ Abel ) )
73 2 72 sylbi ⊢ ( ( 𝐺 GrpIso 𝐻 ) ≠ ∅ → ( 𝐺 ∈ Abel ↔ 𝐻 ∈ Abel ) )
74 1 73 sylbi ⊢ ( 𝐺 ≃𝑔 𝐻 → ( 𝐺 ∈ Abel ↔ 𝐻 ∈ Abel ) )