Metamath Proof Explorer


Theorem smndex1n0mnd

Description: The identity of the monoid M of endofunctions on set NN0 is not contained in the base set of the constructed monoid S . (Contributed by AV, 17-Feb-2024)

Ref Expression
Hypotheses smndex1ibas.m
|- M = ( EndoFMnd ` NN0 )
smndex1ibas.n
|- N e. NN
smndex1ibas.i
|- I = ( x e. NN0 |-> ( x mod N ) )
smndex1ibas.g
|- G = ( n e. ( 0 ..^ N ) |-> ( x e. NN0 |-> n ) )
smndex1mgm.b
|- B = ( { I } u. U_ n e. ( 0 ..^ N ) { ( G ` n ) } )
smndex1mgm.s
|- S = ( M |`s B )
Assertion smndex1n0mnd
|- ( 0g ` M ) e/ B

Proof

Step Hyp Ref Expression
1 smndex1ibas.m
 |-  M = ( EndoFMnd ` NN0 )
2 smndex1ibas.n
 |-  N e. NN
3 smndex1ibas.i
 |-  I = ( x e. NN0 |-> ( x mod N ) )
4 smndex1ibas.g
 |-  G = ( n e. ( 0 ..^ N ) |-> ( x e. NN0 |-> n ) )
5 smndex1mgm.b
 |-  B = ( { I } u. U_ n e. ( 0 ..^ N ) { ( G ` n ) } )
6 smndex1mgm.s
 |-  S = ( M |`s B )
7 nnnn0
 |-  ( N e. NN -> N e. NN0 )
8 fveq2
 |-  ( x = N -> ( ( _I |` NN0 ) ` x ) = ( ( _I |` NN0 ) ` N ) )
9 2 7 ax-mp
 |-  N e. NN0
10 fvresi
 |-  ( N e. NN0 -> ( ( _I |` NN0 ) ` N ) = N )
11 9 10 ax-mp
 |-  ( ( _I |` NN0 ) ` N ) = N
12 8 11 eqtrdi
 |-  ( x = N -> ( ( _I |` NN0 ) ` x ) = N )
13 fveq2
 |-  ( x = N -> ( I ` x ) = ( I ` N ) )
14 12 13 eqeq12d
 |-  ( x = N -> ( ( ( _I |` NN0 ) ` x ) = ( I ` x ) <-> N = ( I ` N ) ) )
15 14 notbid
 |-  ( x = N -> ( -. ( ( _I |` NN0 ) ` x ) = ( I ` x ) <-> -. N = ( I ` N ) ) )
16 15 adantl
 |-  ( ( N e. NN /\ x = N ) -> ( -. ( ( _I |` NN0 ) ` x ) = ( I ` x ) <-> -. N = ( I ` N ) ) )
17 nnne0
 |-  ( N e. NN -> N =/= 0 )
18 17 neneqd
 |-  ( N e. NN -> -. N = 0 )
19 oveq1
 |-  ( x = N -> ( x mod N ) = ( N mod N ) )
20 nnrp
 |-  ( N e. NN -> N e. RR+ )
21 modid0
 |-  ( N e. RR+ -> ( N mod N ) = 0 )
22 20 21 syl
 |-  ( N e. NN -> ( N mod N ) = 0 )
23 19 22 sylan9eqr
 |-  ( ( N e. NN /\ x = N ) -> ( x mod N ) = 0 )
24 c0ex
 |-  0 e. _V
25 24 a1i
 |-  ( N e. NN -> 0 e. _V )
26 3 23 7 25 fvmptd2
 |-  ( N e. NN -> ( I ` N ) = 0 )
27 26 eqeq2d
 |-  ( N e. NN -> ( N = ( I ` N ) <-> N = 0 ) )
28 18 27 mtbird
 |-  ( N e. NN -> -. N = ( I ` N ) )
29 7 16 28 rspcedvd
 |-  ( N e. NN -> E. x e. NN0 -. ( ( _I |` NN0 ) ` x ) = ( I ` x ) )
30 2 29 ax-mp
 |-  E. x e. NN0 -. ( ( _I |` NN0 ) ` x ) = ( I ` x )
31 rexnal
 |-  ( E. x e. NN0 -. ( ( _I |` NN0 ) ` x ) = ( I ` x ) <-> -. A. x e. NN0 ( ( _I |` NN0 ) ` x ) = ( I ` x ) )
32 30 31 mpbi
 |-  -. A. x e. NN0 ( ( _I |` NN0 ) ` x ) = ( I ` x )
33 fnresi
 |-  ( _I |` NN0 ) Fn NN0
34 ovex
 |-  ( x mod N ) e. _V
35 34 3 fnmpti
 |-  I Fn NN0
36 eqfnfv
 |-  ( ( ( _I |` NN0 ) Fn NN0 /\ I Fn NN0 ) -> ( ( _I |` NN0 ) = I <-> A. x e. NN0 ( ( _I |` NN0 ) ` x ) = ( I ` x ) ) )
37 33 35 36 mp2an
 |-  ( ( _I |` NN0 ) = I <-> A. x e. NN0 ( ( _I |` NN0 ) ` x ) = ( I ` x ) )
38 32 37 mtbir
 |-  -. ( _I |` NN0 ) = I
39 9 a1i
 |-  ( n e. ( 0 ..^ N ) -> N e. NN0 )
40 fveq2
 |-  ( x = N -> ( ( G ` n ) ` x ) = ( ( G ` n ) ` N ) )
41 12 40 eqeq12d
 |-  ( x = N -> ( ( ( _I |` NN0 ) ` x ) = ( ( G ` n ) ` x ) <-> N = ( ( G ` n ) ` N ) ) )
42 41 notbid
 |-  ( x = N -> ( -. ( ( _I |` NN0 ) ` x ) = ( ( G ` n ) ` x ) <-> -. N = ( ( G ` n ) ` N ) ) )
43 42 adantl
 |-  ( ( n e. ( 0 ..^ N ) /\ x = N ) -> ( -. ( ( _I |` NN0 ) ` x ) = ( ( G ` n ) ` x ) <-> -. N = ( ( G ` n ) ` N ) ) )
44 fzonel
 |-  -. N e. ( 0 ..^ N )
45 eleq1
 |-  ( n = N -> ( n e. ( 0 ..^ N ) <-> N e. ( 0 ..^ N ) ) )
46 45 eqcoms
 |-  ( N = n -> ( n e. ( 0 ..^ N ) <-> N e. ( 0 ..^ N ) ) )
47 44 46 mtbiri
 |-  ( N = n -> -. n e. ( 0 ..^ N ) )
48 47 con2i
 |-  ( n e. ( 0 ..^ N ) -> -. N = n )
49 nn0ex
 |-  NN0 e. _V
50 49 mptex
 |-  ( x e. NN0 |-> n ) e. _V
51 4 fvmpt2
 |-  ( ( n e. ( 0 ..^ N ) /\ ( x e. NN0 |-> n ) e. _V ) -> ( G ` n ) = ( x e. NN0 |-> n ) )
52 50 51 mpan2
 |-  ( n e. ( 0 ..^ N ) -> ( G ` n ) = ( x e. NN0 |-> n ) )
53 eqidd
 |-  ( ( n e. ( 0 ..^ N ) /\ x = N ) -> n = n )
54 id
 |-  ( n e. ( 0 ..^ N ) -> n e. ( 0 ..^ N ) )
55 52 53 39 54 fvmptd
 |-  ( n e. ( 0 ..^ N ) -> ( ( G ` n ) ` N ) = n )
56 55 eqeq2d
 |-  ( n e. ( 0 ..^ N ) -> ( N = ( ( G ` n ) ` N ) <-> N = n ) )
57 48 56 mtbird
 |-  ( n e. ( 0 ..^ N ) -> -. N = ( ( G ` n ) ` N ) )
58 39 43 57 rspcedvd
 |-  ( n e. ( 0 ..^ N ) -> E. x e. NN0 -. ( ( _I |` NN0 ) ` x ) = ( ( G ` n ) ` x ) )
59 rexnal
 |-  ( E. x e. NN0 -. ( ( _I |` NN0 ) ` x ) = ( ( G ` n ) ` x ) <-> -. A. x e. NN0 ( ( _I |` NN0 ) ` x ) = ( ( G ` n ) ` x ) )
60 58 59 sylib
 |-  ( n e. ( 0 ..^ N ) -> -. A. x e. NN0 ( ( _I |` NN0 ) ` x ) = ( ( G ` n ) ` x ) )
61 vex
 |-  n e. _V
62 eqid
 |-  ( x e. NN0 |-> n ) = ( x e. NN0 |-> n )
63 61 62 fnmpti
 |-  ( x e. NN0 |-> n ) Fn NN0
64 52 fneq1d
 |-  ( n e. ( 0 ..^ N ) -> ( ( G ` n ) Fn NN0 <-> ( x e. NN0 |-> n ) Fn NN0 ) )
65 63 64 mpbiri
 |-  ( n e. ( 0 ..^ N ) -> ( G ` n ) Fn NN0 )
66 eqfnfv
 |-  ( ( ( _I |` NN0 ) Fn NN0 /\ ( G ` n ) Fn NN0 ) -> ( ( _I |` NN0 ) = ( G ` n ) <-> A. x e. NN0 ( ( _I |` NN0 ) ` x ) = ( ( G ` n ) ` x ) ) )
67 33 65 66 sylancr
 |-  ( n e. ( 0 ..^ N ) -> ( ( _I |` NN0 ) = ( G ` n ) <-> A. x e. NN0 ( ( _I |` NN0 ) ` x ) = ( ( G ` n ) ` x ) ) )
68 60 67 mtbird
 |-  ( n e. ( 0 ..^ N ) -> -. ( _I |` NN0 ) = ( G ` n ) )
69 68 nrex
 |-  -. E. n e. ( 0 ..^ N ) ( _I |` NN0 ) = ( G ` n )
70 38 69 pm3.2ni
 |-  -. ( ( _I |` NN0 ) = I \/ E. n e. ( 0 ..^ N ) ( _I |` NN0 ) = ( G ` n ) )
71 1 efmndid
 |-  ( NN0 e. _V -> ( _I |` NN0 ) = ( 0g ` M ) )
72 49 71 ax-mp
 |-  ( _I |` NN0 ) = ( 0g ` M )
73 72 eqcomi
 |-  ( 0g ` M ) = ( _I |` NN0 )
74 73 5 eleq12i
 |-  ( ( 0g ` M ) e. B <-> ( _I |` NN0 ) e. ( { I } u. U_ n e. ( 0 ..^ N ) { ( G ` n ) } ) )
75 elun
 |-  ( ( _I |` NN0 ) e. ( { I } u. U_ n e. ( 0 ..^ N ) { ( G ` n ) } ) <-> ( ( _I |` NN0 ) e. { I } \/ ( _I |` NN0 ) e. U_ n e. ( 0 ..^ N ) { ( G ` n ) } ) )
76 resiexg
 |-  ( NN0 e. _V -> ( _I |` NN0 ) e. _V )
77 49 76 ax-mp
 |-  ( _I |` NN0 ) e. _V
78 77 elsn
 |-  ( ( _I |` NN0 ) e. { I } <-> ( _I |` NN0 ) = I )
79 eliun
 |-  ( ( _I |` NN0 ) e. U_ n e. ( 0 ..^ N ) { ( G ` n ) } <-> E. n e. ( 0 ..^ N ) ( _I |` NN0 ) e. { ( G ` n ) } )
80 77 elsn
 |-  ( ( _I |` NN0 ) e. { ( G ` n ) } <-> ( _I |` NN0 ) = ( G ` n ) )
81 80 rexbii
 |-  ( E. n e. ( 0 ..^ N ) ( _I |` NN0 ) e. { ( G ` n ) } <-> E. n e. ( 0 ..^ N ) ( _I |` NN0 ) = ( G ` n ) )
82 79 81 bitri
 |-  ( ( _I |` NN0 ) e. U_ n e. ( 0 ..^ N ) { ( G ` n ) } <-> E. n e. ( 0 ..^ N ) ( _I |` NN0 ) = ( G ` n ) )
83 78 82 orbi12i
 |-  ( ( ( _I |` NN0 ) e. { I } \/ ( _I |` NN0 ) e. U_ n e. ( 0 ..^ N ) { ( G ` n ) } ) <-> ( ( _I |` NN0 ) = I \/ E. n e. ( 0 ..^ N ) ( _I |` NN0 ) = ( G ` n ) ) )
84 75 83 bitri
 |-  ( ( _I |` NN0 ) e. ( { I } u. U_ n e. ( 0 ..^ N ) { ( G ` n ) } ) <-> ( ( _I |` NN0 ) = I \/ E. n e. ( 0 ..^ N ) ( _I |` NN0 ) = ( G ` n ) ) )
85 74 84 bitri
 |-  ( ( 0g ` M ) e. B <-> ( ( _I |` NN0 ) = I \/ E. n e. ( 0 ..^ N ) ( _I |` NN0 ) = ( G ` n ) ) )
86 70 85 mtbir
 |-  -. ( 0g ` M ) e. B
87 86 nelir
 |-  ( 0g ` M ) e/ B