Metamath Proof Explorer

Theorem finodsubmsubg

Description: A submonoid whose elements have finite order is a subgroup. (Contributed by SN, 31-Jan-2025)

Ref Expression
Hypotheses finodsubmsubg.o ⊢ 𝑂 = ( od ‘ 𝐺 )
finodsubmsubg.g ⊢ ( 𝜑 → 𝐺 ∈ Grp )
finodsubmsubg.s ⊢ ( 𝜑 → 𝑆 ∈ ( SubMnd ‘ 𝐺 ) )
finodsubmsubg.1 ⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝑆 ( 𝑂 ‘ 𝑎 ) ∈ ℕ )
Assertion finodsubmsubg ( 𝜑 → 𝑆 ∈ ( SubGrp ‘ 𝐺 ) )

Proof

Step Hyp Ref Expression
1 finodsubmsubg.o ⊢ 𝑂 = ( od ‘ 𝐺 )
2 finodsubmsubg.g ⊢ ( 𝜑 → 𝐺 ∈ Grp )
3 finodsubmsubg.s ⊢ ( 𝜑 → 𝑆 ∈ ( SubMnd ‘ 𝐺 ) )
4 finodsubmsubg.1 ⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝑆 ( 𝑂 ‘ 𝑎 ) ∈ ℕ )
5 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
6 eqid ⊢ ( .g ‘ 𝐺 ) = ( .g ‘ 𝐺 )
7 eqid ⊢ ( invg ‘ 𝐺 ) = ( invg ‘ 𝐺 )
8 2 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → 𝐺 ∈ Grp )
9 5 submss ⊢ ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) → 𝑆 ⊆ ( Base ‘ 𝐺 ) )
10 3 9 syl ⊢ ( 𝜑 → 𝑆 ⊆ ( Base ‘ 𝐺 ) )
11 10 sselda ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → 𝑎 ∈ ( Base ‘ 𝐺 ) )
12 5 1 6 7 8 11 odm1inv ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( ( ( 𝑂 ‘ 𝑎 ) − 1 ) ( .g ‘ 𝐺 ) 𝑎 ) = ( ( invg ‘ 𝐺 ) ‘ 𝑎 ) )
13 12 adantr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ ( 𝑂 ‘ 𝑎 ) ∈ ℕ ) → ( ( ( 𝑂 ‘ 𝑎 ) − 1 ) ( .g ‘ 𝐺 ) 𝑎 ) = ( ( invg ‘ 𝐺 ) ‘ 𝑎 ) )
14 eqid ⊢ ( Base ‘ ( 𝐺 ↾s 𝑆 ) ) = ( Base ‘ ( 𝐺 ↾s 𝑆 ) )
15 eqid ⊢ ( .g ‘ ( 𝐺 ↾s 𝑆 ) ) = ( .g ‘ ( 𝐺 ↾s 𝑆 ) )
16 eqid ⊢ ( 𝐺 ↾s 𝑆 ) = ( 𝐺 ↾s 𝑆 )
17 16 submmnd ⊢ ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) → ( 𝐺 ↾s 𝑆 ) ∈ Mnd )
18 3 17 syl ⊢ ( 𝜑 → ( 𝐺 ↾s 𝑆 ) ∈ Mnd )
19 18 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ ( 𝑂 ‘ 𝑎 ) ∈ ℕ ) → ( 𝐺 ↾s 𝑆 ) ∈ Mnd )
20 nnm1nn0 ⊢ ( ( 𝑂 ‘ 𝑎 ) ∈ ℕ → ( ( 𝑂 ‘ 𝑎 ) − 1 ) ∈ ℕ0 )
21 20 adantl ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ ( 𝑂 ‘ 𝑎 ) ∈ ℕ ) → ( ( 𝑂 ‘ 𝑎 ) − 1 ) ∈ ℕ0 )
22 simplr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ ( 𝑂 ‘ 𝑎 ) ∈ ℕ ) → 𝑎 ∈ 𝑆 )
23 16 5 ressbas2 ⊢ ( 𝑆 ⊆ ( Base ‘ 𝐺 ) → 𝑆 = ( Base ‘ ( 𝐺 ↾s 𝑆 ) ) )
24 10 23 syl ⊢ ( 𝜑 → 𝑆 = ( Base ‘ ( 𝐺 ↾s 𝑆 ) ) )
25 24 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ ( 𝑂 ‘ 𝑎 ) ∈ ℕ ) → 𝑆 = ( Base ‘ ( 𝐺 ↾s 𝑆 ) ) )
26 22 25 eleqtrd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ ( 𝑂 ‘ 𝑎 ) ∈ ℕ ) → 𝑎 ∈ ( Base ‘ ( 𝐺 ↾s 𝑆 ) ) )
27 14 15 19 21 26 mulgnn0cld ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ ( 𝑂 ‘ 𝑎 ) ∈ ℕ ) → ( ( ( 𝑂 ‘ 𝑎 ) − 1 ) ( .g ‘ ( 𝐺 ↾s 𝑆 ) ) 𝑎 ) ∈ ( Base ‘ ( 𝐺 ↾s 𝑆 ) ) )
28 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ ( 𝑂 ‘ 𝑎 ) ∈ ℕ ) → 𝑆 ∈ ( SubMnd ‘ 𝐺 ) )
29 6 16 15 submmulg ⊢ ( ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ∧ ( ( 𝑂 ‘ 𝑎 ) − 1 ) ∈ ℕ0 ∧ 𝑎 ∈ 𝑆 ) → ( ( ( 𝑂 ‘ 𝑎 ) − 1 ) ( .g ‘ 𝐺 ) 𝑎 ) = ( ( ( 𝑂 ‘ 𝑎 ) − 1 ) ( .g ‘ ( 𝐺 ↾s 𝑆 ) ) 𝑎 ) )
30 28 21 22 29 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ ( 𝑂 ‘ 𝑎 ) ∈ ℕ ) → ( ( ( 𝑂 ‘ 𝑎 ) − 1 ) ( .g ‘ 𝐺 ) 𝑎 ) = ( ( ( 𝑂 ‘ 𝑎 ) − 1 ) ( .g ‘ ( 𝐺 ↾s 𝑆 ) ) 𝑎 ) )
31 27 30 25 3eltr4d ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ ( 𝑂 ‘ 𝑎 ) ∈ ℕ ) → ( ( ( 𝑂 ‘ 𝑎 ) − 1 ) ( .g ‘ 𝐺 ) 𝑎 ) ∈ 𝑆 )
32 13 31 eqeltrrd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ ( 𝑂 ‘ 𝑎 ) ∈ ℕ ) → ( ( invg ‘ 𝐺 ) ‘ 𝑎 ) ∈ 𝑆 )
33 32 ex ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( ( 𝑂 ‘ 𝑎 ) ∈ ℕ → ( ( invg ‘ 𝐺 ) ‘ 𝑎 ) ∈ 𝑆 ) )
34 33 ralimdva ⊢ ( 𝜑 → ( ∀ 𝑎 ∈ 𝑆 ( 𝑂 ‘ 𝑎 ) ∈ ℕ → ∀ 𝑎 ∈ 𝑆 ( ( invg ‘ 𝐺 ) ‘ 𝑎 ) ∈ 𝑆 ) )
35 4 34 mpd ⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝑆 ( ( invg ‘ 𝐺 ) ‘ 𝑎 ) ∈ 𝑆 )
36 7 issubg3 ⊢ ( 𝐺 ∈ Grp → ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ↔ ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ∧ ∀ 𝑎 ∈ 𝑆 ( ( invg ‘ 𝐺 ) ‘ 𝑎 ) ∈ 𝑆 ) ) )
37 2 36 syl ⊢ ( 𝜑 → ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ↔ ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ∧ ∀ 𝑎 ∈ 𝑆 ( ( invg ‘ 𝐺 ) ‘ 𝑎 ) ∈ 𝑆 ) ) )
38 3 35 37 mpbir2and ⊢ ( 𝜑 → 𝑆 ∈ ( SubGrp ‘ 𝐺 ) )