Metamath Proof Explorer


Theorem itcoval2

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

Ref Expression
Assertion itcoval2 Rel F F V IterComp F 2 = 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 2 = seq 0 g V , j V F g i 0 if i = 0 I dom F F 2
3 2 adantl Rel F F V IterComp F 2 = seq 0 g V , j V F g i 0 if i = 0 I dom F F 2
4 nn0uz 0 = 0
5 1nn0 1 0
6 5 a1i Rel F F V 1 0
7 df-2 2 = 1 + 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 1 = IterComp F 1
10 9 adantl Rel F F V seq 0 g V , j V F g i 0 if i = 0 I dom F F 1 = IterComp F 1
11 itcoval1 Rel F F V IterComp F 1 = 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 1 = 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 2ne0 2 0
15 neeq1 i = 2 i 0 2 0
16 14 15 mpbiri i = 2 i 0
17 16 neneqd i = 2 ¬ i = 0
18 17 iffalsed i = 2 if i = 0 I dom F F = F
19 18 adantl Rel F F V i = 2 if i = 0 I dom F F = F
20 2nn0 2 0
21 20 a1i Rel F F V 2 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 2 = 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 2 = 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 g = F F
27 26 ad2antrl F V g = F j = F F g = F F
28 elex F V F V
29 coexg F V F V F F V
30 29 anidms F V F F V
31 25 27 28 28 30 ovmpod F V F g V , j V F g F = F F
32 31 adantl Rel F F V F g V , j V F g F = F F
33 3 24 32 3eqtrd Rel F F V IterComp F 2 = F F