Metamath Proof Explorer

Theorem itcovalpc

Description: The value of the function that returns the n-th iterate of the "plus a constant" function with regard to composition. (Contributed by AV, 4-May-2024)

Ref Expression
Hypothesis itcovalpc.f 
|- F = ( n e. NN0 |-> ( n + C ) )
Assertion itcovalpc 
|- ( ( I e. NN0 /\ C e. NN0 ) -> ( ( IterComp ` F ) ` I ) = ( n e. NN0 |-> ( n + ( C x. I ) ) ) )

Proof

Step Hyp Ref Expression
1 itcovalpc.f 
 |-  F = ( n e. NN0 |-> ( n + C ) )
2 fveq2 
 |-  ( x = 0 -> ( ( IterComp ` F ) ` x ) = ( ( IterComp ` F ) ` 0 ) )
3 oveq2 
 |-  ( x = 0 -> ( C x. x ) = ( C x. 0 ) )
4 3 oveq2d 
 |-  ( x = 0 -> ( n + ( C x. x ) ) = ( n + ( C x. 0 ) ) )
5 4 mpteq2dv 
 |-  ( x = 0 -> ( n e. NN0 |-> ( n + ( C x. x ) ) ) = ( n e. NN0 |-> ( n + ( C x. 0 ) ) ) )
6 2 5 eqeq12d 
 |-  ( x = 0 -> ( ( ( IterComp ` F ) ` x ) = ( n e. NN0 |-> ( n + ( C x. x ) ) ) <-> ( ( IterComp ` F ) ` 0 ) = ( n e. NN0 |-> ( n + ( C x. 0 ) ) ) ) )
7 fveq2 
 |-  ( x = y -> ( ( IterComp ` F ) ` x ) = ( ( IterComp ` F ) ` y ) )
8 oveq2 
 |-  ( x = y -> ( C x. x ) = ( C x. y ) )
9 8 oveq2d 
 |-  ( x = y -> ( n + ( C x. x ) ) = ( n + ( C x. y ) ) )
10 9 mpteq2dv 
 |-  ( x = y -> ( n e. NN0 |-> ( n + ( C x. x ) ) ) = ( n e. NN0 |-> ( n + ( C x. y ) ) ) )
11 7 10 eqeq12d 
 |-  ( x = y -> ( ( ( IterComp ` F ) ` x ) = ( n e. NN0 |-> ( n + ( C x. x ) ) ) <-> ( ( IterComp ` F ) ` y ) = ( n e. NN0 |-> ( n + ( C x. y ) ) ) ) )
12 fveq2 
 |-  ( x = ( y + 1 ) -> ( ( IterComp ` F ) ` x ) = ( ( IterComp ` F ) ` ( y + 1 ) ) )
13 oveq2 
 |-  ( x = ( y + 1 ) -> ( C x. x ) = ( C x. ( y + 1 ) ) )
14 13 oveq2d 
 |-  ( x = ( y + 1 ) -> ( n + ( C x. x ) ) = ( n + ( C x. ( y + 1 ) ) ) )
15 14 mpteq2dv 
 |-  ( x = ( y + 1 ) -> ( n e. NN0 |-> ( n + ( C x. x ) ) ) = ( n e. NN0 |-> ( n + ( C x. ( y + 1 ) ) ) ) )
16 12 15 eqeq12d 
 |-  ( x = ( y + 1 ) -> ( ( ( IterComp ` F ) ` x ) = ( n e. NN0 |-> ( n + ( C x. x ) ) ) <-> ( ( IterComp ` F ) ` ( y + 1 ) ) = ( n e. NN0 |-> ( n + ( C x. ( y + 1 ) ) ) ) ) )
17 fveq2 
 |-  ( x = I -> ( ( IterComp ` F ) ` x ) = ( ( IterComp ` F ) ` I ) )
18 oveq2 
 |-  ( x = I -> ( C x. x ) = ( C x. I ) )
19 18 oveq2d 
 |-  ( x = I -> ( n + ( C x. x ) ) = ( n + ( C x. I ) ) )
20 19 mpteq2dv 
 |-  ( x = I -> ( n e. NN0 |-> ( n + ( C x. x ) ) ) = ( n e. NN0 |-> ( n + ( C x. I ) ) ) )
21 17 20 eqeq12d 
 |-  ( x = I -> ( ( ( IterComp ` F ) ` x ) = ( n e. NN0 |-> ( n + ( C x. x ) ) ) <-> ( ( IterComp ` F ) ` I ) = ( n e. NN0 |-> ( n + ( C x. I ) ) ) ) )
22 1 itcovalpclem1 
 |-  ( C e. NN0 -> ( ( IterComp ` F ) ` 0 ) = ( n e. NN0 |-> ( n + ( C x. 0 ) ) ) )
23 1 itcovalpclem2 
 |-  ( ( y e. NN0 /\ C e. NN0 ) -> ( ( ( IterComp ` F ) ` y ) = ( n e. NN0 |-> ( n + ( C x. y ) ) ) -> ( ( IterComp ` F ) ` ( y + 1 ) ) = ( n e. NN0 |-> ( n + ( C x. ( y + 1 ) ) ) ) ) )
24 23 ancoms 
 |-  ( ( C e. NN0 /\ y e. NN0 ) -> ( ( ( IterComp ` F ) ` y ) = ( n e. NN0 |-> ( n + ( C x. y ) ) ) -> ( ( IterComp ` F ) ` ( y + 1 ) ) = ( n e. NN0 |-> ( n + ( C x. ( y + 1 ) ) ) ) ) )
25 24 imp 
 |-  ( ( ( C e. NN0 /\ y e. NN0 ) /\ ( ( IterComp ` F ) ` y ) = ( n e. NN0 |-> ( n + ( C x. y ) ) ) ) -> ( ( IterComp ` F ) ` ( y + 1 ) ) = ( n e. NN0 |-> ( n + ( C x. ( y + 1 ) ) ) ) )
26 6 11 16 21 22 25 nn0indd 
 |-  ( ( C e. NN0 /\ I e. NN0 ) -> ( ( IterComp ` F ) ` I ) = ( n e. NN0 |-> ( n + ( C x. I ) ) ) )
27 26 ancoms 
 |-  ( ( I e. NN0 /\ C e. NN0 ) -> ( ( IterComp ` F ) ` I ) = ( n e. NN0 |-> ( n + ( C x. I ) ) ) )