Metamath Proof Explorer

Theorem prodindf

Description: The product of indicators is one if and only if all values are in the set. (Contributed by Thierry Arnoux, 11-Dec-2021)

Ref Expression
Hypotheses prodindf.1 
|- ( ph -> O e. V )
prodindf.2 
|- ( ph -> A e. Fin )
prodindf.3 
|- ( ph -> B C_ O )
prodindf.4 
|- ( ph -> F : A --> O )
Assertion prodindf 
|- ( ph -> prod_ k e. A ( ( ( _Ind ` O ) ` B ) ` ( F ` k ) ) = if ( ran F C_ B , 1 , 0 ) )

Proof

Step Hyp Ref Expression
1 prodindf.1 
 |-  ( ph -> O e. V )
2 prodindf.2 
 |-  ( ph -> A e. Fin )
3 prodindf.3 
 |-  ( ph -> B C_ O )
4 prodindf.4 
 |-  ( ph -> F : A --> O )
5 2fveq3 
 |-  ( k = l -> ( ( ( _Ind ` O ) ` B ) ` ( F ` k ) ) = ( ( ( _Ind ` O ) ` B ) ` ( F ` l ) ) )
6 indf 
 |-  ( ( O e. V /\ B C_ O ) -> ( ( _Ind ` O ) ` B ) : O --> { 0 , 1 } )
7 1 3 6 syl2anc 
 |-  ( ph -> ( ( _Ind ` O ) ` B ) : O --> { 0 , 1 } )
8 7 adantr 
 |-  ( ( ph /\ k e. A ) -> ( ( _Ind ` O ) ` B ) : O --> { 0 , 1 } )
9 4 ffvelrnda 
 |-  ( ( ph /\ k e. A ) -> ( F ` k ) e. O )
10 8 9 ffvelrnd 
 |-  ( ( ph /\ k e. A ) -> ( ( ( _Ind ` O ) ` B ) ` ( F ` k ) ) e. { 0 , 1 } )
11 5 2 10 fprodex01 
 |-  ( ph -> prod_ k e. A ( ( ( _Ind ` O ) ` B ) ` ( F ` k ) ) = if ( A. l e. A ( ( ( _Ind ` O ) ` B ) ` ( F ` l ) ) = 1 , 1 , 0 ) )
12 2fveq3 
 |-  ( l = k -> ( ( ( _Ind ` O ) ` B ) ` ( F ` l ) ) = ( ( ( _Ind ` O ) ` B ) ` ( F ` k ) ) )
13 12 eqeq1d 
 |-  ( l = k -> ( ( ( ( _Ind ` O ) ` B ) ` ( F ` l ) ) = 1 <-> ( ( ( _Ind ` O ) ` B ) ` ( F ` k ) ) = 1 ) )
14 13 cbvralvw 
 |-  ( A. l e. A ( ( ( _Ind ` O ) ` B ) ` ( F ` l ) ) = 1 <-> A. k e. A ( ( ( _Ind ` O ) ` B ) ` ( F ` k ) ) = 1 )
15 14 a1i 
 |-  ( ph -> ( A. l e. A ( ( ( _Ind ` O ) ` B ) ` ( F ` l ) ) = 1 <-> A. k e. A ( ( ( _Ind ` O ) ` B ) ` ( F ` k ) ) = 1 ) )
16 15 ifbid 
 |-  ( ph -> if ( A. l e. A ( ( ( _Ind ` O ) ` B ) ` ( F ` l ) ) = 1 , 1 , 0 ) = if ( A. k e. A ( ( ( _Ind ` O ) ` B ) ` ( F ` k ) ) = 1 , 1 , 0 ) )
17 eqid 
 |-  ( k e. A |-> ( F ` k ) ) = ( k e. A |-> ( F ` k ) )
18 17 rnmptss 
 |-  ( A. k e. A ( F ` k ) e. B -> ran ( k e. A |-> ( F ` k ) ) C_ B )
19 nfv 
 |-  F/ k ph
20 nfmpt1 
 |-  F/_ k ( k e. A |-> ( F ` k ) )
21 20 nfrn 
 |-  F/_ k ran ( k e. A |-> ( F ` k ) )
22 nfcv 
 |-  F/_ k B
23 21 22 nfss 
 |-  F/ k ran ( k e. A |-> ( F ` k ) ) C_ B
24 19 23 nfan 
 |-  F/ k ( ph /\ ran ( k e. A |-> ( F ` k ) ) C_ B )
25 simplr 
 |-  ( ( ( ph /\ ran ( k e. A |-> ( F ` k ) ) C_ B ) /\ k e. A ) -> ran ( k e. A |-> ( F ` k ) ) C_ B )
26 4 feqmptd 
 |-  ( ph -> F = ( k e. A |-> ( F ` k ) ) )
27 eqidd 
 |-  ( ph -> k = k )
28 26 27 fveq12d 
 |-  ( ph -> ( F ` k ) = ( ( k e. A |-> ( F ` k ) ) ` k ) )
29 28 ralrimivw 
 |-  ( ph -> A. k e. A ( F ` k ) = ( ( k e. A |-> ( F ` k ) ) ` k ) )
30 29 r19.21bi 
 |-  ( ( ph /\ k e. A ) -> ( F ` k ) = ( ( k e. A |-> ( F ` k ) ) ` k ) )
31 4 ffnd 
 |-  ( ph -> F Fn A )
32 26 fneq1d 
 |-  ( ph -> ( F Fn A <-> ( k e. A |-> ( F ` k ) ) Fn A ) )
33 31 32 mpbid 
 |-  ( ph -> ( k e. A |-> ( F ` k ) ) Fn A )
34 33 adantr 
 |-  ( ( ph /\ k e. A ) -> ( k e. A |-> ( F ` k ) ) Fn A )
35 simpr 
 |-  ( ( ph /\ k e. A ) -> k e. A )
36 fnfvelrn 
 |-  ( ( ( k e. A |-> ( F ` k ) ) Fn A /\ k e. A ) -> ( ( k e. A |-> ( F ` k ) ) ` k ) e. ran ( k e. A |-> ( F ` k ) ) )
37 34 35 36 syl2anc 
 |-  ( ( ph /\ k e. A ) -> ( ( k e. A |-> ( F ` k ) ) ` k ) e. ran ( k e. A |-> ( F ` k ) ) )
38 30 37 eqeltrd 
 |-  ( ( ph /\ k e. A ) -> ( F ` k ) e. ran ( k e. A |-> ( F ` k ) ) )
39 38 adantlr 
 |-  ( ( ( ph /\ ran ( k e. A |-> ( F ` k ) ) C_ B ) /\ k e. A ) -> ( F ` k ) e. ran ( k e. A |-> ( F ` k ) ) )
40 25 39 sseldd 
 |-  ( ( ( ph /\ ran ( k e. A |-> ( F ` k ) ) C_ B ) /\ k e. A ) -> ( F ` k ) e. B )
41 40 ex 
 |-  ( ( ph /\ ran ( k e. A |-> ( F ` k ) ) C_ B ) -> ( k e. A -> ( F ` k ) e. B ) )
42 24 41 ralrimi 
 |-  ( ( ph /\ ran ( k e. A |-> ( F ` k ) ) C_ B ) -> A. k e. A ( F ` k ) e. B )
43 42 ex 
 |-  ( ph -> ( ran ( k e. A |-> ( F ` k ) ) C_ B -> A. k e. A ( F ` k ) e. B ) )
44 18 43 impbid2 
 |-  ( ph -> ( A. k e. A ( F ` k ) e. B <-> ran ( k e. A |-> ( F ` k ) ) C_ B ) )
45 1 adantr 
 |-  ( ( ph /\ k e. A ) -> O e. V )
46 3 adantr 
 |-  ( ( ph /\ k e. A ) -> B C_ O )
47 ind1a 
 |-  ( ( O e. V /\ B C_ O /\ ( F ` k ) e. O ) -> ( ( ( ( _Ind ` O ) ` B ) ` ( F ` k ) ) = 1 <-> ( F ` k ) e. B ) )
48 45 46 9 47 syl3anc 
 |-  ( ( ph /\ k e. A ) -> ( ( ( ( _Ind ` O ) ` B ) ` ( F ` k ) ) = 1 <-> ( F ` k ) e. B ) )
49 48 ralbidva 
 |-  ( ph -> ( A. k e. A ( ( ( _Ind ` O ) ` B ) ` ( F ` k ) ) = 1 <-> A. k e. A ( F ` k ) e. B ) )
50 26 rneqd 
 |-  ( ph -> ran F = ran ( k e. A |-> ( F ` k ) ) )
51 50 sseq1d 
 |-  ( ph -> ( ran F C_ B <-> ran ( k e. A |-> ( F ` k ) ) C_ B ) )
52 44 49 51 3bitr4d 
 |-  ( ph -> ( A. k e. A ( ( ( _Ind ` O ) ` B ) ` ( F ` k ) ) = 1 <-> ran F C_ B ) )
53 52 ifbid 
 |-  ( ph -> if ( A. k e. A ( ( ( _Ind ` O ) ` B ) ` ( F ` k ) ) = 1 , 1 , 0 ) = if ( ran F C_ B , 1 , 0 ) )
54 11 16 53 3eqtrd 
 |-  ( ph -> prod_ k e. A ( ( ( _Ind ` O ) ` B ) ` ( F ` k ) ) = if ( ran F C_ B , 1 , 0 ) )