Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  fourierdlem2 Structured version   Visualization version   Unicode version

Theorem fourierdlem2 38072
Description: Membership in a partition. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypothesis
Ref Expression
fourierdlem2.1  |-  P  =  ( m  e.  NN  |->  { p  e.  ( RR  ^m  ( 0 ... m ) )  |  ( ( ( p `
 0 )  =  A  /\  ( p `
 m )  =  B )  /\  A. i  e.  ( 0..^ m ) ( p `
 i )  < 
( p `  (
i  +  1 ) ) ) } )
Assertion
Ref Expression
fourierdlem2  |-  ( M  e.  NN  ->  ( Q  e.  ( P `  M )  <->  ( Q  e.  ( RR  ^m  (
0 ... M ) )  /\  ( ( ( Q `  0 )  =  A  /\  ( Q `  M )  =  B )  /\  A. i  e.  ( 0..^ M ) ( Q `
 i )  < 
( Q `  (
i  +  1 ) ) ) ) ) )
Distinct variable groups:    A, m, p    B, m, p    i, M, m, p    Q, i, p
Allowed substitution hints:    A( i)    B( i)    P( i, m, p)    Q( m)

Proof of Theorem fourierdlem2
StepHypRef Expression
1 oveq2 6328 . . . . . 6  |-  ( m  =  M  ->  (
0 ... m )  =  ( 0 ... M
) )
21oveq2d 6336 . . . . 5  |-  ( m  =  M  ->  ( RR  ^m  ( 0 ... m ) )  =  ( RR  ^m  (
0 ... M ) ) )
3 fveq2 5892 . . . . . . . 8  |-  ( m  =  M  ->  (
p `  m )  =  ( p `  M ) )
43eqeq1d 2464 . . . . . . 7  |-  ( m  =  M  ->  (
( p `  m
)  =  B  <->  ( p `  M )  =  B ) )
54anbi2d 715 . . . . . 6  |-  ( m  =  M  ->  (
( ( p ` 
0 )  =  A  /\  ( p `  m )  =  B )  <->  ( ( p `
 0 )  =  A  /\  ( p `
 M )  =  B ) ) )
6 oveq2 6328 . . . . . . 7  |-  ( m  =  M  ->  (
0..^ m )  =  ( 0..^ M ) )
76raleqdv 3005 . . . . . 6  |-  ( m  =  M  ->  ( A. i  e.  (
0..^ m ) ( p `  i )  <  ( p `  ( i  +  1 ) )  <->  A. i  e.  ( 0..^ M ) ( p `  i
)  <  ( p `  ( i  +  1 ) ) ) )
85, 7anbi12d 722 . . . . 5  |-  ( m  =  M  ->  (
( ( ( p `
 0 )  =  A  /\  ( p `
 m )  =  B )  /\  A. i  e.  ( 0..^ m ) ( p `
 i )  < 
( p `  (
i  +  1 ) ) )  <->  ( (
( p `  0
)  =  A  /\  ( p `  M
)  =  B )  /\  A. i  e.  ( 0..^ M ) ( p `  i
)  <  ( p `  ( i  +  1 ) ) ) ) )
92, 8rabeqbidv 3052 . . . 4  |-  ( m  =  M  ->  { p  e.  ( RR  ^m  (
0 ... m ) )  |  ( ( ( p `  0 )  =  A  /\  (
p `  m )  =  B )  /\  A. i  e.  ( 0..^ m ) ( p `
 i )  < 
( p `  (
i  +  1 ) ) ) }  =  { p  e.  ( RR  ^m  ( 0 ... M ) )  |  ( ( ( p `
 0 )  =  A  /\  ( p `
 M )  =  B )  /\  A. i  e.  ( 0..^ M ) ( p `
 i )  < 
( p `  (
i  +  1 ) ) ) } )
10 fourierdlem2.1 . . . 4  |-  P  =  ( m  e.  NN  |->  { p  e.  ( RR  ^m  ( 0 ... m ) )  |  ( ( ( p `
 0 )  =  A  /\  ( p `
 m )  =  B )  /\  A. i  e.  ( 0..^ m ) ( p `
 i )  < 
( p `  (
i  +  1 ) ) ) } )
11 ovex 6348 . . . . 5  |-  ( RR 
^m  ( 0 ... M ) )  e. 
_V
1211rabex 4571 . . . 4  |-  { p  e.  ( RR  ^m  (
0 ... M ) )  |  ( ( ( p `  0 )  =  A  /\  (
p `  M )  =  B )  /\  A. i  e.  ( 0..^ M ) ( p `
 i )  < 
( p `  (
i  +  1 ) ) ) }  e.  _V
139, 10, 12fvmpt 5976 . . 3  |-  ( M  e.  NN  ->  ( P `  M )  =  { p  e.  ( RR  ^m  ( 0 ... M ) )  |  ( ( ( p `  0 )  =  A  /\  (
p `  M )  =  B )  /\  A. i  e.  ( 0..^ M ) ( p `
 i )  < 
( p `  (
i  +  1 ) ) ) } )
1413eleq2d 2525 . 2  |-  ( M  e.  NN  ->  ( Q  e.  ( P `  M )  <->  Q  e.  { p  e.  ( RR 
^m  ( 0 ... M ) )  |  ( ( ( p `
 0 )  =  A  /\  ( p `
 M )  =  B )  /\  A. i  e.  ( 0..^ M ) ( p `
 i )  < 
( p `  (
i  +  1 ) ) ) } ) )
15 fveq1 5891 . . . . . 6  |-  ( p  =  Q  ->  (
p `  0 )  =  ( Q ` 
0 ) )
1615eqeq1d 2464 . . . . 5  |-  ( p  =  Q  ->  (
( p `  0
)  =  A  <->  ( Q `  0 )  =  A ) )
17 fveq1 5891 . . . . . 6  |-  ( p  =  Q  ->  (
p `  M )  =  ( Q `  M ) )
1817eqeq1d 2464 . . . . 5  |-  ( p  =  Q  ->  (
( p `  M
)  =  B  <->  ( Q `  M )  =  B ) )
1916, 18anbi12d 722 . . . 4  |-  ( p  =  Q  ->  (
( ( p ` 
0 )  =  A  /\  ( p `  M )  =  B )  <->  ( ( Q `
 0 )  =  A  /\  ( Q `
 M )  =  B ) ) )
20 fveq1 5891 . . . . . 6  |-  ( p  =  Q  ->  (
p `  i )  =  ( Q `  i ) )
21 fveq1 5891 . . . . . 6  |-  ( p  =  Q  ->  (
p `  ( i  +  1 ) )  =  ( Q `  ( i  +  1 ) ) )
2220, 21breq12d 4431 . . . . 5  |-  ( p  =  Q  ->  (
( p `  i
)  <  ( p `  ( i  +  1 ) )  <->  ( Q `  i )  <  ( Q `  ( i  +  1 ) ) ) )
2322ralbidv 2839 . . . 4  |-  ( p  =  Q  ->  ( A. i  e.  (
0..^ M ) ( p `  i )  <  ( p `  ( i  +  1 ) )  <->  A. i  e.  ( 0..^ M ) ( Q `  i
)  <  ( Q `  ( i  +  1 ) ) ) )
2419, 23anbi12d 722 . . 3  |-  ( p  =  Q  ->  (
( ( ( p `
 0 )  =  A  /\  ( p `
 M )  =  B )  /\  A. i  e.  ( 0..^ M ) ( p `
 i )  < 
( p `  (
i  +  1 ) ) )  <->  ( (
( Q `  0
)  =  A  /\  ( Q `  M )  =  B )  /\  A. i  e.  ( 0..^ M ) ( Q `
 i )  < 
( Q `  (
i  +  1 ) ) ) ) )
2524elrab 3208 . 2  |-  ( Q  e.  { p  e.  ( RR  ^m  (
0 ... M ) )  |  ( ( ( p `  0 )  =  A  /\  (
p `  M )  =  B )  /\  A. i  e.  ( 0..^ M ) ( p `
 i )  < 
( p `  (
i  +  1 ) ) ) }  <->  ( Q  e.  ( RR  ^m  (
0 ... M ) )  /\  ( ( ( Q `  0 )  =  A  /\  ( Q `  M )  =  B )  /\  A. i  e.  ( 0..^ M ) ( Q `
 i )  < 
( Q `  (
i  +  1 ) ) ) ) )
2614, 25syl6bb 269 1  |-  ( M  e.  NN  ->  ( Q  e.  ( P `  M )  <->  ( Q  e.  ( RR  ^m  (
0 ... M ) )  /\  ( ( ( Q `  0 )  =  A  /\  ( Q `  M )  =  B )  /\  A. i  e.  ( 0..^ M ) ( Q `
 i )  < 
( Q `  (
i  +  1 ) ) ) ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189    /\ wa 375    = wceq 1455    e. wcel 1898   A.wral 2749   {crab 2753   class class class wbr 4418    |-> cmpt 4477   ` cfv 5605  (class class class)co 6320    ^m cmap 7503   RRcr 9569   0cc0 9570   1c1 9571    + caddc 9573    < clt 9706   NNcn 10642   ...cfz 11819  ..^cfzo 11952
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-sep 4541  ax-nul 4550  ax-pr 4656
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-ral 2754  df-rex 2755  df-rab 2758  df-v 3059  df-sbc 3280  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744  df-if 3894  df-sn 3981  df-pr 3983  df-op 3987  df-uni 4213  df-br 4419  df-opab 4478  df-mpt 4479  df-id 4771  df-xp 4862  df-rel 4863  df-cnv 4864  df-co 4865  df-dm 4866  df-iota 5569  df-fun 5607  df-fv 5613  df-ov 6323
This theorem is referenced by:  fourierdlem11  38081  fourierdlem12  38082  fourierdlem13  38083  fourierdlem14  38084  fourierdlem15  38085  fourierdlem34  38105  fourierdlem37  38108  fourierdlem41  38112  fourierdlem48  38119  fourierdlem49  38120  fourierdlem50  38121  fourierdlem54  38125  fourierdlem63  38134  fourierdlem64  38135  fourierdlem65  38136  fourierdlem69  38140  fourierdlem70  38141  fourierdlem72  38143  fourierdlem74  38145  fourierdlem75  38146  fourierdlem76  38147  fourierdlem79  38150  fourierdlem81  38152  fourierdlem85  38156  fourierdlem88  38159  fourierdlem89  38160  fourierdlem90  38161  fourierdlem91  38162  fourierdlem92  38163  fourierdlem93  38164  fourierdlem94  38165  fourierdlem97  38168  fourierdlem102  38173  fourierdlem103  38174  fourierdlem104  38175  fourierdlem111  38182  fourierdlem113  38184  fourierdlem114  38185
  Copyright terms: Public domain W3C validator