Metamath Proof Explorer


Theorem smndex1gbas

Description: The constant functions ( GK ) are endofunctions on NN0 . (Contributed by AV, 12-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
Assertion smndex1gbas K 0 ..^ N G K Base M

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 elfzonn0 K 0 ..^ N K 0
6 5 adantr K 0 ..^ N x 0 K 0
7 6 ralrimiva K 0 ..^ N x 0 K 0
8 eqid x 0 K = x 0 K
9 8 fmpt x 0 K 0 x 0 K : 0 0
10 7 9 sylib K 0 ..^ N x 0 K : 0 0
11 nn0ex 0 V
12 11 11 elmap x 0 K 0 0 x 0 K : 0 0
13 10 12 sylibr K 0 ..^ N x 0 K 0 0
14 4 a1i K 0 ..^ N G = n 0 ..^ N x 0 n
15 id n = K n = K
16 15 mpteq2dv n = K x 0 n = x 0 K
17 16 adantl K 0 ..^ N n = K x 0 n = x 0 K
18 id K 0 ..^ N K 0 ..^ N
19 11 mptex x 0 K V
20 19 a1i K 0 ..^ N x 0 K V
21 14 17 18 20 fvmptd K 0 ..^ N G K = x 0 K
22 eqid Base M = Base M
23 1 22 efmndbas Base M = 0 0
24 23 a1i K 0 ..^ N Base M = 0 0
25 13 21 24 3eltr4d K 0 ..^ N G K Base M