Metamath Proof Explorer

Theorem itcovalsuc

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

Ref Expression
Assertion itcovalsuc 
|- ( ( F e. V /\ Y e. NN0 /\ ( ( IterComp ` F ) ` Y ) = G ) -> ( ( IterComp ` F ) ` ( Y + 1 ) ) = ( G ( g e. _V , j e. _V |-> ( F o. g ) ) F ) )

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( F e. V /\ Y e. NN0 /\ ( ( IterComp ` F ) ` Y ) = G ) -> F e. V )
2 itcoval 
 |-  ( F e. V -> ( IterComp ` F ) = seq 0 ( ( g e. _V , j e. _V |-> ( F o. g ) ) , ( i e. NN0 |-> if ( i = 0 , ( _I |` dom F ) , F ) ) ) )
3 2 fveq1d 
 |-  ( F e. V -> ( ( IterComp ` F ) ` ( Y + 1 ) ) = ( seq 0 ( ( g e. _V , j e. _V |-> ( F o. g ) ) , ( i e. NN0 |-> if ( i = 0 , ( _I |` dom F ) , F ) ) ) ` ( Y + 1 ) ) )
4 1 3 syl 
 |-  ( ( F e. V /\ Y e. NN0 /\ ( ( IterComp ` F ) ` Y ) = G ) -> ( ( IterComp ` F ) ` ( Y + 1 ) ) = ( seq 0 ( ( g e. _V , j e. _V |-> ( F o. g ) ) , ( i e. NN0 |-> if ( i = 0 , ( _I |` dom F ) , F ) ) ) ` ( Y + 1 ) ) )
5 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
6 simp2 
 |-  ( ( F e. V /\ Y e. NN0 /\ ( ( IterComp ` F ) ` Y ) = G ) -> Y e. NN0 )
7 eqid 
 |-  ( Y + 1 ) = ( Y + 1 )
8 2 adantr 
 |-  ( ( F e. V /\ Y e. NN0 ) -> ( IterComp ` F ) = seq 0 ( ( g e. _V , j e. _V |-> ( F o. g ) ) , ( i e. NN0 |-> if ( i = 0 , ( _I |` dom F ) , F ) ) ) )
9 8 fveq1d 
 |-  ( ( F e. V /\ Y e. NN0 ) -> ( ( IterComp ` F ) ` Y ) = ( seq 0 ( ( g e. _V , j e. _V |-> ( F o. g ) ) , ( i e. NN0 |-> if ( i = 0 , ( _I |` dom F ) , F ) ) ) ` Y ) )
10 9 eqeq1d 
 |-  ( ( F e. V /\ Y e. NN0 ) -> ( ( ( IterComp ` F ) ` Y ) = G <-> ( seq 0 ( ( g e. _V , j e. _V |-> ( F o. g ) ) , ( i e. NN0 |-> if ( i = 0 , ( _I |` dom F ) , F ) ) ) ` Y ) = G ) )
11 10 biimp3a 
 |-  ( ( F e. V /\ Y e. NN0 /\ ( ( IterComp ` F ) ` Y ) = G ) -> ( seq 0 ( ( g e. _V , j e. _V |-> ( F o. g ) ) , ( i e. NN0 |-> if ( i = 0 , ( _I |` dom F ) , F ) ) ) ` Y ) = G )
12 eqidd 
 |-  ( ( F e. V /\ Y e. NN0 /\ ( ( IterComp ` F ) ` Y ) = G ) -> ( i e. NN0 |-> if ( i = 0 , ( _I |` dom F ) , F ) ) = ( i e. NN0 |-> if ( i = 0 , ( _I |` dom F ) , F ) ) )
13 nn0p1gt0 
 |-  ( Y e. NN0 -> 0 < ( Y + 1 ) )
14 13 3ad2ant2 
 |-  ( ( F e. V /\ Y e. NN0 /\ ( ( IterComp ` F ) ` Y ) = G ) -> 0 < ( Y + 1 ) )
15 14 gt0ne0d 
 |-  ( ( F e. V /\ Y e. NN0 /\ ( ( IterComp ` F ) ` Y ) = G ) -> ( Y + 1 ) =/= 0 )
16 15 adantr 
 |-  ( ( ( F e. V /\ Y e. NN0 /\ ( ( IterComp ` F ) ` Y ) = G ) /\ i = ( Y + 1 ) ) -> ( Y + 1 ) =/= 0 )
17 neeq1 
 |-  ( i = ( Y + 1 ) -> ( i =/= 0 <-> ( Y + 1 ) =/= 0 ) )
18 17 adantl 
 |-  ( ( ( F e. V /\ Y e. NN0 /\ ( ( IterComp ` F ) ` Y ) = G ) /\ i = ( Y + 1 ) ) -> ( i =/= 0 <-> ( Y + 1 ) =/= 0 ) )
19 16 18 mpbird 
 |-  ( ( ( F e. V /\ Y e. NN0 /\ ( ( IterComp ` F ) ` Y ) = G ) /\ i = ( Y + 1 ) ) -> i =/= 0 )
20 19 neneqd 
 |-  ( ( ( F e. V /\ Y e. NN0 /\ ( ( IterComp ` F ) ` Y ) = G ) /\ i = ( Y + 1 ) ) -> -. i = 0 )
21 20 iffalsed 
 |-  ( ( ( F e. V /\ Y e. NN0 /\ ( ( IterComp ` F ) ` Y ) = G ) /\ i = ( Y + 1 ) ) -> if ( i = 0 , ( _I |` dom F ) , F ) = F )
22 peano2nn0 
 |-  ( Y e. NN0 -> ( Y + 1 ) e. NN0 )
23 22 3ad2ant2 
 |-  ( ( F e. V /\ Y e. NN0 /\ ( ( IterComp ` F ) ` Y ) = G ) -> ( Y + 1 ) e. NN0 )
24 12 21 23 1 fvmptd 
 |-  ( ( F e. V /\ Y e. NN0 /\ ( ( IterComp ` F ) ` Y ) = G ) -> ( ( i e. NN0 |-> if ( i = 0 , ( _I |` dom F ) , F ) ) ` ( Y + 1 ) ) = F )
25 5 6 7 11 24 seqp1d 
 |-  ( ( F e. V /\ Y e. NN0 /\ ( ( IterComp ` F ) ` Y ) = G ) -> ( seq 0 ( ( g e. _V , j e. _V |-> ( F o. g ) ) , ( i e. NN0 |-> if ( i = 0 , ( _I |` dom F ) , F ) ) ) ` ( Y + 1 ) ) = ( G ( g e. _V , j e. _V |-> ( F o. g ) ) F ) )
26 4 25 eqtrd 
 |-  ( ( F e. V /\ Y e. NN0 /\ ( ( IterComp ` F ) ` Y ) = G ) -> ( ( IterComp ` F ) ` ( Y + 1 ) ) = ( G ( g e. _V , j e. _V |-> ( F o. g ) ) F ) )