Metamath Proof Explorer

Theorem fprodcn

Description: A finite product of functions to complex numbers from a common topological space is continuous. The class expression for B normally contains free variables k and x to index it. (Contributed by Glauco Siliprandi, 8-Apr-2021)

Ref Expression
Hypotheses fprodcn.d 
|- F/ k ph
fprodcn.k 
|- K = ( TopOpen ` CCfld )
fprodcn.j 
|- ( ph -> J e. ( TopOn ` X ) )
fprodcn.a 
|- ( ph -> A e. Fin )
fprodcn.b 
|- ( ( ph /\ k e. A ) -> ( x e. X |-> B ) e. ( J Cn K ) )
Assertion fprodcn 
|- ( ph -> ( x e. X |-> prod_ k e. A B ) e. ( J Cn K ) )

Proof

Step Hyp Ref Expression
1 fprodcn.d 
 |-  F/ k ph
2 fprodcn.k 
 |-  K = ( TopOpen ` CCfld )
3 fprodcn.j 
 |-  ( ph -> J e. ( TopOn ` X ) )
4 fprodcn.a 
 |-  ( ph -> A e. Fin )
5 fprodcn.b 
 |-  ( ( ph /\ k e. A ) -> ( x e. X |-> B ) e. ( J Cn K ) )
6 prodeq1 
 |-  ( y = (/) -> prod_ k e. y B = prod_ k e. (/) B )
7 6 mpteq2dv 
 |-  ( y = (/) -> ( x e. X |-> prod_ k e. y B ) = ( x e. X |-> prod_ k e. (/) B ) )
8 7 eleq1d 
 |-  ( y = (/) -> ( ( x e. X |-> prod_ k e. y B ) e. ( J Cn K ) <-> ( x e. X |-> prod_ k e. (/) B ) e. ( J Cn K ) ) )
9 prodeq1 
 |-  ( y = z -> prod_ k e. y B = prod_ k e. z B )
10 9 mpteq2dv 
 |-  ( y = z -> ( x e. X |-> prod_ k e. y B ) = ( x e. X |-> prod_ k e. z B ) )
11 10 eleq1d 
 |-  ( y = z -> ( ( x e. X |-> prod_ k e. y B ) e. ( J Cn K ) <-> ( x e. X |-> prod_ k e. z B ) e. ( J Cn K ) ) )
12 prodeq1 
 |-  ( y = ( z u. { w } ) -> prod_ k e. y B = prod_ k e. ( z u. { w } ) B )
13 12 mpteq2dv 
 |-  ( y = ( z u. { w } ) -> ( x e. X |-> prod_ k e. y B ) = ( x e. X |-> prod_ k e. ( z u. { w } ) B ) )
14 13 eleq1d 
 |-  ( y = ( z u. { w } ) -> ( ( x e. X |-> prod_ k e. y B ) e. ( J Cn K ) <-> ( x e. X |-> prod_ k e. ( z u. { w } ) B ) e. ( J Cn K ) ) )
15 prodeq1 
 |-  ( y = A -> prod_ k e. y B = prod_ k e. A B )
16 15 mpteq2dv 
 |-  ( y = A -> ( x e. X |-> prod_ k e. y B ) = ( x e. X |-> prod_ k e. A B ) )
17 16 eleq1d 
 |-  ( y = A -> ( ( x e. X |-> prod_ k e. y B ) e. ( J Cn K ) <-> ( x e. X |-> prod_ k e. A B ) e. ( J Cn K ) ) )
18 prod0 
 |-  prod_ k e. (/) B = 1
19 18 mpteq2i 
 |-  ( x e. X |-> prod_ k e. (/) B ) = ( x e. X |-> 1 )
20 eqidd 
 |-  ( x = y -> 1 = 1 )
21 20 cbvmptv 
 |-  ( x e. X |-> 1 ) = ( y e. X |-> 1 )
22 19 21 eqtri 
 |-  ( x e. X |-> prod_ k e. (/) B ) = ( y e. X |-> 1 )
23 22 a1i 
 |-  ( ph -> ( x e. X |-> prod_ k e. (/) B ) = ( y e. X |-> 1 ) )
24 2 cnfldtopon 
 |-  K e. ( TopOn ` CC )
25 24 a1i 
 |-  ( ph -> K e. ( TopOn ` CC ) )
26 1cnd 
 |-  ( ph -> 1 e. CC )
27 3 25 26 cnmptc 
 |-  ( ph -> ( y e. X |-> 1 ) e. ( J Cn K ) )
28 23 27 eqeltrd 
 |-  ( ph -> ( x e. X |-> prod_ k e. (/) B ) e. ( J Cn K ) )
29 nfcv 
 |-  F/_ y prod_ k e. ( z u. { w } ) B
30 nfcv 
 |-  F/_ x ( z u. { w } )
31 nfcsb1v 
 |-  F/_ x [_ y / x ]_ B
32 30 31 nfcprod 
 |-  F/_ x prod_ k e. ( z u. { w } ) [_ y / x ]_ B
33 csbeq1a 
 |-  ( x = y -> B = [_ y / x ]_ B )
34 33 prodeq2ad 
 |-  ( x = y -> prod_ k e. ( z u. { w } ) B = prod_ k e. ( z u. { w } ) [_ y / x ]_ B )
35 29 32 34 cbvmpt 
 |-  ( x e. X |-> prod_ k e. ( z u. { w } ) B ) = ( y e. X |-> prod_ k e. ( z u. { w } ) [_ y / x ]_ B )
36 35 a1i 
 |-  ( ( ( ph /\ ( z C_ A /\ w e. ( A \ z ) ) ) /\ ( x e. X |-> prod_ k e. z B ) e. ( J Cn K ) ) -> ( x e. X |-> prod_ k e. ( z u. { w } ) B ) = ( y e. X |-> prod_ k e. ( z u. { w } ) [_ y / x ]_ B ) )
37 nfv 
 |-  F/ k ( z C_ A /\ w e. ( A \ z ) )
38 1 37 nfan 
 |-  F/ k ( ph /\ ( z C_ A /\ w e. ( A \ z ) ) )
39 nfcv 
 |-  F/_ k X
40 nfcv 
 |-  F/_ k z
41 40 nfcprod1 
 |-  F/_ k prod_ k e. z B
42 39 41 nfmpt 
 |-  F/_ k ( x e. X |-> prod_ k e. z B )
43 nfcv 
 |-  F/_ k ( J Cn K )
44 42 43 nfel 
 |-  F/ k ( x e. X |-> prod_ k e. z B ) e. ( J Cn K )
45 38 44 nfan 
 |-  F/ k ( ( ph /\ ( z C_ A /\ w e. ( A \ z ) ) ) /\ ( x e. X |-> prod_ k e. z B ) e. ( J Cn K ) )
46 3 ad2antrr 
 |-  ( ( ( ph /\ ( z C_ A /\ w e. ( A \ z ) ) ) /\ ( x e. X |-> prod_ k e. z B ) e. ( J Cn K ) ) -> J e. ( TopOn ` X ) )
47 4 ad2antrr 
 |-  ( ( ( ph /\ ( z C_ A /\ w e. ( A \ z ) ) ) /\ ( x e. X |-> prod_ k e. z B ) e. ( J Cn K ) ) -> A e. Fin )
48 nfcv 
 |-  F/_ y B
49 48 31 33 cbvmpt 
 |-  ( x e. X |-> B ) = ( y e. X |-> [_ y / x ]_ B )
50 49 eqcomi 
 |-  ( y e. X |-> [_ y / x ]_ B ) = ( x e. X |-> B )
51 50 a1i 
 |-  ( ( ph /\ k e. A ) -> ( y e. X |-> [_ y / x ]_ B ) = ( x e. X |-> B ) )
52 51 5 eqeltrd 
 |-  ( ( ph /\ k e. A ) -> ( y e. X |-> [_ y / x ]_ B ) e. ( J Cn K ) )
53 52 ad4ant14 
 |-  ( ( ( ( ph /\ ( z C_ A /\ w e. ( A \ z ) ) ) /\ ( x e. X |-> prod_ k e. z B ) e. ( J Cn K ) ) /\ k e. A ) -> ( y e. X |-> [_ y / x ]_ B ) e. ( J Cn K ) )
54 simplrl 
 |-  ( ( ( ph /\ ( z C_ A /\ w e. ( A \ z ) ) ) /\ ( x e. X |-> prod_ k e. z B ) e. ( J Cn K ) ) -> z C_ A )
55 simplrr 
 |-  ( ( ( ph /\ ( z C_ A /\ w e. ( A \ z ) ) ) /\ ( x e. X |-> prod_ k e. z B ) e. ( J Cn K ) ) -> w e. ( A \ z ) )
56 nfcv 
 |-  F/_ y prod_ k e. z B
57 nfcv 
 |-  F/_ x z
58 57 31 nfcprod 
 |-  F/_ x prod_ k e. z [_ y / x ]_ B
59 33 prodeq2sdv 
 |-  ( x = y -> prod_ k e. z B = prod_ k e. z [_ y / x ]_ B )
60 56 58 59 cbvmpt 
 |-  ( x e. X |-> prod_ k e. z B ) = ( y e. X |-> prod_ k e. z [_ y / x ]_ B )
61 60 eleq1i 
 |-  ( ( x e. X |-> prod_ k e. z B ) e. ( J Cn K ) <-> ( y e. X |-> prod_ k e. z [_ y / x ]_ B ) e. ( J Cn K ) )
62 61 biimpi 
 |-  ( ( x e. X |-> prod_ k e. z B ) e. ( J Cn K ) -> ( y e. X |-> prod_ k e. z [_ y / x ]_ B ) e. ( J Cn K ) )
63 62 adantl 
 |-  ( ( ( ph /\ ( z C_ A /\ w e. ( A \ z ) ) ) /\ ( x e. X |-> prod_ k e. z B ) e. ( J Cn K ) ) -> ( y e. X |-> prod_ k e. z [_ y / x ]_ B ) e. ( J Cn K ) )
64 45 2 46 47 53 54 55 63 fprodcnlem 
 |-  ( ( ( ph /\ ( z C_ A /\ w e. ( A \ z ) ) ) /\ ( x e. X |-> prod_ k e. z B ) e. ( J Cn K ) ) -> ( y e. X |-> prod_ k e. ( z u. { w } ) [_ y / x ]_ B ) e. ( J Cn K ) )
65 36 64 eqeltrd 
 |-  ( ( ( ph /\ ( z C_ A /\ w e. ( A \ z ) ) ) /\ ( x e. X |-> prod_ k e. z B ) e. ( J Cn K ) ) -> ( x e. X |-> prod_ k e. ( z u. { w } ) B ) e. ( J Cn K ) )
66 65 ex 
 |-  ( ( ph /\ ( z C_ A /\ w e. ( A \ z ) ) ) -> ( ( x e. X |-> prod_ k e. z B ) e. ( J Cn K ) -> ( x e. X |-> prod_ k e. ( z u. { w } ) B ) e. ( J Cn K ) ) )
67 8 11 14 17 28 66 4 findcard2d 
 |-  ( ph -> ( x e. X |-> prod_ k e. A B ) e. ( J Cn K ) )