Theorem gicabl 43283

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 19197	. 2 ⊢ (𝐺 ≃𝑔 𝐻 ↔ (𝐺 GrpIso 𝐻) ≠ ∅)
2		n0 4303	. . 3 ⊢ ((𝐺 GrpIso 𝐻) ≠ ∅ ↔ ∃𝑥 𝑥 ∈ (𝐺 GrpIso 𝐻))
3		gimghm 19191	. . . . . . . 8 ⊢ (𝑥 ∈ (𝐺 GrpIso 𝐻) → 𝑥 ∈ (𝐺 GrpHom 𝐻))
4		ghmgrp1 19145	. . . . . . . 8 ⊢ (𝑥 ∈ (𝐺 GrpHom 𝐻) → 𝐺 ∈ Grp)
5	3, 4	syl 17	. . . . . . 7 ⊢ (𝑥 ∈ (𝐺 GrpIso 𝐻) → 𝐺 ∈ Grp)
6		ghmgrp2 19146	. . . . . . . 8 ⊢ (𝑥 ∈ (𝐺 GrpHom 𝐻) → 𝐻 ∈ Grp)
7	3, 6	syl 17	. . . . . . 7 ⊢ (𝑥 ∈ (𝐺 GrpIso 𝐻) → 𝐻 ∈ Grp)
8	5, 7	2thd 265	. . . . . 6 ⊢ (𝑥 ∈ (𝐺 GrpIso 𝐻) → (𝐺 ∈ Grp ↔ 𝐻 ∈ Grp))
9	5	grpmndd 18874	. . . . . . . . 9 ⊢ (𝑥 ∈ (𝐺 GrpIso 𝐻) → 𝐺 ∈ Mnd)
10	7	grpmndd 18874	. . . . . . . . 9 ⊢ (𝑥 ∈ (𝐺 GrpIso 𝐻) → 𝐻 ∈ Mnd)
11	9, 10	2thd 265	. . . . . . . 8 ⊢ (𝑥 ∈ (𝐺 GrpIso 𝐻) → (𝐺 ∈ Mnd ↔ 𝐻 ∈ Mnd))
12		eqid 2734	. . . . . . . . . . . . . . . 16 ⊢ (Base‘𝐺) = (Base‘𝐺)
13		eqid 2734	. . . . . . . . . . . . . . . 16 ⊢ (Base‘𝐻) = (Base‘𝐻)
14	12, 13	gimf1o 19190	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (𝐺 GrpIso 𝐻) → 𝑥:(Base‘𝐺)–1-1-onto→(Base‘𝐻))
15		f1of1 6771	. . . . . . . . . . . . . . 15 ⊢ (𝑥:(Base‘𝐺)–1-1-onto→(Base‘𝐻) → 𝑥:(Base‘𝐺)–1-1→(Base‘𝐻))
16	14, 15	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (𝐺 GrpIso 𝐻) → 𝑥:(Base‘𝐺)–1-1→(Base‘𝐻))
17	16	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ (𝐺 GrpIso 𝐻) ∧ (𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) → 𝑥:(Base‘𝐺)–1-1→(Base‘𝐻))
18	5	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ (𝐺 GrpIso 𝐻) ∧ (𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) → 𝐺 ∈ Grp)
19		simprl 770	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ (𝐺 GrpIso 𝐻) ∧ (𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) → 𝑦 ∈ (Base‘𝐺))
20		simprr 772	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ (𝐺 GrpIso 𝐻) ∧ (𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) → 𝑧 ∈ (Base‘𝐺))
21		eqid 2734	. . . . . . . . . . . . . . 15 ⊢ (+g‘𝐺) = (+g‘𝐺)
22	12, 21	grpcl 18869	. . . . . . . . . . . . . 14 ⊢ ((𝐺 ∈ Grp ∧ 𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺)) → (𝑦(+g‘𝐺)𝑧) ∈ (Base‘𝐺))
23	18, 19, 20, 22	syl3anc 1373	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ (𝐺 GrpIso 𝐻) ∧ (𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) → (𝑦(+g‘𝐺)𝑧) ∈ (Base‘𝐺))
24	12, 21	grpcl 18869	. . . . . . . . . . . . . 14 ⊢ ((𝐺 ∈ Grp ∧ 𝑧 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) → (𝑧(+g‘𝐺)𝑦) ∈ (Base‘𝐺))
25	18, 20, 19, 24	syl3anc 1373	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ (𝐺 GrpIso 𝐻) ∧ (𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) → (𝑧(+g‘𝐺)𝑦) ∈ (Base‘𝐺))
26		f1fveq 7206	. . . . . . . . . . . . 13 ⊢ ((𝑥:(Base‘𝐺)–1-1→(Base‘𝐻) ∧ ((𝑦(+g‘𝐺)𝑧) ∈ (Base‘𝐺) ∧ (𝑧(+g‘𝐺)𝑦) ∈ (Base‘𝐺))) → ((𝑥‘(𝑦(+g‘𝐺)𝑧)) = (𝑥‘(𝑧(+g‘𝐺)𝑦)) ↔ (𝑦(+g‘𝐺)𝑧) = (𝑧(+g‘𝐺)𝑦)))
27	17, 23, 25, 26	syl12anc 836	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ (𝐺 GrpIso 𝐻) ∧ (𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) → ((𝑥‘(𝑦(+g‘𝐺)𝑧)) = (𝑥‘(𝑧(+g‘𝐺)𝑦)) ↔ (𝑦(+g‘𝐺)𝑧) = (𝑧(+g‘𝐺)𝑦)))
28	3	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ (𝐺 GrpIso 𝐻) ∧ (𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) → 𝑥 ∈ (𝐺 GrpHom 𝐻))
29		eqid 2734	. . . . . . . . . . . . . . 15 ⊢ (+g‘𝐻) = (+g‘𝐻)
30	12, 21, 29	ghmlin 19148	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺)) → (𝑥‘(𝑦(+g‘𝐺)𝑧)) = ((𝑥‘𝑦)(+g‘𝐻)(𝑥‘𝑧)))
31	28, 19, 20, 30	syl3anc 1373	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ (𝐺 GrpIso 𝐻) ∧ (𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) → (𝑥‘(𝑦(+g‘𝐺)𝑧)) = ((𝑥‘𝑦)(+g‘𝐻)(𝑥‘𝑧)))
32	12, 21, 29	ghmlin 19148	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑧 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) → (𝑥‘(𝑧(+g‘𝐺)𝑦)) = ((𝑥‘𝑧)(+g‘𝐻)(𝑥‘𝑦)))
33	28, 20, 19, 32	syl3anc 1373	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ (𝐺 GrpIso 𝐻) ∧ (𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) → (𝑥‘(𝑧(+g‘𝐺)𝑦)) = ((𝑥‘𝑧)(+g‘𝐻)(𝑥‘𝑦)))
34	31, 33	eqeq12d 2750	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ (𝐺 GrpIso 𝐻) ∧ (𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) → ((𝑥‘(𝑦(+g‘𝐺)𝑧)) = (𝑥‘(𝑧(+g‘𝐺)𝑦)) ↔ ((𝑥‘𝑦)(+g‘𝐻)(𝑥‘𝑧)) = ((𝑥‘𝑧)(+g‘𝐻)(𝑥‘𝑦))))
35	27, 34	bitr3d 281	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ (𝐺 GrpIso 𝐻) ∧ (𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) → ((𝑦(+g‘𝐺)𝑧) = (𝑧(+g‘𝐺)𝑦) ↔ ((𝑥‘𝑦)(+g‘𝐻)(𝑥‘𝑧)) = ((𝑥‘𝑧)(+g‘𝐻)(𝑥‘𝑦))))
36	35	2ralbidva 3196	. . . . . . . . . 10 ⊢ (𝑥 ∈ (𝐺 GrpIso 𝐻) → (∀𝑦 ∈ (Base‘𝐺)∀𝑧 ∈ (Base‘𝐺)(𝑦(+g‘𝐺)𝑧) = (𝑧(+g‘𝐺)𝑦) ↔ ∀𝑦 ∈ (Base‘𝐺)∀𝑧 ∈ (Base‘𝐺)((𝑥‘𝑦)(+g‘𝐻)(𝑥‘𝑧)) = ((𝑥‘𝑧)(+g‘𝐻)(𝑥‘𝑦))))
37		f1ofo 6779	. . . . . . . . . . . . . . 15 ⊢ (𝑥:(Base‘𝐺)–1-1-onto→(Base‘𝐻) → 𝑥:(Base‘𝐺)–onto→(Base‘𝐻))
38		foima 6749	. . . . . . . . . . . . . . 15 ⊢ (𝑥:(Base‘𝐺)–onto→(Base‘𝐻) → (𝑥 “ (Base‘𝐺)) = (Base‘𝐻))
39	37, 38	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝑥:(Base‘𝐺)–1-1-onto→(Base‘𝐻) → (𝑥 “ (Base‘𝐺)) = (Base‘𝐻))
40	14, 39	syl 17	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (𝐺 GrpIso 𝐻) → (𝑥 “ (Base‘𝐺)) = (Base‘𝐻))
41	40	raleqdv 3294	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (𝐺 GrpIso 𝐻) → (∀𝑣 ∈ (𝑥 “ (Base‘𝐺))((𝑥‘𝑦)(+g‘𝐻)𝑣) = (𝑣(+g‘𝐻)(𝑥‘𝑦)) ↔ ∀𝑣 ∈ (Base‘𝐻)((𝑥‘𝑦)(+g‘𝐻)𝑣) = (𝑣(+g‘𝐻)(𝑥‘𝑦))))
42		f1ofn 6773	. . . . . . . . . . . . . 14 ⊢ (𝑥:(Base‘𝐺)–1-1-onto→(Base‘𝐻) → 𝑥 Fn (Base‘𝐺))
43	14, 42	syl 17	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (𝐺 GrpIso 𝐻) → 𝑥 Fn (Base‘𝐺))
44		ssid 3954	. . . . . . . . . . . . 13 ⊢ (Base‘𝐺) ⊆ (Base‘𝐺)
45		oveq2 7364	. . . . . . . . . . . . . . 15 ⊢ (𝑣 = (𝑥‘𝑧) → ((𝑥‘𝑦)(+g‘𝐻)𝑣) = ((𝑥‘𝑦)(+g‘𝐻)(𝑥‘𝑧)))
46		oveq1 7363	. . . . . . . . . . . . . . 15 ⊢ (𝑣 = (𝑥‘𝑧) → (𝑣(+g‘𝐻)(𝑥‘𝑦)) = ((𝑥‘𝑧)(+g‘𝐻)(𝑥‘𝑦)))
47	45, 46	eqeq12d 2750	. . . . . . . . . . . . . 14 ⊢ (𝑣 = (𝑥‘𝑧) → (((𝑥‘𝑦)(+g‘𝐻)𝑣) = (𝑣(+g‘𝐻)(𝑥‘𝑦)) ↔ ((𝑥‘𝑦)(+g‘𝐻)(𝑥‘𝑧)) = ((𝑥‘𝑧)(+g‘𝐻)(𝑥‘𝑦))))
48	47	ralima 7181	. . . . . . . . . . . . 13 ⊢ ((𝑥 Fn (Base‘𝐺) ∧ (Base‘𝐺) ⊆ (Base‘𝐺)) → (∀𝑣 ∈ (𝑥 “ (Base‘𝐺))((𝑥‘𝑦)(+g‘𝐻)𝑣) = (𝑣(+g‘𝐻)(𝑥‘𝑦)) ↔ ∀𝑧 ∈ (Base‘𝐺)((𝑥‘𝑦)(+g‘𝐻)(𝑥‘𝑧)) = ((𝑥‘𝑧)(+g‘𝐻)(𝑥‘𝑦))))
49	43, 44, 48	sylancl 586	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (𝐺 GrpIso 𝐻) → (∀𝑣 ∈ (𝑥 “ (Base‘𝐺))((𝑥‘𝑦)(+g‘𝐻)𝑣) = (𝑣(+g‘𝐻)(𝑥‘𝑦)) ↔ ∀𝑧 ∈ (Base‘𝐺)((𝑥‘𝑦)(+g‘𝐻)(𝑥‘𝑧)) = ((𝑥‘𝑧)(+g‘𝐻)(𝑥‘𝑦))))
50	41, 49	bitr3d 281	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (𝐺 GrpIso 𝐻) → (∀𝑣 ∈ (Base‘𝐻)((𝑥‘𝑦)(+g‘𝐻)𝑣) = (𝑣(+g‘𝐻)(𝑥‘𝑦)) ↔ ∀𝑧 ∈ (Base‘𝐺)((𝑥‘𝑦)(+g‘𝐻)(𝑥‘𝑧)) = ((𝑥‘𝑧)(+g‘𝐻)(𝑥‘𝑦))))
51	50	ralbidv 3157	. . . . . . . . . 10 ⊢ (𝑥 ∈ (𝐺 GrpIso 𝐻) → (∀𝑦 ∈ (Base‘𝐺)∀𝑣 ∈ (Base‘𝐻)((𝑥‘𝑦)(+g‘𝐻)𝑣) = (𝑣(+g‘𝐻)(𝑥‘𝑦)) ↔ ∀𝑦 ∈ (Base‘𝐺)∀𝑧 ∈ (Base‘𝐺)((𝑥‘𝑦)(+g‘𝐻)(𝑥‘𝑧)) = ((𝑥‘𝑧)(+g‘𝐻)(𝑥‘𝑦))))
52	36, 51	bitr4d 282	. . . . . . . . 9 ⊢ (𝑥 ∈ (𝐺 GrpIso 𝐻) → (∀𝑦 ∈ (Base‘𝐺)∀𝑧 ∈ (Base‘𝐺)(𝑦(+g‘𝐺)𝑧) = (𝑧(+g‘𝐺)𝑦) ↔ ∀𝑦 ∈ (Base‘𝐺)∀𝑣 ∈ (Base‘𝐻)((𝑥‘𝑦)(+g‘𝐻)𝑣) = (𝑣(+g‘𝐻)(𝑥‘𝑦))))
53	40	raleqdv 3294	. . . . . . . . . 10 ⊢ (𝑥 ∈ (𝐺 GrpIso 𝐻) → (∀𝑤 ∈ (𝑥 “ (Base‘𝐺))∀𝑣 ∈ (Base‘𝐻)(𝑤(+g‘𝐻)𝑣) = (𝑣(+g‘𝐻)𝑤) ↔ ∀𝑤 ∈ (Base‘𝐻)∀𝑣 ∈ (Base‘𝐻)(𝑤(+g‘𝐻)𝑣) = (𝑣(+g‘𝐻)𝑤)))
54		oveq1 7363	. . . . . . . . . . . . . 14 ⊢ (𝑤 = (𝑥‘𝑦) → (𝑤(+g‘𝐻)𝑣) = ((𝑥‘𝑦)(+g‘𝐻)𝑣))
55		oveq2 7364	. . . . . . . . . . . . . 14 ⊢ (𝑤 = (𝑥‘𝑦) → (𝑣(+g‘𝐻)𝑤) = (𝑣(+g‘𝐻)(𝑥‘𝑦)))
56	54, 55	eqeq12d 2750	. . . . . . . . . . . . 13 ⊢ (𝑤 = (𝑥‘𝑦) → ((𝑤(+g‘𝐻)𝑣) = (𝑣(+g‘𝐻)𝑤) ↔ ((𝑥‘𝑦)(+g‘𝐻)𝑣) = (𝑣(+g‘𝐻)(𝑥‘𝑦))))
57	56	ralbidv 3157	. . . . . . . . . . . 12 ⊢ (𝑤 = (𝑥‘𝑦) → (∀𝑣 ∈ (Base‘𝐻)(𝑤(+g‘𝐻)𝑣) = (𝑣(+g‘𝐻)𝑤) ↔ ∀𝑣 ∈ (Base‘𝐻)((𝑥‘𝑦)(+g‘𝐻)𝑣) = (𝑣(+g‘𝐻)(𝑥‘𝑦))))
58	57	ralima 7181	. . . . . . . . . . 11 ⊢ ((𝑥 Fn (Base‘𝐺) ∧ (Base‘𝐺) ⊆ (Base‘𝐺)) → (∀𝑤 ∈ (𝑥 “ (Base‘𝐺))∀𝑣 ∈ (Base‘𝐻)(𝑤(+g‘𝐻)𝑣) = (𝑣(+g‘𝐻)𝑤) ↔ ∀𝑦 ∈ (Base‘𝐺)∀𝑣 ∈ (Base‘𝐻)((𝑥‘𝑦)(+g‘𝐻)𝑣) = (𝑣(+g‘𝐻)(𝑥‘𝑦))))
59	43, 44, 58	sylancl 586	. . . . . . . . . 10 ⊢ (𝑥 ∈ (𝐺 GrpIso 𝐻) → (∀𝑤 ∈ (𝑥 “ (Base‘𝐺))∀𝑣 ∈ (Base‘𝐻)(𝑤(+g‘𝐻)𝑣) = (𝑣(+g‘𝐻)𝑤) ↔ ∀𝑦 ∈ (Base‘𝐺)∀𝑣 ∈ (Base‘𝐻)((𝑥‘𝑦)(+g‘𝐻)𝑣) = (𝑣(+g‘𝐻)(𝑥‘𝑦))))
60	53, 59	bitr3d 281	. . . . . . . . 9 ⊢ (𝑥 ∈ (𝐺 GrpIso 𝐻) → (∀𝑤 ∈ (Base‘𝐻)∀𝑣 ∈ (Base‘𝐻)(𝑤(+g‘𝐻)𝑣) = (𝑣(+g‘𝐻)𝑤) ↔ ∀𝑦 ∈ (Base‘𝐺)∀𝑣 ∈ (Base‘𝐻)((𝑥‘𝑦)(+g‘𝐻)𝑣) = (𝑣(+g‘𝐻)(𝑥‘𝑦))))
61	52, 60	bitr4d 282	. . . . . . . 8 ⊢ (𝑥 ∈ (𝐺 GrpIso 𝐻) → (∀𝑦 ∈ (Base‘𝐺)∀𝑧 ∈ (Base‘𝐺)(𝑦(+g‘𝐺)𝑧) = (𝑧(+g‘𝐺)𝑦) ↔ ∀𝑤 ∈ (Base‘𝐻)∀𝑣 ∈ (Base‘𝐻)(𝑤(+g‘𝐻)𝑣) = (𝑣(+g‘𝐻)𝑤)))
62	11, 61	anbi12d 632	. . . . . . 7 ⊢ (𝑥 ∈ (𝐺 GrpIso 𝐻) → ((𝐺 ∈ Mnd ∧ ∀𝑦 ∈ (Base‘𝐺)∀𝑧 ∈ (Base‘𝐺)(𝑦(+g‘𝐺)𝑧) = (𝑧(+g‘𝐺)𝑦)) ↔ (𝐻 ∈ Mnd ∧ ∀𝑤 ∈ (Base‘𝐻)∀𝑣 ∈ (Base‘𝐻)(𝑤(+g‘𝐻)𝑣) = (𝑣(+g‘𝐻)𝑤))))
63	12, 21	iscmn 19716	. . . . . . 7 ⊢ (𝐺 ∈ CMnd ↔ (𝐺 ∈ Mnd ∧ ∀𝑦 ∈ (Base‘𝐺)∀𝑧 ∈ (Base‘𝐺)(𝑦(+g‘𝐺)𝑧) = (𝑧(+g‘𝐺)𝑦)))
64	13, 29	iscmn 19716	. . . . . . 7 ⊢ (𝐻 ∈ CMnd ↔ (𝐻 ∈ Mnd ∧ ∀𝑤 ∈ (Base‘𝐻)∀𝑣 ∈ (Base‘𝐻)(𝑤(+g‘𝐻)𝑣) = (𝑣(+g‘𝐻)𝑤)))
65	62, 63, 64	3bitr4g 314	. . . . . 6 ⊢ (𝑥 ∈ (𝐺 GrpIso 𝐻) → (𝐺 ∈ CMnd ↔ 𝐻 ∈ CMnd))
66	8, 65	anbi12d 632	. . . . 5 ⊢ (𝑥 ∈ (𝐺 GrpIso 𝐻) → ((𝐺 ∈ Grp ∧ 𝐺 ∈ CMnd) ↔ (𝐻 ∈ Grp ∧ 𝐻 ∈ CMnd)))
67		isabl 19711	. . . . 5 ⊢ (𝐺 ∈ Abel ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ CMnd))
68		isabl 19711	. . . . 5 ⊢ (𝐻 ∈ Abel ↔ (𝐻 ∈ Grp ∧ 𝐻 ∈ CMnd))
69	66, 67, 68	3bitr4g 314	. . . 4 ⊢ (𝑥 ∈ (𝐺 GrpIso 𝐻) → (𝐺 ∈ Abel ↔ 𝐻 ∈ Abel))
70	69	exlimiv 1931	. . 3 ⊢ (∃𝑥 𝑥 ∈ (𝐺 GrpIso 𝐻) → (𝐺 ∈ Abel ↔ 𝐻 ∈ Abel))
71	2, 70	sylbi 217	. 2 ⊢ ((𝐺 GrpIso 𝐻) ≠ ∅ → (𝐺 ∈ Abel ↔ 𝐻 ∈ Abel))
72	1, 71	sylbi 217	1 ⊢ (𝐺 ≃𝑔 𝐻 → (𝐺 ∈ Abel ↔ 𝐻 ∈ Abel))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1541  ∃wex 1780   ∈ wcel 2113   ≠ wne 2930  ∀wral 3049   ⊆ wss 3899  ∅c0 4283   class class class wbr 5096   “ cima 5625   Fn wfn 6485  –1-1→wf1 6487  –onto→wfo 6488  –1-1-onto→wf1o 6489  ‘cfv 6490  (class class class)co 7356  Basecbs 17134  +_gcplusg 17175  Mndcmnd 18657  Grpcgrp 18861   GrpHom cghm 19139   GrpIso cgim 19184   ≃_𝑔 cgic 19185  CMndccmn 19707  Abelcabl 19708

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2706  ax-sep 5239  ax-nul 5249  ax-pow 5308  ax-pr 5375  ax-un 7678

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2809  df-nfc 2883  df-ne 2931  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-sbc 3739  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-iun 4946  df-br 5097  df-opab 5159  df-mpt 5178  df-id 5517  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-res 5634  df-ima 5635  df-suc 6321  df-iota 6446  df-fun 6492  df-fn 6493  df-f 6494  df-f1 6495  df-fo 6496  df-f1o 6497  df-fv 6498  df-ov 7359  df-oprab 7360  df-mpo 7361  df-1st 7931  df-2nd 7932  df-1o 8395  df-map 8763  df-mgm 18563  df-sgrp 18642  df-mnd 18658  df-grp 18864  df-ghm 19140  df-gim 19186  df-gic 19187  df-cmn 19709  df-abl 19710

This theorem is referenced by:  isnumbasgrplem1  43285