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 ( ( 𝐹 ∈ 𝑉 ∧ 𝑌 ∈ ℕ0 ∧ ( ( IterComp ‘ 𝐹 ) ‘ 𝑌 ) = 𝐺 ) → ( ( IterComp ‘ 𝐹 ) ‘ ( 𝑌 + 1 ) ) = ( 𝐺 ( 𝑔 ∈ V , 𝑗 ∈ V ↦ ( 𝐹 ∘ 𝑔 ) ) 𝐹 ) )

Proof

Step Hyp Ref Expression
1 simp1 ⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝑌 ∈ ℕ0 ∧ ( ( IterComp ‘ 𝐹 ) ‘ 𝑌 ) = 𝐺 ) → 𝐹 ∈ 𝑉 )
2 itcoval ⊢ ( 𝐹 ∈ 𝑉 → ( IterComp ‘ 𝐹 ) = seq 0 ( ( 𝑔 ∈ V , 𝑗 ∈ V ↦ ( 𝐹 ∘ 𝑔 ) ) , ( 𝑖 ∈ ℕ0 ↦ if ( 𝑖 = 0 , ( I ↾ dom 𝐹 ) , 𝐹 ) ) ) )
3 2 fveq1d ⊢ ( 𝐹 ∈ 𝑉 → ( ( IterComp ‘ 𝐹 ) ‘ ( 𝑌 + 1 ) ) = ( seq 0 ( ( 𝑔 ∈ V , 𝑗 ∈ V ↦ ( 𝐹 ∘ 𝑔 ) ) , ( 𝑖 ∈ ℕ0 ↦ if ( 𝑖 = 0 , ( I ↾ dom 𝐹 ) , 𝐹 ) ) ) ‘ ( 𝑌 + 1 ) ) )
4 1 3 syl ⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝑌 ∈ ℕ0 ∧ ( ( IterComp ‘ 𝐹 ) ‘ 𝑌 ) = 𝐺 ) → ( ( IterComp ‘ 𝐹 ) ‘ ( 𝑌 + 1 ) ) = ( seq 0 ( ( 𝑔 ∈ V , 𝑗 ∈ V ↦ ( 𝐹 ∘ 𝑔 ) ) , ( 𝑖 ∈ ℕ0 ↦ if ( 𝑖 = 0 , ( I ↾ dom 𝐹 ) , 𝐹 ) ) ) ‘ ( 𝑌 + 1 ) ) )
5 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
6 simp2 ⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝑌 ∈ ℕ0 ∧ ( ( IterComp ‘ 𝐹 ) ‘ 𝑌 ) = 𝐺 ) → 𝑌 ∈ ℕ0 )
7 eqid ⊢ ( 𝑌 + 1 ) = ( 𝑌 + 1 )
8 2 adantr ⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝑌 ∈ ℕ0 ) → ( IterComp ‘ 𝐹 ) = seq 0 ( ( 𝑔 ∈ V , 𝑗 ∈ V ↦ ( 𝐹 ∘ 𝑔 ) ) , ( 𝑖 ∈ ℕ0 ↦ if ( 𝑖 = 0 , ( I ↾ dom 𝐹 ) , 𝐹 ) ) ) )
9 8 fveq1d ⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝑌 ∈ ℕ0 ) → ( ( IterComp ‘ 𝐹 ) ‘ 𝑌 ) = ( seq 0 ( ( 𝑔 ∈ V , 𝑗 ∈ V ↦ ( 𝐹 ∘ 𝑔 ) ) , ( 𝑖 ∈ ℕ0 ↦ if ( 𝑖 = 0 , ( I ↾ dom 𝐹 ) , 𝐹 ) ) ) ‘ 𝑌 ) )
10 9 eqeq1d ⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝑌 ∈ ℕ0 ) → ( ( ( IterComp ‘ 𝐹 ) ‘ 𝑌 ) = 𝐺 ↔ ( seq 0 ( ( 𝑔 ∈ V , 𝑗 ∈ V ↦ ( 𝐹 ∘ 𝑔 ) ) , ( 𝑖 ∈ ℕ0 ↦ if ( 𝑖 = 0 , ( I ↾ dom 𝐹 ) , 𝐹 ) ) ) ‘ 𝑌 ) = 𝐺 ) )
11 10 biimp3a ⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝑌 ∈ ℕ0 ∧ ( ( IterComp ‘ 𝐹 ) ‘ 𝑌 ) = 𝐺 ) → ( seq 0 ( ( 𝑔 ∈ V , 𝑗 ∈ V ↦ ( 𝐹 ∘ 𝑔 ) ) , ( 𝑖 ∈ ℕ0 ↦ if ( 𝑖 = 0 , ( I ↾ dom 𝐹 ) , 𝐹 ) ) ) ‘ 𝑌 ) = 𝐺 )
12 eqidd ⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝑌 ∈ ℕ0 ∧ ( ( IterComp ‘ 𝐹 ) ‘ 𝑌 ) = 𝐺 ) → ( 𝑖 ∈ ℕ0 ↦ if ( 𝑖 = 0 , ( I ↾ dom 𝐹 ) , 𝐹 ) ) = ( 𝑖 ∈ ℕ0 ↦ if ( 𝑖 = 0 , ( I ↾ dom 𝐹 ) , 𝐹 ) ) )
13 nn0p1gt0 ⊢ ( 𝑌 ∈ ℕ0 → 0 < ( 𝑌 + 1 ) )
14 13 3ad2ant2 ⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝑌 ∈ ℕ0 ∧ ( ( IterComp ‘ 𝐹 ) ‘ 𝑌 ) = 𝐺 ) → 0 < ( 𝑌 + 1 ) )
15 14 gt0ne0d ⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝑌 ∈ ℕ0 ∧ ( ( IterComp ‘ 𝐹 ) ‘ 𝑌 ) = 𝐺 ) → ( 𝑌 + 1 ) ≠ 0 )
16 15 adantr ⊢ ( ( ( 𝐹 ∈ 𝑉 ∧ 𝑌 ∈ ℕ0 ∧ ( ( IterComp ‘ 𝐹 ) ‘ 𝑌 ) = 𝐺 ) ∧ 𝑖 = ( 𝑌 + 1 ) ) → ( 𝑌 + 1 ) ≠ 0 )
17 neeq1 ⊢ ( 𝑖 = ( 𝑌 + 1 ) → ( 𝑖 ≠ 0 ↔ ( 𝑌 + 1 ) ≠ 0 ) )
18 17 adantl ⊢ ( ( ( 𝐹 ∈ 𝑉 ∧ 𝑌 ∈ ℕ0 ∧ ( ( IterComp ‘ 𝐹 ) ‘ 𝑌 ) = 𝐺 ) ∧ 𝑖 = ( 𝑌 + 1 ) ) → ( 𝑖 ≠ 0 ↔ ( 𝑌 + 1 ) ≠ 0 ) )
19 16 18 mpbird ⊢ ( ( ( 𝐹 ∈ 𝑉 ∧ 𝑌 ∈ ℕ0 ∧ ( ( IterComp ‘ 𝐹 ) ‘ 𝑌 ) = 𝐺 ) ∧ 𝑖 = ( 𝑌 + 1 ) ) → 𝑖 ≠ 0 )
20 19 neneqd ⊢ ( ( ( 𝐹 ∈ 𝑉 ∧ 𝑌 ∈ ℕ0 ∧ ( ( IterComp ‘ 𝐹 ) ‘ 𝑌 ) = 𝐺 ) ∧ 𝑖 = ( 𝑌 + 1 ) ) → ¬ 𝑖 = 0 )
21 20 iffalsed ⊢ ( ( ( 𝐹 ∈ 𝑉 ∧ 𝑌 ∈ ℕ0 ∧ ( ( IterComp ‘ 𝐹 ) ‘ 𝑌 ) = 𝐺 ) ∧ 𝑖 = ( 𝑌 + 1 ) ) → if ( 𝑖 = 0 , ( I ↾ dom 𝐹 ) , 𝐹 ) = 𝐹 )
22 peano2nn0 ⊢ ( 𝑌 ∈ ℕ0 → ( 𝑌 + 1 ) ∈ ℕ0 )
23 22 3ad2ant2 ⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝑌 ∈ ℕ0 ∧ ( ( IterComp ‘ 𝐹 ) ‘ 𝑌 ) = 𝐺 ) → ( 𝑌 + 1 ) ∈ ℕ0 )
24 12 21 23 1 fvmptd ⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝑌 ∈ ℕ0 ∧ ( ( IterComp ‘ 𝐹 ) ‘ 𝑌 ) = 𝐺 ) → ( ( 𝑖 ∈ ℕ0 ↦ if ( 𝑖 = 0 , ( I ↾ dom 𝐹 ) , 𝐹 ) ) ‘ ( 𝑌 + 1 ) ) = 𝐹 )
25 5 6 7 11 24 seqp1d ⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝑌 ∈ ℕ0 ∧ ( ( IterComp ‘ 𝐹 ) ‘ 𝑌 ) = 𝐺 ) → ( seq 0 ( ( 𝑔 ∈ V , 𝑗 ∈ V ↦ ( 𝐹 ∘ 𝑔 ) ) , ( 𝑖 ∈ ℕ0 ↦ if ( 𝑖 = 0 , ( I ↾ dom 𝐹 ) , 𝐹 ) ) ) ‘ ( 𝑌 + 1 ) ) = ( 𝐺 ( 𝑔 ∈ V , 𝑗 ∈ V ↦ ( 𝐹 ∘ 𝑔 ) ) 𝐹 ) )
26 4 25 eqtrd ⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝑌 ∈ ℕ0 ∧ ( ( IterComp ‘ 𝐹 ) ‘ 𝑌 ) = 𝐺 ) → ( ( IterComp ‘ 𝐹 ) ‘ ( 𝑌 + 1 ) ) = ( 𝐺 ( 𝑔 ∈ V , 𝑗 ∈ V ↦ ( 𝐹 ∘ 𝑔 ) ) 𝐹 ) )