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) Avoid ax-rep . (Revised by GG, 2-Apr-2026)

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 ) )
Assertion smndex1gid 
|- ( ( F e. ( Base ` M ) /\ K e. ( 0 ..^ N ) ) -> ( ( G ` K ) o. F ) = ( G ` K ) )

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 id 
 |-  ( n = K -> n = K )
6 5 mpteq2dv 
 |-  ( n = K -> ( x e. NN0 |-> n ) = ( x e. NN0 |-> K ) )
7 fconstmpt 
 |-  ( NN0 X. { K } ) = ( x e. NN0 |-> K )
8 nn0ex 
 |-  NN0 e. _V
9 snex 
 |-  { K } e. _V
10 8 9 xpex 
 |-  ( NN0 X. { K } ) e. _V
11 7 10 eqeltrri 
 |-  ( x e. NN0 |-> K ) e. _V
12 6 4 11 fvmpt 
 |-  ( K e. ( 0 ..^ N ) -> ( G ` K ) = ( x e. NN0 |-> K ) )
13 12 adantl 
 |-  ( ( F e. ( Base ` M ) /\ K e. ( 0 ..^ N ) ) -> ( G ` K ) = ( x e. NN0 |-> K ) )
14 13 adantr 
 |-  ( ( ( F e. ( Base ` M ) /\ K e. ( 0 ..^ N ) ) /\ y e. NN0 ) -> ( G ` K ) = ( x e. NN0 |-> K ) )
15 eqidd 
 |-  ( ( ( ( F e. ( Base ` M ) /\ K e. ( 0 ..^ N ) ) /\ y e. NN0 ) /\ x = ( F ` y ) ) -> K = K )
16 eqid 
 |-  ( Base ` M ) = ( Base ` M )
17 1 16 efmndbasf 
 |-  ( F e. ( Base ` M ) -> F : NN0 --> NN0 )
18 ffvelcdm 
 |-  ( ( F : NN0 --> NN0 /\ y e. NN0 ) -> ( F ` y ) e. NN0 )
19 18 ex 
 |-  ( F : NN0 --> NN0 -> ( y e. NN0 -> ( F ` y ) e. NN0 ) )
20 17 19 syl 
 |-  ( F e. ( Base ` M ) -> ( y e. NN0 -> ( F ` y ) e. NN0 ) )
21 20 adantr 
 |-  ( ( F e. ( Base ` M ) /\ K e. ( 0 ..^ N ) ) -> ( y e. NN0 -> ( F ` y ) e. NN0 ) )
22 21 imp 
 |-  ( ( ( F e. ( Base ` M ) /\ K e. ( 0 ..^ N ) ) /\ y e. NN0 ) -> ( F ` y ) e. NN0 )
23 simplr 
 |-  ( ( ( F e. ( Base ` M ) /\ K e. ( 0 ..^ N ) ) /\ y e. NN0 ) -> K e. ( 0 ..^ N ) )
24 14 15 22 23 fvmptd 
 |-  ( ( ( F e. ( Base ` M ) /\ K e. ( 0 ..^ N ) ) /\ y e. NN0 ) -> ( ( G ` K ) ` ( F ` y ) ) = K )
25 24 mpteq2dva 
 |-  ( ( F e. ( Base ` M ) /\ K e. ( 0 ..^ N ) ) -> ( y e. NN0 |-> ( ( G ` K ) ` ( F ` y ) ) ) = ( y e. NN0 |-> K ) )
26 1 2 3 4 smndex1gbas 
 |-  ( K e. ( 0 ..^ N ) -> ( G ` K ) e. ( Base ` M ) )
27 1 16 efmndbasf 
 |-  ( ( G ` K ) e. ( Base ` M ) -> ( G ` K ) : NN0 --> NN0 )
28 26 27 syl 
 |-  ( K e. ( 0 ..^ N ) -> ( G ` K ) : NN0 --> NN0 )
29 fcompt 
 |-  ( ( ( G ` K ) : NN0 --> NN0 /\ F : NN0 --> NN0 ) -> ( ( G ` K ) o. F ) = ( y e. NN0 |-> ( ( G ` K ) ` ( F ` y ) ) ) )
30 28 17 29 syl2anr 
 |-  ( ( F e. ( Base ` M ) /\ K e. ( 0 ..^ N ) ) -> ( ( G ` K ) o. F ) = ( y e. NN0 |-> ( ( G ` K ) ` ( F ` y ) ) ) )
31 eqidd 
 |-  ( x = y -> K = K )
32 31 cbvmptv 
 |-  ( x e. NN0 |-> K ) = ( y e. NN0 |-> K )
33 6 32 eqtrdi 
 |-  ( n = K -> ( x e. NN0 |-> n ) = ( y e. NN0 |-> K ) )
34 fconstmpt 
 |-  ( NN0 X. { K } ) = ( y e. NN0 |-> K )
35 34 10 eqeltrri 
 |-  ( y e. NN0 |-> K ) e. _V
36 33 4 35 fvmpt 
 |-  ( K e. ( 0 ..^ N ) -> ( G ` K ) = ( y e. NN0 |-> K ) )
37 36 adantl 
 |-  ( ( F e. ( Base ` M ) /\ K e. ( 0 ..^ N ) ) -> ( G ` K ) = ( y e. NN0 |-> K ) )
38 25 30 37 3eqtr4d 
 |-  ( ( F e. ( Base ` M ) /\ K e. ( 0 ..^ N ) ) -> ( ( G ` K ) o. F ) = ( G ` K ) )