Metamath Proof Explorer


Theorem fourierdlem2

Description: Membership in a partition. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypothesis fourierdlem2.1 P=mp0m|p0=Apm=Bi0..^mpi<pi+1
Assertion fourierdlem2 MQPMQ0MQ0=AQM=Bi0..^MQi<Qi+1

Proof

Step Hyp Ref Expression
1 fourierdlem2.1 P=mp0m|p0=Apm=Bi0..^mpi<pi+1
2 oveq2 m=M0m=0M
3 2 oveq2d m=M0m=0M
4 fveqeq2 m=Mpm=BpM=B
5 4 anbi2d m=Mp0=Apm=Bp0=ApM=B
6 oveq2 m=M0..^m=0..^M
7 6 raleqdv m=Mi0..^mpi<pi+1i0..^Mpi<pi+1
8 5 7 anbi12d m=Mp0=Apm=Bi0..^mpi<pi+1p0=ApM=Bi0..^Mpi<pi+1
9 3 8 rabeqbidv m=Mp0m|p0=Apm=Bi0..^mpi<pi+1=p0M|p0=ApM=Bi0..^Mpi<pi+1
10 ovex 0MV
11 10 rabex p0M|p0=ApM=Bi0..^Mpi<pi+1V
12 9 1 11 fvmpt MPM=p0M|p0=ApM=Bi0..^Mpi<pi+1
13 12 eleq2d MQPMQp0M|p0=ApM=Bi0..^Mpi<pi+1
14 fveq1 p=Qp0=Q0
15 14 eqeq1d p=Qp0=AQ0=A
16 fveq1 p=QpM=QM
17 16 eqeq1d p=QpM=BQM=B
18 15 17 anbi12d p=Qp0=ApM=BQ0=AQM=B
19 fveq1 p=Qpi=Qi
20 fveq1 p=Qpi+1=Qi+1
21 19 20 breq12d p=Qpi<pi+1Qi<Qi+1
22 21 ralbidv p=Qi0..^Mpi<pi+1i0..^MQi<Qi+1
23 18 22 anbi12d p=Qp0=ApM=Bi0..^Mpi<pi+1Q0=AQM=Bi0..^MQi<Qi+1
24 23 elrab Qp0M|p0=ApM=Bi0..^Mpi<pi+1Q0MQ0=AQM=Bi0..^MQi<Qi+1
25 13 24 bitrdi MQPMQ0MQ0=AQM=Bi0..^MQi<Qi+1