Metamath Proof Explorer

Theorem abliso

Description: The image of an Abelian group by a group isomorphism is also Abelian. (Contributed by Thierry Arnoux, 8-Mar-2018)

Ref Expression
Assertion abliso ( ( 𝑀 ∈ Abel ∧ 𝐹 ∈ ( 𝑀 GrpIso 𝑁 ) ) → 𝑁 ∈ Abel )

Proof

Step Hyp Ref Expression
1 gimghm ⊢ ( 𝐹 ∈ ( 𝑀 GrpIso 𝑁 ) → 𝐹 ∈ ( 𝑀 GrpHom 𝑁 ) )
2 ghmgrp2 ⊢ ( 𝐹 ∈ ( 𝑀 GrpHom 𝑁 ) → 𝑁 ∈ Grp )
3 1 2 syl ⊢ ( 𝐹 ∈ ( 𝑀 GrpIso 𝑁 ) → 𝑁 ∈ Grp )
4 3 adantl ⊢ ( ( 𝑀 ∈ Abel ∧ 𝐹 ∈ ( 𝑀 GrpIso 𝑁 ) ) → 𝑁 ∈ Grp )
5 4 grpmndd ⊢ ( ( 𝑀 ∈ Abel ∧ 𝐹 ∈ ( 𝑀 GrpIso 𝑁 ) ) → 𝑁 ∈ Mnd )
6 simpll ⊢ ( ( ( 𝑀 ∈ Abel ∧ 𝐹 ∈ ( 𝑀 GrpIso 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑁 ) ∧ 𝑦 ∈ ( Base ‘ 𝑁 ) ) ) → 𝑀 ∈ Abel )
7 eqid ⊢ ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 )
8 eqid ⊢ ( Base ‘ 𝑁 ) = ( Base ‘ 𝑁 )
9 7 8 gimf1o ⊢ ( 𝐹 ∈ ( 𝑀 GrpIso 𝑁 ) → 𝐹 : ( Base ‘ 𝑀 ) –1-1-onto→ ( Base ‘ 𝑁 ) )
10 f1ocnv ⊢ ( 𝐹 : ( Base ‘ 𝑀 ) –1-1-onto→ ( Base ‘ 𝑁 ) → ◡ 𝐹 : ( Base ‘ 𝑁 ) –1-1-onto→ ( Base ‘ 𝑀 ) )
11 f1of ⊢ ( ◡ 𝐹 : ( Base ‘ 𝑁 ) –1-1-onto→ ( Base ‘ 𝑀 ) → ◡ 𝐹 : ( Base ‘ 𝑁 ) ⟶ ( Base ‘ 𝑀 ) )
12 9 10 11 3syl ⊢ ( 𝐹 ∈ ( 𝑀 GrpIso 𝑁 ) → ◡ 𝐹 : ( Base ‘ 𝑁 ) ⟶ ( Base ‘ 𝑀 ) )
13 12 ad2antlr ⊢ ( ( ( 𝑀 ∈ Abel ∧ 𝐹 ∈ ( 𝑀 GrpIso 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑁 ) ∧ 𝑦 ∈ ( Base ‘ 𝑁 ) ) ) → ◡ 𝐹 : ( Base ‘ 𝑁 ) ⟶ ( Base ‘ 𝑀 ) )
14 simprl ⊢ ( ( ( 𝑀 ∈ Abel ∧ 𝐹 ∈ ( 𝑀 GrpIso 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑁 ) ∧ 𝑦 ∈ ( Base ‘ 𝑁 ) ) ) → 𝑥 ∈ ( Base ‘ 𝑁 ) )
15 13 14 ffvelcdmd ⊢ ( ( ( 𝑀 ∈ Abel ∧ 𝐹 ∈ ( 𝑀 GrpIso 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑁 ) ∧ 𝑦 ∈ ( Base ‘ 𝑁 ) ) ) → ( ◡ 𝐹 ‘ 𝑥 ) ∈ ( Base ‘ 𝑀 ) )
16 simprr ⊢ ( ( ( 𝑀 ∈ Abel ∧ 𝐹 ∈ ( 𝑀 GrpIso 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑁 ) ∧ 𝑦 ∈ ( Base ‘ 𝑁 ) ) ) → 𝑦 ∈ ( Base ‘ 𝑁 ) )
17 13 16 ffvelcdmd ⊢ ( ( ( 𝑀 ∈ Abel ∧ 𝐹 ∈ ( 𝑀 GrpIso 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑁 ) ∧ 𝑦 ∈ ( Base ‘ 𝑁 ) ) ) → ( ◡ 𝐹 ‘ 𝑦 ) ∈ ( Base ‘ 𝑀 ) )
18 eqid ⊢ ( +g ‘ 𝑀 ) = ( +g ‘ 𝑀 )
19 7 18 ablcom ⊢ ( ( 𝑀 ∈ Abel ∧ ( ◡ 𝐹 ‘ 𝑥 ) ∈ ( Base ‘ 𝑀 ) ∧ ( ◡ 𝐹 ‘ 𝑦 ) ∈ ( Base ‘ 𝑀 ) ) → ( ( ◡ 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑀 ) ( ◡ 𝐹 ‘ 𝑦 ) ) = ( ( ◡ 𝐹 ‘ 𝑦 ) ( +g ‘ 𝑀 ) ( ◡ 𝐹 ‘ 𝑥 ) ) )
20 6 15 17 19 syl3anc ⊢ ( ( ( 𝑀 ∈ Abel ∧ 𝐹 ∈ ( 𝑀 GrpIso 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑁 ) ∧ 𝑦 ∈ ( Base ‘ 𝑁 ) ) ) → ( ( ◡ 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑀 ) ( ◡ 𝐹 ‘ 𝑦 ) ) = ( ( ◡ 𝐹 ‘ 𝑦 ) ( +g ‘ 𝑀 ) ( ◡ 𝐹 ‘ 𝑥 ) ) )
21 gimcnv ⊢ ( 𝐹 ∈ ( 𝑀 GrpIso 𝑁 ) → ◡ 𝐹 ∈ ( 𝑁 GrpIso 𝑀 ) )
22 21 ad2antlr ⊢ ( ( ( 𝑀 ∈ Abel ∧ 𝐹 ∈ ( 𝑀 GrpIso 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑁 ) ∧ 𝑦 ∈ ( Base ‘ 𝑁 ) ) ) → ◡ 𝐹 ∈ ( 𝑁 GrpIso 𝑀 ) )
23 gimghm ⊢ ( ◡ 𝐹 ∈ ( 𝑁 GrpIso 𝑀 ) → ◡ 𝐹 ∈ ( 𝑁 GrpHom 𝑀 ) )
24 22 23 syl ⊢ ( ( ( 𝑀 ∈ Abel ∧ 𝐹 ∈ ( 𝑀 GrpIso 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑁 ) ∧ 𝑦 ∈ ( Base ‘ 𝑁 ) ) ) → ◡ 𝐹 ∈ ( 𝑁 GrpHom 𝑀 ) )
25 eqid ⊢ ( +g ‘ 𝑁 ) = ( +g ‘ 𝑁 )
26 8 25 18 ghmlin ⊢ ( ( ◡ 𝐹 ∈ ( 𝑁 GrpHom 𝑀 ) ∧ 𝑥 ∈ ( Base ‘ 𝑁 ) ∧ 𝑦 ∈ ( Base ‘ 𝑁 ) ) → ( ◡ 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑁 ) 𝑦 ) ) = ( ( ◡ 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑀 ) ( ◡ 𝐹 ‘ 𝑦 ) ) )
27 24 14 16 26 syl3anc ⊢ ( ( ( 𝑀 ∈ Abel ∧ 𝐹 ∈ ( 𝑀 GrpIso 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑁 ) ∧ 𝑦 ∈ ( Base ‘ 𝑁 ) ) ) → ( ◡ 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑁 ) 𝑦 ) ) = ( ( ◡ 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑀 ) ( ◡ 𝐹 ‘ 𝑦 ) ) )
28 8 25 18 ghmlin ⊢ ( ( ◡ 𝐹 ∈ ( 𝑁 GrpHom 𝑀 ) ∧ 𝑦 ∈ ( Base ‘ 𝑁 ) ∧ 𝑥 ∈ ( Base ‘ 𝑁 ) ) → ( ◡ 𝐹 ‘ ( 𝑦 ( +g ‘ 𝑁 ) 𝑥 ) ) = ( ( ◡ 𝐹 ‘ 𝑦 ) ( +g ‘ 𝑀 ) ( ◡ 𝐹 ‘ 𝑥 ) ) )
29 24 16 14 28 syl3anc ⊢ ( ( ( 𝑀 ∈ Abel ∧ 𝐹 ∈ ( 𝑀 GrpIso 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑁 ) ∧ 𝑦 ∈ ( Base ‘ 𝑁 ) ) ) → ( ◡ 𝐹 ‘ ( 𝑦 ( +g ‘ 𝑁 ) 𝑥 ) ) = ( ( ◡ 𝐹 ‘ 𝑦 ) ( +g ‘ 𝑀 ) ( ◡ 𝐹 ‘ 𝑥 ) ) )
30 20 27 29 3eqtr4d ⊢ ( ( ( 𝑀 ∈ Abel ∧ 𝐹 ∈ ( 𝑀 GrpIso 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑁 ) ∧ 𝑦 ∈ ( Base ‘ 𝑁 ) ) ) → ( ◡ 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑁 ) 𝑦 ) ) = ( ◡ 𝐹 ‘ ( 𝑦 ( +g ‘ 𝑁 ) 𝑥 ) ) )
31 30 fveq2d ⊢ ( ( ( 𝑀 ∈ Abel ∧ 𝐹 ∈ ( 𝑀 GrpIso 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑁 ) ∧ 𝑦 ∈ ( Base ‘ 𝑁 ) ) ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑁 ) 𝑦 ) ) ) = ( 𝐹 ‘ ( ◡ 𝐹 ‘ ( 𝑦 ( +g ‘ 𝑁 ) 𝑥 ) ) ) )
32 9 ad2antlr ⊢ ( ( ( 𝑀 ∈ Abel ∧ 𝐹 ∈ ( 𝑀 GrpIso 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑁 ) ∧ 𝑦 ∈ ( Base ‘ 𝑁 ) ) ) → 𝐹 : ( Base ‘ 𝑀 ) –1-1-onto→ ( Base ‘ 𝑁 ) )
33 3 ad2antlr ⊢ ( ( ( 𝑀 ∈ Abel ∧ 𝐹 ∈ ( 𝑀 GrpIso 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑁 ) ∧ 𝑦 ∈ ( Base ‘ 𝑁 ) ) ) → 𝑁 ∈ Grp )
34 8 25 grpcl ⊢ ( ( 𝑁 ∈ Grp ∧ 𝑥 ∈ ( Base ‘ 𝑁 ) ∧ 𝑦 ∈ ( Base ‘ 𝑁 ) ) → ( 𝑥 ( +g ‘ 𝑁 ) 𝑦 ) ∈ ( Base ‘ 𝑁 ) )
35 33 14 16 34 syl3anc ⊢ ( ( ( 𝑀 ∈ Abel ∧ 𝐹 ∈ ( 𝑀 GrpIso 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑁 ) ∧ 𝑦 ∈ ( Base ‘ 𝑁 ) ) ) → ( 𝑥 ( +g ‘ 𝑁 ) 𝑦 ) ∈ ( Base ‘ 𝑁 ) )
36 f1ocnvfv2 ⊢ ( ( 𝐹 : ( Base ‘ 𝑀 ) –1-1-onto→ ( Base ‘ 𝑁 ) ∧ ( 𝑥 ( +g ‘ 𝑁 ) 𝑦 ) ∈ ( Base ‘ 𝑁 ) ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑁 ) 𝑦 ) ) ) = ( 𝑥 ( +g ‘ 𝑁 ) 𝑦 ) )
37 32 35 36 syl2anc ⊢ ( ( ( 𝑀 ∈ Abel ∧ 𝐹 ∈ ( 𝑀 GrpIso 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑁 ) ∧ 𝑦 ∈ ( Base ‘ 𝑁 ) ) ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑁 ) 𝑦 ) ) ) = ( 𝑥 ( +g ‘ 𝑁 ) 𝑦 ) )
38 8 25 grpcl ⊢ ( ( 𝑁 ∈ Grp ∧ 𝑦 ∈ ( Base ‘ 𝑁 ) ∧ 𝑥 ∈ ( Base ‘ 𝑁 ) ) → ( 𝑦 ( +g ‘ 𝑁 ) 𝑥 ) ∈ ( Base ‘ 𝑁 ) )
39 33 16 14 38 syl3anc ⊢ ( ( ( 𝑀 ∈ Abel ∧ 𝐹 ∈ ( 𝑀 GrpIso 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑁 ) ∧ 𝑦 ∈ ( Base ‘ 𝑁 ) ) ) → ( 𝑦 ( +g ‘ 𝑁 ) 𝑥 ) ∈ ( Base ‘ 𝑁 ) )
40 f1ocnvfv2 ⊢ ( ( 𝐹 : ( Base ‘ 𝑀 ) –1-1-onto→ ( Base ‘ 𝑁 ) ∧ ( 𝑦 ( +g ‘ 𝑁 ) 𝑥 ) ∈ ( Base ‘ 𝑁 ) ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ ( 𝑦 ( +g ‘ 𝑁 ) 𝑥 ) ) ) = ( 𝑦 ( +g ‘ 𝑁 ) 𝑥 ) )
41 32 39 40 syl2anc ⊢ ( ( ( 𝑀 ∈ Abel ∧ 𝐹 ∈ ( 𝑀 GrpIso 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑁 ) ∧ 𝑦 ∈ ( Base ‘ 𝑁 ) ) ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ ( 𝑦 ( +g ‘ 𝑁 ) 𝑥 ) ) ) = ( 𝑦 ( +g ‘ 𝑁 ) 𝑥 ) )
42 31 37 41 3eqtr3d ⊢ ( ( ( 𝑀 ∈ Abel ∧ 𝐹 ∈ ( 𝑀 GrpIso 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑁 ) ∧ 𝑦 ∈ ( Base ‘ 𝑁 ) ) ) → ( 𝑥 ( +g ‘ 𝑁 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑁 ) 𝑥 ) )
43 42 ralrimivva ⊢ ( ( 𝑀 ∈ Abel ∧ 𝐹 ∈ ( 𝑀 GrpIso 𝑁 ) ) → ∀ 𝑥 ∈ ( Base ‘ 𝑁 ) ∀ 𝑦 ∈ ( Base ‘ 𝑁 ) ( 𝑥 ( +g ‘ 𝑁 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑁 ) 𝑥 ) )
44 8 25 iscmn ⊢ ( 𝑁 ∈ CMnd ↔ ( 𝑁 ∈ Mnd ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑁 ) ∀ 𝑦 ∈ ( Base ‘ 𝑁 ) ( 𝑥 ( +g ‘ 𝑁 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑁 ) 𝑥 ) ) )
45 5 43 44 sylanbrc ⊢ ( ( 𝑀 ∈ Abel ∧ 𝐹 ∈ ( 𝑀 GrpIso 𝑁 ) ) → 𝑁 ∈ CMnd )
46 isabl ⊢ ( 𝑁 ∈ Abel ↔ ( 𝑁 ∈ Grp ∧ 𝑁 ∈ CMnd ) )
47 4 45 46 sylanbrc ⊢ ( ( 𝑀 ∈ Abel ∧ 𝐹 ∈ ( 𝑀 GrpIso 𝑁 ) ) → 𝑁 ∈ Abel )