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 ) ) ) ) ) )