Metamath Proof Explorer


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 mulid1d ( 𝐶 ∈ ℕ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 ) ) ) ) ) )