Metamath Proof Explorer

Theorem itcovalpclem1

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

Ref Expression
Hypothesis itcovalpc.f 
|- F = ( n e. NN0 |-> ( n + C ) )
Assertion itcovalpclem1 
|- ( C e. NN0 -> ( ( IterComp ` F ) ` 0 ) = ( n e. NN0 |-> ( n + ( C x. 0 ) ) ) )

Proof

Step Hyp Ref Expression
1 itcovalpc.f 
 |-  F = ( n e. NN0 |-> ( n + C ) )
2 nn0ex 
 |-  NN0 e. _V
3 ovexd 
 |-  ( n e. NN0 -> ( n + C ) e. _V )
4 3 rgen 
 |-  A. n e. NN0 ( n + C ) e. _V
5 1 itcoval0mpt 
 |-  ( ( NN0 e. _V /\ A. n e. NN0 ( n + C ) e. _V ) -> ( ( IterComp ` F ) ` 0 ) = ( n e. NN0 |-> n ) )
6 2 4 5 mp2an 
 |-  ( ( IterComp ` F ) ` 0 ) = ( n e. NN0 |-> n )
7 nn0cn 
 |-  ( C e. NN0 -> C e. CC )
8 7 mul01d 
 |-  ( C e. NN0 -> ( C x. 0 ) = 0 )
9 8 adantr 
 |-  ( ( C e. NN0 /\ n e. NN0 ) -> ( C x. 0 ) = 0 )
10 9 oveq2d 
 |-  ( ( C e. NN0 /\ n e. NN0 ) -> ( n + ( C x. 0 ) ) = ( n + 0 ) )
11 nn0cn 
 |-  ( n e. NN0 -> n e. CC )
12 11 addid1d 
 |-  ( n e. NN0 -> ( n + 0 ) = n )
13 12 adantl 
 |-  ( ( C e. NN0 /\ n e. NN0 ) -> ( n + 0 ) = n )
14 10 13 eqtr2d 
 |-  ( ( C e. NN0 /\ n e. NN0 ) -> n = ( n + ( C x. 0 ) ) )
15 14 mpteq2dva 
 |-  ( C e. NN0 -> ( n e. NN0 |-> n ) = ( n e. NN0 |-> ( n + ( C x. 0 ) ) ) )
16 6 15 syl5eq 
 |-  ( C e. NN0 -> ( ( IterComp ` F ) ` 0 ) = ( n e. NN0 |-> ( n + ( C x. 0 ) ) ) )