Theorem itcovalpclem2

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

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

Proof

Step	Hyp	Ref	Expression
1		itcovalpc.f	⊢ 𝐹 = ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + 𝐶 ) )
2		nn0ex	⊢ ℕ0 ∈ V
3	2	mptex	⊢ ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + 𝐶 ) ) ∈ V
4	1 3	eqeltri	⊢ 𝐹 ∈ V
5		simpl	⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) → 𝑦 ∈ ℕ0 )
6		simpr	⊢ ( ( ( 𝑦 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) ∧ ( ( IterComp ‘ 𝐹 ) ‘ 𝑦 ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + ( 𝐶 · 𝑦 ) ) ) ) → ( ( IterComp ‘ 𝐹 ) ‘ 𝑦 ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + ( 𝐶 · 𝑦 ) ) ) )
7		itcovalsucov	⊢ ( ( 𝐹 ∈ V ∧ 𝑦 ∈ ℕ0 ∧ ( ( IterComp ‘ 𝐹 ) ‘ 𝑦 ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + ( 𝐶 · 𝑦 ) ) ) ) → ( ( IterComp ‘ 𝐹 ) ‘ ( 𝑦 + 1 ) ) = ( 𝐹 ∘ ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + ( 𝐶 · 𝑦 ) ) ) ) )
8	4 5 6 7	mp3an2ani	⊢ ( ( ( 𝑦 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) ∧ ( ( IterComp ‘ 𝐹 ) ‘ 𝑦 ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + ( 𝐶 · 𝑦 ) ) ) ) → ( ( IterComp ‘ 𝐹 ) ‘ ( 𝑦 + 1 ) ) = ( 𝐹 ∘ ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + ( 𝐶 · 𝑦 ) ) ) ) )
9		simpr	⊢ ( ( ( 𝑦 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑛 ∈ ℕ0 ) → 𝑛 ∈ ℕ0 )
10		simplr	⊢ ( ( ( 𝑦 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑛 ∈ ℕ0 ) → 𝐶 ∈ ℕ0 )
11	5	adantr	⊢ ( ( ( 𝑦 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑛 ∈ ℕ0 ) → 𝑦 ∈ ℕ0 )
12	10 11	nn0mulcld	⊢ ( ( ( 𝑦 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝐶 · 𝑦 ) ∈ ℕ0 )
13	9 12	nn0addcld	⊢ ( ( ( 𝑦 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑛 + ( 𝐶 · 𝑦 ) ) ∈ ℕ0 )
14		eqidd	⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) → ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + ( 𝐶 · 𝑦 ) ) ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + ( 𝐶 · 𝑦 ) ) ) )
15		oveq1	⊢ ( 𝑛 = 𝑚 → ( 𝑛 + 𝐶 ) = ( 𝑚 + 𝐶 ) )
16	15	cbvmptv	⊢ ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + 𝐶 ) ) = ( 𝑚 ∈ ℕ0 ↦ ( 𝑚 + 𝐶 ) )
17	1 16	eqtri	⊢ 𝐹 = ( 𝑚 ∈ ℕ0 ↦ ( 𝑚 + 𝐶 ) )
18	17	a1i	⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) → 𝐹 = ( 𝑚 ∈ ℕ0 ↦ ( 𝑚 + 𝐶 ) ) )
19		oveq1	⊢ ( 𝑚 = ( 𝑛 + ( 𝐶 · 𝑦 ) ) → ( 𝑚 + 𝐶 ) = ( ( 𝑛 + ( 𝐶 · 𝑦 ) ) + 𝐶 ) )
20	13 14 18 19	fmptco	⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) → ( 𝐹 ∘ ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + ( 𝐶 · 𝑦 ) ) ) ) = ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 + ( 𝐶 · 𝑦 ) ) + 𝐶 ) ) )
21	9	nn0cnd	⊢ ( ( ( 𝑦 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑛 ∈ ℕ0 ) → 𝑛 ∈ ℂ )
22	12	nn0cnd	⊢ ( ( ( 𝑦 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝐶 · 𝑦 ) ∈ ℂ )
23	10	nn0cnd	⊢ ( ( ( 𝑦 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑛 ∈ ℕ0 ) → 𝐶 ∈ ℂ )
24	21 22 23	addassd	⊢ ( ( ( 𝑦 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑛 + ( 𝐶 · 𝑦 ) ) + 𝐶 ) = ( 𝑛 + ( ( 𝐶 · 𝑦 ) + 𝐶 ) ) )
25		nn0cn	⊢ ( 𝐶 ∈ ℕ0 → 𝐶 ∈ ℂ )
26	25	mulridd	⊢ ( 𝐶 ∈ ℕ0 → ( 𝐶 · 1 ) = 𝐶 )
27	26	adantl	⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) → ( 𝐶 · 1 ) = 𝐶 )
28	27	eqcomd	⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) → 𝐶 = ( 𝐶 · 1 ) )
29	28	oveq2d	⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) → ( ( 𝐶 · 𝑦 ) + 𝐶 ) = ( ( 𝐶 · 𝑦 ) + ( 𝐶 · 1 ) ) )
30		simpr	⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) → 𝐶 ∈ ℕ0 )
31	30	nn0cnd	⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) → 𝐶 ∈ ℂ )
32	5	nn0cnd	⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) → 𝑦 ∈ ℂ )
33		1cnd	⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) → 1 ∈ ℂ )
34	31 32 33	adddid	⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) → ( 𝐶 · ( 𝑦 + 1 ) ) = ( ( 𝐶 · 𝑦 ) + ( 𝐶 · 1 ) ) )
35	29 34	eqtr4d	⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) → ( ( 𝐶 · 𝑦 ) + 𝐶 ) = ( 𝐶 · ( 𝑦 + 1 ) ) )
36	35	oveq2d	⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) → ( 𝑛 + ( ( 𝐶 · 𝑦 ) + 𝐶 ) ) = ( 𝑛 + ( 𝐶 · ( 𝑦 + 1 ) ) ) )
37	36	adantr	⊢ ( ( ( 𝑦 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑛 + ( ( 𝐶 · 𝑦 ) + 𝐶 ) ) = ( 𝑛 + ( 𝐶 · ( 𝑦 + 1 ) ) ) )
38	24 37	eqtrd	⊢ ( ( ( 𝑦 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑛 + ( 𝐶 · 𝑦 ) ) + 𝐶 ) = ( 𝑛 + ( 𝐶 · ( 𝑦 + 1 ) ) ) )
39	38	mpteq2dva	⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) → ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 + ( 𝐶 · 𝑦 ) ) + 𝐶 ) ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + ( 𝐶 · ( 𝑦 + 1 ) ) ) ) )
40	20 39	eqtrd	⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) → ( 𝐹 ∘ ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + ( 𝐶 · 𝑦 ) ) ) ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + ( 𝐶 · ( 𝑦 + 1 ) ) ) ) )
41	40	adantr	⊢ ( ( ( 𝑦 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) ∧ ( ( IterComp ‘ 𝐹 ) ‘ 𝑦 ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + ( 𝐶 · 𝑦 ) ) ) ) → ( 𝐹 ∘ ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + ( 𝐶 · 𝑦 ) ) ) ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + ( 𝐶 · ( 𝑦 + 1 ) ) ) ) )
42	8 41	eqtrd	⊢ ( ( ( 𝑦 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) ∧ ( ( IterComp ‘ 𝐹 ) ‘ 𝑦 ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + ( 𝐶 · 𝑦 ) ) ) ) → ( ( IterComp ‘ 𝐹 ) ‘ ( 𝑦 + 1 ) ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + ( 𝐶 · ( 𝑦 + 1 ) ) ) ) )
43	42	ex	⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) → ( ( ( IterComp ‘ 𝐹 ) ‘ 𝑦 ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + ( 𝐶 · 𝑦 ) ) ) → ( ( IterComp ‘ 𝐹 ) ‘ ( 𝑦 + 1 ) ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + ( 𝐶 · ( 𝑦 + 1 ) ) ) ) ) )