itcoval3

Description: A function iterated three times. (Contributed by AV, 2-May-2024)

		Ref	Expression
	Assertion	itcoval3	$⊢ (Rel F \land F \in V) \to IterComp (F) (3) = F \circ (F \circ F)$

Proof

Step	Hyp	Ref	Expression
1		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)))$
2	1	fveq1d	$⊢ F \in V \to IterComp (F) (3) = seq 0 ((g \in V, j \in V ⟼ F \circ g), (i \in ℕ_{0} ⟼ if (i = 0, {I ↾}_{dom F}, F))) (3)$
3	2	adantl	$⊢ (Rel F \land F \in V) \to IterComp (F) (3) = seq 0 ((g \in V, j \in V ⟼ F \circ g), (i \in ℕ_{0} ⟼ if (i = 0, {I ↾}_{dom F}, F))) (3)$
4		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
5		2nn0	$⊢ 2 \in ℕ_{0}$
6	5	a1i	$⊢ (Rel F \land F \in V) \to 2 \in ℕ_{0}$
7		df-3	$⊢ 3 = 2 + 1$
8	1	eqcomd	$⊢ F \in V \to seq 0 ((g \in V, j \in V ⟼ F \circ g), (i \in ℕ_{0} ⟼ if (i = 0, {I ↾}_{dom F}, F))) = IterComp (F)$
9	8	fveq1d	$⊢ F \in V \to seq 0 ((g \in V, j \in V ⟼ F \circ g), (i \in ℕ_{0} ⟼ if (i = 0, {I ↾}_{dom F}, F))) (2) = IterComp (F) (2)$
10	9	adantl	$⊢ (Rel F \land F \in V) \to seq 0 ((g \in V, j \in V ⟼ F \circ g), (i \in ℕ_{0} ⟼ if (i = 0, {I ↾}_{dom F}, F))) (2) = IterComp (F) (2)$
11		itcoval2	$⊢ (Rel F \land F \in V) \to IterComp (F) (2) = F \circ F$
12	10 11	eqtrd	$⊢ (Rel F \land F \in V) \to seq 0 ((g \in V, j \in V ⟼ F \circ g), (i \in ℕ_{0} ⟼ if (i = 0, {I ↾}_{dom F}, F))) (2) = F \circ F$
13		eqidd	$⊢ (Rel F \land F \in V) \to (i \in ℕ_{0} ⟼ if (i = 0, {I ↾}_{dom F}, F)) = (i \in ℕ_{0} ⟼ if (i = 0, {I ↾}_{dom F}, F))$
14		3ne0	$⊢ 3 \neq 0$
15		neeq1	$⊢ i = 3 \to (i \neq 0 \leftrightarrow 3 \neq 0)$
16	14 15	mpbiri	$⊢ i = 3 \to i \neq 0$
17	16	neneqd	$⊢ i = 3 \to \neg i = 0$
18	17	iffalsed	$⊢ i = 3 \to if (i = 0, {I ↾}_{dom F}, F) = F$
19	18	adantl	$⊢ ((Rel F \land F \in V) \land i = 3) \to if (i = 0, {I ↾}_{dom F}, F) = F$
20		3nn0	$⊢ 3 \in ℕ_{0}$
21	20	a1i	$⊢ (Rel F \land F \in V) \to 3 \in ℕ_{0}$
22		simpr	$⊢ (Rel F \land F \in V) \to F \in V$
23	13 19 21 22	fvmptd	$⊢ (Rel F \land F \in V) \to (i \in ℕ_{0} ⟼ if (i = 0, {I ↾}_{dom F}, F)) (3) = F$
24	4 6 7 12 23	seqp1d	$⊢ (Rel F \land F \in V) \to seq 0 ((g \in V, j \in V ⟼ F \circ g), (i \in ℕ_{0} ⟼ if (i = 0, {I ↾}_{dom F}, F))) (3) = (F \circ F) (g \in V, j \in V ⟼ F \circ g) F$
25		eqidd	$⊢ F \in V \to (g \in V, j \in V ⟼ F \circ g) = (g \in V, j \in V ⟼ F \circ g)$
26		coeq2	$⊢ g = F \circ F \to F \circ g = F \circ (F \circ F)$
27	26	ad2antrl	$⊢ (F \in V \land (g = F \circ F \land j = F)) \to F \circ g = F \circ (F \circ F)$
28		coexg	$⊢ (F \in V \land F \in V) \to F \circ F \in V$
29	28	anidms	$⊢ F \in V \to F \circ F \in V$
30		elex	$⊢ F \in V \to F \in V$
31		coexg	$⊢ (F \in V \land F \circ F \in V) \to F \circ (F \circ F) \in V$
32	28 31	syldan	$⊢ (F \in V \land F \in V) \to F \circ (F \circ F) \in V$
33	32	anidms	$⊢ F \in V \to F \circ (F \circ F) \in V$
34	25 27 29 30 33	ovmpod	$⊢ F \in V \to (F \circ F) (g \in V, j \in V ⟼ F \circ g) F = F \circ (F \circ F)$
35	34	adantl	$⊢ (Rel F \land F \in V) \to (F \circ F) (g \in V, j \in V ⟼ F \circ g) F = F \circ (F \circ F)$
36	3 24 35	3eqtrd	$⊢ (Rel F \land F \in V) \to IterComp (F) (3) = F \circ (F \circ F)$

Metamath Proof Explorer

Theorem itcoval3

Proof