Metamath Proof Explorer


Theorem itcovalpclem2

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

Ref Expression
Hypothesis itcovalpc.f
|- F = ( n e. NN0 |-> ( n + C ) )
Assertion itcovalpclem2
|- ( ( 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 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 itcovalpc.f
 |-  F = ( n e. NN0 |-> ( n + C ) )
2 nn0ex
 |-  NN0 e. _V
3 2 mptex
 |-  ( n e. NN0 |-> ( n + C ) ) e. _V
4 1 3 eqeltri
 |-  F e. _V
5 simpl
 |-  ( ( y e. NN0 /\ C e. NN0 ) -> y e. NN0 )
6 simpr
 |-  ( ( ( 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 ) ) ) )
7 itcovalsucov
 |-  ( ( 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 ) ) ) ) )
8 4 5 6 7 mp3an2ani
 |-  ( ( ( 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 ) ) ) ) )
9 simpr
 |-  ( ( ( y e. NN0 /\ C e. NN0 ) /\ n e. NN0 ) -> n e. NN0 )
10 simplr
 |-  ( ( ( y e. NN0 /\ C e. NN0 ) /\ n e. NN0 ) -> C e. NN0 )
11 5 adantr
 |-  ( ( ( y e. NN0 /\ C e. NN0 ) /\ n e. NN0 ) -> y e. NN0 )
12 10 11 nn0mulcld
 |-  ( ( ( y e. NN0 /\ C e. NN0 ) /\ n e. NN0 ) -> ( C x. y ) e. NN0 )
13 9 12 nn0addcld
 |-  ( ( ( y e. NN0 /\ C e. NN0 ) /\ n e. NN0 ) -> ( n + ( C x. y ) ) e. NN0 )
14 eqidd
 |-  ( ( y e. NN0 /\ C e. NN0 ) -> ( n e. NN0 |-> ( n + ( C x. y ) ) ) = ( n e. NN0 |-> ( n + ( C x. y ) ) ) )
15 oveq1
 |-  ( n = m -> ( n + C ) = ( m + C ) )
16 15 cbvmptv
 |-  ( n e. NN0 |-> ( n + C ) ) = ( m e. NN0 |-> ( m + C ) )
17 1 16 eqtri
 |-  F = ( m e. NN0 |-> ( m + C ) )
18 17 a1i
 |-  ( ( y e. NN0 /\ C e. NN0 ) -> F = ( m e. NN0 |-> ( m + C ) ) )
19 oveq1
 |-  ( m = ( n + ( C x. y ) ) -> ( m + C ) = ( ( n + ( C x. y ) ) + C ) )
20 13 14 18 19 fmptco
 |-  ( ( y e. NN0 /\ C e. NN0 ) -> ( F o. ( n e. NN0 |-> ( n + ( C x. y ) ) ) ) = ( n e. NN0 |-> ( ( n + ( C x. y ) ) + C ) ) )
21 9 nn0cnd
 |-  ( ( ( y e. NN0 /\ C e. NN0 ) /\ n e. NN0 ) -> n e. CC )
22 12 nn0cnd
 |-  ( ( ( y e. NN0 /\ C e. NN0 ) /\ n e. NN0 ) -> ( C x. y ) e. CC )
23 10 nn0cnd
 |-  ( ( ( y e. NN0 /\ C e. NN0 ) /\ n e. NN0 ) -> C e. CC )
24 21 22 23 addassd
 |-  ( ( ( y e. NN0 /\ C e. NN0 ) /\ n e. NN0 ) -> ( ( n + ( C x. y ) ) + C ) = ( n + ( ( C x. y ) + C ) ) )
25 nn0cn
 |-  ( C e. NN0 -> C e. CC )
26 25 mulid1d
 |-  ( C e. NN0 -> ( C x. 1 ) = C )
27 26 adantl
 |-  ( ( y e. NN0 /\ C e. NN0 ) -> ( C x. 1 ) = C )
28 27 eqcomd
 |-  ( ( y e. NN0 /\ C e. NN0 ) -> C = ( C x. 1 ) )
29 28 oveq2d
 |-  ( ( y e. NN0 /\ C e. NN0 ) -> ( ( C x. y ) + C ) = ( ( C x. y ) + ( C x. 1 ) ) )
30 simpr
 |-  ( ( y e. NN0 /\ C e. NN0 ) -> C e. NN0 )
31 30 nn0cnd
 |-  ( ( y e. NN0 /\ C e. NN0 ) -> C e. CC )
32 5 nn0cnd
 |-  ( ( y e. NN0 /\ C e. NN0 ) -> y e. CC )
33 1cnd
 |-  ( ( y e. NN0 /\ C e. NN0 ) -> 1 e. CC )
34 31 32 33 adddid
 |-  ( ( y e. NN0 /\ C e. NN0 ) -> ( C x. ( y + 1 ) ) = ( ( C x. y ) + ( C x. 1 ) ) )
35 29 34 eqtr4d
 |-  ( ( y e. NN0 /\ C e. NN0 ) -> ( ( C x. y ) + C ) = ( C x. ( y + 1 ) ) )
36 35 oveq2d
 |-  ( ( y e. NN0 /\ C e. NN0 ) -> ( n + ( ( C x. y ) + C ) ) = ( n + ( C x. ( y + 1 ) ) ) )
37 36 adantr
 |-  ( ( ( y e. NN0 /\ C e. NN0 ) /\ n e. NN0 ) -> ( n + ( ( C x. y ) + C ) ) = ( n + ( C x. ( y + 1 ) ) ) )
38 24 37 eqtrd
 |-  ( ( ( y e. NN0 /\ C e. NN0 ) /\ n e. NN0 ) -> ( ( n + ( C x. y ) ) + C ) = ( n + ( C x. ( y + 1 ) ) ) )
39 38 mpteq2dva
 |-  ( ( y e. NN0 /\ C e. NN0 ) -> ( n e. NN0 |-> ( ( n + ( C x. y ) ) + C ) ) = ( n e. NN0 |-> ( n + ( C x. ( y + 1 ) ) ) ) )
40 20 39 eqtrd
 |-  ( ( y e. NN0 /\ C e. NN0 ) -> ( F o. ( n e. NN0 |-> ( n + ( C x. y ) ) ) ) = ( n e. NN0 |-> ( n + ( C x. ( y + 1 ) ) ) ) )
41 40 adantr
 |-  ( ( ( 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 ) ) ) ) )
42 8 41 eqtrd
 |-  ( ( ( 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 ) ) ) ) )
43 42 ex
 |-  ( ( 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 ) ) ) ) ) )