Metamath Proof Explorer


Theorem itcoval3

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

Ref Expression
Assertion itcoval3 Rel F F V IterComp F 3 = F F 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 3 = seq 0 g V , j V F g i 0 if i = 0 I dom F F 3
3 2 adantl Rel F F V IterComp F 3 = seq 0 g V , j V F g i 0 if i = 0 I dom F F 3
4 nn0uz 0 = 0
5 2nn0 2 0
6 5 a1i Rel F F V 2 0
7 df-3 3 = 2 + 1
8 1 eqcomd F V seq 0 g V , j V F g i 0 if i = 0 I dom F F = IterComp F
9 8 fveq1d F V seq 0 g V , j V F g i 0 if i = 0 I dom F F 2 = IterComp F 2
10 9 adantl Rel F F V seq 0 g V , j V F g i 0 if i = 0 I dom F F 2 = IterComp F 2
11 itcoval2 Rel F F V IterComp F 2 = F F
12 10 11 eqtrd Rel F F V seq 0 g V , j V F g i 0 if i = 0 I dom F F 2 = F F
13 eqidd Rel F F V i 0 if i = 0 I dom F F = i 0 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 V i = 3 if i = 0 I dom F F = F
20 3nn0 3 0
21 20 a1i Rel F F V 3 0
22 simpr Rel F F V F V
23 13 19 21 22 fvmptd Rel F F V i 0 if i = 0 I dom F F 3 = F
24 4 6 7 12 23 seqp1d Rel F F V seq 0 g V , j V F g i 0 if i = 0 I dom F F 3 = F F g V , j V F g F
25 eqidd F V g V , j V F g = g V , j V F g
26 coeq2 g = F F F g = F F F
27 26 ad2antrl F V g = F F j = F F g = F F F
28 coexg F V F V F F V
29 28 anidms F V F F V
30 elex F V F V
31 coexg F V F F V F F F V
32 28 31 syldan F V F V F F F V
33 32 anidms F V F F F V
34 25 27 29 30 33 ovmpod F V F F g V , j V F g F = F F F
35 34 adantl Rel F F V F F g V , j V F g F = F F F
36 3 24 35 3eqtrd Rel F F V IterComp F 3 = F F F