Theorem itcovalpclem1

Description: Lemma 1 for itcovalpc : induction basis. (Contributed by AV, 4-May-2024)

	Ref	Expression
Hypothesis	itcovalpc.f	⊢ 𝐹 = ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + 𝐶 ) )
Assertion	itcovalpclem1	⊢ ( 𝐶 ∈ ℕ0 → ( ( IterComp ‘ 𝐹 ) ‘ 0 ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + ( 𝐶 · 0 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		itcovalpc.f	⊢ 𝐹 = ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + 𝐶 ) )
2		nn0ex	⊢ ℕ0 ∈ V
3		ovexd	⊢ ( 𝑛 ∈ ℕ0 → ( 𝑛 + 𝐶 ) ∈ V )
4	3	rgen	⊢ ∀ 𝑛 ∈ ℕ0 ( 𝑛 + 𝐶 ) ∈ V
5	1	itcoval0mpt	⊢ ( ( ℕ0 ∈ V ∧ ∀ 𝑛 ∈ ℕ0 ( 𝑛 + 𝐶 ) ∈ V ) → ( ( IterComp ‘ 𝐹 ) ‘ 0 ) = ( 𝑛 ∈ ℕ0 ↦ 𝑛 ) )
6	2 4 5	mp2an	⊢ ( ( IterComp ‘ 𝐹 ) ‘ 0 ) = ( 𝑛 ∈ ℕ0 ↦ 𝑛 )
7		nn0cn	⊢ ( 𝐶 ∈ ℕ0 → 𝐶 ∈ ℂ )
8	7	mul01d	⊢ ( 𝐶 ∈ ℕ0 → ( 𝐶 · 0 ) = 0 )
9	8	adantr	⊢ ( ( 𝐶 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) → ( 𝐶 · 0 ) = 0 )
10	9	oveq2d	⊢ ( ( 𝐶 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) → ( 𝑛 + ( 𝐶 · 0 ) ) = ( 𝑛 + 0 ) )
11		nn0cn	⊢ ( 𝑛 ∈ ℕ0 → 𝑛 ∈ ℂ )
12	11	addid1d	⊢ ( 𝑛 ∈ ℕ0 → ( 𝑛 + 0 ) = 𝑛 )
13	12	adantl	⊢ ( ( 𝐶 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) → ( 𝑛 + 0 ) = 𝑛 )
14	10 13	eqtr2d	⊢ ( ( 𝐶 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) → 𝑛 = ( 𝑛 + ( 𝐶 · 0 ) ) )
15	14	mpteq2dva	⊢ ( 𝐶 ∈ ℕ0 → ( 𝑛 ∈ ℕ0 ↦ 𝑛 ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + ( 𝐶 · 0 ) ) ) )
16	6 15	syl5eq	⊢ ( 𝐶 ∈ ℕ0 → ( ( IterComp ‘ 𝐹 ) ‘ 0 ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + ( 𝐶 · 0 ) ) ) )