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