itcoval2

		Ref	Expression
	Assertion	itcoval2	$⊢ (Rel F \land F \in V) \to IterComp (F) (2) = 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) (2) = seq 0 ((g \in V, j \in V ⟼ F \circ g), (i \in ℕ_{0} ⟼ if (i = 0, {I ↾}_{dom F}, F))) (2)$
3	2	adantl	$⊢ (Rel F \land F \in V) \to IterComp (F) (2) = seq 0 ((g \in V, j \in V ⟼ F \circ g), (i \in ℕ_{0} ⟼ if (i = 0, {I ↾}_{dom F}, F))) (2)$
4		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
5		1nn0	$⊢ 1 \in ℕ_{0}$
6	5	a1i	$⊢ (Rel F \land F \in V) \to 1 \in ℕ_{0}$
7		df-2	$⊢ 2 = 1 + 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))) (1) = IterComp (F) (1)$
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))) (1) = IterComp (F) (1)$
11		itcoval1	$⊢ (Rel F \land F \in V) \to IterComp (F) (1) = 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))) (1) = 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		2ne0	$⊢ 2 \neq 0$
15		neeq1	$⊢ i = 2 \to (i \neq 0 \leftrightarrow 2 \neq 0)$
16	14 15	mpbiri	$⊢ i = 2 \to i \neq 0$
17	16	neneqd	$⊢ i = 2 \to \neg i = 0$
18	17	iffalsed	$⊢ i = 2 \to if (i = 0, {I ↾}_{dom F}, F) = F$
19	18	adantl	$⊢ ((Rel F \land F \in V) \land i = 2) \to if (i = 0, {I ↾}_{dom F}, F) = F$
20		2nn0	$⊢ 2 \in ℕ_{0}$
21	20	a1i	$⊢ (Rel F \land F \in V) \to 2 \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)) (2) = 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))) (2) = 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 \to F \circ g = F \circ F$
27	26	ad2antrl	$⊢ (F \in V \land (g = F \land j = F)) \to F \circ g = F \circ F$
28		elex	$⊢ F \in V \to F \in V$
29		coexg	$⊢ (F \in V \land F \in V) \to F \circ F \in V$
30	29	anidms	$⊢ F \in V \to F \circ F \in V$
31	25 27 28 28 30	ovmpod	$⊢ F \in V \to F (g \in V, j \in V ⟼ F \circ g) F = F \circ F$
32	31	adantl	$⊢ (Rel F \land F \in V) \to F (g \in V, j \in V ⟼ F \circ g) F = F \circ F$
33	3 24 32	3eqtrd	$⊢ (Rel F \land F \in V) \to IterComp (F) (2) = F \circ F$

Metamath Proof Explorer

Theorem itcoval2

Proof