Metamath Proof Explorer

Theorem knoppcnlem1

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

Ref Expression
Hypotheses knoppcnlem1.f 
|- F = ( y e. RR |-> ( n e. NN0 |-> ( ( C ^ n ) x. ( T ` ( ( ( 2 x. N ) ^ n ) x. y ) ) ) ) )
knoppcnlem1.2 
|- ( ph -> A e. RR )
knoppcnlem1.3 
|- ( ph -> M e. NN0 )
Assertion knoppcnlem1 
|- ( ph -> ( ( F ` A ) ` M ) = ( ( C ^ M ) x. ( T ` ( ( ( 2 x. N ) ^ M ) x. A ) ) ) )

Proof

Step Hyp Ref Expression
1 knoppcnlem1.f 
 |-  F = ( y e. RR |-> ( n e. NN0 |-> ( ( C ^ n ) x. ( T ` ( ( ( 2 x. N ) ^ n ) x. y ) ) ) ) )
2 knoppcnlem1.2 
 |-  ( ph -> A e. RR )
3 knoppcnlem1.3 
 |-  ( ph -> M e. NN0 )
4 oveq2 
 |-  ( y = A -> ( ( ( 2 x. N ) ^ n ) x. y ) = ( ( ( 2 x. N ) ^ n ) x. A ) )
5 4 fveq2d 
 |-  ( y = A -> ( T ` ( ( ( 2 x. N ) ^ n ) x. y ) ) = ( T ` ( ( ( 2 x. N ) ^ n ) x. A ) ) )
6 5 oveq2d 
 |-  ( y = A -> ( ( C ^ n ) x. ( T ` ( ( ( 2 x. N ) ^ n ) x. y ) ) ) = ( ( C ^ n ) x. ( T ` ( ( ( 2 x. N ) ^ n ) x. A ) ) ) )
7 6 mpteq2dv 
 |-  ( y = A -> ( n e. NN0 |-> ( ( C ^ n ) x. ( T ` ( ( ( 2 x. N ) ^ n ) x. y ) ) ) ) = ( n e. NN0 |-> ( ( C ^ n ) x. ( T ` ( ( ( 2 x. N ) ^ n ) x. A ) ) ) ) )
8 nn0ex 
 |-  NN0 e. _V
9 8 mptex 
 |-  ( n e. NN0 |-> ( ( C ^ n ) x. ( T ` ( ( ( 2 x. N ) ^ n ) x. A ) ) ) ) e. _V
10 9 a1i 
 |-  ( ph -> ( n e. NN0 |-> ( ( C ^ n ) x. ( T ` ( ( ( 2 x. N ) ^ n ) x. A ) ) ) ) e. _V )
11 1 7 2 10 fvmptd3 
 |-  ( ph -> ( F ` A ) = ( n e. NN0 |-> ( ( C ^ n ) x. ( T ` ( ( ( 2 x. N ) ^ n ) x. A ) ) ) ) )
12 oveq2 
 |-  ( n = M -> ( C ^ n ) = ( C ^ M ) )
13 oveq2 
 |-  ( n = M -> ( ( 2 x. N ) ^ n ) = ( ( 2 x. N ) ^ M ) )
14 13 fvoveq1d 
 |-  ( n = M -> ( T ` ( ( ( 2 x. N ) ^ n ) x. A ) ) = ( T ` ( ( ( 2 x. N ) ^ M ) x. A ) ) )
15 12 14 oveq12d 
 |-  ( n = M -> ( ( C ^ n ) x. ( T ` ( ( ( 2 x. N ) ^ n ) x. A ) ) ) = ( ( C ^ M ) x. ( T ` ( ( ( 2 x. N ) ^ M ) x. A ) ) ) )
16 15 adantl 
 |-  ( ( ph /\ n = M ) -> ( ( C ^ n ) x. ( T ` ( ( ( 2 x. N ) ^ n ) x. A ) ) ) = ( ( C ^ M ) x. ( T ` ( ( ( 2 x. N ) ^ M ) x. A ) ) ) )
17 ovexd 
 |-  ( ph -> ( ( C ^ M ) x. ( T ` ( ( ( 2 x. N ) ^ M ) x. A ) ) ) e. _V )
18 11 16 3 17 fvmptd 
 |-  ( ph -> ( ( F ` A ) ` M ) = ( ( C ^ M ) x. ( T ` ( ( ( 2 x. N ) ^ M ) x. A ) ) ) )