Metamath Proof Explorer

Theorem itcovalpc

Description: The value of the function that returns the n-th iterate of the "plus a constant" function with regard to composition. (Contributed by AV, 4-May-2024)

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

Proof

Step Hyp Ref Expression
1 itcovalpc.f ⊢ 𝐹 = ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + 𝐶 ) )
2 fveq2 ⊢ ( 𝑥 = 0 → ( ( IterComp ‘ 𝐹 ) ‘ 𝑥 ) = ( ( IterComp ‘ 𝐹 ) ‘ 0 ) )
3 oveq2 ⊢ ( 𝑥 = 0 → ( 𝐶 · 𝑥 ) = ( 𝐶 · 0 ) )
4 3 oveq2d ⊢ ( 𝑥 = 0 → ( 𝑛 + ( 𝐶 · 𝑥 ) ) = ( 𝑛 + ( 𝐶 · 0 ) ) )
5 4 mpteq2dv ⊢ ( 𝑥 = 0 → ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + ( 𝐶 · 𝑥 ) ) ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + ( 𝐶 · 0 ) ) ) )
6 2 5 eqeq12d ⊢ ( 𝑥 = 0 → ( ( ( IterComp ‘ 𝐹 ) ‘ 𝑥 ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + ( 𝐶 · 𝑥 ) ) ) ↔ ( ( IterComp ‘ 𝐹 ) ‘ 0 ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + ( 𝐶 · 0 ) ) ) ) )
7 fveq2 ⊢ ( 𝑥 = 𝑦 → ( ( IterComp ‘ 𝐹 ) ‘ 𝑥 ) = ( ( IterComp ‘ 𝐹 ) ‘ 𝑦 ) )
8 oveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝐶 · 𝑥 ) = ( 𝐶 · 𝑦 ) )
9 8 oveq2d ⊢ ( 𝑥 = 𝑦 → ( 𝑛 + ( 𝐶 · 𝑥 ) ) = ( 𝑛 + ( 𝐶 · 𝑦 ) ) )
10 9 mpteq2dv ⊢ ( 𝑥 = 𝑦 → ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + ( 𝐶 · 𝑥 ) ) ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + ( 𝐶 · 𝑦 ) ) ) )
11 7 10 eqeq12d ⊢ ( 𝑥 = 𝑦 → ( ( ( IterComp ‘ 𝐹 ) ‘ 𝑥 ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + ( 𝐶 · 𝑥 ) ) ) ↔ ( ( IterComp ‘ 𝐹 ) ‘ 𝑦 ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + ( 𝐶 · 𝑦 ) ) ) ) )
12 fveq2 ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ( IterComp ‘ 𝐹 ) ‘ 𝑥 ) = ( ( IterComp ‘ 𝐹 ) ‘ ( 𝑦 + 1 ) ) )
13 oveq2 ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( 𝐶 · 𝑥 ) = ( 𝐶 · ( 𝑦 + 1 ) ) )
14 13 oveq2d ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( 𝑛 + ( 𝐶 · 𝑥 ) ) = ( 𝑛 + ( 𝐶 · ( 𝑦 + 1 ) ) ) )
15 14 mpteq2dv ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + ( 𝐶 · 𝑥 ) ) ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + ( 𝐶 · ( 𝑦 + 1 ) ) ) ) )
16 12 15 eqeq12d ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ( ( IterComp ‘ 𝐹 ) ‘ 𝑥 ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + ( 𝐶 · 𝑥 ) ) ) ↔ ( ( IterComp ‘ 𝐹 ) ‘ ( 𝑦 + 1 ) ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + ( 𝐶 · ( 𝑦 + 1 ) ) ) ) ) )
17 fveq2 ⊢ ( 𝑥 = 𝐼 → ( ( IterComp ‘ 𝐹 ) ‘ 𝑥 ) = ( ( IterComp ‘ 𝐹 ) ‘ 𝐼 ) )
18 oveq2 ⊢ ( 𝑥 = 𝐼 → ( 𝐶 · 𝑥 ) = ( 𝐶 · 𝐼 ) )
19 18 oveq2d ⊢ ( 𝑥 = 𝐼 → ( 𝑛 + ( 𝐶 · 𝑥 ) ) = ( 𝑛 + ( 𝐶 · 𝐼 ) ) )
20 19 mpteq2dv ⊢ ( 𝑥 = 𝐼 → ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + ( 𝐶 · 𝑥 ) ) ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + ( 𝐶 · 𝐼 ) ) ) )
21 17 20 eqeq12d ⊢ ( 𝑥 = 𝐼 → ( ( ( IterComp ‘ 𝐹 ) ‘ 𝑥 ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + ( 𝐶 · 𝑥 ) ) ) ↔ ( ( IterComp ‘ 𝐹 ) ‘ 𝐼 ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + ( 𝐶 · 𝐼 ) ) ) ) )
22 1 itcovalpclem1 ⊢ ( 𝐶 ∈ ℕ0 → ( ( IterComp ‘ 𝐹 ) ‘ 0 ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + ( 𝐶 · 0 ) ) ) )
23 1 itcovalpclem2 ⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) → ( ( ( IterComp ‘ 𝐹 ) ‘ 𝑦 ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + ( 𝐶 · 𝑦 ) ) ) → ( ( IterComp ‘ 𝐹 ) ‘ ( 𝑦 + 1 ) ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + ( 𝐶 · ( 𝑦 + 1 ) ) ) ) ) )
24 23 ancoms ⊢ ( ( 𝐶 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0 ) → ( ( ( IterComp ‘ 𝐹 ) ‘ 𝑦 ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + ( 𝐶 · 𝑦 ) ) ) → ( ( IterComp ‘ 𝐹 ) ‘ ( 𝑦 + 1 ) ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + ( 𝐶 · ( 𝑦 + 1 ) ) ) ) ) )
25 24 imp ⊢ ( ( ( 𝐶 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0 ) ∧ ( ( IterComp ‘ 𝐹 ) ‘ 𝑦 ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + ( 𝐶 · 𝑦 ) ) ) ) → ( ( IterComp ‘ 𝐹 ) ‘ ( 𝑦 + 1 ) ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + ( 𝐶 · ( 𝑦 + 1 ) ) ) ) )
26 6 11 16 21 22 25 nn0indd ⊢ ( ( 𝐶 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ) → ( ( IterComp ‘ 𝐹 ) ‘ 𝐼 ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + ( 𝐶 · 𝐼 ) ) ) )
27 26 ancoms ⊢ ( ( 𝐼 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) → ( ( IterComp ‘ 𝐹 ) ‘ 𝐼 ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + ( 𝐶 · 𝐼 ) ) ) )