Metamath Proof Explorer

Theorem itcoval0

Description: A function iterated zero times (defined as identity function). (Contributed by AV, 2-May-2024)

Ref Expression
Assertion itcoval0 
|- ( F e. V -> ( ( IterComp ` F ) ` 0 ) = ( _I |` dom F ) )

Proof

Step Hyp Ref Expression
1 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 ) ) ) )
2 1 fveq1d 
 |-  ( F e. V -> ( ( IterComp ` F ) ` 0 ) = ( seq 0 ( ( g e. _V , j e. _V |-> ( F o. g ) ) , ( i e. NN0 |-> if ( i = 0 , ( _I |` dom F ) , F ) ) ) ` 0 ) )
3 0z 
 |-  0 e. ZZ
4 eqidd 
 |-  ( F e. V -> ( i e. NN0 |-> if ( i = 0 , ( _I |` dom F ) , F ) ) = ( i e. NN0 |-> if ( i = 0 , ( _I |` dom F ) , F ) ) )
5 iftrue 
 |-  ( i = 0 -> if ( i = 0 , ( _I |` dom F ) , F ) = ( _I |` dom F ) )
6 5 adantl 
 |-  ( ( F e. V /\ i = 0 ) -> if ( i = 0 , ( _I |` dom F ) , F ) = ( _I |` dom F ) )
7 0nn0 
 |-  0 e. NN0
8 7 a1i 
 |-  ( F e. V -> 0 e. NN0 )
9 dmexg 
 |-  ( F e. V -> dom F e. _V )
10 9 resiexd 
 |-  ( F e. V -> ( _I |` dom F ) e. _V )
11 4 6 8 10 fvmptd 
 |-  ( F e. V -> ( ( i e. NN0 |-> if ( i = 0 , ( _I |` dom F ) , F ) ) ` 0 ) = ( _I |` dom F ) )
12 3 11 seq1i 
 |-  ( F e. V -> ( seq 0 ( ( g e. _V , j e. _V |-> ( F o. g ) ) , ( i e. NN0 |-> if ( i = 0 , ( _I |` dom F ) , F ) ) ) ` 0 ) = ( _I |` dom F ) )
13 2 12 eqtrd 
 |-  ( F e. V -> ( ( IterComp ` F ) ` 0 ) = ( _I |` dom F ) )