Theorem itcovalpclem2

Description: Lemma 2 for itcovalpc : induction step. (Contributed by AV, 4-May-2024)

	Ref	Expression
Hypothesis	itcovalpc.f	$$⊢F=\left(n\in {\mathbb{N}}_0⟼n+C\right)$$
Assertion	itcovalpclem2	Could not format assertion : No typesetting found for |- ( ( y e. NN0 /\ C e. NN0 ) -> ( ( ( IterComp ` F ) ` y ) = ( n e. NN0 |-> ( n + ( C x. y ) ) ) -> ( ( IterComp ` F ) ` ( y + 1 ) ) = ( n e. NN0 |-> ( n + ( C x. ( y + 1 ) ) ) ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		itcovalpc.f	$$⊢F=\left(n\in {\mathbb{N}}_0⟼n+C\right)$$
2		nn0ex	$$⊢{\mathbb{N}}_0\in \mathrm{V}$$
3	2	mptex	$$⊢\left(n\in {\mathbb{N}}_0⟼n+C\right)\in \mathrm{V}$$
4	1 3	eqeltri	$$⊢F\in \mathrm{V}$$
5		simpl	$$⊢\left(y\in {\mathbb{N}}_0\wedge C\in {\mathbb{N}}_0\right)\to y\in {\mathbb{N}}_0$$
6		simpr	Could not format ( ( ( y e. NN0 /\ C e. NN0 ) /\ ( ( IterComp ` F ) ` y ) = ( n e. NN0 |-> ( n + ( C x. y ) ) ) ) -> ( ( IterComp ` F ) ` y ) = ( n e. NN0 |-> ( n + ( C x. y ) ) ) ) : No typesetting found for |- ( ( ( y e. NN0 /\ C e. NN0 ) /\ ( ( IterComp ` F ) ` y ) = ( n e. NN0 |-> ( n + ( C x. y ) ) ) ) -> ( ( IterComp ` F ) ` y ) = ( n e. NN0 |-> ( n + ( C x. y ) ) ) ) with typecode |-
7		itcovalsucov	Could not format ( ( F e. _V /\ y e. NN0 /\ ( ( IterComp ` F ) ` y ) = ( n e. NN0 |-> ( n + ( C x. y ) ) ) ) -> ( ( IterComp ` F ) ` ( y + 1 ) ) = ( F o. ( n e. NN0 |-> ( n + ( C x. y ) ) ) ) ) : No typesetting found for |- ( ( F e. _V /\ y e. NN0 /\ ( ( IterComp ` F ) ` y ) = ( n e. NN0 |-> ( n + ( C x. y ) ) ) ) -> ( ( IterComp ` F ) ` ( y + 1 ) ) = ( F o. ( n e. NN0 |-> ( n + ( C x. y ) ) ) ) ) with typecode |-
8	4 5 6 7	mp3an2ani	Could not format ( ( ( y e. NN0 /\ C e. NN0 ) /\ ( ( IterComp ` F ) ` y ) = ( n e. NN0 |-> ( n + ( C x. y ) ) ) ) -> ( ( IterComp ` F ) ` ( y + 1 ) ) = ( F o. ( n e. NN0 |-> ( n + ( C x. y ) ) ) ) ) : No typesetting found for |- ( ( ( y e. NN0 /\ C e. NN0 ) /\ ( ( IterComp ` F ) ` y ) = ( n e. NN0 |-> ( n + ( C x. y ) ) ) ) -> ( ( IterComp ` F ) ` ( y + 1 ) ) = ( F o. ( n e. NN0 |-> ( n + ( C x. y ) ) ) ) ) with typecode |-
9		simpr	$$⊢\left(\left(y\in {\mathbb{N}}_0\wedge C\in {\mathbb{N}}_0\right)\wedge n\in {\mathbb{N}}_0\right)\to n\in {\mathbb{N}}_0$$
10		simplr	$$⊢\left(\left(y\in {\mathbb{N}}_0\wedge C\in {\mathbb{N}}_0\right)\wedge n\in {\mathbb{N}}_0\right)\to C\in {\mathbb{N}}_0$$
11	5	adantr	$$⊢\left(\left(y\in {\mathbb{N}}_0\wedge C\in {\mathbb{N}}_0\right)\wedge n\in {\mathbb{N}}_0\right)\to y\in {\mathbb{N}}_0$$
12	10 11	nn0mulcld	$$⊢\left(\left(y\in {\mathbb{N}}_0\wedge C\in {\mathbb{N}}_0\right)\wedge n\in {\mathbb{N}}_0\right)\to Cy\in {\mathbb{N}}_0$$
13	9 12	nn0addcld	$$⊢\left(\left(y\in {\mathbb{N}}_0\wedge C\in {\mathbb{N}}_0\right)\wedge n\in {\mathbb{N}}_0\right)\to n+Cy\in {\mathbb{N}}_0$$
14		eqidd	$$⊢\left(y\in {\mathbb{N}}_0\wedge C\in {\mathbb{N}}_0\right)\to \left(n\in {\mathbb{N}}_0⟼n+Cy\right)=\left(n\in {\mathbb{N}}_0⟼n+Cy\right)$$
15		oveq1	$$⊢n=m\to n+C=m+C$$
16	15	cbvmptv	$$⊢\left(n\in {\mathbb{N}}_0⟼n+C\right)=\left(m\in {\mathbb{N}}_0⟼m+C\right)$$
17	1 16	eqtri	$$⊢F=\left(m\in {\mathbb{N}}_0⟼m+C\right)$$
18	17	a1i	$$⊢\left(y\in {\mathbb{N}}_0\wedge C\in {\mathbb{N}}_0\right)\to F=\left(m\in {\mathbb{N}}_0⟼m+C\right)$$
19		oveq1	$$⊢m=n+Cy\to m+C=n+Cy+C$$
20	13 14 18 19	fmptco	$$⊢\left(y\in {\mathbb{N}}_0\wedge C\in {\mathbb{N}}_0\right)\to F\circ \left(n\in {\mathbb{N}}_0⟼n+Cy\right)=\left(n\in {\mathbb{N}}_0⟼n+Cy+C\right)$$
21	9	nn0cnd	$$⊢\left(\left(y\in {\mathbb{N}}_0\wedge C\in {\mathbb{N}}_0\right)\wedge n\in {\mathbb{N}}_0\right)\to n\in ℂ$$
22	12	nn0cnd	$$⊢\left(\left(y\in {\mathbb{N}}_0\wedge C\in {\mathbb{N}}_0\right)\wedge n\in {\mathbb{N}}_0\right)\to Cy\in ℂ$$
23	10	nn0cnd	$$⊢\left(\left(y\in {\mathbb{N}}_0\wedge C\in {\mathbb{N}}_0\right)\wedge n\in {\mathbb{N}}_0\right)\to C\in ℂ$$
24	21 22 23	addassd	$$⊢\left(\left(y\in {\mathbb{N}}_0\wedge C\in {\mathbb{N}}_0\right)\wedge n\in {\mathbb{N}}_0\right)\to n+Cy+C=n+Cy+C$$
25		nn0cn	$$⊢C\in {\mathbb{N}}_0\to C\in ℂ$$
26	25	mulridd	$$⊢C\in {\mathbb{N}}_0\to C\cdot 1=C$$
27	26	adantl	$$⊢\left(y\in {\mathbb{N}}_0\wedge C\in {\mathbb{N}}_0\right)\to C\cdot 1=C$$
28	27	eqcomd	$$⊢\left(y\in {\mathbb{N}}_0\wedge C\in {\mathbb{N}}_0\right)\to C=C\cdot 1$$
29	28	oveq2d	$$⊢\left(y\in {\mathbb{N}}_0\wedge C\in {\mathbb{N}}_0\right)\to Cy+C=Cy+C\cdot 1$$
30		simpr	$$⊢\left(y\in {\mathbb{N}}_0\wedge C\in {\mathbb{N}}_0\right)\to C\in {\mathbb{N}}_0$$
31	30	nn0cnd	$$⊢\left(y\in {\mathbb{N}}_0\wedge C\in {\mathbb{N}}_0\right)\to C\in ℂ$$
32	5	nn0cnd	$$⊢\left(y\in {\mathbb{N}}_0\wedge C\in {\mathbb{N}}_0\right)\to y\in ℂ$$
33		1cnd	$$⊢\left(y\in {\mathbb{N}}_0\wedge C\in {\mathbb{N}}_0\right)\to 1\in ℂ$$
34	31 32 33	adddid	$$⊢\left(y\in {\mathbb{N}}_0\wedge C\in {\mathbb{N}}_0\right)\to C\left(y+1\right)=Cy+C\cdot 1$$
35	29 34	eqtr4d	$$⊢\left(y\in {\mathbb{N}}_0\wedge C\in {\mathbb{N}}_0\right)\to Cy+C=C\left(y+1\right)$$
36	35	oveq2d	$$⊢\left(y\in {\mathbb{N}}_0\wedge C\in {\mathbb{N}}_0\right)\to n+Cy+C=n+C\left(y+1\right)$$
37	36	adantr	$$⊢\left(\left(y\in {\mathbb{N}}_0\wedge C\in {\mathbb{N}}_0\right)\wedge n\in {\mathbb{N}}_0\right)\to n+Cy+C=n+C\left(y+1\right)$$
38	24 37	eqtrd	$$⊢\left(\left(y\in {\mathbb{N}}_0\wedge C\in {\mathbb{N}}_0\right)\wedge n\in {\mathbb{N}}_0\right)\to n+Cy+C=n+C\left(y+1\right)$$
39	38	mpteq2dva	$$⊢\left(y\in {\mathbb{N}}_0\wedge C\in {\mathbb{N}}_0\right)\to \left(n\in {\mathbb{N}}_0⟼n+Cy+C\right)=\left(n\in {\mathbb{N}}_0⟼n+C\left(y+1\right)\right)$$
40	20 39	eqtrd	$$⊢\left(y\in {\mathbb{N}}_0\wedge C\in {\mathbb{N}}_0\right)\to F\circ \left(n\in {\mathbb{N}}_0⟼n+Cy\right)=\left(n\in {\mathbb{N}}_0⟼n+C\left(y+1\right)\right)$$
41	40	adantr	Could not format ( ( ( y e. NN0 /\ C e. NN0 ) /\ ( ( IterComp ` F ) ` y ) = ( n e. NN0 |-> ( n + ( C x. y ) ) ) ) -> ( F o. ( n e. NN0 |-> ( n + ( C x. y ) ) ) ) = ( n e. NN0 |-> ( n + ( C x. ( y + 1 ) ) ) ) ) : No typesetting found for |- ( ( ( y e. NN0 /\ C e. NN0 ) /\ ( ( IterComp ` F ) ` y ) = ( n e. NN0 |-> ( n + ( C x. y ) ) ) ) -> ( F o. ( n e. NN0 |-> ( n + ( C x. y ) ) ) ) = ( n e. NN0 |-> ( n + ( C x. ( y + 1 ) ) ) ) ) with typecode |-
42	8 41	eqtrd	Could not format ( ( ( y e. NN0 /\ C e. NN0 ) /\ ( ( IterComp ` F ) ` y ) = ( n e. NN0 |-> ( n + ( C x. y ) ) ) ) -> ( ( IterComp ` F ) ` ( y + 1 ) ) = ( n e. NN0 |-> ( n + ( C x. ( y + 1 ) ) ) ) ) : No typesetting found for |- ( ( ( y e. NN0 /\ C e. NN0 ) /\ ( ( IterComp ` F ) ` y ) = ( n e. NN0 |-> ( n + ( C x. y ) ) ) ) -> ( ( IterComp ` F ) ` ( y + 1 ) ) = ( n e. NN0 |-> ( n + ( C x. ( y + 1 ) ) ) ) ) with typecode |-
43	42	ex	Could not format ( ( y e. NN0 /\ C e. NN0 ) -> ( ( ( IterComp ` F ) ` y ) = ( n e. NN0 |-> ( n + ( C x. y ) ) ) -> ( ( IterComp ` F ) ` ( y + 1 ) ) = ( n e. NN0 |-> ( n + ( C x. ( y + 1 ) ) ) ) ) ) : No typesetting found for |- ( ( y e. NN0 /\ C e. NN0 ) -> ( ( ( IterComp ` F ) ` y ) = ( n e. NN0 |-> ( n + ( C x. y ) ) ) -> ( ( IterComp ` F ) ` ( y + 1 ) ) = ( n e. NN0 |-> ( n + ( C x. ( y + 1 ) ) ) ) ) ) with typecode |-