Metamath Proof Explorer

Theorem smndex1mgm

Description: The monoid of endofunctions on NN0 restricted to the modulo function I and the constant functions ( GK ) is a magma. (Contributed by AV, 14-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 smndex1mgm 
|- S e. Mgm

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 1 2 3 4 5 smndex1basss 
 |-  B C_ ( Base ` M )
8 ssel 
 |-  ( B C_ ( Base ` M ) -> ( a e. B -> a e. ( Base ` M ) ) )
9 ssel 
 |-  ( B C_ ( Base ` M ) -> ( b e. B -> b e. ( Base ` M ) ) )
10 8 9 anim12d 
 |-  ( B C_ ( Base ` M ) -> ( ( a e. B /\ b e. B ) -> ( a e. ( Base ` M ) /\ b e. ( Base ` M ) ) ) )
11 7 10 ax-mp 
 |-  ( ( a e. B /\ b e. B ) -> ( a e. ( Base ` M ) /\ b e. ( Base ` M ) ) )
12 eqid 
 |-  ( Base ` M ) = ( Base ` M )
13 eqid 
 |-  ( +g ` M ) = ( +g ` M )
14 1 12 13 efmndov 
 |-  ( ( a e. ( Base ` M ) /\ b e. ( Base ` M ) ) -> ( a ( +g ` M ) b ) = ( a o. b ) )
15 11 14 syl 
 |-  ( ( a e. B /\ b e. B ) -> ( a ( +g ` M ) b ) = ( a o. b ) )
16 simpl 
 |-  ( ( a = I /\ b = I ) -> a = I )
17 simpr 
 |-  ( ( a = I /\ b = I ) -> b = I )
18 16 17 coeq12d 
 |-  ( ( a = I /\ b = I ) -> ( a o. b ) = ( I o. I ) )
19 1 2 3 smndex1iidm 
 |-  ( I o. I ) = I
20 18 19 eqtrdi 
 |-  ( ( a = I /\ b = I ) -> ( a o. b ) = I )
21 20 orcd 
 |-  ( ( a = I /\ b = I ) -> ( ( a o. b ) = I \/ E. k e. ( 0 ..^ N ) ( a o. b ) = ( G ` k ) ) )
22 21 ex 
 |-  ( a = I -> ( b = I -> ( ( a o. b ) = I \/ E. k e. ( 0 ..^ N ) ( a o. b ) = ( G ` k ) ) ) )
23 simpll 
 |-  ( ( ( a = I /\ k e. ( 0 ..^ N ) ) /\ b = ( G ` k ) ) -> a = I )
24 simpr 
 |-  ( ( ( a = I /\ k e. ( 0 ..^ N ) ) /\ b = ( G ` k ) ) -> b = ( G ` k ) )
25 23 24 coeq12d 
 |-  ( ( ( a = I /\ k e. ( 0 ..^ N ) ) /\ b = ( G ` k ) ) -> ( a o. b ) = ( I o. ( G ` k ) ) )
26 1 2 3 4 smndex1igid 
 |-  ( k e. ( 0 ..^ N ) -> ( I o. ( G ` k ) ) = ( G ` k ) )
27 26 ad2antlr 
 |-  ( ( ( a = I /\ k e. ( 0 ..^ N ) ) /\ b = ( G ` k ) ) -> ( I o. ( G ` k ) ) = ( G ` k ) )
28 25 27 eqtrd 
 |-  ( ( ( a = I /\ k e. ( 0 ..^ N ) ) /\ b = ( G ` k ) ) -> ( a o. b ) = ( G ` k ) )
29 28 ex 
 |-  ( ( a = I /\ k e. ( 0 ..^ N ) ) -> ( b = ( G ` k ) -> ( a o. b ) = ( G ` k ) ) )
30 29 reximdva 
 |-  ( a = I -> ( E. k e. ( 0 ..^ N ) b = ( G ` k ) -> E. k e. ( 0 ..^ N ) ( a o. b ) = ( G ` k ) ) )
31 30 imp 
 |-  ( ( a = I /\ E. k e. ( 0 ..^ N ) b = ( G ` k ) ) -> E. k e. ( 0 ..^ N ) ( a o. b ) = ( G ` k ) )
32 31 olcd 
 |-  ( ( a = I /\ E. k e. ( 0 ..^ N ) b = ( G ` k ) ) -> ( ( a o. b ) = I \/ E. k e. ( 0 ..^ N ) ( a o. b ) = ( G ` k ) ) )
33 32 ex 
 |-  ( a = I -> ( E. k e. ( 0 ..^ N ) b = ( G ` k ) -> ( ( a o. b ) = I \/ E. k e. ( 0 ..^ N ) ( a o. b ) = ( G ` k ) ) ) )
34 22 33 jaod 
 |-  ( a = I -> ( ( b = I \/ E. k e. ( 0 ..^ N ) b = ( G ` k ) ) -> ( ( a o. b ) = I \/ E. k e. ( 0 ..^ N ) ( a o. b ) = ( G ` k ) ) ) )
35 simpr 
 |-  ( ( ( b = I /\ k e. ( 0 ..^ N ) ) /\ a = ( G ` k ) ) -> a = ( G ` k ) )
36 simpll 
 |-  ( ( ( b = I /\ k e. ( 0 ..^ N ) ) /\ a = ( G ` k ) ) -> b = I )
37 35 36 coeq12d 
 |-  ( ( ( b = I /\ k e. ( 0 ..^ N ) ) /\ a = ( G ` k ) ) -> ( a o. b ) = ( ( G ` k ) o. I ) )
38 1 2 3 smndex1ibas 
 |-  I e. ( Base ` M )
39 1 2 3 4 smndex1gid 
 |-  ( ( I e. ( Base ` M ) /\ k e. ( 0 ..^ N ) ) -> ( ( G ` k ) o. I ) = ( G ` k ) )
40 38 39 mpan 
 |-  ( k e. ( 0 ..^ N ) -> ( ( G ` k ) o. I ) = ( G ` k ) )
41 40 ad2antlr 
 |-  ( ( ( b = I /\ k e. ( 0 ..^ N ) ) /\ a = ( G ` k ) ) -> ( ( G ` k ) o. I ) = ( G ` k ) )
42 37 41 eqtrd 
 |-  ( ( ( b = I /\ k e. ( 0 ..^ N ) ) /\ a = ( G ` k ) ) -> ( a o. b ) = ( G ` k ) )
43 42 ex 
 |-  ( ( b = I /\ k e. ( 0 ..^ N ) ) -> ( a = ( G ` k ) -> ( a o. b ) = ( G ` k ) ) )
44 43 reximdva 
 |-  ( b = I -> ( E. k e. ( 0 ..^ N ) a = ( G ` k ) -> E. k e. ( 0 ..^ N ) ( a o. b ) = ( G ` k ) ) )
45 44 imp 
 |-  ( ( b = I /\ E. k e. ( 0 ..^ N ) a = ( G ` k ) ) -> E. k e. ( 0 ..^ N ) ( a o. b ) = ( G ` k ) )
46 45 olcd 
 |-  ( ( b = I /\ E. k e. ( 0 ..^ N ) a = ( G ` k ) ) -> ( ( a o. b ) = I \/ E. k e. ( 0 ..^ N ) ( a o. b ) = ( G ` k ) ) )
47 46 expcom 
 |-  ( E. k e. ( 0 ..^ N ) a = ( G ` k ) -> ( b = I -> ( ( a o. b ) = I \/ E. k e. ( 0 ..^ N ) ( a o. b ) = ( G ` k ) ) ) )
48 fveq2 
 |-  ( k = m -> ( G ` k ) = ( G ` m ) )
49 48 eqeq2d 
 |-  ( k = m -> ( b = ( G ` k ) <-> b = ( G ` m ) ) )
50 49 cbvrexvw 
 |-  ( E. k e. ( 0 ..^ N ) b = ( G ` k ) <-> E. m e. ( 0 ..^ N ) b = ( G ` m ) )
51 simpr 
 |-  ( ( ( ( m e. ( 0 ..^ N ) /\ b = ( G ` m ) ) /\ k e. ( 0 ..^ N ) ) /\ a = ( G ` k ) ) -> a = ( G ` k ) )
52 simpllr 
 |-  ( ( ( ( m e. ( 0 ..^ N ) /\ b = ( G ` m ) ) /\ k e. ( 0 ..^ N ) ) /\ a = ( G ` k ) ) -> b = ( G ` m ) )
53 51 52 coeq12d 
 |-  ( ( ( ( m e. ( 0 ..^ N ) /\ b = ( G ` m ) ) /\ k e. ( 0 ..^ N ) ) /\ a = ( G ` k ) ) -> ( a o. b ) = ( ( G ` k ) o. ( G ` m ) ) )
54 1 2 3 4 smndex1gbas 
 |-  ( m e. ( 0 ..^ N ) -> ( G ` m ) e. ( Base ` M ) )
55 1 2 3 4 smndex1gid 
 |-  ( ( ( G ` m ) e. ( Base ` M ) /\ k e. ( 0 ..^ N ) ) -> ( ( G ` k ) o. ( G ` m ) ) = ( G ` k ) )
56 54 55 sylan 
 |-  ( ( m e. ( 0 ..^ N ) /\ k e. ( 0 ..^ N ) ) -> ( ( G ` k ) o. ( G ` m ) ) = ( G ` k ) )
57 56 ad4ant13 
 |-  ( ( ( ( m e. ( 0 ..^ N ) /\ b = ( G ` m ) ) /\ k e. ( 0 ..^ N ) ) /\ a = ( G ` k ) ) -> ( ( G ` k ) o. ( G ` m ) ) = ( G ` k ) )
58 53 57 eqtrd 
 |-  ( ( ( ( m e. ( 0 ..^ N ) /\ b = ( G ` m ) ) /\ k e. ( 0 ..^ N ) ) /\ a = ( G ` k ) ) -> ( a o. b ) = ( G ` k ) )
59 58 ex 
 |-  ( ( ( m e. ( 0 ..^ N ) /\ b = ( G ` m ) ) /\ k e. ( 0 ..^ N ) ) -> ( a = ( G ` k ) -> ( a o. b ) = ( G ` k ) ) )
60 59 reximdva 
 |-  ( ( m e. ( 0 ..^ N ) /\ b = ( G ` m ) ) -> ( E. k e. ( 0 ..^ N ) a = ( G ` k ) -> E. k e. ( 0 ..^ N ) ( a o. b ) = ( G ` k ) ) )
61 60 rexlimiva 
 |-  ( E. m e. ( 0 ..^ N ) b = ( G ` m ) -> ( E. k e. ( 0 ..^ N ) a = ( G ` k ) -> E. k e. ( 0 ..^ N ) ( a o. b ) = ( G ` k ) ) )
62 61 imp 
 |-  ( ( E. m e. ( 0 ..^ N ) b = ( G ` m ) /\ E. k e. ( 0 ..^ N ) a = ( G ` k ) ) -> E. k e. ( 0 ..^ N ) ( a o. b ) = ( G ` k ) )
63 62 olcd 
 |-  ( ( E. m e. ( 0 ..^ N ) b = ( G ` m ) /\ E. k e. ( 0 ..^ N ) a = ( G ` k ) ) -> ( ( a o. b ) = I \/ E. k e. ( 0 ..^ N ) ( a o. b ) = ( G ` k ) ) )
64 63 expcom 
 |-  ( E. k e. ( 0 ..^ N ) a = ( G ` k ) -> ( E. m e. ( 0 ..^ N ) b = ( G ` m ) -> ( ( a o. b ) = I \/ E. k e. ( 0 ..^ N ) ( a o. b ) = ( G ` k ) ) ) )
65 50 64 syl5bi 
 |-  ( E. k e. ( 0 ..^ N ) a = ( G ` k ) -> ( E. k e. ( 0 ..^ N ) b = ( G ` k ) -> ( ( a o. b ) = I \/ E. k e. ( 0 ..^ N ) ( a o. b ) = ( G ` k ) ) ) )
66 47 65 jaod 
 |-  ( E. k e. ( 0 ..^ N ) a = ( G ` k ) -> ( ( b = I \/ E. k e. ( 0 ..^ N ) b = ( G ` k ) ) -> ( ( a o. b ) = I \/ E. k e. ( 0 ..^ N ) ( a o. b ) = ( G ` k ) ) ) )
67 34 66 jaoi 
 |-  ( ( a = I \/ E. k e. ( 0 ..^ N ) a = ( G ` k ) ) -> ( ( b = I \/ E. k e. ( 0 ..^ N ) b = ( G ` k ) ) -> ( ( a o. b ) = I \/ E. k e. ( 0 ..^ N ) ( a o. b ) = ( G ` k ) ) ) )
68 67 imp 
 |-  ( ( ( a = I \/ E. k e. ( 0 ..^ N ) a = ( G ` k ) ) /\ ( b = I \/ E. k e. ( 0 ..^ N ) b = ( G ` k ) ) ) -> ( ( a o. b ) = I \/ E. k e. ( 0 ..^ N ) ( a o. b ) = ( G ` k ) ) )
69 5 eleq2i 
 |-  ( a e. B <-> a e. ( { I } u. U_ n e. ( 0 ..^ N ) { ( G ` n ) } ) )
70 fveq2 
 |-  ( n = k -> ( G ` n ) = ( G ` k ) )
71 70 sneqd 
 |-  ( n = k -> { ( G ` n ) } = { ( G ` k ) } )
72 71 cbviunv 
 |-  U_ n e. ( 0 ..^ N ) { ( G ` n ) } = U_ k e. ( 0 ..^ N ) { ( G ` k ) }
73 72 uneq2i 
 |-  ( { I } u. U_ n e. ( 0 ..^ N ) { ( G ` n ) } ) = ( { I } u. U_ k e. ( 0 ..^ N ) { ( G ` k ) } )
74 73 eleq2i 
 |-  ( a e. ( { I } u. U_ n e. ( 0 ..^ N ) { ( G ` n ) } ) <-> a e. ( { I } u. U_ k e. ( 0 ..^ N ) { ( G ` k ) } ) )
75 69 74 bitri 
 |-  ( a e. B <-> a e. ( { I } u. U_ k e. ( 0 ..^ N ) { ( G ` k ) } ) )
76 elun 
 |-  ( a e. ( { I } u. U_ k e. ( 0 ..^ N ) { ( G ` k ) } ) <-> ( a e. { I } \/ a e. U_ k e. ( 0 ..^ N ) { ( G ` k ) } ) )
77 velsn 
 |-  ( a e. { I } <-> a = I )
78 eliun 
 |-  ( a e. U_ k e. ( 0 ..^ N ) { ( G ` k ) } <-> E. k e. ( 0 ..^ N ) a e. { ( G ` k ) } )
79 velsn 
 |-  ( a e. { ( G ` k ) } <-> a = ( G ` k ) )
80 79 rexbii 
 |-  ( E. k e. ( 0 ..^ N ) a e. { ( G ` k ) } <-> E. k e. ( 0 ..^ N ) a = ( G ` k ) )
81 78 80 bitri 
 |-  ( a e. U_ k e. ( 0 ..^ N ) { ( G ` k ) } <-> E. k e. ( 0 ..^ N ) a = ( G ` k ) )
82 77 81 orbi12i 
 |-  ( ( a e. { I } \/ a e. U_ k e. ( 0 ..^ N ) { ( G ` k ) } ) <-> ( a = I \/ E. k e. ( 0 ..^ N ) a = ( G ` k ) ) )
83 75 76 82 3bitri 
 |-  ( a e. B <-> ( a = I \/ E. k e. ( 0 ..^ N ) a = ( G ` k ) ) )
84 5 eleq2i 
 |-  ( b e. B <-> b e. ( { I } u. U_ n e. ( 0 ..^ N ) { ( G ` n ) } ) )
85 73 eleq2i 
 |-  ( b e. ( { I } u. U_ n e. ( 0 ..^ N ) { ( G ` n ) } ) <-> b e. ( { I } u. U_ k e. ( 0 ..^ N ) { ( G ` k ) } ) )
86 84 85 bitri 
 |-  ( b e. B <-> b e. ( { I } u. U_ k e. ( 0 ..^ N ) { ( G ` k ) } ) )
87 elun 
 |-  ( b e. ( { I } u. U_ k e. ( 0 ..^ N ) { ( G ` k ) } ) <-> ( b e. { I } \/ b e. U_ k e. ( 0 ..^ N ) { ( G ` k ) } ) )
88 velsn 
 |-  ( b e. { I } <-> b = I )
89 eliun 
 |-  ( b e. U_ k e. ( 0 ..^ N ) { ( G ` k ) } <-> E. k e. ( 0 ..^ N ) b e. { ( G ` k ) } )
90 velsn 
 |-  ( b e. { ( G ` k ) } <-> b = ( G ` k ) )
91 90 rexbii 
 |-  ( E. k e. ( 0 ..^ N ) b e. { ( G ` k ) } <-> E. k e. ( 0 ..^ N ) b = ( G ` k ) )
92 89 91 bitri 
 |-  ( b e. U_ k e. ( 0 ..^ N ) { ( G ` k ) } <-> E. k e. ( 0 ..^ N ) b = ( G ` k ) )
93 88 92 orbi12i 
 |-  ( ( b e. { I } \/ b e. U_ k e. ( 0 ..^ N ) { ( G ` k ) } ) <-> ( b = I \/ E. k e. ( 0 ..^ N ) b = ( G ` k ) ) )
94 86 87 93 3bitri 
 |-  ( b e. B <-> ( b = I \/ E. k e. ( 0 ..^ N ) b = ( G ` k ) ) )
95 83 94 anbi12i 
 |-  ( ( a e. B /\ b e. B ) <-> ( ( a = I \/ E. k e. ( 0 ..^ N ) a = ( G ` k ) ) /\ ( b = I \/ E. k e. ( 0 ..^ N ) b = ( G ` k ) ) ) )
96 5 eleq2i 
 |-  ( ( a o. b ) e. B <-> ( a o. b ) e. ( { I } u. U_ n e. ( 0 ..^ N ) { ( G ` n ) } ) )
97 73 eleq2i 
 |-  ( ( a o. b ) e. ( { I } u. U_ n e. ( 0 ..^ N ) { ( G ` n ) } ) <-> ( a o. b ) e. ( { I } u. U_ k e. ( 0 ..^ N ) { ( G ` k ) } ) )
98 96 97 bitri 
 |-  ( ( a o. b ) e. B <-> ( a o. b ) e. ( { I } u. U_ k e. ( 0 ..^ N ) { ( G ` k ) } ) )
99 elun 
 |-  ( ( a o. b ) e. ( { I } u. U_ k e. ( 0 ..^ N ) { ( G ` k ) } ) <-> ( ( a o. b ) e. { I } \/ ( a o. b ) e. U_ k e. ( 0 ..^ N ) { ( G ` k ) } ) )
100 vex 
 |-  a e. _V
101 vex 
 |-  b e. _V
102 100 101 coex 
 |-  ( a o. b ) e. _V
103 102 elsn 
 |-  ( ( a o. b ) e. { I } <-> ( a o. b ) = I )
104 eliun 
 |-  ( ( a o. b ) e. U_ k e. ( 0 ..^ N ) { ( G ` k ) } <-> E. k e. ( 0 ..^ N ) ( a o. b ) e. { ( G ` k ) } )
105 102 elsn 
 |-  ( ( a o. b ) e. { ( G ` k ) } <-> ( a o. b ) = ( G ` k ) )
106 105 rexbii 
 |-  ( E. k e. ( 0 ..^ N ) ( a o. b ) e. { ( G ` k ) } <-> E. k e. ( 0 ..^ N ) ( a o. b ) = ( G ` k ) )
107 104 106 bitri 
 |-  ( ( a o. b ) e. U_ k e. ( 0 ..^ N ) { ( G ` k ) } <-> E. k e. ( 0 ..^ N ) ( a o. b ) = ( G ` k ) )
108 103 107 orbi12i 
 |-  ( ( ( a o. b ) e. { I } \/ ( a o. b ) e. U_ k e. ( 0 ..^ N ) { ( G ` k ) } ) <-> ( ( a o. b ) = I \/ E. k e. ( 0 ..^ N ) ( a o. b ) = ( G ` k ) ) )
109 98 99 108 3bitri 
 |-  ( ( a o. b ) e. B <-> ( ( a o. b ) = I \/ E. k e. ( 0 ..^ N ) ( a o. b ) = ( G ` k ) ) )
110 68 95 109 3imtr4i 
 |-  ( ( a e. B /\ b e. B ) -> ( a o. b ) e. B )
111 15 110 eqeltrd 
 |-  ( ( a e. B /\ b e. B ) -> ( a ( +g ` M ) b ) e. B )
112 111 rgen2 
 |-  A. a e. B A. b e. B ( a ( +g ` M ) b ) e. B
113 6 ovexi 
 |-  S e. _V
114 1 2 3 4 5 6 smndex1bas 
 |-  ( Base ` S ) = B
115 114 eqcomi 
 |-  B = ( Base ` S )
116 115 fvexi 
 |-  B e. _V
117 6 13 ressplusg 
 |-  ( B e. _V -> ( +g ` M ) = ( +g ` S ) )
118 116 117 ax-mp 
 |-  ( +g ` M ) = ( +g ` S )
119 115 118 ismgm 
 |-  ( S e. _V -> ( S e. Mgm <-> A. a e. B A. b e. B ( a ( +g ` M ) b ) e. B ) )
120 113 119 ax-mp 
 |-  ( S e. Mgm <-> A. a e. B A. b e. B ( a ( +g ` M ) b ) e. B )
121 112 120 mpbir 
 |-  S e. Mgm