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 ⊢ F ∈ V → IterComp ⁡ F ⁡ 0 = I ↾ dom ⁡ 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 ⁡ 0 = seq 0 g ∈ V , j ∈ V ⟼ F ∘ g i ∈ ℕ 0 ⟼ if i = 0 I ↾ dom ⁡ F F ⁡ 0
3 0z ⊢ 0 ∈ ℤ
4 eqidd ⊢ F ∈ V → i ∈ ℕ 0 ⟼ if i = 0 I ↾ dom ⁡ F F = i ∈ ℕ 0 ⟼ if i = 0 I ↾ dom ⁡ F F
5 iftrue ⊢ i = 0 → if i = 0 I ↾ dom ⁡ F F = I ↾ dom ⁡ F
6 5 adantl ⊢ F ∈ V ∧ i = 0 → if i = 0 I ↾ dom ⁡ F F = I ↾ dom ⁡ F
7 0nn0 ⊢ 0 ∈ ℕ 0
8 7 a1i ⊢ F ∈ V → 0 ∈ ℕ 0
9 dmexg ⊢ F ∈ V → dom ⁡ F ∈ V
10 9 resiexd ⊢ F ∈ V → I ↾ dom ⁡ F ∈ V
11 4 6 8 10 fvmptd ⊢ F ∈ V → i ∈ ℕ 0 ⟼ if i = 0 I ↾ dom ⁡ F F ⁡ 0 = I ↾ dom ⁡ F
12 3 11 seq1i ⊢ F ∈ V → seq 0 g ∈ V , j ∈ V ⟼ F ∘ g i ∈ ℕ 0 ⟼ if i = 0 I ↾ dom ⁡ F F ⁡ 0 = I ↾ dom ⁡ F
13 2 12 eqtrd ⊢ F ∈ V → IterComp ⁡ F ⁡ 0 = I ↾ dom ⁡ F