Metamath Proof Explorer

Theorem knoppcnlem7

Description: Lemma for knoppcn . (Contributed by Asger C. Ipsen, 4-Apr-2021) (Revised by Asger C. Ipsen, 5-Jul-2021)

Ref Expression
Hypotheses knoppcnlem7.t 
|- T = ( x e. RR |-> ( abs ` ( ( |_ ` ( x + ( 1 / 2 ) ) ) - x ) ) )
knoppcnlem7.f 
|- F = ( y e. RR |-> ( n e. NN0 |-> ( ( C ^ n ) x. ( T ` ( ( ( 2 x. N ) ^ n ) x. y ) ) ) ) )
knoppcnlem7.n 
|- ( ph -> N e. NN )
knoppcnlem7.1 
|- ( ph -> C e. RR )
knoppcnlem7.2 
|- ( ph -> M e. NN0 )
Assertion knoppcnlem7 
|- ( ph -> ( seq 0 ( oF + , ( m e. NN0 |-> ( z e. RR |-> ( ( F ` z ) ` m ) ) ) ) ` M ) = ( w e. RR |-> ( seq 0 ( + , ( F ` w ) ) ` M ) ) )

Proof

Step Hyp Ref Expression
1 knoppcnlem7.t 
 |-  T = ( x e. RR |-> ( abs ` ( ( |_ ` ( x + ( 1 / 2 ) ) ) - x ) ) )
2 knoppcnlem7.f 
 |-  F = ( y e. RR |-> ( n e. NN0 |-> ( ( C ^ n ) x. ( T ` ( ( ( 2 x. N ) ^ n ) x. y ) ) ) ) )
3 knoppcnlem7.n 
 |-  ( ph -> N e. NN )
4 knoppcnlem7.1 
 |-  ( ph -> C e. RR )
5 knoppcnlem7.2 
 |-  ( ph -> M e. NN0 )
6 reex 
 |-  RR e. _V
7 6 a1i 
 |-  ( ph -> RR e. _V )
8 elnn0uz 
 |-  ( M e. NN0 <-> M e. ( ZZ>= ` 0 ) )
9 5 8 sylib 
 |-  ( ph -> M e. ( ZZ>= ` 0 ) )
10 eqid 
 |-  ( m e. NN0 |-> ( z e. RR |-> ( ( F ` z ) ` m ) ) ) = ( m e. NN0 |-> ( z e. RR |-> ( ( F ` z ) ` m ) ) )
11 10 a1i 
 |-  ( ( ph /\ k e. ( 0 ... M ) ) -> ( m e. NN0 |-> ( z e. RR |-> ( ( F ` z ) ` m ) ) ) = ( m e. NN0 |-> ( z e. RR |-> ( ( F ` z ) ` m ) ) ) )
12 fveq2 
 |-  ( z = w -> ( F ` z ) = ( F ` w ) )
13 12 fveq1d 
 |-  ( z = w -> ( ( F ` z ) ` m ) = ( ( F ` w ) ` m ) )
14 13 cbvmptv 
 |-  ( z e. RR |-> ( ( F ` z ) ` m ) ) = ( w e. RR |-> ( ( F ` w ) ` m ) )
15 14 a1i 
 |-  ( ( ( ph /\ k e. ( 0 ... M ) ) /\ m = k ) -> ( z e. RR |-> ( ( F ` z ) ` m ) ) = ( w e. RR |-> ( ( F ` w ) ` m ) ) )
16 fveq2 
 |-  ( m = k -> ( ( F ` w ) ` m ) = ( ( F ` w ) ` k ) )
17 16 mpteq2dv 
 |-  ( m = k -> ( w e. RR |-> ( ( F ` w ) ` m ) ) = ( w e. RR |-> ( ( F ` w ) ` k ) ) )
18 17 adantl 
 |-  ( ( ( ph /\ k e. ( 0 ... M ) ) /\ m = k ) -> ( w e. RR |-> ( ( F ` w ) ` m ) ) = ( w e. RR |-> ( ( F ` w ) ` k ) ) )
19 15 18 eqtrd 
 |-  ( ( ( ph /\ k e. ( 0 ... M ) ) /\ m = k ) -> ( z e. RR |-> ( ( F ` z ) ` m ) ) = ( w e. RR |-> ( ( F ` w ) ` k ) ) )
20 elfznn0 
 |-  ( k e. ( 0 ... M ) -> k e. NN0 )
21 20 adantl 
 |-  ( ( ph /\ k e. ( 0 ... M ) ) -> k e. NN0 )
22 6 mptex 
 |-  ( w e. RR |-> ( ( F ` w ) ` k ) ) e. _V
23 22 a1i 
 |-  ( ( ph /\ k e. ( 0 ... M ) ) -> ( w e. RR |-> ( ( F ` w ) ` k ) ) e. _V )
24 11 19 21 23 fvmptd 
 |-  ( ( ph /\ k e. ( 0 ... M ) ) -> ( ( m e. NN0 |-> ( z e. RR |-> ( ( F ` z ) ` m ) ) ) ` k ) = ( w e. RR |-> ( ( F ` w ) ` k ) ) )
25 7 9 24 seqof 
 |-  ( ph -> ( seq 0 ( oF + , ( m e. NN0 |-> ( z e. RR |-> ( ( F ` z ) ` m ) ) ) ) ` M ) = ( w e. RR |-> ( seq 0 ( + , ( F ` w ) ) ` M ) ) )