Metamath Proof Explorer


Theorem itcoval1

Description: A function iterated once. (Contributed by AV, 2-May-2024)

Ref Expression
Assertion itcoval1
|- ( ( Rel F /\ F e. V ) -> ( ( IterComp ` F ) ` 1 ) = 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 ) ` 1 ) = ( seq 0 ( ( g e. _V , j e. _V |-> ( F o. g ) ) , ( i e. NN0 |-> if ( i = 0 , ( _I |` dom F ) , F ) ) ) ` 1 ) )
3 2 adantl
 |-  ( ( Rel F /\ F e. V ) -> ( ( IterComp ` F ) ` 1 ) = ( seq 0 ( ( g e. _V , j e. _V |-> ( F o. g ) ) , ( i e. NN0 |-> if ( i = 0 , ( _I |` dom F ) , F ) ) ) ` 1 ) )
4 nn0uz
 |-  NN0 = ( ZZ>= ` 0 )
5 0nn0
 |-  0 e. NN0
6 5 a1i
 |-  ( ( Rel F /\ F e. V ) -> 0 e. NN0 )
7 1e0p1
 |-  1 = ( 0 + 1 )
8 1 eqcomd
 |-  ( F e. V -> seq 0 ( ( g e. _V , j e. _V |-> ( F o. g ) ) , ( i e. NN0 |-> if ( i = 0 , ( _I |` dom F ) , F ) ) ) = ( IterComp ` F ) )
9 8 fveq1d
 |-  ( 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 ) = ( ( IterComp ` F ) ` 0 ) )
10 itcoval0
 |-  ( F e. V -> ( ( IterComp ` F ) ` 0 ) = ( _I |` dom F ) )
11 9 10 eqtrd
 |-  ( 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 ) )
12 11 adantl
 |-  ( ( Rel F /\ 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 eqidd
 |-  ( ( Rel F /\ F e. V ) -> ( i e. NN0 |-> if ( i = 0 , ( _I |` dom F ) , F ) ) = ( i e. NN0 |-> if ( i = 0 , ( _I |` dom F ) , F ) ) )
14 ax-1ne0
 |-  1 =/= 0
15 14 neii
 |-  -. 1 = 0
16 eqeq1
 |-  ( i = 1 -> ( i = 0 <-> 1 = 0 ) )
17 15 16 mtbiri
 |-  ( i = 1 -> -. i = 0 )
18 17 iffalsed
 |-  ( i = 1 -> if ( i = 0 , ( _I |` dom F ) , F ) = F )
19 18 adantl
 |-  ( ( ( Rel F /\ F e. V ) /\ i = 1 ) -> if ( i = 0 , ( _I |` dom F ) , F ) = F )
20 1nn0
 |-  1 e. NN0
21 20 a1i
 |-  ( ( Rel F /\ F e. V ) -> 1 e. NN0 )
22 simpr
 |-  ( ( Rel F /\ F e. V ) -> F e. V )
23 13 19 21 22 fvmptd
 |-  ( ( Rel F /\ F e. V ) -> ( ( i e. NN0 |-> if ( i = 0 , ( _I |` dom F ) , F ) ) ` 1 ) = F )
24 4 6 7 12 23 seqp1d
 |-  ( ( Rel F /\ F e. V ) -> ( seq 0 ( ( g e. _V , j e. _V |-> ( F o. g ) ) , ( i e. NN0 |-> if ( i = 0 , ( _I |` dom F ) , F ) ) ) ` 1 ) = ( ( _I |` dom F ) ( g e. _V , j e. _V |-> ( F o. g ) ) F ) )
25 eqidd
 |-  ( F e. V -> ( g e. _V , j e. _V |-> ( F o. g ) ) = ( g e. _V , j e. _V |-> ( F o. g ) ) )
26 coeq2
 |-  ( g = ( _I |` dom F ) -> ( F o. g ) = ( F o. ( _I |` dom F ) ) )
27 26 ad2antrl
 |-  ( ( F e. V /\ ( g = ( _I |` dom F ) /\ j = F ) ) -> ( F o. g ) = ( F o. ( _I |` dom F ) ) )
28 dmexg
 |-  ( F e. V -> dom F e. _V )
29 28 resiexd
 |-  ( F e. V -> ( _I |` dom F ) e. _V )
30 elex
 |-  ( F e. V -> F e. _V )
31 coexg
 |-  ( ( F e. V /\ ( _I |` dom F ) e. _V ) -> ( F o. ( _I |` dom F ) ) e. _V )
32 29 31 mpdan
 |-  ( F e. V -> ( F o. ( _I |` dom F ) ) e. _V )
33 25 27 29 30 32 ovmpod
 |-  ( F e. V -> ( ( _I |` dom F ) ( g e. _V , j e. _V |-> ( F o. g ) ) F ) = ( F o. ( _I |` dom F ) ) )
34 33 adantl
 |-  ( ( Rel F /\ F e. V ) -> ( ( _I |` dom F ) ( g e. _V , j e. _V |-> ( F o. g ) ) F ) = ( F o. ( _I |` dom F ) ) )
35 coires1
 |-  ( F o. ( _I |` dom F ) ) = ( F |` dom F )
36 resdm
 |-  ( Rel F -> ( F |` dom F ) = F )
37 36 adantr
 |-  ( ( Rel F /\ F e. V ) -> ( F |` dom F ) = F )
38 35 37 syl5eq
 |-  ( ( Rel F /\ F e. V ) -> ( F o. ( _I |` dom F ) ) = F )
39 34 38 eqtrd
 |-  ( ( Rel F /\ F e. V ) -> ( ( _I |` dom F ) ( g e. _V , j e. _V |-> ( F o. g ) ) F ) = F )
40 24 39 eqtrd
 |-  ( ( Rel F /\ F e. V ) -> ( seq 0 ( ( g e. _V , j e. _V |-> ( F o. g ) ) , ( i e. NN0 |-> if ( i = 0 , ( _I |` dom F ) , F ) ) ) ` 1 ) = F )
41 3 40 eqtrd
 |-  ( ( Rel F /\ F e. V ) -> ( ( IterComp ` F ) ` 1 ) = F )