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	$⊢ (M \in Abel \land F \in (M GrpIso N)) \to N \in Abel$

Proof

Step	Hyp	Ref	Expression
1		gimghm	$⊢ F \in (M GrpIso N) \to F \in (M GrpHom N)$
2		ghmgrp2	$⊢ F \in (M GrpHom N) \to N \in Grp$
3	1 2	syl	$⊢ F \in (M GrpIso N) \to N \in Grp$
4	3	adantl	$⊢ (M \in Abel \land F \in (M GrpIso N)) \to N \in Grp$
5	4	grpmndd	$⊢ (M \in Abel \land F \in (M GrpIso N)) \to N \in Mnd$
6		simpll	$⊢ ((M \in Abel \land F \in (M GrpIso N)) \land (x \in {Base}_{N} \land y \in {Base}_{N})) \to M \in Abel$
7		eqid	$⊢ {Base}_{M} = {Base}_{M}$
8		eqid	$⊢ {Base}_{N} = {Base}_{N}$
9	7 8	gimf1o	$⊢ F \in (M GrpIso N) \to F : {Base}_{M} \underset{1-1 onto}{⟶} {Base}_{N}$
10		f1ocnv	$⊢ F : {Base}_{M} \underset{1-1 onto}{⟶} {Base}_{N} \to F^{-1} : {Base}_{N} \underset{1-1 onto}{⟶} {Base}_{M}$
11		f1of	$⊢ F^{-1} : {Base}_{N} \underset{1-1 onto}{⟶} {Base}_{M} \to F^{-1} : {Base}_{N} ⟶ {Base}_{M}$
12	9 10 11	3syl	$⊢ F \in (M GrpIso N) \to F^{-1} : {Base}_{N} ⟶ {Base}_{M}$
13	12	ad2antlr	$⊢ ((M \in Abel \land F \in (M GrpIso N)) \land (x \in {Base}_{N} \land y \in {Base}_{N})) \to F^{-1} : {Base}_{N} ⟶ {Base}_{M}$
14		simprl	$⊢ ((M \in Abel \land F \in (M GrpIso N)) \land (x \in {Base}_{N} \land y \in {Base}_{N})) \to x \in {Base}_{N}$
15	13 14	ffvelcdmd	$⊢ ((M \in Abel \land F \in (M GrpIso N)) \land (x \in {Base}_{N} \land y \in {Base}_{N})) \to F^{-1} (x) \in {Base}_{M}$
16		simprr	$⊢ ((M \in Abel \land F \in (M GrpIso N)) \land (x \in {Base}_{N} \land y \in {Base}_{N})) \to y \in {Base}_{N}$
17	13 16	ffvelcdmd	$⊢ ((M \in Abel \land F \in (M GrpIso N)) \land (x \in {Base}_{N} \land y \in {Base}_{N})) \to F^{-1} (y) \in {Base}_{M}$
18		eqid	$⊢ +_{M} = +_{M}$
19	7 18	ablcom	$⊢ (M \in Abel \land F^{-1} (x) \in {Base}_{M} \land F^{-1} (y) \in {Base}_{M}) \to F^{-1} (x) +_{M} F^{-1} (y) = F^{-1} (y) +_{M} F^{-1} (x)$
20	6 15 17 19	syl3anc	$⊢ ((M \in Abel \land F \in (M GrpIso N)) \land (x \in {Base}_{N} \land y \in {Base}_{N})) \to F^{-1} (x) +_{M} F^{-1} (y) = F^{-1} (y) +_{M} F^{-1} (x)$
21		gimcnv	$⊢ F \in (M GrpIso N) \to F^{-1} \in (N GrpIso M)$
22	21	ad2antlr	$⊢ ((M \in Abel \land F \in (M GrpIso N)) \land (x \in {Base}_{N} \land y \in {Base}_{N})) \to F^{-1} \in (N GrpIso M)$
23		gimghm	$⊢ F^{-1} \in (N GrpIso M) \to F^{-1} \in (N GrpHom M)$
24	22 23	syl	$⊢ ((M \in Abel \land F \in (M GrpIso N)) \land (x \in {Base}_{N} \land y \in {Base}_{N})) \to F^{-1} \in (N GrpHom M)$
25		eqid	$⊢ +_{N} = +_{N}$
26	8 25 18	ghmlin	$⊢ (F^{-1} \in (N GrpHom M) \land x \in {Base}_{N} \land y \in {Base}_{N}) \to F^{-1} (x +_{N} y) = F^{-1} (x) +_{M} F^{-1} (y)$
27	24 14 16 26	syl3anc	$⊢ ((M \in Abel \land F \in (M GrpIso N)) \land (x \in {Base}_{N} \land y \in {Base}_{N})) \to F^{-1} (x +_{N} y) = F^{-1} (x) +_{M} F^{-1} (y)$
28	8 25 18	ghmlin	$⊢ (F^{-1} \in (N GrpHom M) \land y \in {Base}_{N} \land x \in {Base}_{N}) \to F^{-1} (y +_{N} x) = F^{-1} (y) +_{M} F^{-1} (x)$
29	24 16 14 28	syl3anc	$⊢ ((M \in Abel \land F \in (M GrpIso N)) \land (x \in {Base}_{N} \land y \in {Base}_{N})) \to F^{-1} (y +_{N} x) = F^{-1} (y) +_{M} F^{-1} (x)$
30	20 27 29	3eqtr4d	$⊢ ((M \in Abel \land F \in (M GrpIso N)) \land (x \in {Base}_{N} \land y \in {Base}_{N})) \to F^{-1} (x +_{N} y) = F^{-1} (y +_{N} x)$
31	30	fveq2d	$⊢ ((M \in Abel \land F \in (M GrpIso N)) \land (x \in {Base}_{N} \land y \in {Base}_{N})) \to F (F^{-1} (x +_{N} y)) = F (F^{-1} (y +_{N} x))$
32	9	ad2antlr	$⊢ ((M \in Abel \land F \in (M GrpIso N)) \land (x \in {Base}_{N} \land y \in {Base}_{N})) \to F : {Base}_{M} \underset{1-1 onto}{⟶} {Base}_{N}$
33	3	ad2antlr	$⊢ ((M \in Abel \land F \in (M GrpIso N)) \land (x \in {Base}_{N} \land y \in {Base}_{N})) \to N \in Grp$
34	8 25	grpcl	$⊢ (N \in Grp \land x \in {Base}_{N} \land y \in {Base}_{N}) \to x +_{N} y \in {Base}_{N}$
35	33 14 16 34	syl3anc	$⊢ ((M \in Abel \land F \in (M GrpIso N)) \land (x \in {Base}_{N} \land y \in {Base}_{N})) \to x +_{N} y \in {Base}_{N}$
36		f1ocnvfv2	$⊢ (F : {Base}_{M} \underset{1-1 onto}{⟶} {Base}_{N} \land x +_{N} y \in {Base}_{N}) \to F (F^{-1} (x +_{N} y)) = x +_{N} y$
37	32 35 36	syl2anc	$⊢ ((M \in Abel \land F \in (M GrpIso N)) \land (x \in {Base}_{N} \land y \in {Base}_{N})) \to F (F^{-1} (x +_{N} y)) = x +_{N} y$
38	8 25	grpcl	$⊢ (N \in Grp \land y \in {Base}_{N} \land x \in {Base}_{N}) \to y +_{N} x \in {Base}_{N}$
39	33 16 14 38	syl3anc	$⊢ ((M \in Abel \land F \in (M GrpIso N)) \land (x \in {Base}_{N} \land y \in {Base}_{N})) \to y +_{N} x \in {Base}_{N}$
40		f1ocnvfv2	$⊢ (F : {Base}_{M} \underset{1-1 onto}{⟶} {Base}_{N} \land y +_{N} x \in {Base}_{N}) \to F (F^{-1} (y +_{N} x)) = y +_{N} x$
41	32 39 40	syl2anc	$⊢ ((M \in Abel \land F \in (M GrpIso N)) \land (x \in {Base}_{N} \land y \in {Base}_{N})) \to F (F^{-1} (y +_{N} x)) = y +_{N} x$
42	31 37 41	3eqtr3d	$⊢ ((M \in Abel \land F \in (M GrpIso N)) \land (x \in {Base}_{N} \land y \in {Base}_{N})) \to x +_{N} y = y +_{N} x$
43	42	ralrimivva	$⊢ (M \in Abel \land F \in (M GrpIso N)) \to \forall x \in {Base}_{N} \forall y \in {Base}_{N} x +_{N} y = y +_{N} x$
44	8 25	iscmn	$⊢ N \in CMnd \leftrightarrow (N \in Mnd \land \forall x \in {Base}_{N} \forall y \in {Base}_{N} x +_{N} y = y +_{N} x)$
45	5 43 44	sylanbrc	$⊢ (M \in Abel \land F \in (M GrpIso N)) \to N \in CMnd$
46		isabl	$⊢ N \in Abel \leftrightarrow (N \in Grp \land N \in CMnd)$
47	4 45 46	sylanbrc	$⊢ (M \in Abel \land F \in (M GrpIso N)) \to N \in Abel$

Metamath Proof Explorer

Theorem abliso

Proof