itcovalsuc

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

		Ref	Expression
	Assertion	itcovalsuc	$⊢ (F \in V \land Y \in ℕ_{0} \land IterComp (F) (Y) = G) \to IterComp (F) (Y + 1) = G (g \in V, j \in V ⟼ F \circ g) F$

Proof

Step	Hyp	Ref	Expression
1		simp1	$⊢ (F \in V \land Y \in ℕ_{0} \land IterComp (F) (Y) = G) \to F \in V$
2		itcoval	$⊢ F \in V \to IterComp (F) = seq 0 ((g \in V, j \in V ⟼ F \circ g), (i \in ℕ_{0} ⟼ if (i = 0, {I ↾}_{dom F}, F)))$
3	2	fveq1d	$⊢ F \in V \to IterComp (F) (Y + 1) = seq 0 ((g \in V, j \in V ⟼ F \circ g), (i \in ℕ_{0} ⟼ if (i = 0, {I ↾}_{dom F}, F))) (Y + 1)$
4	1 3	syl	$⊢ (F \in V \land Y \in ℕ_{0} \land IterComp (F) (Y) = G) \to IterComp (F) (Y + 1) = seq 0 ((g \in V, j \in V ⟼ F \circ g), (i \in ℕ_{0} ⟼ if (i = 0, {I ↾}_{dom F}, F))) (Y + 1)$
5		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
6		simp2	$⊢ (F \in V \land Y \in ℕ_{0} \land IterComp (F) (Y) = G) \to Y \in ℕ_{0}$
7		eqid	$⊢ Y + 1 = Y + 1$
8	2	adantr	$⊢ (F \in V \land Y \in ℕ_{0}) \to IterComp (F) = seq 0 ((g \in V, j \in V ⟼ F \circ g), (i \in ℕ_{0} ⟼ if (i = 0, {I ↾}_{dom F}, F)))$
9	8	fveq1d	$⊢ (F \in V \land Y \in ℕ_{0}) \to IterComp (F) (Y) = seq 0 ((g \in V, j \in V ⟼ F \circ g), (i \in ℕ_{0} ⟼ if (i = 0, {I ↾}_{dom F}, F))) (Y)$
10	9	eqeq1d	$⊢ (F \in V \land Y \in ℕ_{0}) \to (IterComp (F) (Y) = G \leftrightarrow seq 0 ((g \in V, j \in V ⟼ F \circ g), (i \in ℕ_{0} ⟼ if (i = 0, {I ↾}_{dom F}, F))) (Y) = G)$
11	10	biimp3a	$⊢ (F \in V \land Y \in ℕ_{0} \land IterComp (F) (Y) = G) \to seq 0 ((g \in V, j \in V ⟼ F \circ g), (i \in ℕ_{0} ⟼ if (i = 0, {I ↾}_{dom F}, F))) (Y) = G$
12		eqidd	$⊢ (F \in V \land Y \in ℕ_{0} \land IterComp (F) (Y) = G) \to (i \in ℕ_{0} ⟼ if (i = 0, {I ↾}_{dom F}, F)) = (i \in ℕ_{0} ⟼ if (i = 0, {I ↾}_{dom F}, F))$
13		nn0p1gt0	$⊢ Y \in ℕ_{0} \to 0 < Y + 1$
14	13	3ad2ant2	$⊢ (F \in V \land Y \in ℕ_{0} \land IterComp (F) (Y) = G) \to 0 < Y + 1$
15	14	gt0ne0d	$⊢ (F \in V \land Y \in ℕ_{0} \land IterComp (F) (Y) = G) \to Y + 1 \neq 0$
16	15	adantr	$⊢ ((F \in V \land Y \in ℕ_{0} \land IterComp (F) (Y) = G) \land i = Y + 1) \to Y + 1 \neq 0$
17		neeq1	$⊢ i = Y + 1 \to (i \neq 0 \leftrightarrow Y + 1 \neq 0)$
18	17	adantl	$⊢ ((F \in V \land Y \in ℕ_{0} \land IterComp (F) (Y) = G) \land i = Y + 1) \to (i \neq 0 \leftrightarrow Y + 1 \neq 0)$
19	16 18	mpbird	$⊢ ((F \in V \land Y \in ℕ_{0} \land IterComp (F) (Y) = G) \land i = Y + 1) \to i \neq 0$
20	19	neneqd	$⊢ ((F \in V \land Y \in ℕ_{0} \land IterComp (F) (Y) = G) \land i = Y + 1) \to \neg i = 0$
21	20	iffalsed	$⊢ ((F \in V \land Y \in ℕ_{0} \land IterComp (F) (Y) = G) \land i = Y + 1) \to if (i = 0, {I ↾}_{dom F}, F) = F$
22		peano2nn0	$⊢ Y \in ℕ_{0} \to Y + 1 \in ℕ_{0}$
23	22	3ad2ant2	$⊢ (F \in V \land Y \in ℕ_{0} \land IterComp (F) (Y) = G) \to Y + 1 \in ℕ_{0}$
24	12 21 23 1	fvmptd	$⊢ (F \in V \land Y \in ℕ_{0} \land IterComp (F) (Y) = G) \to (i \in ℕ_{0} ⟼ if (i = 0, {I ↾}_{dom F}, F)) (Y + 1) = F$
25	5 6 7 11 24	seqp1d	$⊢ (F \in V \land Y \in ℕ_{0} \land IterComp (F) (Y) = G) \to seq 0 ((g \in V, j \in V ⟼ F \circ g), (i \in ℕ_{0} ⟼ if (i = 0, {I ↾}_{dom F}, F))) (Y + 1) = G (g \in V, j \in V ⟼ F \circ g) F$
26	4 25	eqtrd	$⊢ (F \in V \land Y \in ℕ_{0} \land IterComp (F) (Y) = G) \to IterComp (F) (Y + 1) = G (g \in V, j \in V ⟼ F \circ g) F$

Metamath Proof Explorer

Theorem itcovalsuc

Proof