Metamath Proof Explorer

Theorem itcoval3

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

Ref Expression
Assertion itcoval3 
|- ( ( Rel F /\ F e. V ) -> ( ( IterComp ` F ) ` 3 ) = ( F o. ( F o. 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 ) ` 3 ) = ( seq 0 ( ( g e. _V , j e. _V |-> ( F o. g ) ) , ( i e. NN0 |-> if ( i = 0 , ( _I |` dom F ) , F ) ) ) ` 3 ) )
3 2 adantl 
 |-  ( ( Rel F /\ F e. V ) -> ( ( IterComp ` F ) ` 3 ) = ( seq 0 ( ( g e. _V , j e. _V |-> ( F o. g ) ) , ( i e. NN0 |-> if ( i = 0 , ( _I |` dom F ) , F ) ) ) ` 3 ) )
4 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
5 2nn0 
 |-  2 e. NN0
6 5 a1i 
 |-  ( ( Rel F /\ F e. V ) -> 2 e. NN0 )
7 df-3 
 |-  3 = ( 2 + 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 ) ) ) ` 2 ) = ( ( IterComp ` F ) ` 2 ) )
10 9 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 ) ) ) ` 2 ) = ( ( IterComp ` F ) ` 2 ) )
11 itcoval2 
 |-  ( ( Rel F /\ F e. V ) -> ( ( IterComp ` F ) ` 2 ) = ( F o. F ) )
12 10 11 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 ) ) ) ` 2 ) = ( F o. 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 3ne0 
 |-  3 =/= 0
15 neeq1 
 |-  ( i = 3 -> ( i =/= 0 <-> 3 =/= 0 ) )
16 14 15 mpbiri 
 |-  ( i = 3 -> i =/= 0 )
17 16 neneqd 
 |-  ( i = 3 -> -. i = 0 )
18 17 iffalsed 
 |-  ( i = 3 -> if ( i = 0 , ( _I |` dom F ) , F ) = F )
19 18 adantl 
 |-  ( ( ( Rel F /\ F e. V ) /\ i = 3 ) -> if ( i = 0 , ( _I |` dom F ) , F ) = F )
20 3nn0 
 |-  3 e. NN0
21 20 a1i 
 |-  ( ( Rel F /\ F e. V ) -> 3 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 ) ) ` 3 ) = 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 ) ) ) ` 3 ) = ( ( F o. 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 = ( F o. F ) -> ( F o. g ) = ( F o. ( F o. F ) ) )
27 26 ad2antrl 
 |-  ( ( F e. V /\ ( g = ( F o. F ) /\ j = F ) ) -> ( F o. g ) = ( F o. ( F o. F ) ) )
28 coexg 
 |-  ( ( F e. V /\ F e. V ) -> ( F o. F ) e. _V )
29 28 anidms 
 |-  ( F e. V -> ( F o. F ) e. _V )
30 elex 
 |-  ( F e. V -> F e. _V )
31 coexg 
 |-  ( ( F e. V /\ ( F o. F ) e. _V ) -> ( F o. ( F o. F ) ) e. _V )
32 28 31 syldan 
 |-  ( ( F e. V /\ F e. V ) -> ( F o. ( F o. F ) ) e. _V )
33 32 anidms 
 |-  ( F e. V -> ( F o. ( F o. F ) ) e. _V )
34 25 27 29 30 33 ovmpod 
 |-  ( F e. V -> ( ( F o. F ) ( g e. _V , j e. _V |-> ( F o. g ) ) F ) = ( F o. ( F o. F ) ) )
35 34 adantl 
 |-  ( ( Rel F /\ F e. V ) -> ( ( F o. F ) ( g e. _V , j e. _V |-> ( F o. g ) ) F ) = ( F o. ( F o. F ) ) )
36 3 24 35 3eqtrd 
 |-  ( ( Rel F /\ F e. V ) -> ( ( IterComp ` F ) ` 3 ) = ( F o. ( F o. F ) ) )