Theorem gicabl 40924

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 18885	. 2 ⊢ (𝐺 ≃𝑔 𝐻 ↔ (𝐺 GrpIso 𝐻) ≠ ∅)
2		n0 4280	. . 3 ⊢ ((𝐺 GrpIso 𝐻) ≠ ∅ ↔ ∃𝑥 𝑥 ∈ (𝐺 GrpIso 𝐻))
3		gimghm 18880	. . . . . . . 8 ⊢ (𝑥 ∈ (𝐺 GrpIso 𝐻) → 𝑥 ∈ (𝐺 GrpHom 𝐻))
4		ghmgrp1 18836	. . . . . . . 8 ⊢ (𝑥 ∈ (𝐺 GrpHom 𝐻) → 𝐺 ∈ Grp)
5	3, 4	syl 17	. . . . . . 7 ⊢ (𝑥 ∈ (𝐺 GrpIso 𝐻) → 𝐺 ∈ Grp)
6		ghmgrp2 18837	. . . . . . . 8 ⊢ (𝑥 ∈ (𝐺 GrpHom 𝐻) → 𝐻 ∈ Grp)
7	3, 6	syl 17	. . . . . . 7 ⊢ (𝑥 ∈ (𝐺 GrpIso 𝐻) → 𝐻 ∈ Grp)
8	5, 7	2thd 264	. . . . . 6 ⊢ (𝑥 ∈ (𝐺 GrpIso 𝐻) → (𝐺 ∈ Grp ↔ 𝐻 ∈ Grp))
9	5	grpmndd 18589	. . . . . . . . 9 ⊢ (𝑥 ∈ (𝐺 GrpIso 𝐻) → 𝐺 ∈ Mnd)
10	7	grpmndd 18589	. . . . . . . . 9 ⊢ (𝑥 ∈ (𝐺 GrpIso 𝐻) → 𝐻 ∈ Mnd)
11	9, 10	2thd 264	. . . . . . . 8 ⊢ (𝑥 ∈ (𝐺 GrpIso 𝐻) → (𝐺 ∈ Mnd ↔ 𝐻 ∈ Mnd))
12		eqid 2738	. . . . . . . . . . . . . . . 16 ⊢ (Base‘𝐺) = (Base‘𝐺)
13		eqid 2738	. . . . . . . . . . . . . . . 16 ⊢ (Base‘𝐻) = (Base‘𝐻)
14	12, 13	gimf1o 18879	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (𝐺 GrpIso 𝐻) → 𝑥:(Base‘𝐺)–1-1-onto→(Base‘𝐻))
15		f1of1 6715	. . . . . . . . . . . . . . 15 ⊢ (𝑥:(Base‘𝐺)–1-1-onto→(Base‘𝐻) → 𝑥:(Base‘𝐺)–1-1→(Base‘𝐻))
16	14, 15	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (𝐺 GrpIso 𝐻) → 𝑥:(Base‘𝐺)–1-1→(Base‘𝐻))
17	16	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ (𝐺 GrpIso 𝐻) ∧ (𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) → 𝑥:(Base‘𝐺)–1-1→(Base‘𝐻))
18	5	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ (𝐺 GrpIso 𝐻) ∧ (𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) → 𝐺 ∈ Grp)
19		simprl 768	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ (𝐺 GrpIso 𝐻) ∧ (𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) → 𝑦 ∈ (Base‘𝐺))
20		simprr 770	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ (𝐺 GrpIso 𝐻) ∧ (𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) → 𝑧 ∈ (Base‘𝐺))
21		eqid 2738	. . . . . . . . . . . . . . 15 ⊢ (+g‘𝐺) = (+g‘𝐺)
22	12, 21	grpcl 18585	. . . . . . . . . . . . . 14 ⊢ ((𝐺 ∈ Grp ∧ 𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺)) → (𝑦(+g‘𝐺)𝑧) ∈ (Base‘𝐺))
23	18, 19, 20, 22	syl3anc 1370	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ (𝐺 GrpIso 𝐻) ∧ (𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) → (𝑦(+g‘𝐺)𝑧) ∈ (Base‘𝐺))
24	12, 21	grpcl 18585	. . . . . . . . . . . . . 14 ⊢ ((𝐺 ∈ Grp ∧ 𝑧 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) → (𝑧(+g‘𝐺)𝑦) ∈ (Base‘𝐺))
25	18, 20, 19, 24	syl3anc 1370	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ (𝐺 GrpIso 𝐻) ∧ (𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) → (𝑧(+g‘𝐺)𝑦) ∈ (Base‘𝐺))
26		f1fveq 7135	. . . . . . . . . . . . 13 ⊢ ((𝑥:(Base‘𝐺)–1-1→(Base‘𝐻) ∧ ((𝑦(+g‘𝐺)𝑧) ∈ (Base‘𝐺) ∧ (𝑧(+g‘𝐺)𝑦) ∈ (Base‘𝐺))) → ((𝑥‘(𝑦(+g‘𝐺)𝑧)) = (𝑥‘(𝑧(+g‘𝐺)𝑦)) ↔ (𝑦(+g‘𝐺)𝑧) = (𝑧(+g‘𝐺)𝑦)))
27	17, 23, 25, 26	syl12anc 834	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ (𝐺 GrpIso 𝐻) ∧ (𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) → ((𝑥‘(𝑦(+g‘𝐺)𝑧)) = (𝑥‘(𝑧(+g‘𝐺)𝑦)) ↔ (𝑦(+g‘𝐺)𝑧) = (𝑧(+g‘𝐺)𝑦)))
28	3	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ (𝐺 GrpIso 𝐻) ∧ (𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) → 𝑥 ∈ (𝐺 GrpHom 𝐻))
29		eqid 2738	. . . . . . . . . . . . . . 15 ⊢ (+g‘𝐻) = (+g‘𝐻)
30	12, 21, 29	ghmlin 18839	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺)) → (𝑥‘(𝑦(+g‘𝐺)𝑧)) = ((𝑥‘𝑦)(+g‘𝐻)(𝑥‘𝑧)))
31	28, 19, 20, 30	syl3anc 1370	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ (𝐺 GrpIso 𝐻) ∧ (𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) → (𝑥‘(𝑦(+g‘𝐺)𝑧)) = ((𝑥‘𝑦)(+g‘𝐻)(𝑥‘𝑧)))
32	12, 21, 29	ghmlin 18839	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑧 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) → (𝑥‘(𝑧(+g‘𝐺)𝑦)) = ((𝑥‘𝑧)(+g‘𝐻)(𝑥‘𝑦)))
33	28, 20, 19, 32	syl3anc 1370	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ (𝐺 GrpIso 𝐻) ∧ (𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) → (𝑥‘(𝑧(+g‘𝐺)𝑦)) = ((𝑥‘𝑧)(+g‘𝐻)(𝑥‘𝑦)))
34	31, 33	eqeq12d 2754	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ (𝐺 GrpIso 𝐻) ∧ (𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) → ((𝑥‘(𝑦(+g‘𝐺)𝑧)) = (𝑥‘(𝑧(+g‘𝐺)𝑦)) ↔ ((𝑥‘𝑦)(+g‘𝐻)(𝑥‘𝑧)) = ((𝑥‘𝑧)(+g‘𝐻)(𝑥‘𝑦))))
35	27, 34	bitr3d 280	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ (𝐺 GrpIso 𝐻) ∧ (𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) → ((𝑦(+g‘𝐺)𝑧) = (𝑧(+g‘𝐺)𝑦) ↔ ((𝑥‘𝑦)(+g‘𝐻)(𝑥‘𝑧)) = ((𝑥‘𝑧)(+g‘𝐻)(𝑥‘𝑦))))
36	35	2ralbidva 3128	. . . . . . . . . 10 ⊢ (𝑥 ∈ (𝐺 GrpIso 𝐻) → (∀𝑦 ∈ (Base‘𝐺)∀𝑧 ∈ (Base‘𝐺)(𝑦(+g‘𝐺)𝑧) = (𝑧(+g‘𝐺)𝑦) ↔ ∀𝑦 ∈ (Base‘𝐺)∀𝑧 ∈ (Base‘𝐺)((𝑥‘𝑦)(+g‘𝐻)(𝑥‘𝑧)) = ((𝑥‘𝑧)(+g‘𝐻)(𝑥‘𝑦))))
37		f1ofo 6723	. . . . . . . . . . . . . . 15 ⊢ (𝑥:(Base‘𝐺)–1-1-onto→(Base‘𝐻) → 𝑥:(Base‘𝐺)–onto→(Base‘𝐻))
38		foima 6693	. . . . . . . . . . . . . . 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 3348	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (𝐺 GrpIso 𝐻) → (∀𝑣 ∈ (𝑥 “ (Base‘𝐺))((𝑥‘𝑦)(+g‘𝐻)𝑣) = (𝑣(+g‘𝐻)(𝑥‘𝑦)) ↔ ∀𝑣 ∈ (Base‘𝐻)((𝑥‘𝑦)(+g‘𝐻)𝑣) = (𝑣(+g‘𝐻)(𝑥‘𝑦))))
42		f1ofn 6717	. . . . . . . . . . . . . 14 ⊢ (𝑥:(Base‘𝐺)–1-1-onto→(Base‘𝐻) → 𝑥 Fn (Base‘𝐺))
43	14, 42	syl 17	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (𝐺 GrpIso 𝐻) → 𝑥 Fn (Base‘𝐺))
44		ssid 3943	. . . . . . . . . . . . 13 ⊢ (Base‘𝐺) ⊆ (Base‘𝐺)
45		oveq2 7283	. . . . . . . . . . . . . . 15 ⊢ (𝑣 = (𝑥‘𝑧) → ((𝑥‘𝑦)(+g‘𝐻)𝑣) = ((𝑥‘𝑦)(+g‘𝐻)(𝑥‘𝑧)))
46		oveq1 7282	. . . . . . . . . . . . . . 15 ⊢ (𝑣 = (𝑥‘𝑧) → (𝑣(+g‘𝐻)(𝑥‘𝑦)) = ((𝑥‘𝑧)(+g‘𝐻)(𝑥‘𝑦)))
47	45, 46	eqeq12d 2754	. . . . . . . . . . . . . 14 ⊢ (𝑣 = (𝑥‘𝑧) → (((𝑥‘𝑦)(+g‘𝐻)𝑣) = (𝑣(+g‘𝐻)(𝑥‘𝑦)) ↔ ((𝑥‘𝑦)(+g‘𝐻)(𝑥‘𝑧)) = ((𝑥‘𝑧)(+g‘𝐻)(𝑥‘𝑦))))
48	47	ralima 7114	. . . . . . . . . . . . 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 280	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (𝐺 GrpIso 𝐻) → (∀𝑣 ∈ (Base‘𝐻)((𝑥‘𝑦)(+g‘𝐻)𝑣) = (𝑣(+g‘𝐻)(𝑥‘𝑦)) ↔ ∀𝑧 ∈ (Base‘𝐺)((𝑥‘𝑦)(+g‘𝐻)(𝑥‘𝑧)) = ((𝑥‘𝑧)(+g‘𝐻)(𝑥‘𝑦))))
51	50	ralbidv 3112	. . . . . . . . . 10 ⊢ (𝑥 ∈ (𝐺 GrpIso 𝐻) → (∀𝑦 ∈ (Base‘𝐺)∀𝑣 ∈ (Base‘𝐻)((𝑥‘𝑦)(+g‘𝐻)𝑣) = (𝑣(+g‘𝐻)(𝑥‘𝑦)) ↔ ∀𝑦 ∈ (Base‘𝐺)∀𝑧 ∈ (Base‘𝐺)((𝑥‘𝑦)(+g‘𝐻)(𝑥‘𝑧)) = ((𝑥‘𝑧)(+g‘𝐻)(𝑥‘𝑦))))
52	36, 51	bitr4d 281	. . . . . . . . 9 ⊢ (𝑥 ∈ (𝐺 GrpIso 𝐻) → (∀𝑦 ∈ (Base‘𝐺)∀𝑧 ∈ (Base‘𝐺)(𝑦(+g‘𝐺)𝑧) = (𝑧(+g‘𝐺)𝑦) ↔ ∀𝑦 ∈ (Base‘𝐺)∀𝑣 ∈ (Base‘𝐻)((𝑥‘𝑦)(+g‘𝐻)𝑣) = (𝑣(+g‘𝐻)(𝑥‘𝑦))))
53	40	raleqdv 3348	. . . . . . . . . 10 ⊢ (𝑥 ∈ (𝐺 GrpIso 𝐻) → (∀𝑤 ∈ (𝑥 “ (Base‘𝐺))∀𝑣 ∈ (Base‘𝐻)(𝑤(+g‘𝐻)𝑣) = (𝑣(+g‘𝐻)𝑤) ↔ ∀𝑤 ∈ (Base‘𝐻)∀𝑣 ∈ (Base‘𝐻)(𝑤(+g‘𝐻)𝑣) = (𝑣(+g‘𝐻)𝑤)))
54		oveq1 7282	. . . . . . . . . . . . . 14 ⊢ (𝑤 = (𝑥‘𝑦) → (𝑤(+g‘𝐻)𝑣) = ((𝑥‘𝑦)(+g‘𝐻)𝑣))
55		oveq2 7283	. . . . . . . . . . . . . 14 ⊢ (𝑤 = (𝑥‘𝑦) → (𝑣(+g‘𝐻)𝑤) = (𝑣(+g‘𝐻)(𝑥‘𝑦)))
56	54, 55	eqeq12d 2754	. . . . . . . . . . . . 13 ⊢ (𝑤 = (𝑥‘𝑦) → ((𝑤(+g‘𝐻)𝑣) = (𝑣(+g‘𝐻)𝑤) ↔ ((𝑥‘𝑦)(+g‘𝐻)𝑣) = (𝑣(+g‘𝐻)(𝑥‘𝑦))))
57	56	ralbidv 3112	. . . . . . . . . . . 12 ⊢ (𝑤 = (𝑥‘𝑦) → (∀𝑣 ∈ (Base‘𝐻)(𝑤(+g‘𝐻)𝑣) = (𝑣(+g‘𝐻)𝑤) ↔ ∀𝑣 ∈ (Base‘𝐻)((𝑥‘𝑦)(+g‘𝐻)𝑣) = (𝑣(+g‘𝐻)(𝑥‘𝑦))))
58	57	ralima 7114	. . . . . . . . . . 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 280	. . . . . . . . 9 ⊢ (𝑥 ∈ (𝐺 GrpIso 𝐻) → (∀𝑤 ∈ (Base‘𝐻)∀𝑣 ∈ (Base‘𝐻)(𝑤(+g‘𝐻)𝑣) = (𝑣(+g‘𝐻)𝑤) ↔ ∀𝑦 ∈ (Base‘𝐺)∀𝑣 ∈ (Base‘𝐻)((𝑥‘𝑦)(+g‘𝐻)𝑣) = (𝑣(+g‘𝐻)(𝑥‘𝑦))))
61	52, 60	bitr4d 281	. . . . . . . 8 ⊢ (𝑥 ∈ (𝐺 GrpIso 𝐻) → (∀𝑦 ∈ (Base‘𝐺)∀𝑧 ∈ (Base‘𝐺)(𝑦(+g‘𝐺)𝑧) = (𝑧(+g‘𝐺)𝑦) ↔ ∀𝑤 ∈ (Base‘𝐻)∀𝑣 ∈ (Base‘𝐻)(𝑤(+g‘𝐻)𝑣) = (𝑣(+g‘𝐻)𝑤)))
62	11, 61	anbi12d 631	. . . . . . 7 ⊢ (𝑥 ∈ (𝐺 GrpIso 𝐻) → ((𝐺 ∈ Mnd ∧ ∀𝑦 ∈ (Base‘𝐺)∀𝑧 ∈ (Base‘𝐺)(𝑦(+g‘𝐺)𝑧) = (𝑧(+g‘𝐺)𝑦)) ↔ (𝐻 ∈ Mnd ∧ ∀𝑤 ∈ (Base‘𝐻)∀𝑣 ∈ (Base‘𝐻)(𝑤(+g‘𝐻)𝑣) = (𝑣(+g‘𝐻)𝑤))))
63	12, 21	iscmn 19394	. . . . . . 7 ⊢ (𝐺 ∈ CMnd ↔ (𝐺 ∈ Mnd ∧ ∀𝑦 ∈ (Base‘𝐺)∀𝑧 ∈ (Base‘𝐺)(𝑦(+g‘𝐺)𝑧) = (𝑧(+g‘𝐺)𝑦)))
64	13, 29	iscmn 19394	. . . . . . 7 ⊢ (𝐻 ∈ CMnd ↔ (𝐻 ∈ Mnd ∧ ∀𝑤 ∈ (Base‘𝐻)∀𝑣 ∈ (Base‘𝐻)(𝑤(+g‘𝐻)𝑣) = (𝑣(+g‘𝐻)𝑤)))
65	62, 63, 64	3bitr4g 314	. . . . . 6 ⊢ (𝑥 ∈ (𝐺 GrpIso 𝐻) → (𝐺 ∈ CMnd ↔ 𝐻 ∈ CMnd))
66	8, 65	anbi12d 631	. . . . 5 ⊢ (𝑥 ∈ (𝐺 GrpIso 𝐻) → ((𝐺 ∈ Grp ∧ 𝐺 ∈ CMnd) ↔ (𝐻 ∈ Grp ∧ 𝐻 ∈ CMnd)))
67		isabl 19390	. . . . 5 ⊢ (𝐺 ∈ Abel ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ CMnd))
68		isabl 19390	. . . . 5 ⊢ (𝐻 ∈ Abel ↔ (𝐻 ∈ Grp ∧ 𝐻 ∈ CMnd))
69	66, 67, 68	3bitr4g 314	. . . 4 ⊢ (𝑥 ∈ (𝐺 GrpIso 𝐻) → (𝐺 ∈ Abel ↔ 𝐻 ∈ Abel))
70	69	exlimiv 1933	. . 3 ⊢ (∃𝑥 𝑥 ∈ (𝐺 GrpIso 𝐻) → (𝐺 ∈ Abel ↔ 𝐻 ∈ Abel))
71	2, 70	sylbi 216	. 2 ⊢ ((𝐺 GrpIso 𝐻) ≠ ∅ → (𝐺 ∈ Abel ↔ 𝐻 ∈ Abel))
72	1, 71	sylbi 216	1 ⊢ (𝐺 ≃𝑔 𝐻 → (𝐺 ∈ Abel ↔ 𝐻 ∈ Abel))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1539  ∃wex 1782   ∈ wcel 2106   ≠ wne 2943  ∀wral 3064   ⊆ wss 3887  ∅c0 4256   class class class wbr 5074   “ cima 5592   Fn wfn 6428  –1-1→wf1 6430  –onto→wfo 6431  –1-1-onto→wf1o 6432  ‘cfv 6433  (class class class)co 7275  Basecbs 16912  +_gcplusg 16962  Mndcmnd 18385  Grpcgrp 18577   GrpHom cghm 18831   GrpIso cgim 18873   ≃_𝑔 cgic 18874  CMndccmn 19386  Abelcabl 19387

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-rep 5209  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7588

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-ral 3069  df-rex 3070  df-reu 3072  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-iun 4926  df-br 5075  df-opab 5137  df-mpt 5158  df-id 5489  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-suc 6272  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-f1 6438  df-fo 6439  df-f1o 6440  df-fv 6441  df-ov 7278  df-oprab 7279  df-mpo 7280  df-1st 7831  df-2nd 7832  df-1o 8297  df-mgm 18326  df-sgrp 18375  df-mnd 18386  df-grp 18580  df-ghm 18832  df-gim 18875  df-gic 18876  df-cmn 19388  df-abl 19389

This theorem is referenced by:  isnumbasgrplem1  40926