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 𝐹 ) )