Theorem torsubg

Description: The set of all elements of finite order forms a subgroup of any abelian group, called the torsion subgroup. (Contributed by Mario Carneiro, 20-Oct-2015)

	Ref	Expression
Hypothesis	torsubg.1	⊢ 𝑂 = ( od ‘ 𝐺 )
Assertion	torsubg	⊢ ( 𝐺 ∈ Abel → ( ◡ 𝑂 “ ℕ ) ∈ ( SubGrp ‘ 𝐺 ) )

Proof

Step	Hyp	Ref	Expression
1		torsubg.1	⊢ 𝑂 = ( od ‘ 𝐺 )
2		cnvimass	⊢ ( ◡ 𝑂 “ ℕ ) ⊆ dom 𝑂
3		eqid	⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
4	3 1	odf	⊢ 𝑂 : ( Base ‘ 𝐺 ) ⟶ ℕ0
5	4	fdmi	⊢ dom 𝑂 = ( Base ‘ 𝐺 )
6	2 5	sseqtri	⊢ ( ◡ 𝑂 “ ℕ ) ⊆ ( Base ‘ 𝐺 )
7	6	a1i	⊢ ( 𝐺 ∈ Abel → ( ◡ 𝑂 “ ℕ ) ⊆ ( Base ‘ 𝐺 ) )
8		ablgrp	⊢ ( 𝐺 ∈ Abel → 𝐺 ∈ Grp )
9		eqid	⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
10	3 9	grpidcl	⊢ ( 𝐺 ∈ Grp → ( 0g ‘ 𝐺 ) ∈ ( Base ‘ 𝐺 ) )
11	8 10	syl	⊢ ( 𝐺 ∈ Abel → ( 0g ‘ 𝐺 ) ∈ ( Base ‘ 𝐺 ) )
12	1 9	od1	⊢ ( 𝐺 ∈ Grp → ( 𝑂 ‘ ( 0g ‘ 𝐺 ) ) = 1 )
13	8 12	syl	⊢ ( 𝐺 ∈ Abel → ( 𝑂 ‘ ( 0g ‘ 𝐺 ) ) = 1 )
14		1nn	⊢ 1 ∈ ℕ
15	13 14	eqeltrdi	⊢ ( 𝐺 ∈ Abel → ( 𝑂 ‘ ( 0g ‘ 𝐺 ) ) ∈ ℕ )
16		ffn	⊢ ( 𝑂 : ( Base ‘ 𝐺 ) ⟶ ℕ0 → 𝑂 Fn ( Base ‘ 𝐺 ) )
17	4 16	ax-mp	⊢ 𝑂 Fn ( Base ‘ 𝐺 )
18		elpreima	⊢ ( 𝑂 Fn ( Base ‘ 𝐺 ) → ( ( 0g ‘ 𝐺 ) ∈ ( ◡ 𝑂 “ ℕ ) ↔ ( ( 0g ‘ 𝐺 ) ∈ ( Base ‘ 𝐺 ) ∧ ( 𝑂 ‘ ( 0g ‘ 𝐺 ) ) ∈ ℕ ) ) )
19	17 18	ax-mp	⊢ ( ( 0g ‘ 𝐺 ) ∈ ( ◡ 𝑂 “ ℕ ) ↔ ( ( 0g ‘ 𝐺 ) ∈ ( Base ‘ 𝐺 ) ∧ ( 𝑂 ‘ ( 0g ‘ 𝐺 ) ) ∈ ℕ ) )
20	11 15 19	sylanbrc	⊢ ( 𝐺 ∈ Abel → ( 0g ‘ 𝐺 ) ∈ ( ◡ 𝑂 “ ℕ ) )
21	20	ne0d	⊢ ( 𝐺 ∈ Abel → ( ◡ 𝑂 “ ℕ ) ≠ ∅ )
22	8	ad2antrr	⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝑥 ∈ ( ◡ 𝑂 “ ℕ ) ) ∧ 𝑦 ∈ ( ◡ 𝑂 “ ℕ ) ) → 𝐺 ∈ Grp )
23	6	sseli	⊢ ( 𝑥 ∈ ( ◡ 𝑂 “ ℕ ) → 𝑥 ∈ ( Base ‘ 𝐺 ) )
24	23	ad2antlr	⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝑥 ∈ ( ◡ 𝑂 “ ℕ ) ) ∧ 𝑦 ∈ ( ◡ 𝑂 “ ℕ ) ) → 𝑥 ∈ ( Base ‘ 𝐺 ) )
25	6	sseli	⊢ ( 𝑦 ∈ ( ◡ 𝑂 “ ℕ ) → 𝑦 ∈ ( Base ‘ 𝐺 ) )
26	25	adantl	⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝑥 ∈ ( ◡ 𝑂 “ ℕ ) ) ∧ 𝑦 ∈ ( ◡ 𝑂 “ ℕ ) ) → 𝑦 ∈ ( Base ‘ 𝐺 ) )
27		eqid	⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
28	3 27	grpcl	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ ( Base ‘ 𝐺 ) )
29	22 24 26 28	syl3anc	⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝑥 ∈ ( ◡ 𝑂 “ ℕ ) ) ∧ 𝑦 ∈ ( ◡ 𝑂 “ ℕ ) ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ ( Base ‘ 𝐺 ) )
30		0nnn	⊢ ¬ 0 ∈ ℕ
31	3 1	odcl	⊢ ( 𝑥 ∈ ( Base ‘ 𝐺 ) → ( 𝑂 ‘ 𝑥 ) ∈ ℕ0 )
32	24 31	syl	⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝑥 ∈ ( ◡ 𝑂 “ ℕ ) ) ∧ 𝑦 ∈ ( ◡ 𝑂 “ ℕ ) ) → ( 𝑂 ‘ 𝑥 ) ∈ ℕ0 )
33	32	nn0zd	⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝑥 ∈ ( ◡ 𝑂 “ ℕ ) ) ∧ 𝑦 ∈ ( ◡ 𝑂 “ ℕ ) ) → ( 𝑂 ‘ 𝑥 ) ∈ ℤ )
34	3 1	odcl	⊢ ( 𝑦 ∈ ( Base ‘ 𝐺 ) → ( 𝑂 ‘ 𝑦 ) ∈ ℕ0 )
35	26 34	syl	⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝑥 ∈ ( ◡ 𝑂 “ ℕ ) ) ∧ 𝑦 ∈ ( ◡ 𝑂 “ ℕ ) ) → ( 𝑂 ‘ 𝑦 ) ∈ ℕ0 )
36	35	nn0zd	⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝑥 ∈ ( ◡ 𝑂 “ ℕ ) ) ∧ 𝑦 ∈ ( ◡ 𝑂 “ ℕ ) ) → ( 𝑂 ‘ 𝑦 ) ∈ ℤ )
37	33 36	gcdcld	⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝑥 ∈ ( ◡ 𝑂 “ ℕ ) ) ∧ 𝑦 ∈ ( ◡ 𝑂 “ ℕ ) ) → ( ( 𝑂 ‘ 𝑥 ) gcd ( 𝑂 ‘ 𝑦 ) ) ∈ ℕ0 )
38	37	nn0cnd	⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝑥 ∈ ( ◡ 𝑂 “ ℕ ) ) ∧ 𝑦 ∈ ( ◡ 𝑂 “ ℕ ) ) → ( ( 𝑂 ‘ 𝑥 ) gcd ( 𝑂 ‘ 𝑦 ) ) ∈ ℂ )
39	38	mul02d	⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝑥 ∈ ( ◡ 𝑂 “ ℕ ) ) ∧ 𝑦 ∈ ( ◡ 𝑂 “ ℕ ) ) → ( 0 · ( ( 𝑂 ‘ 𝑥 ) gcd ( 𝑂 ‘ 𝑦 ) ) ) = 0 )
40	39	breq1d	⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝑥 ∈ ( ◡ 𝑂 “ ℕ ) ) ∧ 𝑦 ∈ ( ◡ 𝑂 “ ℕ ) ) → ( ( 0 · ( ( 𝑂 ‘ 𝑥 ) gcd ( 𝑂 ‘ 𝑦 ) ) ) ∥ ( ( 𝑂 ‘ 𝑥 ) · ( 𝑂 ‘ 𝑦 ) ) ↔ 0 ∥ ( ( 𝑂 ‘ 𝑥 ) · ( 𝑂 ‘ 𝑦 ) ) ) )
41	33 36	zmulcld	⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝑥 ∈ ( ◡ 𝑂 “ ℕ ) ) ∧ 𝑦 ∈ ( ◡ 𝑂 “ ℕ ) ) → ( ( 𝑂 ‘ 𝑥 ) · ( 𝑂 ‘ 𝑦 ) ) ∈ ℤ )
42		0dvds	⊢ ( ( ( 𝑂 ‘ 𝑥 ) · ( 𝑂 ‘ 𝑦 ) ) ∈ ℤ → ( 0 ∥ ( ( 𝑂 ‘ 𝑥 ) · ( 𝑂 ‘ 𝑦 ) ) ↔ ( ( 𝑂 ‘ 𝑥 ) · ( 𝑂 ‘ 𝑦 ) ) = 0 ) )
43	41 42	syl	⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝑥 ∈ ( ◡ 𝑂 “ ℕ ) ) ∧ 𝑦 ∈ ( ◡ 𝑂 “ ℕ ) ) → ( 0 ∥ ( ( 𝑂 ‘ 𝑥 ) · ( 𝑂 ‘ 𝑦 ) ) ↔ ( ( 𝑂 ‘ 𝑥 ) · ( 𝑂 ‘ 𝑦 ) ) = 0 ) )
44	40 43	bitrd	⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝑥 ∈ ( ◡ 𝑂 “ ℕ ) ) ∧ 𝑦 ∈ ( ◡ 𝑂 “ ℕ ) ) → ( ( 0 · ( ( 𝑂 ‘ 𝑥 ) gcd ( 𝑂 ‘ 𝑦 ) ) ) ∥ ( ( 𝑂 ‘ 𝑥 ) · ( 𝑂 ‘ 𝑦 ) ) ↔ ( ( 𝑂 ‘ 𝑥 ) · ( 𝑂 ‘ 𝑦 ) ) = 0 ) )
45		elpreima	⊢ ( 𝑂 Fn ( Base ‘ 𝐺 ) → ( 𝑥 ∈ ( ◡ 𝑂 “ ℕ ) ↔ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ ( 𝑂 ‘ 𝑥 ) ∈ ℕ ) ) )
46	17 45	ax-mp	⊢ ( 𝑥 ∈ ( ◡ 𝑂 “ ℕ ) ↔ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ ( 𝑂 ‘ 𝑥 ) ∈ ℕ ) )
47	46	simprbi	⊢ ( 𝑥 ∈ ( ◡ 𝑂 “ ℕ ) → ( 𝑂 ‘ 𝑥 ) ∈ ℕ )
48	47	ad2antlr	⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝑥 ∈ ( ◡ 𝑂 “ ℕ ) ) ∧ 𝑦 ∈ ( ◡ 𝑂 “ ℕ ) ) → ( 𝑂 ‘ 𝑥 ) ∈ ℕ )
49		elpreima	⊢ ( 𝑂 Fn ( Base ‘ 𝐺 ) → ( 𝑦 ∈ ( ◡ 𝑂 “ ℕ ) ↔ ( 𝑦 ∈ ( Base ‘ 𝐺 ) ∧ ( 𝑂 ‘ 𝑦 ) ∈ ℕ ) ) )
50	17 49	ax-mp	⊢ ( 𝑦 ∈ ( ◡ 𝑂 “ ℕ ) ↔ ( 𝑦 ∈ ( Base ‘ 𝐺 ) ∧ ( 𝑂 ‘ 𝑦 ) ∈ ℕ ) )
51	50	simprbi	⊢ ( 𝑦 ∈ ( ◡ 𝑂 “ ℕ ) → ( 𝑂 ‘ 𝑦 ) ∈ ℕ )
52	51	adantl	⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝑥 ∈ ( ◡ 𝑂 “ ℕ ) ) ∧ 𝑦 ∈ ( ◡ 𝑂 “ ℕ ) ) → ( 𝑂 ‘ 𝑦 ) ∈ ℕ )
53	48 52	nnmulcld	⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝑥 ∈ ( ◡ 𝑂 “ ℕ ) ) ∧ 𝑦 ∈ ( ◡ 𝑂 “ ℕ ) ) → ( ( 𝑂 ‘ 𝑥 ) · ( 𝑂 ‘ 𝑦 ) ) ∈ ℕ )
54		eleq1	⊢ ( ( ( 𝑂 ‘ 𝑥 ) · ( 𝑂 ‘ 𝑦 ) ) = 0 → ( ( ( 𝑂 ‘ 𝑥 ) · ( 𝑂 ‘ 𝑦 ) ) ∈ ℕ ↔ 0 ∈ ℕ ) )
55	53 54	syl5ibcom	⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝑥 ∈ ( ◡ 𝑂 “ ℕ ) ) ∧ 𝑦 ∈ ( ◡ 𝑂 “ ℕ ) ) → ( ( ( 𝑂 ‘ 𝑥 ) · ( 𝑂 ‘ 𝑦 ) ) = 0 → 0 ∈ ℕ ) )
56	44 55	sylbid	⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝑥 ∈ ( ◡ 𝑂 “ ℕ ) ) ∧ 𝑦 ∈ ( ◡ 𝑂 “ ℕ ) ) → ( ( 0 · ( ( 𝑂 ‘ 𝑥 ) gcd ( 𝑂 ‘ 𝑦 ) ) ) ∥ ( ( 𝑂 ‘ 𝑥 ) · ( 𝑂 ‘ 𝑦 ) ) → 0 ∈ ℕ ) )
57	30 56	mtoi	⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝑥 ∈ ( ◡ 𝑂 “ ℕ ) ) ∧ 𝑦 ∈ ( ◡ 𝑂 “ ℕ ) ) → ¬ ( 0 · ( ( 𝑂 ‘ 𝑥 ) gcd ( 𝑂 ‘ 𝑦 ) ) ) ∥ ( ( 𝑂 ‘ 𝑥 ) · ( 𝑂 ‘ 𝑦 ) ) )
58		simpll	⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝑥 ∈ ( ◡ 𝑂 “ ℕ ) ) ∧ 𝑦 ∈ ( ◡ 𝑂 “ ℕ ) ) → 𝐺 ∈ Abel )
59	1 3 27	odadd1	⊢ ( ( 𝐺 ∈ Abel ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) → ( ( 𝑂 ‘ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) · ( ( 𝑂 ‘ 𝑥 ) gcd ( 𝑂 ‘ 𝑦 ) ) ) ∥ ( ( 𝑂 ‘ 𝑥 ) · ( 𝑂 ‘ 𝑦 ) ) )
60	58 24 26 59	syl3anc	⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝑥 ∈ ( ◡ 𝑂 “ ℕ ) ) ∧ 𝑦 ∈ ( ◡ 𝑂 “ ℕ ) ) → ( ( 𝑂 ‘ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) · ( ( 𝑂 ‘ 𝑥 ) gcd ( 𝑂 ‘ 𝑦 ) ) ) ∥ ( ( 𝑂 ‘ 𝑥 ) · ( 𝑂 ‘ 𝑦 ) ) )
61		oveq1	⊢ ( ( 𝑂 ‘ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) = 0 → ( ( 𝑂 ‘ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) · ( ( 𝑂 ‘ 𝑥 ) gcd ( 𝑂 ‘ 𝑦 ) ) ) = ( 0 · ( ( 𝑂 ‘ 𝑥 ) gcd ( 𝑂 ‘ 𝑦 ) ) ) )
62	61	breq1d	⊢ ( ( 𝑂 ‘ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) = 0 → ( ( ( 𝑂 ‘ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) · ( ( 𝑂 ‘ 𝑥 ) gcd ( 𝑂 ‘ 𝑦 ) ) ) ∥ ( ( 𝑂 ‘ 𝑥 ) · ( 𝑂 ‘ 𝑦 ) ) ↔ ( 0 · ( ( 𝑂 ‘ 𝑥 ) gcd ( 𝑂 ‘ 𝑦 ) ) ) ∥ ( ( 𝑂 ‘ 𝑥 ) · ( 𝑂 ‘ 𝑦 ) ) ) )
63	60 62	syl5ibcom	⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝑥 ∈ ( ◡ 𝑂 “ ℕ ) ) ∧ 𝑦 ∈ ( ◡ 𝑂 “ ℕ ) ) → ( ( 𝑂 ‘ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) = 0 → ( 0 · ( ( 𝑂 ‘ 𝑥 ) gcd ( 𝑂 ‘ 𝑦 ) ) ) ∥ ( ( 𝑂 ‘ 𝑥 ) · ( 𝑂 ‘ 𝑦 ) ) ) )
64	57 63	mtod	⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝑥 ∈ ( ◡ 𝑂 “ ℕ ) ) ∧ 𝑦 ∈ ( ◡ 𝑂 “ ℕ ) ) → ¬ ( 𝑂 ‘ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) = 0 )
65	3 1	odcl	⊢ ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ ( Base ‘ 𝐺 ) → ( 𝑂 ‘ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) ∈ ℕ0 )
66	29 65	syl	⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝑥 ∈ ( ◡ 𝑂 “ ℕ ) ) ∧ 𝑦 ∈ ( ◡ 𝑂 “ ℕ ) ) → ( 𝑂 ‘ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) ∈ ℕ0 )
67		elnn0	⊢ ( ( 𝑂 ‘ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) ∈ ℕ0 ↔ ( ( 𝑂 ‘ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) ∈ ℕ ∨ ( 𝑂 ‘ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) = 0 ) )
68	66 67	sylib	⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝑥 ∈ ( ◡ 𝑂 “ ℕ ) ) ∧ 𝑦 ∈ ( ◡ 𝑂 “ ℕ ) ) → ( ( 𝑂 ‘ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) ∈ ℕ ∨ ( 𝑂 ‘ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) = 0 ) )
69	68	ord	⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝑥 ∈ ( ◡ 𝑂 “ ℕ ) ) ∧ 𝑦 ∈ ( ◡ 𝑂 “ ℕ ) ) → ( ¬ ( 𝑂 ‘ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) ∈ ℕ → ( 𝑂 ‘ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) = 0 ) )
70	64 69	mt3d	⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝑥 ∈ ( ◡ 𝑂 “ ℕ ) ) ∧ 𝑦 ∈ ( ◡ 𝑂 “ ℕ ) ) → ( 𝑂 ‘ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) ∈ ℕ )
71		elpreima	⊢ ( 𝑂 Fn ( Base ‘ 𝐺 ) → ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ ( ◡ 𝑂 “ ℕ ) ↔ ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ ( Base ‘ 𝐺 ) ∧ ( 𝑂 ‘ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) ∈ ℕ ) ) )
72	17 71	ax-mp	⊢ ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ ( ◡ 𝑂 “ ℕ ) ↔ ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ ( Base ‘ 𝐺 ) ∧ ( 𝑂 ‘ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) ∈ ℕ ) )
73	29 70 72	sylanbrc	⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝑥 ∈ ( ◡ 𝑂 “ ℕ ) ) ∧ 𝑦 ∈ ( ◡ 𝑂 “ ℕ ) ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ ( ◡ 𝑂 “ ℕ ) )
74	73	ralrimiva	⊢ ( ( 𝐺 ∈ Abel ∧ 𝑥 ∈ ( ◡ 𝑂 “ ℕ ) ) → ∀ 𝑦 ∈ ( ◡ 𝑂 “ ℕ ) ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ ( ◡ 𝑂 “ ℕ ) )
75		eqid	⊢ ( invg ‘ 𝐺 ) = ( invg ‘ 𝐺 )
76	3 75	grpinvcl	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) → ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝐺 ) )
77	8 23 76	syl2an	⊢ ( ( 𝐺 ∈ Abel ∧ 𝑥 ∈ ( ◡ 𝑂 “ ℕ ) ) → ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝐺 ) )
78	1 75 3	odinv	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) → ( 𝑂 ‘ ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ) = ( 𝑂 ‘ 𝑥 ) )
79	8 23 78	syl2an	⊢ ( ( 𝐺 ∈ Abel ∧ 𝑥 ∈ ( ◡ 𝑂 “ ℕ ) ) → ( 𝑂 ‘ ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ) = ( 𝑂 ‘ 𝑥 ) )
80	47	adantl	⊢ ( ( 𝐺 ∈ Abel ∧ 𝑥 ∈ ( ◡ 𝑂 “ ℕ ) ) → ( 𝑂 ‘ 𝑥 ) ∈ ℕ )
81	79 80	eqeltrd	⊢ ( ( 𝐺 ∈ Abel ∧ 𝑥 ∈ ( ◡ 𝑂 “ ℕ ) ) → ( 𝑂 ‘ ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ) ∈ ℕ )
82		elpreima	⊢ ( 𝑂 Fn ( Base ‘ 𝐺 ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ ( ◡ 𝑂 “ ℕ ) ↔ ( ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝐺 ) ∧ ( 𝑂 ‘ ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ) ∈ ℕ ) ) )
83	17 82	ax-mp	⊢ ( ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ ( ◡ 𝑂 “ ℕ ) ↔ ( ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝐺 ) ∧ ( 𝑂 ‘ ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ) ∈ ℕ ) )
84	77 81 83	sylanbrc	⊢ ( ( 𝐺 ∈ Abel ∧ 𝑥 ∈ ( ◡ 𝑂 “ ℕ ) ) → ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ ( ◡ 𝑂 “ ℕ ) )
85	74 84	jca	⊢ ( ( 𝐺 ∈ Abel ∧ 𝑥 ∈ ( ◡ 𝑂 “ ℕ ) ) → ( ∀ 𝑦 ∈ ( ◡ 𝑂 “ ℕ ) ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ ( ◡ 𝑂 “ ℕ ) ∧ ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ ( ◡ 𝑂 “ ℕ ) ) )
86	85	ralrimiva	⊢ ( 𝐺 ∈ Abel → ∀ 𝑥 ∈ ( ◡ 𝑂 “ ℕ ) ( ∀ 𝑦 ∈ ( ◡ 𝑂 “ ℕ ) ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ ( ◡ 𝑂 “ ℕ ) ∧ ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ ( ◡ 𝑂 “ ℕ ) ) )
87	3 27 75	issubg2	⊢ ( 𝐺 ∈ Grp → ( ( ◡ 𝑂 “ ℕ ) ∈ ( SubGrp ‘ 𝐺 ) ↔ ( ( ◡ 𝑂 “ ℕ ) ⊆ ( Base ‘ 𝐺 ) ∧ ( ◡ 𝑂 “ ℕ ) ≠ ∅ ∧ ∀ 𝑥 ∈ ( ◡ 𝑂 “ ℕ ) ( ∀ 𝑦 ∈ ( ◡ 𝑂 “ ℕ ) ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ ( ◡ 𝑂 “ ℕ ) ∧ ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ ( ◡ 𝑂 “ ℕ ) ) ) ) )
88	8 87	syl	⊢ ( 𝐺 ∈ Abel → ( ( ◡ 𝑂 “ ℕ ) ∈ ( SubGrp ‘ 𝐺 ) ↔ ( ( ◡ 𝑂 “ ℕ ) ⊆ ( Base ‘ 𝐺 ) ∧ ( ◡ 𝑂 “ ℕ ) ≠ ∅ ∧ ∀ 𝑥 ∈ ( ◡ 𝑂 “ ℕ ) ( ∀ 𝑦 ∈ ( ◡ 𝑂 “ ℕ ) ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ ( ◡ 𝑂 “ ℕ ) ∧ ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ ( ◡ 𝑂 “ ℕ ) ) ) ) )
89	7 21 86 88	mpbir3and	⊢ ( 𝐺 ∈ Abel → ( ◡ 𝑂 “ ℕ ) ∈ ( SubGrp ‘ 𝐺 ) )