Metamath Proof Explorer


Theorem smndex1gid

Description: The composition of a constant function ( GK ) with another endofunction on NN0 results in ( GK ) itself. (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
Assertion smndex1gid F Base M K 0 ..^ N G K F = G K

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 4 a1i K 0 ..^ N G = n 0 ..^ N x 0 n
6 id n = K n = K
7 6 mpteq2dv n = K x 0 n = x 0 K
8 7 adantl K 0 ..^ N n = K x 0 n = x 0 K
9 id K 0 ..^ N K 0 ..^ N
10 nn0ex 0 V
11 10 mptex x 0 K V
12 11 a1i K 0 ..^ N x 0 K V
13 5 8 9 12 fvmptd K 0 ..^ N G K = x 0 K
14 13 adantl F Base M K 0 ..^ N G K = x 0 K
15 14 adantr F Base M K 0 ..^ N y 0 G K = x 0 K
16 eqidd F Base M K 0 ..^ N y 0 x = F y K = K
17 eqid Base M = Base M
18 1 17 efmndbasf F Base M F : 0 0
19 ffvelrn F : 0 0 y 0 F y 0
20 19 ex F : 0 0 y 0 F y 0
21 18 20 syl F Base M y 0 F y 0
22 21 adantr F Base M K 0 ..^ N y 0 F y 0
23 22 imp F Base M K 0 ..^ N y 0 F y 0
24 simplr F Base M K 0 ..^ N y 0 K 0 ..^ N
25 15 16 23 24 fvmptd F Base M K 0 ..^ N y 0 G K F y = K
26 25 mpteq2dva F Base M K 0 ..^ N y 0 G K F y = y 0 K
27 1 2 3 4 smndex1gbas K 0 ..^ N G K Base M
28 1 17 efmndbasf G K Base M G K : 0 0
29 27 28 syl K 0 ..^ N G K : 0 0
30 fcompt G K : 0 0 F : 0 0 G K F = y 0 G K F y
31 29 18 30 syl2anr F Base M K 0 ..^ N G K F = y 0 G K F y
32 eqidd x = y K = K
33 32 cbvmptv x 0 K = y 0 K
34 7 33 eqtrdi n = K x 0 n = y 0 K
35 34 adantl K 0 ..^ N n = K x 0 n = y 0 K
36 10 mptex y 0 K V
37 36 a1i K 0 ..^ N y 0 K V
38 5 35 9 37 fvmptd K 0 ..^ N G K = y 0 K
39 38 adantl F Base M K 0 ..^ N G K = y 0 K
40 26 31 39 3eqtr4d F Base M K 0 ..^ N G K F = G K