This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝐹 ∈ 𝑉 → ( ( IterComp ‘ 𝐹 ) ‘ 0 ) = ( I ↾ dom 𝐹 ) )

Proof

Step Hyp Ref Expression
1 itcoval ⊢ ( 𝐹 ∈ 𝑉 → ( IterComp ‘ 𝐹 ) = seq 0 ( ( 𝑔 ∈ V , 𝑗 ∈ V ↦ ( 𝐹 ∘ 𝑔 ) ) , ( 𝑖 ∈ ℕ0 ↦ if ( 𝑖 = 0 , ( I ↾ dom 𝐹 ) , 𝐹 ) ) ) )
2 1 fveq1d ⊢ ( 𝐹 ∈ 𝑉 → ( ( IterComp ‘ 𝐹 ) ‘ 0 ) = ( seq 0 ( ( 𝑔 ∈ V , 𝑗 ∈ V ↦ ( 𝐹 ∘ 𝑔 ) ) , ( 𝑖 ∈ ℕ0 ↦ if ( 𝑖 = 0 , ( I ↾ dom 𝐹 ) , 𝐹 ) ) ) ‘ 0 ) )
3 0z ⊢ 0 ∈ ℤ
4 eqidd ⊢ ( 𝐹 ∈ 𝑉 → ( 𝑖 ∈ ℕ0 ↦ if ( 𝑖 = 0 , ( I ↾ dom 𝐹 ) , 𝐹 ) ) = ( 𝑖 ∈ ℕ0 ↦ if ( 𝑖 = 0 , ( I ↾ dom 𝐹 ) , 𝐹 ) ) )
5 iftrue ⊢ ( 𝑖 = 0 → if ( 𝑖 = 0 , ( I ↾ dom 𝐹 ) , 𝐹 ) = ( I ↾ dom 𝐹 ) )
6 5 adantl ⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝑖 = 0 ) → if ( 𝑖 = 0 , ( I ↾ dom 𝐹 ) , 𝐹 ) = ( I ↾ dom 𝐹 ) )
7 0nn0 ⊢ 0 ∈ ℕ0
8 7 a1i ⊢ ( 𝐹 ∈ 𝑉 → 0 ∈ ℕ0 )
9 dmexg ⊢ ( 𝐹 ∈ 𝑉 → dom 𝐹 ∈ V )
10 9 resiexd ⊢ ( 𝐹 ∈ 𝑉 → ( I ↾ dom 𝐹 ) ∈ V )
11 4 6 8 10 fvmptd ⊢ ( 𝐹 ∈ 𝑉 → ( ( 𝑖 ∈ ℕ0 ↦ if ( 𝑖 = 0 , ( I ↾ dom 𝐹 ) , 𝐹 ) ) ‘ 0 ) = ( I ↾ dom 𝐹 ) )
12 3 11 seq1i ⊢ ( 𝐹 ∈ 𝑉 → ( seq 0 ( ( 𝑔 ∈ V , 𝑗 ∈ V ↦ ( 𝐹 ∘ 𝑔 ) ) , ( 𝑖 ∈ ℕ0 ↦ if ( 𝑖 = 0 , ( I ↾ dom 𝐹 ) , 𝐹 ) ) ) ‘ 0 ) = ( I ↾ dom 𝐹 ) )
13 2 12 eqtrd ⊢ ( 𝐹 ∈ 𝑉 → ( ( IterComp ‘ 𝐹 ) ‘ 0 ) = ( I ↾ dom 𝐹 ) )