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 V IterComp F 0 = I dom F

Proof

Step Hyp Ref Expression
1 itcoval F V IterComp F = seq 0 g V , j V F g i 0 if i = 0 I dom F F
2 1 fveq1d F V IterComp F 0 = seq 0 g V , j V F g i 0 if i = 0 I dom F F 0
3 0z 0
4 eqidd F V i 0 if i = 0 I dom F F = i 0 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 V i = 0 if i = 0 I dom F F = I dom F
7 0nn0 0 0
8 7 a1i F V 0 0
9 dmexg F V dom F V
10 9 resiexd F V I dom F V
11 4 6 8 10 fvmptd F V i 0 if i = 0 I dom F F 0 = I dom F
12 3 11 seq1i F V seq 0 g V , j V F g i 0 if i = 0 I dom F F 0 = I dom F
13 2 12 eqtrd F V IterComp F 0 = I dom F