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 No typesetting found for |- M = ( EndoFMnd ` NN0 ) with typecode |-
smndex1ibas.n N
smndex1ibas.i I = x 0 x mod N
smndex1ibas.g G = n 0 ..^ N x 0 n
smndex1mgm.b B = I n 0 ..^ N G n
smndex1mgm.s S = M 𝑠 B
Assertion smndex1mgm S Mgm

Proof

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