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