Theorem gicabl 43846

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

Assertion

Ref	Expression
gicabl	⊢ (𝐺 ≃𝑔 𝐻 → (𝐺 ∈ Abel ↔ 𝐻 ∈ Abel))

Proof of Theorem gicabl

Dummy variables 𝑤 𝑣 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		brgic 19335	. 2 ⊢ (𝐺 ≃𝑔 𝐻 ↔ (𝐺 GrpIso 𝐻) ≠ ∅)
2		n0 4307	. . 3 ⊢ ((𝐺 GrpIso 𝐻) ≠ ∅ ↔ ∃𝑥 𝑥 ∈ (𝐺 GrpIso 𝐻))
3		gimghm 19329	. . . . . . . 8 ⊢ (𝑥 ∈ (𝐺 GrpIso 𝐻) → 𝑥 ∈ (𝐺 GrpHom 𝐻))
4		ghmgrp1 19283	. . . . . . . 8 ⊢ (𝑥 ∈ (𝐺 GrpHom 𝐻) → 𝐺 ∈ Grp)
5	3, 4	syl 18	. . . . . . 7 ⊢ (𝑥 ∈ (𝐺 GrpIso 𝐻) → 𝐺 ∈ Grp)
6		ghmgrp2 19284	. . . . . . . 8 ⊢ (𝑥 ∈ (𝐺 GrpHom 𝐻) → 𝐻 ∈ Grp)
7	3, 6	syl 18	. . . . . . 7 ⊢ (𝑥 ∈ (𝐺 GrpIso 𝐻) → 𝐻 ∈ Grp)
8	5, 7	2thd 268	. . . . . 6 ⊢ (𝑥 ∈ (𝐺 GrpIso 𝐻) → (𝐺 ∈ Grp ↔ 𝐻 ∈ Grp))
9	5	grpmndd 19008	. . . . . . . . 9 ⊢ (𝑥 ∈ (𝐺 GrpIso 𝐻) → 𝐺 ∈ Mnd)
10	7	grpmndd 19008	. . . . . . . . 9 ⊢ (𝑥 ∈ (𝐺 GrpIso 𝐻) → 𝐻 ∈ Mnd)
11	9, 10	2thd 268	. . . . . . . 8 ⊢ (𝑥 ∈ (𝐺 GrpIso 𝐻) → (𝐺 ∈ Mnd ↔ 𝐻 ∈ Mnd))
12		eqid 2763	. . . . . . . . . . . . . . . 16 ⊢ (Base‘𝐺) = (Base‘𝐺)
13		eqid 2763	. . . . . . . . . . . . . . . 16 ⊢ (Base‘𝐻) = (Base‘𝐻)
14	12, 13	gimf1o 19328	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (𝐺 GrpIso 𝐻) → 𝑥:(Base‘𝐺)–1-1-onto→(Base‘𝐻))
15		f1of1 6819	. . . . . . . . . . . . . . 15 ⊢ (𝑥:(Base‘𝐺)–1-1-onto→(Base‘𝐻) → 𝑥:(Base‘𝐺)–1-1→(Base‘𝐻))
16	14, 15	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (𝐺 GrpIso 𝐻) → 𝑥:(Base‘𝐺)–1-1→(Base‘𝐻))
17	16	adantr 485	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ (𝐺 GrpIso 𝐻) ∧ (𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) → 𝑥:(Base‘𝐺)–1-1→(Base‘𝐻))
18	5	adantr 485	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ (𝐺 GrpIso 𝐻) ∧ (𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) → 𝐺 ∈ Grp)
19		simprl 782	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ (𝐺 GrpIso 𝐻) ∧ (𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) → 𝑦 ∈ (Base‘𝐺))
20		simprr 784	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ (𝐺 GrpIso 𝐻) ∧ (𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) → 𝑧 ∈ (Base‘𝐺))
21		eqid 2763	. . . . . . . . . . . . . . 15 ⊢ (+g‘𝐺) = (+g‘𝐺)
22	12, 21	grpcl 19003	. . . . . . . . . . . . . 14 ⊢ ((𝐺 ∈ Grp ∧ 𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺)) → (𝑦(+g‘𝐺)𝑧) ∈ (Base‘𝐺))
23	18, 19, 20, 22	syl3anc 1398	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ (𝐺 GrpIso 𝐻) ∧ (𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) → (𝑦(+g‘𝐺)𝑧) ∈ (Base‘𝐺))
24	12, 21	grpcl 19003	. . . . . . . . . . . . . 14 ⊢ ((𝐺 ∈ Grp ∧ 𝑧 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) → (𝑧(+g‘𝐺)𝑦) ∈ (Base‘𝐺))
25	18, 20, 19, 24	syl3anc 1398	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ (𝐺 GrpIso 𝐻) ∧ (𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) → (𝑧(+g‘𝐺)𝑦) ∈ (Base‘𝐺))
26		f1fveq 7260	. . . . . . . . . . . . 13 ⊢ ((𝑥:(Base‘𝐺)–1-1→(Base‘𝐻) ∧ ((𝑦(+g‘𝐺)𝑧) ∈ (Base‘𝐺) ∧ (𝑧(+g‘𝐺)𝑦) ∈ (Base‘𝐺))) → ((𝑥‘(𝑦(+g‘𝐺)𝑧)) = (𝑥‘(𝑧(+g‘𝐺)𝑦)) ↔ (𝑦(+g‘𝐺)𝑧) = (𝑧(+g‘𝐺)𝑦)))
27	17, 23, 25, 26	syl12anc 849	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ (𝐺 GrpIso 𝐻) ∧ (𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) → ((𝑥‘(𝑦(+g‘𝐺)𝑧)) = (𝑥‘(𝑧(+g‘𝐺)𝑦)) ↔ (𝑦(+g‘𝐺)𝑧) = (𝑧(+g‘𝐺)𝑦)))
28	3	adantr 485	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ (𝐺 GrpIso 𝐻) ∧ (𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) → 𝑥 ∈ (𝐺 GrpHom 𝐻))
29		eqid 2763	. . . . . . . . . . . . . . 15 ⊢ (+g‘𝐻) = (+g‘𝐻)
30	12, 21, 29	ghmlin 19286	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺)) → (𝑥‘(𝑦(+g‘𝐺)𝑧)) = ((𝑥‘𝑦)(+g‘𝐻)(𝑥‘𝑧)))
31	28, 19, 20, 30	syl3anc 1398	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ (𝐺 GrpIso 𝐻) ∧ (𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) → (𝑥‘(𝑦(+g‘𝐺)𝑧)) = ((𝑥‘𝑦)(+g‘𝐻)(𝑥‘𝑧)))
32	12, 21, 29	ghmlin 19286	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑧 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) → (𝑥‘(𝑧(+g‘𝐺)𝑦)) = ((𝑥‘𝑧)(+g‘𝐻)(𝑥‘𝑦)))
33	28, 20, 19, 32	syl3anc 1398	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ (𝐺 GrpIso 𝐻) ∧ (𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) → (𝑥‘(𝑧(+g‘𝐺)𝑦)) = ((𝑥‘𝑧)(+g‘𝐻)(𝑥‘𝑦)))
34	31, 33	eqeq12d 2779	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ (𝐺 GrpIso 𝐻) ∧ (𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) → ((𝑥‘(𝑦(+g‘𝐺)𝑧)) = (𝑥‘(𝑧(+g‘𝐺)𝑦)) ↔ ((𝑥‘𝑦)(+g‘𝐻)(𝑥‘𝑧)) = ((𝑥‘𝑧)(+g‘𝐻)(𝑥‘𝑦))))
35	27, 34	bitr3d 284	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ (𝐺 GrpIso 𝐻) ∧ (𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) → ((𝑦(+g‘𝐺)𝑧) = (𝑧(+g‘𝐺)𝑦) ↔ ((𝑥‘𝑦)(+g‘𝐻)(𝑥‘𝑧)) = ((𝑥‘𝑧)(+g‘𝐻)(𝑥‘𝑦))))
36	35	2ralbidva 3227	. . . . . . . . . 10 ⊢ (𝑥 ∈ (𝐺 GrpIso 𝐻) → (∀𝑦 ∈ (Base‘𝐺)∀𝑧 ∈ (Base‘𝐺)(𝑦(+g‘𝐺)𝑧) = (𝑧(+g‘𝐺)𝑦) ↔ ∀𝑦 ∈ (Base‘𝐺)∀𝑧 ∈ (Base‘𝐺)((𝑥‘𝑦)(+g‘𝐻)(𝑥‘𝑧)) = ((𝑥‘𝑧)(+g‘𝐻)(𝑥‘𝑦))))
37		f1ofo 6828	. . . . . . . . . . . . . . 15 ⊢ (𝑥:(Base‘𝐺)–1-1-onto→(Base‘𝐻) → 𝑥:(Base‘𝐺)–onto→(Base‘𝐻))
38		foima 6797	. . . . . . . . . . . . . . 15 ⊢ (𝑥:(Base‘𝐺)–onto→(Base‘𝐻) → (𝑥 “ (Base‘𝐺)) = (Base‘𝐻))
39	37, 38	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝑥:(Base‘𝐺)–1-1-onto→(Base‘𝐻) → (𝑥 “ (Base‘𝐺)) = (Base‘𝐻))
40	14, 39	syl 18	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (𝐺 GrpIso 𝐻) → (𝑥 “ (Base‘𝐺)) = (Base‘𝐻))
41	40	raleqdv 3323	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (𝐺 GrpIso 𝐻) → (∀𝑣 ∈ (𝑥 “ (Base‘𝐺))((𝑥‘𝑦)(+g‘𝐻)𝑣) = (𝑣(+g‘𝐻)(𝑥‘𝑦)) ↔ ∀𝑣 ∈ (Base‘𝐻)((𝑥‘𝑦)(+g‘𝐻)𝑣) = (𝑣(+g‘𝐻)(𝑥‘𝑦))))
42		f1ofn 6821	. . . . . . . . . . . . . 14 ⊢ (𝑥:(Base‘𝐺)–1-1-onto→(Base‘𝐻) → 𝑥 Fn (Base‘𝐺))
43	14, 42	syl 18	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (𝐺 GrpIso 𝐻) → 𝑥 Fn (Base‘𝐺))
44		ssid 3959	. . . . . . . . . . . . 13 ⊢ (Base‘𝐺) ⊆ (Base‘𝐺)
45		oveq2 7418	. . . . . . . . . . . . . . 15 ⊢ (𝑣 = (𝑥‘𝑧) → ((𝑥‘𝑦)(+g‘𝐻)𝑣) = ((𝑥‘𝑦)(+g‘𝐻)(𝑥‘𝑧)))
46		oveq1 7417	. . . . . . . . . . . . . . 15 ⊢ (𝑣 = (𝑥‘𝑧) → (𝑣(+g‘𝐻)(𝑥‘𝑦)) = ((𝑥‘𝑧)(+g‘𝐻)(𝑥‘𝑦)))
47	45, 46	eqeq12d 2779	. . . . . . . . . . . . . 14 ⊢ (𝑣 = (𝑥‘𝑧) → (((𝑥‘𝑦)(+g‘𝐻)𝑣) = (𝑣(+g‘𝐻)(𝑥‘𝑦)) ↔ ((𝑥‘𝑦)(+g‘𝐻)(𝑥‘𝑧)) = ((𝑥‘𝑧)(+g‘𝐻)(𝑥‘𝑦))))
48	47	ralima 7235	. . . . . . . . . . . . 13 ⊢ ((𝑥 Fn (Base‘𝐺) ∧ (Base‘𝐺) ⊆ (Base‘𝐺)) → (∀𝑣 ∈ (𝑥 “ (Base‘𝐺))((𝑥‘𝑦)(+g‘𝐻)𝑣) = (𝑣(+g‘𝐻)(𝑥‘𝑦)) ↔ ∀𝑧 ∈ (Base‘𝐺)((𝑥‘𝑦)(+g‘𝐻)(𝑥‘𝑧)) = ((𝑥‘𝑧)(+g‘𝐻)(𝑥‘𝑦))))
49	43, 44, 48	sylancl 597	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (𝐺 GrpIso 𝐻) → (∀𝑣 ∈ (𝑥 “ (Base‘𝐺))((𝑥‘𝑦)(+g‘𝐻)𝑣) = (𝑣(+g‘𝐻)(𝑥‘𝑦)) ↔ ∀𝑧 ∈ (Base‘𝐺)((𝑥‘𝑦)(+g‘𝐻)(𝑥‘𝑧)) = ((𝑥‘𝑧)(+g‘𝐻)(𝑥‘𝑦))))
50	41, 49	bitr3d 284	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (𝐺 GrpIso 𝐻) → (∀𝑣 ∈ (Base‘𝐻)((𝑥‘𝑦)(+g‘𝐻)𝑣) = (𝑣(+g‘𝐻)(𝑥‘𝑦)) ↔ ∀𝑧 ∈ (Base‘𝐺)((𝑥‘𝑦)(+g‘𝐻)(𝑥‘𝑧)) = ((𝑥‘𝑧)(+g‘𝐻)(𝑥‘𝑦))))
51	50	ralbidv 3188	. . . . . . . . . 10 ⊢ (𝑥 ∈ (𝐺 GrpIso 𝐻) → (∀𝑦 ∈ (Base‘𝐺)∀𝑣 ∈ (Base‘𝐻)((𝑥‘𝑦)(+g‘𝐻)𝑣) = (𝑣(+g‘𝐻)(𝑥‘𝑦)) ↔ ∀𝑦 ∈ (Base‘𝐺)∀𝑧 ∈ (Base‘𝐺)((𝑥‘𝑦)(+g‘𝐻)(𝑥‘𝑧)) = ((𝑥‘𝑧)(+g‘𝐻)(𝑥‘𝑦))))
52	36, 51	bitr4d 285	. . . . . . . . 9 ⊢ (𝑥 ∈ (𝐺 GrpIso 𝐻) → (∀𝑦 ∈ (Base‘𝐺)∀𝑧 ∈ (Base‘𝐺)(𝑦(+g‘𝐺)𝑧) = (𝑧(+g‘𝐺)𝑦) ↔ ∀𝑦 ∈ (Base‘𝐺)∀𝑣 ∈ (Base‘𝐻)((𝑥‘𝑦)(+g‘𝐻)𝑣) = (𝑣(+g‘𝐻)(𝑥‘𝑦))))
53	40	raleqdv 3323	. . . . . . . . . 10 ⊢ (𝑥 ∈ (𝐺 GrpIso 𝐻) → (∀𝑤 ∈ (𝑥 “ (Base‘𝐺))∀𝑣 ∈ (Base‘𝐻)(𝑤(+g‘𝐻)𝑣) = (𝑣(+g‘𝐻)𝑤) ↔ ∀𝑤 ∈ (Base‘𝐻)∀𝑣 ∈ (Base‘𝐻)(𝑤(+g‘𝐻)𝑣) = (𝑣(+g‘𝐻)𝑤)))
54		oveq1 7417	. . . . . . . . . . . . . 14 ⊢ (𝑤 = (𝑥‘𝑦) → (𝑤(+g‘𝐻)𝑣) = ((𝑥‘𝑦)(+g‘𝐻)𝑣))
55		oveq2 7418	. . . . . . . . . . . . . 14 ⊢ (𝑤 = (𝑥‘𝑦) → (𝑣(+g‘𝐻)𝑤) = (𝑣(+g‘𝐻)(𝑥‘𝑦)))
56	54, 55	eqeq12d 2779	. . . . . . . . . . . . 13 ⊢ (𝑤 = (𝑥‘𝑦) → ((𝑤(+g‘𝐻)𝑣) = (𝑣(+g‘𝐻)𝑤) ↔ ((𝑥‘𝑦)(+g‘𝐻)𝑣) = (𝑣(+g‘𝐻)(𝑥‘𝑦))))
57	56	ralbidv 3188	. . . . . . . . . . . 12 ⊢ (𝑤 = (𝑥‘𝑦) → (∀𝑣 ∈ (Base‘𝐻)(𝑤(+g‘𝐻)𝑣) = (𝑣(+g‘𝐻)𝑤) ↔ ∀𝑣 ∈ (Base‘𝐻)((𝑥‘𝑦)(+g‘𝐻)𝑣) = (𝑣(+g‘𝐻)(𝑥‘𝑦))))
58	57	ralima 7235	. . . . . . . . . . 11 ⊢ ((𝑥 Fn (Base‘𝐺) ∧ (Base‘𝐺) ⊆ (Base‘𝐺)) → (∀𝑤 ∈ (𝑥 “ (Base‘𝐺))∀𝑣 ∈ (Base‘𝐻)(𝑤(+g‘𝐻)𝑣) = (𝑣(+g‘𝐻)𝑤) ↔ ∀𝑦 ∈ (Base‘𝐺)∀𝑣 ∈ (Base‘𝐻)((𝑥‘𝑦)(+g‘𝐻)𝑣) = (𝑣(+g‘𝐻)(𝑥‘𝑦))))
59	43, 44, 58	sylancl 597	. . . . . . . . . 10 ⊢ (𝑥 ∈ (𝐺 GrpIso 𝐻) → (∀𝑤 ∈ (𝑥 “ (Base‘𝐺))∀𝑣 ∈ (Base‘𝐻)(𝑤(+g‘𝐻)𝑣) = (𝑣(+g‘𝐻)𝑤) ↔ ∀𝑦 ∈ (Base‘𝐺)∀𝑣 ∈ (Base‘𝐻)((𝑥‘𝑦)(+g‘𝐻)𝑣) = (𝑣(+g‘𝐻)(𝑥‘𝑦))))
60	53, 59	bitr3d 284	. . . . . . . . 9 ⊢ (𝑥 ∈ (𝐺 GrpIso 𝐻) → (∀𝑤 ∈ (Base‘𝐻)∀𝑣 ∈ (Base‘𝐻)(𝑤(+g‘𝐻)𝑣) = (𝑣(+g‘𝐻)𝑤) ↔ ∀𝑦 ∈ (Base‘𝐺)∀𝑣 ∈ (Base‘𝐻)((𝑥‘𝑦)(+g‘𝐻)𝑣) = (𝑣(+g‘𝐻)(𝑥‘𝑦))))
61	52, 60	bitr4d 285	. . . . . . . 8 ⊢ (𝑥 ∈ (𝐺 GrpIso 𝐻) → (∀𝑦 ∈ (Base‘𝐺)∀𝑧 ∈ (Base‘𝐺)(𝑦(+g‘𝐺)𝑧) = (𝑧(+g‘𝐺)𝑦) ↔ ∀𝑤 ∈ (Base‘𝐻)∀𝑣 ∈ (Base‘𝐻)(𝑤(+g‘𝐻)𝑣) = (𝑣(+g‘𝐻)𝑤)))
62	11, 61	anbi12d 643	. . . . . . 7 ⊢ (𝑥 ∈ (𝐺 GrpIso 𝐻) → ((𝐺 ∈ Mnd ∧ ∀𝑦 ∈ (Base‘𝐺)∀𝑧 ∈ (Base‘𝐺)(𝑦(+g‘𝐺)𝑧) = (𝑧(+g‘𝐺)𝑦)) ↔ (𝐻 ∈ Mnd ∧ ∀𝑤 ∈ (Base‘𝐻)∀𝑣 ∈ (Base‘𝐻)(𝑤(+g‘𝐻)𝑣) = (𝑣(+g‘𝐻)𝑤))))
63	12, 21	iscmn 19854	. . . . . . 7 ⊢ (𝐺 ∈ CMnd ↔ (𝐺 ∈ Mnd ∧ ∀𝑦 ∈ (Base‘𝐺)∀𝑧 ∈ (Base‘𝐺)(𝑦(+g‘𝐺)𝑧) = (𝑧(+g‘𝐺)𝑦)))
64	13, 29	iscmn 19854	. . . . . . 7 ⊢ (𝐻 ∈ CMnd ↔ (𝐻 ∈ Mnd ∧ ∀𝑤 ∈ (Base‘𝐻)∀𝑣 ∈ (Base‘𝐻)(𝑤(+g‘𝐻)𝑣) = (𝑣(+g‘𝐻)𝑤)))
65	62, 63, 64	3bitr4g 317	. . . . . 6 ⊢ (𝑥 ∈ (𝐺 GrpIso 𝐻) → (𝐺 ∈ CMnd ↔ 𝐻 ∈ CMnd))
66	8, 65	anbi12d 643	. . . . 5 ⊢ (𝑥 ∈ (𝐺 GrpIso 𝐻) → ((𝐺 ∈ Grp ∧ 𝐺 ∈ CMnd) ↔ (𝐻 ∈ Grp ∧ 𝐻 ∈ CMnd)))
67		isabl 19849	. . . . 5 ⊢ (𝐺 ∈ Abel ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ CMnd))
68		isabl 19849	. . . . 5 ⊢ (𝐻 ∈ Abel ↔ (𝐻 ∈ Grp ∧ 𝐻 ∈ CMnd))
69	66, 67, 68	3bitr4g 317	. . . 4 ⊢ (𝑥 ∈ (𝐺 GrpIso 𝐻) → (𝐺 ∈ Abel ↔ 𝐻 ∈ Abel))
70	69	exlimiv 1960	. . 3 ⊢ (∃𝑥 𝑥 ∈ (𝐺 GrpIso 𝐻) → (𝐺 ∈ Abel ↔ 𝐻 ∈ Abel))
71	2, 70	sylbi 220	. 2 ⊢ ((𝐺 GrpIso 𝐻) ≠ ∅ → (𝐺 ∈ Abel ↔ 𝐻 ∈ Abel))
72	1, 71	sylbi 220	1 ⊢ (𝐺 ≃𝑔 𝐻 → (𝐺 ∈ Abel ↔ 𝐻 ∈ Abel))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1570  ∃wex 1809   ∈ wcel 2143   ≠ wne 2958  ∀wral 3079   ⊆ wss 3905  ∅c0 4286   class class class wbr 5109   “ cima 5664   Fn wfn 6531  –1-1→wf1 6533  –onto→wfo 6534  –1-1-onto→wf1o 6535  ‘cfv 6536  (class class class)co 7410  Basecbs 17264  +_gcplusg 17305  Mndcmnd 18787  Grpcgrp 18995   GrpHom cghm 19278   GrpIso cgim 19322   ≃_𝑔 cgic 19323  CMndccmn 19845  Abelcabl 19846

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5257  ax-nul 5269  ax-pow 5336  ax-pr 5404  ax-un 7732

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-iun 4958  df-br 5110  df-opab 5174  df-mpt 5193  df-id 5556  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-suc 6366  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-ov 7413  df-oprab 7414  df-mpo 7415  df-1st 7982  df-2nd 7983  df-1o 8449  df-map 8822  df-mgm 18693  df-sgrp 18772  df-mnd 18788  df-grp 18998  df-ghm 19279  df-gim 19324  df-gic 19325  df-cmn 19847  df-abl 19848

This theorem is referenced by:  isnumbasgrplem1  43848