Metamath Proof Explorer

Theorem hashreprin

Description: Express a sum of representations over an intersection using a product of the indicator function. (Contributed by Thierry Arnoux, 11-Dec-2021)

Ref Expression
Hypotheses reprval.a 
|- ( ph -> A C_ NN )
reprval.m 
|- ( ph -> M e. ZZ )
reprval.s 
|- ( ph -> S e. NN0 )
hashreprin.b 
|- ( ph -> B e. Fin )
hashreprin.1 
|- ( ph -> B C_ NN )
Assertion hashreprin 
|- ( ph -> ( # ` ( ( A i^i B ) ( repr ` S ) M ) ) = sum_ c e. ( B ( repr ` S ) M ) prod_ a e. ( 0 ..^ S ) ( ( ( _Ind ` NN ) ` A ) ` ( c ` a ) ) )

Proof

Step Hyp Ref Expression
1 reprval.a 
 |-  ( ph -> A C_ NN )
2 reprval.m 
 |-  ( ph -> M e. ZZ )
3 reprval.s 
 |-  ( ph -> S e. NN0 )
4 hashreprin.b 
 |-  ( ph -> B e. Fin )
5 hashreprin.1 
 |-  ( ph -> B C_ NN )
6 5 2 3 4 reprfi 
 |-  ( ph -> ( B ( repr ` S ) M ) e. Fin )
7 inss2 
 |-  ( A i^i B ) C_ B
8 7 a1i 
 |-  ( ph -> ( A i^i B ) C_ B )
9 5 2 3 8 reprss 
 |-  ( ph -> ( ( A i^i B ) ( repr ` S ) M ) C_ ( B ( repr ` S ) M ) )
10 6 9 ssfid 
 |-  ( ph -> ( ( A i^i B ) ( repr ` S ) M ) e. Fin )
11 1cnd 
 |-  ( ph -> 1 e. CC )
12 fsumconst 
 |-  ( ( ( ( A i^i B ) ( repr ` S ) M ) e. Fin /\ 1 e. CC ) -> sum_ c e. ( ( A i^i B ) ( repr ` S ) M ) 1 = ( ( # ` ( ( A i^i B ) ( repr ` S ) M ) ) x. 1 ) )
13 10 11 12 syl2anc 
 |-  ( ph -> sum_ c e. ( ( A i^i B ) ( repr ` S ) M ) 1 = ( ( # ` ( ( A i^i B ) ( repr ` S ) M ) ) x. 1 ) )
14 11 ralrimivw 
 |-  ( ph -> A. c e. ( ( A i^i B ) ( repr ` S ) M ) 1 e. CC )
15 6 olcd 
 |-  ( ph -> ( ( B ( repr ` S ) M ) C_ ( ZZ>= ` 0 ) \/ ( B ( repr ` S ) M ) e. Fin ) )
16 sumss2 
 |-  ( ( ( ( ( A i^i B ) ( repr ` S ) M ) C_ ( B ( repr ` S ) M ) /\ A. c e. ( ( A i^i B ) ( repr ` S ) M ) 1 e. CC ) /\ ( ( B ( repr ` S ) M ) C_ ( ZZ>= ` 0 ) \/ ( B ( repr ` S ) M ) e. Fin ) ) -> sum_ c e. ( ( A i^i B ) ( repr ` S ) M ) 1 = sum_ c e. ( B ( repr ` S ) M ) if ( c e. ( ( A i^i B ) ( repr ` S ) M ) , 1 , 0 ) )
17 9 14 15 16 syl21anc 
 |-  ( ph -> sum_ c e. ( ( A i^i B ) ( repr ` S ) M ) 1 = sum_ c e. ( B ( repr ` S ) M ) if ( c e. ( ( A i^i B ) ( repr ` S ) M ) , 1 , 0 ) )
18 5 2 3 reprinrn 
 |-  ( ph -> ( c e. ( ( B i^i A ) ( repr ` S ) M ) <-> ( c e. ( B ( repr ` S ) M ) /\ ran c C_ A ) ) )
19 incom 
 |-  ( B i^i A ) = ( A i^i B )
20 19 oveq1i 
 |-  ( ( B i^i A ) ( repr ` S ) M ) = ( ( A i^i B ) ( repr ` S ) M )
21 20 eleq2i 
 |-  ( c e. ( ( B i^i A ) ( repr ` S ) M ) <-> c e. ( ( A i^i B ) ( repr ` S ) M ) )
22 21 bibi1i 
 |-  ( ( c e. ( ( B i^i A ) ( repr ` S ) M ) <-> ( c e. ( B ( repr ` S ) M ) /\ ran c C_ A ) ) <-> ( c e. ( ( A i^i B ) ( repr ` S ) M ) <-> ( c e. ( B ( repr ` S ) M ) /\ ran c C_ A ) ) )
23 22 imbi2i 
 |-  ( ( ph -> ( c e. ( ( B i^i A ) ( repr ` S ) M ) <-> ( c e. ( B ( repr ` S ) M ) /\ ran c C_ A ) ) ) <-> ( ph -> ( c e. ( ( A i^i B ) ( repr ` S ) M ) <-> ( c e. ( B ( repr ` S ) M ) /\ ran c C_ A ) ) ) )
24 18 23 mpbi 
 |-  ( ph -> ( c e. ( ( A i^i B ) ( repr ` S ) M ) <-> ( c e. ( B ( repr ` S ) M ) /\ ran c C_ A ) ) )
25 24 baibd 
 |-  ( ( ph /\ c e. ( B ( repr ` S ) M ) ) -> ( c e. ( ( A i^i B ) ( repr ` S ) M ) <-> ran c C_ A ) )
26 25 ifbid 
 |-  ( ( ph /\ c e. ( B ( repr ` S ) M ) ) -> if ( c e. ( ( A i^i B ) ( repr ` S ) M ) , 1 , 0 ) = if ( ran c C_ A , 1 , 0 ) )
27 nnex 
 |-  NN e. _V
28 27 a1i 
 |-  ( ph -> NN e. _V )
29 28 ralrimivw 
 |-  ( ph -> A. c e. ( B ( repr ` S ) M ) NN e. _V )
30 29 r19.21bi 
 |-  ( ( ph /\ c e. ( B ( repr ` S ) M ) ) -> NN e. _V )
31 fzofi 
 |-  ( 0 ..^ S ) e. Fin
32 31 a1i 
 |-  ( ( ph /\ c e. ( B ( repr ` S ) M ) ) -> ( 0 ..^ S ) e. Fin )
33 1 adantr 
 |-  ( ( ph /\ c e. ( B ( repr ` S ) M ) ) -> A C_ NN )
34 5 adantr 
 |-  ( ( ph /\ c e. ( B ( repr ` S ) M ) ) -> B C_ NN )
35 2 adantr 
 |-  ( ( ph /\ c e. ( B ( repr ` S ) M ) ) -> M e. ZZ )
36 3 adantr 
 |-  ( ( ph /\ c e. ( B ( repr ` S ) M ) ) -> S e. NN0 )
37 simpr 
 |-  ( ( ph /\ c e. ( B ( repr ` S ) M ) ) -> c e. ( B ( repr ` S ) M ) )
38 34 35 36 37 reprf 
 |-  ( ( ph /\ c e. ( B ( repr ` S ) M ) ) -> c : ( 0 ..^ S ) --> B )
39 38 34 fssd 
 |-  ( ( ph /\ c e. ( B ( repr ` S ) M ) ) -> c : ( 0 ..^ S ) --> NN )
40 30 32 33 39 prodindf 
 |-  ( ( ph /\ c e. ( B ( repr ` S ) M ) ) -> prod_ a e. ( 0 ..^ S ) ( ( ( _Ind ` NN ) ` A ) ` ( c ` a ) ) = if ( ran c C_ A , 1 , 0 ) )
41 26 40 eqtr4d 
 |-  ( ( ph /\ c e. ( B ( repr ` S ) M ) ) -> if ( c e. ( ( A i^i B ) ( repr ` S ) M ) , 1 , 0 ) = prod_ a e. ( 0 ..^ S ) ( ( ( _Ind ` NN ) ` A ) ` ( c ` a ) ) )
42 41 sumeq2dv 
 |-  ( ph -> sum_ c e. ( B ( repr ` S ) M ) if ( c e. ( ( A i^i B ) ( repr ` S ) M ) , 1 , 0 ) = sum_ c e. ( B ( repr ` S ) M ) prod_ a e. ( 0 ..^ S ) ( ( ( _Ind ` NN ) ` A ) ` ( c ` a ) ) )
43 17 42 eqtrd 
 |-  ( ph -> sum_ c e. ( ( A i^i B ) ( repr ` S ) M ) 1 = sum_ c e. ( B ( repr ` S ) M ) prod_ a e. ( 0 ..^ S ) ( ( ( _Ind ` NN ) ` A ) ` ( c ` a ) ) )
44 hashcl 
 |-  ( ( ( A i^i B ) ( repr ` S ) M ) e. Fin -> ( # ` ( ( A i^i B ) ( repr ` S ) M ) ) e. NN0 )
45 10 44 syl 
 |-  ( ph -> ( # ` ( ( A i^i B ) ( repr ` S ) M ) ) e. NN0 )
46 45 nn0cnd 
 |-  ( ph -> ( # ` ( ( A i^i B ) ( repr ` S ) M ) ) e. CC )
47 46 mulid1d 
 |-  ( ph -> ( ( # ` ( ( A i^i B ) ( repr ` S ) M ) ) x. 1 ) = ( # ` ( ( A i^i B ) ( repr ` S ) M ) ) )
48 13 43 47 3eqtr3rd 
 |-  ( ph -> ( # ` ( ( A i^i B ) ( repr ` S ) M ) ) = sum_ c e. ( B ( repr ` S ) M ) prod_ a e. ( 0 ..^ S ) ( ( ( _Ind ` NN ) ` A ) ` ( c ` a ) ) )