Metamath Proof Explorer

Theorem fourierdlem13

Description: Value of V in terms of value of Q . (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem13.a 
|- ( ph -> A e. RR )
fourierdlem13.b 
|- ( ph -> B e. RR )
fourierdlem13.x 
|- ( ph -> X e. RR )
fourierdlem13.p 
|- P = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = ( A + X ) /\ ( p ` m ) = ( B + X ) ) /\ A. i e. ( 0 ..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )
fourierdlem13.m 
|- ( ph -> M e. NN )
fourierdlem13.v 
|- ( ph -> V e. ( P ` M ) )
fourierdlem13.i 
|- ( ph -> I e. ( 0 ... M ) )
fourierdlem13.q 
|- Q = ( i e. ( 0 ... M ) |-> ( ( V ` i ) - X ) )
Assertion fourierdlem13 
|- ( ph -> ( ( Q ` I ) = ( ( V ` I ) - X ) /\ ( V ` I ) = ( X + ( Q ` I ) ) ) )

Proof

Step Hyp Ref Expression
1 fourierdlem13.a 
 |-  ( ph -> A e. RR )
2 fourierdlem13.b 
 |-  ( ph -> B e. RR )
3 fourierdlem13.x 
 |-  ( ph -> X e. RR )
4 fourierdlem13.p 
 |-  P = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = ( A + X ) /\ ( p ` m ) = ( B + X ) ) /\ A. i e. ( 0 ..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )
5 fourierdlem13.m 
 |-  ( ph -> M e. NN )
6 fourierdlem13.v 
 |-  ( ph -> V e. ( P ` M ) )
7 fourierdlem13.i 
 |-  ( ph -> I e. ( 0 ... M ) )
8 fourierdlem13.q 
 |-  Q = ( i e. ( 0 ... M ) |-> ( ( V ` i ) - X ) )
9 8 a1i 
 |-  ( ph -> Q = ( i e. ( 0 ... M ) |-> ( ( V ` i ) - X ) ) )
10 simpr 
 |-  ( ( ph /\ i = I ) -> i = I )
11 10 fveq2d 
 |-  ( ( ph /\ i = I ) -> ( V ` i ) = ( V ` I ) )
12 11 oveq1d 
 |-  ( ( ph /\ i = I ) -> ( ( V ` i ) - X ) = ( ( V ` I ) - X ) )
13 4 fourierdlem2 
 |-  ( M e. NN -> ( V e. ( P ` M ) <-> ( V e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( V ` 0 ) = ( A + X ) /\ ( V ` M ) = ( B + X ) ) /\ A. i e. ( 0 ..^ M ) ( V ` i ) < ( V ` ( i + 1 ) ) ) ) ) )
14 5 13 syl 
 |-  ( ph -> ( V e. ( P ` M ) <-> ( V e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( V ` 0 ) = ( A + X ) /\ ( V ` M ) = ( B + X ) ) /\ A. i e. ( 0 ..^ M ) ( V ` i ) < ( V ` ( i + 1 ) ) ) ) ) )
15 6 14 mpbid 
 |-  ( ph -> ( V e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( V ` 0 ) = ( A + X ) /\ ( V ` M ) = ( B + X ) ) /\ A. i e. ( 0 ..^ M ) ( V ` i ) < ( V ` ( i + 1 ) ) ) ) )
16 15 simpld 
 |-  ( ph -> V e. ( RR ^m ( 0 ... M ) ) )
17 elmapi 
 |-  ( V e. ( RR ^m ( 0 ... M ) ) -> V : ( 0 ... M ) --> RR )
18 16 17 syl 
 |-  ( ph -> V : ( 0 ... M ) --> RR )
19 18 7 ffvelrnd 
 |-  ( ph -> ( V ` I ) e. RR )
20 19 3 resubcld 
 |-  ( ph -> ( ( V ` I ) - X ) e. RR )
21 9 12 7 20 fvmptd 
 |-  ( ph -> ( Q ` I ) = ( ( V ` I ) - X ) )
22 21 oveq2d 
 |-  ( ph -> ( X + ( Q ` I ) ) = ( X + ( ( V ` I ) - X ) ) )
23 3 recnd 
 |-  ( ph -> X e. CC )
24 19 recnd 
 |-  ( ph -> ( V ` I ) e. CC )
25 23 24 pncan3d 
 |-  ( ph -> ( X + ( ( V ` I ) - X ) ) = ( V ` I ) )
26 22 25 eqtr2d 
 |-  ( ph -> ( V ` I ) = ( X + ( Q ` I ) ) )
27 21 26 jca 
 |-  ( ph -> ( ( Q ` I ) = ( ( V ` I ) - X ) /\ ( V ` I ) = ( X + ( Q ` I ) ) ) )