This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nsmndex1

Description: The base set B of the constructed monoid S is not a submonoid of the monoid M of endofunctions on set NN0 , although M e. Mnd and S e. Mnd and B C_ ( BaseM ) hold. (Contributed by AV, 17-Feb-2024)

Ref Expression
Hypotheses smndex1ibas.m ⊢ 𝑀 = ( EndoFMnd ‘ ℕ0 )
smndex1ibas.n ⊢ 𝑁 ∈ ℕ
smndex1ibas.i ⊢ 𝐼 = ( 𝑥 ∈ ℕ0 ↦ ( 𝑥 mod 𝑁 ) )
smndex1ibas.g ⊢ 𝐺 = ( 𝑛 ∈ ( 0 ..^ 𝑁 ) ↦ ( 𝑥 ∈ ℕ0 ↦ 𝑛 ) )
smndex1mgm.b ⊢ 𝐵 = ( { 𝐼 } ∪ ∪ 𝑛 ∈ ( 0 ..^ 𝑁 ) { ( 𝐺 ‘ 𝑛 ) } )
smndex1mgm.s ⊢ 𝑆 = ( 𝑀 ↾s 𝐵 )
Assertion nsmndex1 𝐵 ∉ ( SubMnd ‘ 𝑀 )

Proof

Step Hyp Ref Expression
1 smndex1ibas.m ⊢ 𝑀 = ( EndoFMnd ‘ ℕ0 )
2 smndex1ibas.n ⊢ 𝑁 ∈ ℕ
3 smndex1ibas.i ⊢ 𝐼 = ( 𝑥 ∈ ℕ0 ↦ ( 𝑥 mod 𝑁 ) )
4 smndex1ibas.g ⊢ 𝐺 = ( 𝑛 ∈ ( 0 ..^ 𝑁 ) ↦ ( 𝑥 ∈ ℕ0 ↦ 𝑛 ) )
5 smndex1mgm.b ⊢ 𝐵 = ( { 𝐼 } ∪ ∪ 𝑛 ∈ ( 0 ..^ 𝑁 ) { ( 𝐺 ‘ 𝑛 ) } )
6 smndex1mgm.s ⊢ 𝑆 = ( 𝑀 ↾s 𝐵 )
7 1 2 3 4 5 6 smndex1n0mnd ⊢ ( 0g ‘ 𝑀 ) ∉ 𝐵
8 7 neli ⊢ ¬ ( 0g ‘ 𝑀 ) ∈ 𝐵
9 8 intnan ⊢ ¬ ( 𝐵 ⊆ ( Base ‘ 𝑀 ) ∧ ( 0g ‘ 𝑀 ) ∈ 𝐵 )
10 9 intnan ⊢ ¬ ( ( 𝑀 ∈ Mnd ∧ ( 𝑀 ↾s 𝐵 ) ∈ Mnd ) ∧ ( 𝐵 ⊆ ( Base ‘ 𝑀 ) ∧ ( 0g ‘ 𝑀 ) ∈ 𝐵 ) )
11 eqid ⊢ ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 )
12 eqid ⊢ ( 0g ‘ 𝑀 ) = ( 0g ‘ 𝑀 )
13 11 12 issubmndb ⊢ ( 𝐵 ∈ ( SubMnd ‘ 𝑀 ) ↔ ( ( 𝑀 ∈ Mnd ∧ ( 𝑀 ↾s 𝐵 ) ∈ Mnd ) ∧ ( 𝐵 ⊆ ( Base ‘ 𝑀 ) ∧ ( 0g ‘ 𝑀 ) ∈ 𝐵 ) ) )
14 10 13 mtbir ⊢ ¬ 𝐵 ∈ ( SubMnd ‘ 𝑀 )
15 14 nelir ⊢ 𝐵 ∉ ( SubMnd ‘ 𝑀 )