Theorem gicabl 43752

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 19340	. 2 ⊢ (𝐺 ≃𝑔 𝐻 ↔ (𝐺 GrpIso 𝐻) ≠ ∅)
2		n0 4315	. . 3 ⊢ ((𝐺 GrpIso 𝐻) ≠ ∅ ↔ ∃𝑥 𝑥 ∈ (𝐺 GrpIso 𝐻))
3		gimghm 19334	. . . . . . . 8 ⊢ (𝑥 ∈ (𝐺 GrpIso 𝐻) → 𝑥 ∈ (𝐺 GrpHom 𝐻))
4		ghmgrp1 19288	. . . . . . . 8 ⊢ (𝑥 ∈ (𝐺 GrpHom 𝐻) → 𝐺 ∈ Grp)
5	3, 4	syl 18	. . . . . . 7 ⊢ (𝑥 ∈ (𝐺 GrpIso 𝐻) → 𝐺 ∈ Grp)
6		ghmgrp2 19289	. . . . . . . 8 ⊢ (𝑥 ∈ (𝐺 GrpHom 𝐻) → 𝐻 ∈ Grp)
7	3, 6	syl 18	. . . . . . 7 ⊢ (𝑥 ∈ (𝐺 GrpIso 𝐻) → 𝐻 ∈ Grp)
8	5, 7	2thd 268	. . . . . 6 ⊢ (𝑥 ∈ (𝐺 GrpIso 𝐻) → (𝐺 ∈ Grp ↔ 𝐻 ∈ Grp))
9	5	grpmndd 19013	. . . . . . . . 9 ⊢ (𝑥 ∈ (𝐺 GrpIso 𝐻) → 𝐺 ∈ Mnd)
10	7	grpmndd 19013	. . . . . . . . 9 ⊢ (𝑥 ∈ (𝐺 GrpIso 𝐻) → 𝐻 ∈ Mnd)
11	9, 10	2thd 268	. . . . . . . 8 ⊢ (𝑥 ∈ (𝐺 GrpIso 𝐻) → (𝐺 ∈ Mnd ↔ 𝐻 ∈ Mnd))
12		eqid 2769	. . . . . . . . . . . . . . . 16 ⊢ (Base‘𝐺) = (Base‘𝐺)
13		eqid 2769	. . . . . . . . . . . . . . . 16 ⊢ (Base‘𝐻) = (Base‘𝐻)
14	12, 13	gimf1o 19333	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (𝐺 GrpIso 𝐻) → 𝑥:(Base‘𝐺)–1-1-onto→(Base‘𝐻))
15		f1of1 6820	. . . . . . . . . . . . . . 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 2769	. . . . . . . . . . . . . . 15 ⊢ (+g‘𝐺) = (+g‘𝐺)
22	12, 21	grpcl 19008	. . . . . . . . . . . . . 14 ⊢ ((𝐺 ∈ Grp ∧ 𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺)) → (𝑦(+g‘𝐺)𝑧) ∈ (Base‘𝐺))
23	18, 19, 20, 22	syl3anc 1396	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ (𝐺 GrpIso 𝐻) ∧ (𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) → (𝑦(+g‘𝐺)𝑧) ∈ (Base‘𝐺))
24	12, 21	grpcl 19008	. . . . . . . . . . . . . 14 ⊢ ((𝐺 ∈ Grp ∧ 𝑧 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) → (𝑧(+g‘𝐺)𝑦) ∈ (Base‘𝐺))
25	18, 20, 19, 24	syl3anc 1396	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ (𝐺 GrpIso 𝐻) ∧ (𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) → (𝑧(+g‘𝐺)𝑦) ∈ (Base‘𝐺))
26		f1fveq 7261	. . . . . . . . . . . . 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 2769	. . . . . . . . . . . . . . 15 ⊢ (+g‘𝐻) = (+g‘𝐻)
30	12, 21, 29	ghmlin 19291	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺)) → (𝑥‘(𝑦(+g‘𝐺)𝑧)) = ((𝑥‘𝑦)(+g‘𝐻)(𝑥‘𝑧)))
31	28, 19, 20, 30	syl3anc 1396	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ (𝐺 GrpIso 𝐻) ∧ (𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) → (𝑥‘(𝑦(+g‘𝐺)𝑧)) = ((𝑥‘𝑦)(+g‘𝐻)(𝑥‘𝑧)))
32	12, 21, 29	ghmlin 19291	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑧 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) → (𝑥‘(𝑧(+g‘𝐺)𝑦)) = ((𝑥‘𝑧)(+g‘𝐻)(𝑥‘𝑦)))
33	28, 20, 19, 32	syl3anc 1396	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ (𝐺 GrpIso 𝐻) ∧ (𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) → (𝑥‘(𝑧(+g‘𝐺)𝑦)) = ((𝑥‘𝑧)(+g‘𝐻)(𝑥‘𝑦)))
34	31, 33	eqeq12d 2785	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ (𝐺 GrpIso 𝐻) ∧ (𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) → ((𝑥‘(𝑦(+g‘𝐺)𝑧)) = (𝑥‘(𝑧(+g‘𝐺)𝑦)) ↔ ((𝑥‘𝑦)(+g‘𝐻)(𝑥‘𝑧)) = ((𝑥‘𝑧)(+g‘𝐻)(𝑥‘𝑦))))
35	27, 34	bitr3d 284	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ (𝐺 GrpIso 𝐻) ∧ (𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) → ((𝑦(+g‘𝐺)𝑧) = (𝑧(+g‘𝐺)𝑦) ↔ ((𝑥‘𝑦)(+g‘𝐻)(𝑥‘𝑧)) = ((𝑥‘𝑧)(+g‘𝐻)(𝑥‘𝑦))))
36	35	2ralbidva 3233	. . . . . . . . . 10 ⊢ (𝑥 ∈ (𝐺 GrpIso 𝐻) → (∀𝑦 ∈ (Base‘𝐺)∀𝑧 ∈ (Base‘𝐺)(𝑦(+g‘𝐺)𝑧) = (𝑧(+g‘𝐺)𝑦) ↔ ∀𝑦 ∈ (Base‘𝐺)∀𝑧 ∈ (Base‘𝐺)((𝑥‘𝑦)(+g‘𝐻)(𝑥‘𝑧)) = ((𝑥‘𝑧)(+g‘𝐻)(𝑥‘𝑦))))
37		f1ofo 6829	. . . . . . . . . . . . . . 15 ⊢ (𝑥:(Base‘𝐺)–1-1-onto→(Base‘𝐻) → 𝑥:(Base‘𝐺)–onto→(Base‘𝐻))
38		foima 6798	. . . . . . . . . . . . . . 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 3329	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (𝐺 GrpIso 𝐻) → (∀𝑣 ∈ (𝑥 “ (Base‘𝐺))((𝑥‘𝑦)(+g‘𝐻)𝑣) = (𝑣(+g‘𝐻)(𝑥‘𝑦)) ↔ ∀𝑣 ∈ (Base‘𝐻)((𝑥‘𝑦)(+g‘𝐻)𝑣) = (𝑣(+g‘𝐻)(𝑥‘𝑦))))
42		f1ofn 6822	. . . . . . . . . . . . . 14 ⊢ (𝑥:(Base‘𝐺)–1-1-onto→(Base‘𝐻) → 𝑥 Fn (Base‘𝐺))
43	14, 42	syl 18	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (𝐺 GrpIso 𝐻) → 𝑥 Fn (Base‘𝐺))
44		ssid 3967	. . . . . . . . . . . . 13 ⊢ (Base‘𝐺) ⊆ (Base‘𝐺)
45		oveq2 7419	. . . . . . . . . . . . . . 15 ⊢ (𝑣 = (𝑥‘𝑧) → ((𝑥‘𝑦)(+g‘𝐻)𝑣) = ((𝑥‘𝑦)(+g‘𝐻)(𝑥‘𝑧)))
46		oveq1 7418	. . . . . . . . . . . . . . 15 ⊢ (𝑣 = (𝑥‘𝑧) → (𝑣(+g‘𝐻)(𝑥‘𝑦)) = ((𝑥‘𝑧)(+g‘𝐻)(𝑥‘𝑦)))
47	45, 46	eqeq12d 2785	. . . . . . . . . . . . . 14 ⊢ (𝑣 = (𝑥‘𝑧) → (((𝑥‘𝑦)(+g‘𝐻)𝑣) = (𝑣(+g‘𝐻)(𝑥‘𝑦)) ↔ ((𝑥‘𝑦)(+g‘𝐻)(𝑥‘𝑧)) = ((𝑥‘𝑧)(+g‘𝐻)(𝑥‘𝑦))))
48	47	ralima 7236	. . . . . . . . . . . . 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 3194	. . . . . . . . . 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 3329	. . . . . . . . . 10 ⊢ (𝑥 ∈ (𝐺 GrpIso 𝐻) → (∀𝑤 ∈ (𝑥 “ (Base‘𝐺))∀𝑣 ∈ (Base‘𝐻)(𝑤(+g‘𝐻)𝑣) = (𝑣(+g‘𝐻)𝑤) ↔ ∀𝑤 ∈ (Base‘𝐻)∀𝑣 ∈ (Base‘𝐻)(𝑤(+g‘𝐻)𝑣) = (𝑣(+g‘𝐻)𝑤)))
54		oveq1 7418	. . . . . . . . . . . . . 14 ⊢ (𝑤 = (𝑥‘𝑦) → (𝑤(+g‘𝐻)𝑣) = ((𝑥‘𝑦)(+g‘𝐻)𝑣))
55		oveq2 7419	. . . . . . . . . . . . . 14 ⊢ (𝑤 = (𝑥‘𝑦) → (𝑣(+g‘𝐻)𝑤) = (𝑣(+g‘𝐻)(𝑥‘𝑦)))
56	54, 55	eqeq12d 2785	. . . . . . . . . . . . 13 ⊢ (𝑤 = (𝑥‘𝑦) → ((𝑤(+g‘𝐻)𝑣) = (𝑣(+g‘𝐻)𝑤) ↔ ((𝑥‘𝑦)(+g‘𝐻)𝑣) = (𝑣(+g‘𝐻)(𝑥‘𝑦))))
57	56	ralbidv 3194	. . . . . . . . . . . 12 ⊢ (𝑤 = (𝑥‘𝑦) → (∀𝑣 ∈ (Base‘𝐻)(𝑤(+g‘𝐻)𝑣) = (𝑣(+g‘𝐻)𝑤) ↔ ∀𝑣 ∈ (Base‘𝐻)((𝑥‘𝑦)(+g‘𝐻)𝑣) = (𝑣(+g‘𝐻)(𝑥‘𝑦))))
58	57	ralima 7236	. . . . . . . . . . 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 19859	. . . . . . 7 ⊢ (𝐺 ∈ CMnd ↔ (𝐺 ∈ Mnd ∧ ∀𝑦 ∈ (Base‘𝐺)∀𝑧 ∈ (Base‘𝐺)(𝑦(+g‘𝐺)𝑧) = (𝑧(+g‘𝐺)𝑦)))
64	13, 29	iscmn 19859	. . . . . . 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 19854	. . . . 5 ⊢ (𝐺 ∈ Abel ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ CMnd))
68		isabl 19854	. . . . 5 ⊢ (𝐻 ∈ Abel ↔ (𝐻 ∈ Grp ∧ 𝐻 ∈ CMnd))
69	66, 67, 68	3bitr4g 317	. . . 4 ⊢ (𝑥 ∈ (𝐺 GrpIso 𝐻) → (𝐺 ∈ Abel ↔ 𝐻 ∈ Abel))
70	69	exlimiv 1957	. . 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 1567  ∃wex 1806   ∈ wcel 2149   ≠ wne 2964  ∀wral 3085   ⊆ wss 3913  ∅c0 4294   class class class wbr 5113   “ cima 5665   Fn wfn 6532  –1-1→wf1 6534  –onto→wfo 6535  –1-1-onto→wf1o 6536  ‘cfv 6537  (class class class)co 7411  Basecbs 17269  +_gcplusg 17310  Mndcmnd 18792  Grpcgrp 19000   GrpHom cghm 19283   GrpIso cgim 19327   ≃_𝑔 cgic 19328  CMndccmn 19850  Abelcabl 19851

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5261  ax-nul 5271  ax-pow 5337  ax-pr 5405  ax-un 7733

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-iun 4962  df-br 5114  df-opab 5178  df-mpt 5197  df-id 5557  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-rn 5673  df-res 5674  df-ima 5675  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-ov 7414  df-oprab 7415  df-mpo 7416  df-1st 7986  df-2nd 7987  df-1o 8453  df-map 8826  df-mgm 18698  df-sgrp 18777  df-mnd 18793  df-grp 19003  df-ghm 19284  df-gim 19329  df-gic 19330  df-cmn 19852  df-abl 19853

This theorem is referenced by:  isnumbasgrplem1  43754