Metamath Proof Explorer

Theorem reprdifc

Description: Express the representations as a sum of integers in a difference of sets using conditions on each of the indices. (Contributed by Thierry Arnoux, 27-Dec-2021)

Ref Expression
Hypotheses reprdifc.c 
|- C = { c e. ( A ( repr ` S ) M ) | -. ( c ` x ) e. B }
reprdifc.a 
|- ( ph -> A C_ NN )
reprdifc.b 
|- ( ph -> B C_ NN )
reprdifc.m 
|- ( ph -> M e. NN0 )
reprdifc.s 
|- ( ph -> S e. NN0 )
Assertion reprdifc 
|- ( ph -> ( ( A ( repr ` S ) M ) \ ( B ( repr ` S ) M ) ) = U_ x e. ( 0 ..^ S ) C )

Proof

Step Hyp Ref Expression
1 reprdifc.c 
 |-  C = { c e. ( A ( repr ` S ) M ) | -. ( c ` x ) e. B }
2 reprdifc.a 
 |-  ( ph -> A C_ NN )
3 reprdifc.b 
 |-  ( ph -> B C_ NN )
4 reprdifc.m 
 |-  ( ph -> M e. NN0 )
5 reprdifc.s 
 |-  ( ph -> S e. NN0 )
6 nfv 
 |-  F/ d ph
7 nfrab1 
 |-  F/_ d { d e. ( ( A ^m ( 0 ..^ S ) ) \ ( B ^m ( 0 ..^ S ) ) ) | sum_ a e. ( 0 ..^ S ) ( d ` a ) = M }
8 nfcv 
 |-  F/_ d U_ x e. ( 0 ..^ S ) { c e. ( A ( repr ` S ) M ) | -. ( c ` x ) e. B }
9 4 nn0zd 
 |-  ( ph -> M e. ZZ )
10 2 9 5 reprval 
 |-  ( ph -> ( A ( repr ` S ) M ) = { d e. ( A ^m ( 0 ..^ S ) ) | sum_ a e. ( 0 ..^ S ) ( d ` a ) = M } )
11 10 eleq2d 
 |-  ( ph -> ( d e. ( A ( repr ` S ) M ) <-> d e. { d e. ( A ^m ( 0 ..^ S ) ) | sum_ a e. ( 0 ..^ S ) ( d ` a ) = M } ) )
12 rabid 
 |-  ( d e. { d e. ( A ^m ( 0 ..^ S ) ) | sum_ a e. ( 0 ..^ S ) ( d ` a ) = M } <-> ( d e. ( A ^m ( 0 ..^ S ) ) /\ sum_ a e. ( 0 ..^ S ) ( d ` a ) = M ) )
13 11 12 bitrdi 
 |-  ( ph -> ( d e. ( A ( repr ` S ) M ) <-> ( d e. ( A ^m ( 0 ..^ S ) ) /\ sum_ a e. ( 0 ..^ S ) ( d ` a ) = M ) ) )
14 13 anbi1d 
 |-  ( ph -> ( ( d e. ( A ( repr ` S ) M ) /\ -. d e. ( B ^m ( 0 ..^ S ) ) ) <-> ( ( d e. ( A ^m ( 0 ..^ S ) ) /\ sum_ a e. ( 0 ..^ S ) ( d ` a ) = M ) /\ -. d e. ( B ^m ( 0 ..^ S ) ) ) ) )
15 eldif 
 |-  ( d e. ( ( A ^m ( 0 ..^ S ) ) \ ( B ^m ( 0 ..^ S ) ) ) <-> ( d e. ( A ^m ( 0 ..^ S ) ) /\ -. d e. ( B ^m ( 0 ..^ S ) ) ) )
16 15 anbi1i 
 |-  ( ( d e. ( ( A ^m ( 0 ..^ S ) ) \ ( B ^m ( 0 ..^ S ) ) ) /\ sum_ a e. ( 0 ..^ S ) ( d ` a ) = M ) <-> ( ( d e. ( A ^m ( 0 ..^ S ) ) /\ -. d e. ( B ^m ( 0 ..^ S ) ) ) /\ sum_ a e. ( 0 ..^ S ) ( d ` a ) = M ) )
17 an32 
 |-  ( ( ( d e. ( A ^m ( 0 ..^ S ) ) /\ -. d e. ( B ^m ( 0 ..^ S ) ) ) /\ sum_ a e. ( 0 ..^ S ) ( d ` a ) = M ) <-> ( ( d e. ( A ^m ( 0 ..^ S ) ) /\ sum_ a e. ( 0 ..^ S ) ( d ` a ) = M ) /\ -. d e. ( B ^m ( 0 ..^ S ) ) ) )
18 16 17 bitri 
 |-  ( ( d e. ( ( A ^m ( 0 ..^ S ) ) \ ( B ^m ( 0 ..^ S ) ) ) /\ sum_ a e. ( 0 ..^ S ) ( d ` a ) = M ) <-> ( ( d e. ( A ^m ( 0 ..^ S ) ) /\ sum_ a e. ( 0 ..^ S ) ( d ` a ) = M ) /\ -. d e. ( B ^m ( 0 ..^ S ) ) ) )
19 18 a1i 
 |-  ( ph -> ( ( d e. ( ( A ^m ( 0 ..^ S ) ) \ ( B ^m ( 0 ..^ S ) ) ) /\ sum_ a e. ( 0 ..^ S ) ( d ` a ) = M ) <-> ( ( d e. ( A ^m ( 0 ..^ S ) ) /\ sum_ a e. ( 0 ..^ S ) ( d ` a ) = M ) /\ -. d e. ( B ^m ( 0 ..^ S ) ) ) ) )
20 14 19 bitr4d 
 |-  ( ph -> ( ( d e. ( A ( repr ` S ) M ) /\ -. d e. ( B ^m ( 0 ..^ S ) ) ) <-> ( d e. ( ( A ^m ( 0 ..^ S ) ) \ ( B ^m ( 0 ..^ S ) ) ) /\ sum_ a e. ( 0 ..^ S ) ( d ` a ) = M ) ) )
21 nnex 
 |-  NN e. _V
22 21 a1i 
 |-  ( ph -> NN e. _V )
23 22 3 ssexd 
 |-  ( ph -> B e. _V )
24 ovexd 
 |-  ( ph -> ( 0 ..^ S ) e. _V )
25 elmapg 
 |-  ( ( B e. _V /\ ( 0 ..^ S ) e. _V ) -> ( d e. ( B ^m ( 0 ..^ S ) ) <-> d : ( 0 ..^ S ) --> B ) )
26 23 24 25 syl2anc 
 |-  ( ph -> ( d e. ( B ^m ( 0 ..^ S ) ) <-> d : ( 0 ..^ S ) --> B ) )
27 26 adantr 
 |-  ( ( ph /\ d e. ( A ( repr ` S ) M ) ) -> ( d e. ( B ^m ( 0 ..^ S ) ) <-> d : ( 0 ..^ S ) --> B ) )
28 ffnfv 
 |-  ( d : ( 0 ..^ S ) --> B <-> ( d Fn ( 0 ..^ S ) /\ A. x e. ( 0 ..^ S ) ( d ` x ) e. B ) )
29 2 adantr 
 |-  ( ( ph /\ d e. ( A ( repr ` S ) M ) ) -> A C_ NN )
30 9 adantr 
 |-  ( ( ph /\ d e. ( A ( repr ` S ) M ) ) -> M e. ZZ )
31 5 adantr 
 |-  ( ( ph /\ d e. ( A ( repr ` S ) M ) ) -> S e. NN0 )
32 simpr 
 |-  ( ( ph /\ d e. ( A ( repr ` S ) M ) ) -> d e. ( A ( repr ` S ) M ) )
33 29 30 31 32 reprf 
 |-  ( ( ph /\ d e. ( A ( repr ` S ) M ) ) -> d : ( 0 ..^ S ) --> A )
34 33 ffnd 
 |-  ( ( ph /\ d e. ( A ( repr ` S ) M ) ) -> d Fn ( 0 ..^ S ) )
35 34 biantrurd 
 |-  ( ( ph /\ d e. ( A ( repr ` S ) M ) ) -> ( A. x e. ( 0 ..^ S ) ( d ` x ) e. B <-> ( d Fn ( 0 ..^ S ) /\ A. x e. ( 0 ..^ S ) ( d ` x ) e. B ) ) )
36 28 35 bitr4id 
 |-  ( ( ph /\ d e. ( A ( repr ` S ) M ) ) -> ( d : ( 0 ..^ S ) --> B <-> A. x e. ( 0 ..^ S ) ( d ` x ) e. B ) )
37 27 36 bitrd 
 |-  ( ( ph /\ d e. ( A ( repr ` S ) M ) ) -> ( d e. ( B ^m ( 0 ..^ S ) ) <-> A. x e. ( 0 ..^ S ) ( d ` x ) e. B ) )
38 37 notbid 
 |-  ( ( ph /\ d e. ( A ( repr ` S ) M ) ) -> ( -. d e. ( B ^m ( 0 ..^ S ) ) <-> -. A. x e. ( 0 ..^ S ) ( d ` x ) e. B ) )
39 rexnal 
 |-  ( E. x e. ( 0 ..^ S ) -. ( d ` x ) e. B <-> -. A. x e. ( 0 ..^ S ) ( d ` x ) e. B )
40 38 39 bitr4di 
 |-  ( ( ph /\ d e. ( A ( repr ` S ) M ) ) -> ( -. d e. ( B ^m ( 0 ..^ S ) ) <-> E. x e. ( 0 ..^ S ) -. ( d ` x ) e. B ) )
41 40 pm5.32da 
 |-  ( ph -> ( ( d e. ( A ( repr ` S ) M ) /\ -. d e. ( B ^m ( 0 ..^ S ) ) ) <-> ( d e. ( A ( repr ` S ) M ) /\ E. x e. ( 0 ..^ S ) -. ( d ` x ) e. B ) ) )
42 20 41 bitr3d 
 |-  ( ph -> ( ( d e. ( ( A ^m ( 0 ..^ S ) ) \ ( B ^m ( 0 ..^ S ) ) ) /\ sum_ a e. ( 0 ..^ S ) ( d ` a ) = M ) <-> ( d e. ( A ( repr ` S ) M ) /\ E. x e. ( 0 ..^ S ) -. ( d ` x ) e. B ) ) )
43 fveq1 
 |-  ( c = d -> ( c ` x ) = ( d ` x ) )
44 43 eleq1d 
 |-  ( c = d -> ( ( c ` x ) e. B <-> ( d ` x ) e. B ) )
45 44 notbid 
 |-  ( c = d -> ( -. ( c ` x ) e. B <-> -. ( d ` x ) e. B ) )
46 45 elrab 
 |-  ( d e. { c e. ( A ( repr ` S ) M ) | -. ( c ` x ) e. B } <-> ( d e. ( A ( repr ` S ) M ) /\ -. ( d ` x ) e. B ) )
47 46 rexbii 
 |-  ( E. x e. ( 0 ..^ S ) d e. { c e. ( A ( repr ` S ) M ) | -. ( c ` x ) e. B } <-> E. x e. ( 0 ..^ S ) ( d e. ( A ( repr ` S ) M ) /\ -. ( d ` x ) e. B ) )
48 r19.42v 
 |-  ( E. x e. ( 0 ..^ S ) ( d e. ( A ( repr ` S ) M ) /\ -. ( d ` x ) e. B ) <-> ( d e. ( A ( repr ` S ) M ) /\ E. x e. ( 0 ..^ S ) -. ( d ` x ) e. B ) )
49 47 48 bitri 
 |-  ( E. x e. ( 0 ..^ S ) d e. { c e. ( A ( repr ` S ) M ) | -. ( c ` x ) e. B } <-> ( d e. ( A ( repr ` S ) M ) /\ E. x e. ( 0 ..^ S ) -. ( d ` x ) e. B ) )
50 42 49 bitr4di 
 |-  ( ph -> ( ( d e. ( ( A ^m ( 0 ..^ S ) ) \ ( B ^m ( 0 ..^ S ) ) ) /\ sum_ a e. ( 0 ..^ S ) ( d ` a ) = M ) <-> E. x e. ( 0 ..^ S ) d e. { c e. ( A ( repr ` S ) M ) | -. ( c ` x ) e. B } ) )
51 rabid 
 |-  ( d e. { d e. ( ( A ^m ( 0 ..^ S ) ) \ ( B ^m ( 0 ..^ S ) ) ) | sum_ a e. ( 0 ..^ S ) ( d ` a ) = M } <-> ( d e. ( ( A ^m ( 0 ..^ S ) ) \ ( B ^m ( 0 ..^ S ) ) ) /\ sum_ a e. ( 0 ..^ S ) ( d ` a ) = M ) )
52 eliun 
 |-  ( d e. U_ x e. ( 0 ..^ S ) { c e. ( A ( repr ` S ) M ) | -. ( c ` x ) e. B } <-> E. x e. ( 0 ..^ S ) d e. { c e. ( A ( repr ` S ) M ) | -. ( c ` x ) e. B } )
53 50 51 52 3bitr4g 
 |-  ( ph -> ( d e. { d e. ( ( A ^m ( 0 ..^ S ) ) \ ( B ^m ( 0 ..^ S ) ) ) | sum_ a e. ( 0 ..^ S ) ( d ` a ) = M } <-> d e. U_ x e. ( 0 ..^ S ) { c e. ( A ( repr ` S ) M ) | -. ( c ` x ) e. B } ) )
54 6 7 8 53 eqrd 
 |-  ( ph -> { d e. ( ( A ^m ( 0 ..^ S ) ) \ ( B ^m ( 0 ..^ S ) ) ) | sum_ a e. ( 0 ..^ S ) ( d ` a ) = M } = U_ x e. ( 0 ..^ S ) { c e. ( A ( repr ` S ) M ) | -. ( c ` x ) e. B } )
55 3 9 5 reprval 
 |-  ( ph -> ( B ( repr ` S ) M ) = { d e. ( B ^m ( 0 ..^ S ) ) | sum_ a e. ( 0 ..^ S ) ( d ` a ) = M } )
56 10 55 difeq12d 
 |-  ( ph -> ( ( A ( repr ` S ) M ) \ ( B ( repr ` S ) M ) ) = ( { d e. ( A ^m ( 0 ..^ S ) ) | sum_ a e. ( 0 ..^ S ) ( d ` a ) = M } \ { d e. ( B ^m ( 0 ..^ S ) ) | sum_ a e. ( 0 ..^ S ) ( d ` a ) = M } ) )
57 difrab2 
 |-  ( { d e. ( A ^m ( 0 ..^ S ) ) | sum_ a e. ( 0 ..^ S ) ( d ` a ) = M } \ { d e. ( B ^m ( 0 ..^ S ) ) | sum_ a e. ( 0 ..^ S ) ( d ` a ) = M } ) = { d e. ( ( A ^m ( 0 ..^ S ) ) \ ( B ^m ( 0 ..^ S ) ) ) | sum_ a e. ( 0 ..^ S ) ( d ` a ) = M }
58 56 57 eqtrdi 
 |-  ( ph -> ( ( A ( repr ` S ) M ) \ ( B ( repr ` S ) M ) ) = { d e. ( ( A ^m ( 0 ..^ S ) ) \ ( B ^m ( 0 ..^ S ) ) ) | sum_ a e. ( 0 ..^ S ) ( d ` a ) = M } )
59 1 a1i 
 |-  ( ph -> C = { c e. ( A ( repr ` S ) M ) | -. ( c ` x ) e. B } )
60 59 iuneq2d 
 |-  ( ph -> U_ x e. ( 0 ..^ S ) C = U_ x e. ( 0 ..^ S ) { c e. ( A ( repr ` S ) M ) | -. ( c ` x ) e. B } )
61 54 58 60 3eqtr4d 
 |-  ( ph -> ( ( A ( repr ` S ) M ) \ ( B ( repr ` S ) M ) ) = U_ x e. ( 0 ..^ S ) C )