Metamath Proof Explorer

Theorem itcoval3

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

Ref Expression
Assertion itcoval3 ( ( Rel 𝐹 ∧ 𝐹 ∈ 𝑉 ) → ( ( IterComp ‘ 𝐹 ) ‘ 3 ) = ( 𝐹 ∘ ( 𝐹 ∘ 𝐹 ) ) )

Proof

Step Hyp Ref Expression
1 itcoval ⊢ ( 𝐹 ∈ 𝑉 → ( IterComp ‘ 𝐹 ) = seq 0 ( ( 𝑔 ∈ V , 𝑗 ∈ V ↦ ( 𝐹 ∘ 𝑔 ) ) , ( 𝑖 ∈ ℕ0 ↦ if ( 𝑖 = 0 , ( I ↾ dom 𝐹 ) , 𝐹 ) ) ) )
2 1 fveq1d ⊢ ( 𝐹 ∈ 𝑉 → ( ( IterComp ‘ 𝐹 ) ‘ 3 ) = ( seq 0 ( ( 𝑔 ∈ V , 𝑗 ∈ V ↦ ( 𝐹 ∘ 𝑔 ) ) , ( 𝑖 ∈ ℕ0 ↦ if ( 𝑖 = 0 , ( I ↾ dom 𝐹 ) , 𝐹 ) ) ) ‘ 3 ) )
3 2 adantl ⊢ ( ( Rel 𝐹 ∧ 𝐹 ∈ 𝑉 ) → ( ( IterComp ‘ 𝐹 ) ‘ 3 ) = ( seq 0 ( ( 𝑔 ∈ V , 𝑗 ∈ V ↦ ( 𝐹 ∘ 𝑔 ) ) , ( 𝑖 ∈ ℕ0 ↦ if ( 𝑖 = 0 , ( I ↾ dom 𝐹 ) , 𝐹 ) ) ) ‘ 3 ) )
4 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
5 2nn0 ⊢ 2 ∈ ℕ0
6 5 a1i ⊢ ( ( Rel 𝐹 ∧ 𝐹 ∈ 𝑉 ) → 2 ∈ ℕ0 )
7 df-3 ⊢ 3 = ( 2 + 1 )
8 1 eqcomd ⊢ ( 𝐹 ∈ 𝑉 → seq 0 ( ( 𝑔 ∈ V , 𝑗 ∈ V ↦ ( 𝐹 ∘ 𝑔 ) ) , ( 𝑖 ∈ ℕ0 ↦ if ( 𝑖 = 0 , ( I ↾ dom 𝐹 ) , 𝐹 ) ) ) = ( IterComp ‘ 𝐹 ) )
9 8 fveq1d ⊢ ( 𝐹 ∈ 𝑉 → ( seq 0 ( ( 𝑔 ∈ V , 𝑗 ∈ V ↦ ( 𝐹 ∘ 𝑔 ) ) , ( 𝑖 ∈ ℕ0 ↦ if ( 𝑖 = 0 , ( I ↾ dom 𝐹 ) , 𝐹 ) ) ) ‘ 2 ) = ( ( IterComp ‘ 𝐹 ) ‘ 2 ) )
10 9 adantl ⊢ ( ( Rel 𝐹 ∧ 𝐹 ∈ 𝑉 ) → ( seq 0 ( ( 𝑔 ∈ V , 𝑗 ∈ V ↦ ( 𝐹 ∘ 𝑔 ) ) , ( 𝑖 ∈ ℕ0 ↦ if ( 𝑖 = 0 , ( I ↾ dom 𝐹 ) , 𝐹 ) ) ) ‘ 2 ) = ( ( IterComp ‘ 𝐹 ) ‘ 2 ) )
11 itcoval2 ⊢ ( ( Rel 𝐹 ∧ 𝐹 ∈ 𝑉 ) → ( ( IterComp ‘ 𝐹 ) ‘ 2 ) = ( 𝐹 ∘ 𝐹 ) )
12 10 11 eqtrd ⊢ ( ( Rel 𝐹 ∧ 𝐹 ∈ 𝑉 ) → ( seq 0 ( ( 𝑔 ∈ V , 𝑗 ∈ V ↦ ( 𝐹 ∘ 𝑔 ) ) , ( 𝑖 ∈ ℕ0 ↦ if ( 𝑖 = 0 , ( I ↾ dom 𝐹 ) , 𝐹 ) ) ) ‘ 2 ) = ( 𝐹 ∘ 𝐹 ) )
13 eqidd ⊢ ( ( Rel 𝐹 ∧ 𝐹 ∈ 𝑉 ) → ( 𝑖 ∈ ℕ0 ↦ if ( 𝑖 = 0 , ( I ↾ dom 𝐹 ) , 𝐹 ) ) = ( 𝑖 ∈ ℕ0 ↦ if ( 𝑖 = 0 , ( I ↾ dom 𝐹 ) , 𝐹 ) ) )
14 3ne0 ⊢ 3 ≠ 0
15 neeq1 ⊢ ( 𝑖 = 3 → ( 𝑖 ≠ 0 ↔ 3 ≠ 0 ) )
16 14 15 mpbiri ⊢ ( 𝑖 = 3 → 𝑖 ≠ 0 )
17 16 neneqd ⊢ ( 𝑖 = 3 → ¬ 𝑖 = 0 )
18 17 iffalsed ⊢ ( 𝑖 = 3 → if ( 𝑖 = 0 , ( I ↾ dom 𝐹 ) , 𝐹 ) = 𝐹 )
19 18 adantl ⊢ ( ( ( Rel 𝐹 ∧ 𝐹 ∈ 𝑉 ) ∧ 𝑖 = 3 ) → if ( 𝑖 = 0 , ( I ↾ dom 𝐹 ) , 𝐹 ) = 𝐹 )
20 3nn0 ⊢ 3 ∈ ℕ0
21 20 a1i ⊢ ( ( Rel 𝐹 ∧ 𝐹 ∈ 𝑉 ) → 3 ∈ ℕ0 )
22 simpr ⊢ ( ( Rel 𝐹 ∧ 𝐹 ∈ 𝑉 ) → 𝐹 ∈ 𝑉 )
23 13 19 21 22 fvmptd ⊢ ( ( Rel 𝐹 ∧ 𝐹 ∈ 𝑉 ) → ( ( 𝑖 ∈ ℕ0 ↦ if ( 𝑖 = 0 , ( I ↾ dom 𝐹 ) , 𝐹 ) ) ‘ 3 ) = 𝐹 )
24 4 6 7 12 23 seqp1d ⊢ ( ( Rel 𝐹 ∧ 𝐹 ∈ 𝑉 ) → ( seq 0 ( ( 𝑔 ∈ V , 𝑗 ∈ V ↦ ( 𝐹 ∘ 𝑔 ) ) , ( 𝑖 ∈ ℕ0 ↦ if ( 𝑖 = 0 , ( I ↾ dom 𝐹 ) , 𝐹 ) ) ) ‘ 3 ) = ( ( 𝐹 ∘ 𝐹 ) ( 𝑔 ∈ V , 𝑗 ∈ V ↦ ( 𝐹 ∘ 𝑔 ) ) 𝐹 ) )
25 eqidd ⊢ ( 𝐹 ∈ 𝑉 → ( 𝑔 ∈ V , 𝑗 ∈ V ↦ ( 𝐹 ∘ 𝑔 ) ) = ( 𝑔 ∈ V , 𝑗 ∈ V ↦ ( 𝐹 ∘ 𝑔 ) ) )
26 coeq2 ⊢ ( 𝑔 = ( 𝐹 ∘ 𝐹 ) → ( 𝐹 ∘ 𝑔 ) = ( 𝐹 ∘ ( 𝐹 ∘ 𝐹 ) ) )
27 26 ad2antrl ⊢ ( ( 𝐹 ∈ 𝑉 ∧ ( 𝑔 = ( 𝐹 ∘ 𝐹 ) ∧ 𝑗 = 𝐹 ) ) → ( 𝐹 ∘ 𝑔 ) = ( 𝐹 ∘ ( 𝐹 ∘ 𝐹 ) ) )
28 coexg ⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝐹 ∈ 𝑉 ) → ( 𝐹 ∘ 𝐹 ) ∈ V )
29 28 anidms ⊢ ( 𝐹 ∈ 𝑉 → ( 𝐹 ∘ 𝐹 ) ∈ V )
30 elex ⊢ ( 𝐹 ∈ 𝑉 → 𝐹 ∈ V )
31 coexg ⊢ ( ( 𝐹 ∈ 𝑉 ∧ ( 𝐹 ∘ 𝐹 ) ∈ V ) → ( 𝐹 ∘ ( 𝐹 ∘ 𝐹 ) ) ∈ V )
32 28 31 syldan ⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝐹 ∈ 𝑉 ) → ( 𝐹 ∘ ( 𝐹 ∘ 𝐹 ) ) ∈ V )
33 32 anidms ⊢ ( 𝐹 ∈ 𝑉 → ( 𝐹 ∘ ( 𝐹 ∘ 𝐹 ) ) ∈ V )
34 25 27 29 30 33 ovmpod ⊢ ( 𝐹 ∈ 𝑉 → ( ( 𝐹 ∘ 𝐹 ) ( 𝑔 ∈ V , 𝑗 ∈ V ↦ ( 𝐹 ∘ 𝑔 ) ) 𝐹 ) = ( 𝐹 ∘ ( 𝐹 ∘ 𝐹 ) ) )
35 34 adantl ⊢ ( ( Rel 𝐹 ∧ 𝐹 ∈ 𝑉 ) → ( ( 𝐹 ∘ 𝐹 ) ( 𝑔 ∈ V , 𝑗 ∈ V ↦ ( 𝐹 ∘ 𝑔 ) ) 𝐹 ) = ( 𝐹 ∘ ( 𝐹 ∘ 𝐹 ) ) )
36 3 24 35 3eqtrd ⊢ ( ( Rel 𝐹 ∧ 𝐹 ∈ 𝑉 ) → ( ( IterComp ‘ 𝐹 ) ‘ 3 ) = ( 𝐹 ∘ ( 𝐹 ∘ 𝐹 ) ) )