Metamath Proof Explorer

Theorem cycsubm

Description: The set of nonnegative integer powers of an element A of a monoid forms a submonoid containing A (see cycsubmcl ), called the cyclic monoid generated by the element A . This corresponds to the statement in Lang p. 6. (Contributed by AV, 28-Dec-2023)

Ref Expression
Hypotheses cycsubm.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
cycsubm.t ⊢ · = ( .g ‘ 𝐺 )
cycsubm.f ⊢ 𝐹 = ( 𝑥 ∈ ℕ0 ↦ ( 𝑥 · 𝐴 ) )
cycsubm.c ⊢ 𝐶 = ran 𝐹
Assertion cycsubm ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ) → 𝐶 ∈ ( SubMnd ‘ 𝐺 ) )

Proof

Step Hyp Ref Expression
1 cycsubm.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 cycsubm.t ⊢ · = ( .g ‘ 𝐺 )
3 cycsubm.f ⊢ 𝐹 = ( 𝑥 ∈ ℕ0 ↦ ( 𝑥 · 𝐴 ) )
4 cycsubm.c ⊢ 𝐶 = ran 𝐹
5 1 2 mulgnn0cl ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑥 ∈ ℕ0 ∧ 𝐴 ∈ 𝐵 ) → ( 𝑥 · 𝐴 ) ∈ 𝐵 )
6 5 3expa ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝑥 ∈ ℕ0 ) ∧ 𝐴 ∈ 𝐵 ) → ( 𝑥 · 𝐴 ) ∈ 𝐵 )
7 6 an32s ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ) ∧ 𝑥 ∈ ℕ0 ) → ( 𝑥 · 𝐴 ) ∈ 𝐵 )
8 7 3 fmptd ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ) → 𝐹 : ℕ0 ⟶ 𝐵 )
9 8 frnd ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ) → ran 𝐹 ⊆ 𝐵 )
10 4 9 eqsstrid ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ) → 𝐶 ⊆ 𝐵 )
11 0nn0 ⊢ 0 ∈ ℕ0
12 11 a1i ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ) → 0 ∈ ℕ0 )
13 oveq1 ⊢ ( 𝑖 = 0 → ( 𝑖 · 𝐴 ) = ( 0 · 𝐴 ) )
14 13 eqeq2d ⊢ ( 𝑖 = 0 → ( ( 0g ‘ 𝐺 ) = ( 𝑖 · 𝐴 ) ↔ ( 0g ‘ 𝐺 ) = ( 0 · 𝐴 ) ) )
15 14 adantl ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ) ∧ 𝑖 = 0 ) → ( ( 0g ‘ 𝐺 ) = ( 𝑖 · 𝐴 ) ↔ ( 0g ‘ 𝐺 ) = ( 0 · 𝐴 ) ) )
16 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
17 1 16 2 mulg0 ⊢ ( 𝐴 ∈ 𝐵 → ( 0 · 𝐴 ) = ( 0g ‘ 𝐺 ) )
18 17 adantl ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ) → ( 0 · 𝐴 ) = ( 0g ‘ 𝐺 ) )
19 18 eqcomd ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ) → ( 0g ‘ 𝐺 ) = ( 0 · 𝐴 ) )
20 12 15 19 rspcedvd ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ) → ∃ 𝑖 ∈ ℕ0 ( 0g ‘ 𝐺 ) = ( 𝑖 · 𝐴 ) )
21 1 2 3 4 cycsubmel ⊢ ( ( 0g ‘ 𝐺 ) ∈ 𝐶 ↔ ∃ 𝑖 ∈ ℕ0 ( 0g ‘ 𝐺 ) = ( 𝑖 · 𝐴 ) )
22 20 21 sylibr ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ) → ( 0g ‘ 𝐺 ) ∈ 𝐶 )
23 simplr ⊢ ( ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ) ∧ 𝑖 ∈ ℕ0 ) ∧ 𝑗 ∈ ℕ0 ) → 𝑖 ∈ ℕ0 )
24 simpr ⊢ ( ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ) ∧ 𝑖 ∈ ℕ0 ) ∧ 𝑗 ∈ ℕ0 ) → 𝑗 ∈ ℕ0 )
25 23 24 nn0addcld ⊢ ( ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ) ∧ 𝑖 ∈ ℕ0 ) ∧ 𝑗 ∈ ℕ0 ) → ( 𝑖 + 𝑗 ) ∈ ℕ0 )
26 25 adantr ⊢ ( ( ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ) ∧ 𝑖 ∈ ℕ0 ) ∧ 𝑗 ∈ ℕ0 ) ∧ ( 𝑏 = ( 𝑗 · 𝐴 ) ∧ 𝑎 = ( 𝑖 · 𝐴 ) ) ) → ( 𝑖 + 𝑗 ) ∈ ℕ0 )
27 oveq1 ⊢ ( 𝑘 = ( 𝑖 + 𝑗 ) → ( 𝑘 · 𝐴 ) = ( ( 𝑖 + 𝑗 ) · 𝐴 ) )
28 27 eqeq2d ⊢ ( 𝑘 = ( 𝑖 + 𝑗 ) → ( ( 𝑎 ( +g ‘ 𝐺 ) 𝑏 ) = ( 𝑘 · 𝐴 ) ↔ ( 𝑎 ( +g ‘ 𝐺 ) 𝑏 ) = ( ( 𝑖 + 𝑗 ) · 𝐴 ) ) )
29 28 adantl ⊢ ( ( ( ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ) ∧ 𝑖 ∈ ℕ0 ) ∧ 𝑗 ∈ ℕ0 ) ∧ ( 𝑏 = ( 𝑗 · 𝐴 ) ∧ 𝑎 = ( 𝑖 · 𝐴 ) ) ) ∧ 𝑘 = ( 𝑖 + 𝑗 ) ) → ( ( 𝑎 ( +g ‘ 𝐺 ) 𝑏 ) = ( 𝑘 · 𝐴 ) ↔ ( 𝑎 ( +g ‘ 𝐺 ) 𝑏 ) = ( ( 𝑖 + 𝑗 ) · 𝐴 ) ) )
30 oveq12 ⊢ ( ( 𝑎 = ( 𝑖 · 𝐴 ) ∧ 𝑏 = ( 𝑗 · 𝐴 ) ) → ( 𝑎 ( +g ‘ 𝐺 ) 𝑏 ) = ( ( 𝑖 · 𝐴 ) ( +g ‘ 𝐺 ) ( 𝑗 · 𝐴 ) ) )
31 30 ancoms ⊢ ( ( 𝑏 = ( 𝑗 · 𝐴 ) ∧ 𝑎 = ( 𝑖 · 𝐴 ) ) → ( 𝑎 ( +g ‘ 𝐺 ) 𝑏 ) = ( ( 𝑖 · 𝐴 ) ( +g ‘ 𝐺 ) ( 𝑗 · 𝐴 ) ) )
32 simplll ⊢ ( ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ) ∧ 𝑖 ∈ ℕ0 ) ∧ 𝑗 ∈ ℕ0 ) → 𝐺 ∈ Mnd )
33 simpllr ⊢ ( ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ) ∧ 𝑖 ∈ ℕ0 ) ∧ 𝑗 ∈ ℕ0 ) → 𝐴 ∈ 𝐵 )
34 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
35 1 2 34 mulgnn0dir ⊢ ( ( 𝐺 ∈ Mnd ∧ ( 𝑖 ∈ ℕ0 ∧ 𝑗 ∈ ℕ0 ∧ 𝐴 ∈ 𝐵 ) ) → ( ( 𝑖 + 𝑗 ) · 𝐴 ) = ( ( 𝑖 · 𝐴 ) ( +g ‘ 𝐺 ) ( 𝑗 · 𝐴 ) ) )
36 32 23 24 33 35 syl13anc ⊢ ( ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ) ∧ 𝑖 ∈ ℕ0 ) ∧ 𝑗 ∈ ℕ0 ) → ( ( 𝑖 + 𝑗 ) · 𝐴 ) = ( ( 𝑖 · 𝐴 ) ( +g ‘ 𝐺 ) ( 𝑗 · 𝐴 ) ) )
37 36 eqcomd ⊢ ( ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ) ∧ 𝑖 ∈ ℕ0 ) ∧ 𝑗 ∈ ℕ0 ) → ( ( 𝑖 · 𝐴 ) ( +g ‘ 𝐺 ) ( 𝑗 · 𝐴 ) ) = ( ( 𝑖 + 𝑗 ) · 𝐴 ) )
38 31 37 sylan9eqr ⊢ ( ( ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ) ∧ 𝑖 ∈ ℕ0 ) ∧ 𝑗 ∈ ℕ0 ) ∧ ( 𝑏 = ( 𝑗 · 𝐴 ) ∧ 𝑎 = ( 𝑖 · 𝐴 ) ) ) → ( 𝑎 ( +g ‘ 𝐺 ) 𝑏 ) = ( ( 𝑖 + 𝑗 ) · 𝐴 ) )
39 26 29 38 rspcedvd ⊢ ( ( ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ) ∧ 𝑖 ∈ ℕ0 ) ∧ 𝑗 ∈ ℕ0 ) ∧ ( 𝑏 = ( 𝑗 · 𝐴 ) ∧ 𝑎 = ( 𝑖 · 𝐴 ) ) ) → ∃ 𝑘 ∈ ℕ0 ( 𝑎 ( +g ‘ 𝐺 ) 𝑏 ) = ( 𝑘 · 𝐴 ) )
40 39 exp32 ⊢ ( ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ) ∧ 𝑖 ∈ ℕ0 ) ∧ 𝑗 ∈ ℕ0 ) → ( 𝑏 = ( 𝑗 · 𝐴 ) → ( 𝑎 = ( 𝑖 · 𝐴 ) → ∃ 𝑘 ∈ ℕ0 ( 𝑎 ( +g ‘ 𝐺 ) 𝑏 ) = ( 𝑘 · 𝐴 ) ) ) )
41 40 rexlimdva ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ) ∧ 𝑖 ∈ ℕ0 ) → ( ∃ 𝑗 ∈ ℕ0 𝑏 = ( 𝑗 · 𝐴 ) → ( 𝑎 = ( 𝑖 · 𝐴 ) → ∃ 𝑘 ∈ ℕ0 ( 𝑎 ( +g ‘ 𝐺 ) 𝑏 ) = ( 𝑘 · 𝐴 ) ) ) )
42 41 com23 ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ) ∧ 𝑖 ∈ ℕ0 ) → ( 𝑎 = ( 𝑖 · 𝐴 ) → ( ∃ 𝑗 ∈ ℕ0 𝑏 = ( 𝑗 · 𝐴 ) → ∃ 𝑘 ∈ ℕ0 ( 𝑎 ( +g ‘ 𝐺 ) 𝑏 ) = ( 𝑘 · 𝐴 ) ) ) )
43 42 rexlimdva ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ) → ( ∃ 𝑖 ∈ ℕ0 𝑎 = ( 𝑖 · 𝐴 ) → ( ∃ 𝑗 ∈ ℕ0 𝑏 = ( 𝑗 · 𝐴 ) → ∃ 𝑘 ∈ ℕ0 ( 𝑎 ( +g ‘ 𝐺 ) 𝑏 ) = ( 𝑘 · 𝐴 ) ) ) )
44 43 impd ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ) → ( ( ∃ 𝑖 ∈ ℕ0 𝑎 = ( 𝑖 · 𝐴 ) ∧ ∃ 𝑗 ∈ ℕ0 𝑏 = ( 𝑗 · 𝐴 ) ) → ∃ 𝑘 ∈ ℕ0 ( 𝑎 ( +g ‘ 𝐺 ) 𝑏 ) = ( 𝑘 · 𝐴 ) ) )
45 1 2 3 4 cycsubmel ⊢ ( 𝑎 ∈ 𝐶 ↔ ∃ 𝑖 ∈ ℕ0 𝑎 = ( 𝑖 · 𝐴 ) )
46 1 2 3 4 cycsubmel ⊢ ( 𝑏 ∈ 𝐶 ↔ ∃ 𝑗 ∈ ℕ0 𝑏 = ( 𝑗 · 𝐴 ) )
47 45 46 anbi12i ⊢ ( ( 𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶 ) ↔ ( ∃ 𝑖 ∈ ℕ0 𝑎 = ( 𝑖 · 𝐴 ) ∧ ∃ 𝑗 ∈ ℕ0 𝑏 = ( 𝑗 · 𝐴 ) ) )
48 1 2 3 4 cycsubmel ⊢ ( ( 𝑎 ( +g ‘ 𝐺 ) 𝑏 ) ∈ 𝐶 ↔ ∃ 𝑘 ∈ ℕ0 ( 𝑎 ( +g ‘ 𝐺 ) 𝑏 ) = ( 𝑘 · 𝐴 ) )
49 44 47 48 3imtr4g ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ) → ( ( 𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶 ) → ( 𝑎 ( +g ‘ 𝐺 ) 𝑏 ) ∈ 𝐶 ) )
50 49 ralrimivv ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ) → ∀ 𝑎 ∈ 𝐶 ∀ 𝑏 ∈ 𝐶 ( 𝑎 ( +g ‘ 𝐺 ) 𝑏 ) ∈ 𝐶 )
51 1 16 34 issubm ⊢ ( 𝐺 ∈ Mnd → ( 𝐶 ∈ ( SubMnd ‘ 𝐺 ) ↔ ( 𝐶 ⊆ 𝐵 ∧ ( 0g ‘ 𝐺 ) ∈ 𝐶 ∧ ∀ 𝑎 ∈ 𝐶 ∀ 𝑏 ∈ 𝐶 ( 𝑎 ( +g ‘ 𝐺 ) 𝑏 ) ∈ 𝐶 ) ) )
52 51 adantr ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ) → ( 𝐶 ∈ ( SubMnd ‘ 𝐺 ) ↔ ( 𝐶 ⊆ 𝐵 ∧ ( 0g ‘ 𝐺 ) ∈ 𝐶 ∧ ∀ 𝑎 ∈ 𝐶 ∀ 𝑏 ∈ 𝐶 ( 𝑎 ( +g ‘ 𝐺 ) 𝑏 ) ∈ 𝐶 ) ) )
53 10 22 50 52 mpbir3and ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ) → 𝐶 ∈ ( SubMnd ‘ 𝐺 ) )