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 V Y 0 IterComp F Y = G IterComp F Y + 1 = G g V , j V F g F

Proof

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