Metamath Proof Explorer

Theorem fprodcncf

Description: The finite product of continuous complex functions is continuous. (Contributed by Glauco Siliprandi, 5-Apr-2020)

Ref Expression
Hypotheses fprodcncf.a 
|- ( ph -> A C_ CC )
fprodcncf.b 
|- ( ph -> B e. Fin )
fprodcncf.c 
|- ( ( ph /\ x e. A /\ k e. B ) -> C e. CC )
fprodcncf.cn 
|- ( ( ph /\ k e. B ) -> ( x e. A |-> C ) e. ( A -cn-> CC ) )
Assertion fprodcncf 
|- ( ph -> ( x e. A |-> prod_ k e. B C ) e. ( A -cn-> CC ) )

Proof

Step Hyp Ref Expression
1 fprodcncf.a 
 |-  ( ph -> A C_ CC )
2 fprodcncf.b 
 |-  ( ph -> B e. Fin )
3 fprodcncf.c 
 |-  ( ( ph /\ x e. A /\ k e. B ) -> C e. CC )
4 fprodcncf.cn 
 |-  ( ( ph /\ k e. B ) -> ( x e. A |-> C ) e. ( A -cn-> CC ) )
5 prodeq1 
 |-  ( w = (/) -> prod_ k e. w C = prod_ k e. (/) C )
6 5 mpteq2dv 
 |-  ( w = (/) -> ( x e. A |-> prod_ k e. w C ) = ( x e. A |-> prod_ k e. (/) C ) )
7 6 eleq1d 
 |-  ( w = (/) -> ( ( x e. A |-> prod_ k e. w C ) e. ( A -cn-> CC ) <-> ( x e. A |-> prod_ k e. (/) C ) e. ( A -cn-> CC ) ) )
8 prodeq1 
 |-  ( w = z -> prod_ k e. w C = prod_ k e. z C )
9 8 mpteq2dv 
 |-  ( w = z -> ( x e. A |-> prod_ k e. w C ) = ( x e. A |-> prod_ k e. z C ) )
10 9 eleq1d 
 |-  ( w = z -> ( ( x e. A |-> prod_ k e. w C ) e. ( A -cn-> CC ) <-> ( x e. A |-> prod_ k e. z C ) e. ( A -cn-> CC ) ) )
11 prodeq1 
 |-  ( w = ( z u. { y } ) -> prod_ k e. w C = prod_ k e. ( z u. { y } ) C )
12 11 mpteq2dv 
 |-  ( w = ( z u. { y } ) -> ( x e. A |-> prod_ k e. w C ) = ( x e. A |-> prod_ k e. ( z u. { y } ) C ) )
13 12 eleq1d 
 |-  ( w = ( z u. { y } ) -> ( ( x e. A |-> prod_ k e. w C ) e. ( A -cn-> CC ) <-> ( x e. A |-> prod_ k e. ( z u. { y } ) C ) e. ( A -cn-> CC ) ) )
14 prodeq1 
 |-  ( w = B -> prod_ k e. w C = prod_ k e. B C )
15 14 mpteq2dv 
 |-  ( w = B -> ( x e. A |-> prod_ k e. w C ) = ( x e. A |-> prod_ k e. B C ) )
16 15 eleq1d 
 |-  ( w = B -> ( ( x e. A |-> prod_ k e. w C ) e. ( A -cn-> CC ) <-> ( x e. A |-> prod_ k e. B C ) e. ( A -cn-> CC ) ) )
17 prod0 
 |-  prod_ k e. (/) C = 1
18 17 a1i 
 |-  ( ph -> prod_ k e. (/) C = 1 )
19 18 mpteq2dv 
 |-  ( ph -> ( x e. A |-> prod_ k e. (/) C ) = ( x e. A |-> 1 ) )
20 1cnd 
 |-  ( ph -> 1 e. CC )
21 ssidd 
 |-  ( ph -> CC C_ CC )
22 1 20 21 constcncfg 
 |-  ( ph -> ( x e. A |-> 1 ) e. ( A -cn-> CC ) )
23 19 22 eqeltrd 
 |-  ( ph -> ( x e. A |-> prod_ k e. (/) C ) e. ( A -cn-> CC ) )
24 nfcv 
 |-  F/_ u prod_ k e. ( z u. { y } ) C
25 nfcv 
 |-  F/_ x ( z u. { y } )
26 nfcsb1v 
 |-  F/_ x [_ u / x ]_ C
27 25 26 nfcprod 
 |-  F/_ x prod_ k e. ( z u. { y } ) [_ u / x ]_ C
28 csbeq1a 
 |-  ( x = u -> C = [_ u / x ]_ C )
29 28 adantr 
 |-  ( ( x = u /\ k e. ( z u. { y } ) ) -> C = [_ u / x ]_ C )
30 29 prodeq2dv 
 |-  ( x = u -> prod_ k e. ( z u. { y } ) C = prod_ k e. ( z u. { y } ) [_ u / x ]_ C )
31 24 27 30 cbvmpt 
 |-  ( x e. A |-> prod_ k e. ( z u. { y } ) C ) = ( u e. A |-> prod_ k e. ( z u. { y } ) [_ u / x ]_ C )
32 31 a1i 
 |-  ( ( ( ph /\ ( z C_ B /\ y e. ( B \ z ) ) ) /\ ( x e. A |-> prod_ k e. z C ) e. ( A -cn-> CC ) ) -> ( x e. A |-> prod_ k e. ( z u. { y } ) C ) = ( u e. A |-> prod_ k e. ( z u. { y } ) [_ u / x ]_ C ) )
33 nfv 
 |-  F/ k ( ( ph /\ ( z C_ B /\ y e. ( B \ z ) ) ) /\ u e. A )
34 nfcsb1v 
 |-  F/_ k [_ y / k ]_ [_ u / x ]_ C
35 2 adantr 
 |-  ( ( ph /\ z C_ B ) -> B e. Fin )
36 simpr 
 |-  ( ( ph /\ z C_ B ) -> z C_ B )
37 ssfi 
 |-  ( ( B e. Fin /\ z C_ B ) -> z e. Fin )
38 35 36 37 syl2anc 
 |-  ( ( ph /\ z C_ B ) -> z e. Fin )
39 38 adantrr 
 |-  ( ( ph /\ ( z C_ B /\ y e. ( B \ z ) ) ) -> z e. Fin )
40 39 adantr 
 |-  ( ( ( ph /\ ( z C_ B /\ y e. ( B \ z ) ) ) /\ u e. A ) -> z e. Fin )
41 vex 
 |-  y e. _V
42 41 a1i 
 |-  ( ( ( ph /\ ( z C_ B /\ y e. ( B \ z ) ) ) /\ u e. A ) -> y e. _V )
43 eldifn 
 |-  ( y e. ( B \ z ) -> -. y e. z )
44 43 ad2antll 
 |-  ( ( ph /\ ( z C_ B /\ y e. ( B \ z ) ) ) -> -. y e. z )
45 44 adantr 
 |-  ( ( ( ph /\ ( z C_ B /\ y e. ( B \ z ) ) ) /\ u e. A ) -> -. y e. z )
46 simplll 
 |-  ( ( ( ( ph /\ ( z C_ B /\ y e. ( B \ z ) ) ) /\ u e. A ) /\ k e. z ) -> ph )
47 simplr 
 |-  ( ( ( ( ph /\ ( z C_ B /\ y e. ( B \ z ) ) ) /\ u e. A ) /\ k e. z ) -> u e. A )
48 36 adantrr 
 |-  ( ( ph /\ ( z C_ B /\ y e. ( B \ z ) ) ) -> z C_ B )
49 48 ad2antrr 
 |-  ( ( ( ( ph /\ ( z C_ B /\ y e. ( B \ z ) ) ) /\ u e. A ) /\ k e. z ) -> z C_ B )
50 simpr 
 |-  ( ( ( ( ph /\ ( z C_ B /\ y e. ( B \ z ) ) ) /\ u e. A ) /\ k e. z ) -> k e. z )
51 49 50 sseldd 
 |-  ( ( ( ( ph /\ ( z C_ B /\ y e. ( B \ z ) ) ) /\ u e. A ) /\ k e. z ) -> k e. B )
52 nfv 
 |-  F/ x ( ph /\ u e. A /\ k e. B )
53 26 nfel1 
 |-  F/ x [_ u / x ]_ C e. CC
54 52 53 nfim 
 |-  F/ x ( ( ph /\ u e. A /\ k e. B ) -> [_ u / x ]_ C e. CC )
55 eleq1w 
 |-  ( x = u -> ( x e. A <-> u e. A ) )
56 55 3anbi2d 
 |-  ( x = u -> ( ( ph /\ x e. A /\ k e. B ) <-> ( ph /\ u e. A /\ k e. B ) ) )
57 28 eleq1d 
 |-  ( x = u -> ( C e. CC <-> [_ u / x ]_ C e. CC ) )
58 56 57 imbi12d 
 |-  ( x = u -> ( ( ( ph /\ x e. A /\ k e. B ) -> C e. CC ) <-> ( ( ph /\ u e. A /\ k e. B ) -> [_ u / x ]_ C e. CC ) ) )
59 54 58 3 chvarfv 
 |-  ( ( ph /\ u e. A /\ k e. B ) -> [_ u / x ]_ C e. CC )
60 46 47 51 59 syl3anc 
 |-  ( ( ( ( ph /\ ( z C_ B /\ y e. ( B \ z ) ) ) /\ u e. A ) /\ k e. z ) -> [_ u / x ]_ C e. CC )
61 csbeq1a 
 |-  ( k = y -> [_ u / x ]_ C = [_ y / k ]_ [_ u / x ]_ C )
62 simpll 
 |-  ( ( ( ph /\ ( z C_ B /\ y e. ( B \ z ) ) ) /\ u e. A ) -> ph )
63 eldifi 
 |-  ( y e. ( B \ z ) -> y e. B )
64 63 ad2antll 
 |-  ( ( ph /\ ( z C_ B /\ y e. ( B \ z ) ) ) -> y e. B )
65 64 adantr 
 |-  ( ( ( ph /\ ( z C_ B /\ y e. ( B \ z ) ) ) /\ u e. A ) -> y e. B )
66 simpr 
 |-  ( ( ( ph /\ ( z C_ B /\ y e. ( B \ z ) ) ) /\ u e. A ) -> u e. A )
67 simpll 
 |-  ( ( ( ph /\ y e. B ) /\ u e. A ) -> ph )
68 simpr 
 |-  ( ( ( ph /\ y e. B ) /\ u e. A ) -> u e. A )
69 simplr 
 |-  ( ( ( ph /\ y e. B ) /\ u e. A ) -> y e. B )
70 nfv 
 |-  F/ k ( ph /\ u e. A /\ y e. B )
71 nfcv 
 |-  F/_ k CC
72 34 71 nfel 
 |-  F/ k [_ y / k ]_ [_ u / x ]_ C e. CC
73 70 72 nfim 
 |-  F/ k ( ( ph /\ u e. A /\ y e. B ) -> [_ y / k ]_ [_ u / x ]_ C e. CC )
74 eleq1w 
 |-  ( k = y -> ( k e. B <-> y e. B ) )
75 74 3anbi3d 
 |-  ( k = y -> ( ( ph /\ u e. A /\ k e. B ) <-> ( ph /\ u e. A /\ y e. B ) ) )
76 61 eleq1d 
 |-  ( k = y -> ( [_ u / x ]_ C e. CC <-> [_ y / k ]_ [_ u / x ]_ C e. CC ) )
77 75 76 imbi12d 
 |-  ( k = y -> ( ( ( ph /\ u e. A /\ k e. B ) -> [_ u / x ]_ C e. CC ) <-> ( ( ph /\ u e. A /\ y e. B ) -> [_ y / k ]_ [_ u / x ]_ C e. CC ) ) )
78 73 77 59 chvarfv 
 |-  ( ( ph /\ u e. A /\ y e. B ) -> [_ y / k ]_ [_ u / x ]_ C e. CC )
79 67 68 69 78 syl3anc 
 |-  ( ( ( ph /\ y e. B ) /\ u e. A ) -> [_ y / k ]_ [_ u / x ]_ C e. CC )
80 62 65 66 79 syl21anc 
 |-  ( ( ( ph /\ ( z C_ B /\ y e. ( B \ z ) ) ) /\ u e. A ) -> [_ y / k ]_ [_ u / x ]_ C e. CC )
81 33 34 40 42 45 60 61 80 fprodsplitsn 
 |-  ( ( ( ph /\ ( z C_ B /\ y e. ( B \ z ) ) ) /\ u e. A ) -> prod_ k e. ( z u. { y } ) [_ u / x ]_ C = ( prod_ k e. z [_ u / x ]_ C x. [_ y / k ]_ [_ u / x ]_ C ) )
82 81 mpteq2dva 
 |-  ( ( ph /\ ( z C_ B /\ y e. ( B \ z ) ) ) -> ( u e. A |-> prod_ k e. ( z u. { y } ) [_ u / x ]_ C ) = ( u e. A |-> ( prod_ k e. z [_ u / x ]_ C x. [_ y / k ]_ [_ u / x ]_ C ) ) )
83 82 adantr 
 |-  ( ( ( ph /\ ( z C_ B /\ y e. ( B \ z ) ) ) /\ ( x e. A |-> prod_ k e. z C ) e. ( A -cn-> CC ) ) -> ( u e. A |-> prod_ k e. ( z u. { y } ) [_ u / x ]_ C ) = ( u e. A |-> ( prod_ k e. z [_ u / x ]_ C x. [_ y / k ]_ [_ u / x ]_ C ) ) )
84 nfcv 
 |-  F/_ u prod_ k e. z C
85 nfcv 
 |-  F/_ x z
86 85 26 nfcprod 
 |-  F/_ x prod_ k e. z [_ u / x ]_ C
87 28 adantr 
 |-  ( ( x = u /\ k e. z ) -> C = [_ u / x ]_ C )
88 87 prodeq2dv 
 |-  ( x = u -> prod_ k e. z C = prod_ k e. z [_ u / x ]_ C )
89 84 86 88 cbvmpt 
 |-  ( x e. A |-> prod_ k e. z C ) = ( u e. A |-> prod_ k e. z [_ u / x ]_ C )
90 89 eqcomi 
 |-  ( u e. A |-> prod_ k e. z [_ u / x ]_ C ) = ( x e. A |-> prod_ k e. z C )
91 90 a1i 
 |-  ( ( x e. A |-> prod_ k e. z C ) e. ( A -cn-> CC ) -> ( u e. A |-> prod_ k e. z [_ u / x ]_ C ) = ( x e. A |-> prod_ k e. z C ) )
92 id 
 |-  ( ( x e. A |-> prod_ k e. z C ) e. ( A -cn-> CC ) -> ( x e. A |-> prod_ k e. z C ) e. ( A -cn-> CC ) )
93 91 92 eqeltrd 
 |-  ( ( x e. A |-> prod_ k e. z C ) e. ( A -cn-> CC ) -> ( u e. A |-> prod_ k e. z [_ u / x ]_ C ) e. ( A -cn-> CC ) )
94 93 adantl 
 |-  ( ( ( ph /\ ( z C_ B /\ y e. ( B \ z ) ) ) /\ ( x e. A |-> prod_ k e. z C ) e. ( A -cn-> CC ) ) -> ( u e. A |-> prod_ k e. z [_ u / x ]_ C ) e. ( A -cn-> CC ) )
95 nfv 
 |-  F/ k ( ph /\ y e. B )
96 nfcv 
 |-  F/_ k A
97 96 34 nfmpt 
 |-  F/_ k ( u e. A |-> [_ y / k ]_ [_ u / x ]_ C )
98 nfcv 
 |-  F/_ k ( A -cn-> CC )
99 97 98 nfel 
 |-  F/ k ( u e. A |-> [_ y / k ]_ [_ u / x ]_ C ) e. ( A -cn-> CC )
100 95 99 nfim 
 |-  F/ k ( ( ph /\ y e. B ) -> ( u e. A |-> [_ y / k ]_ [_ u / x ]_ C ) e. ( A -cn-> CC ) )
101 74 anbi2d 
 |-  ( k = y -> ( ( ph /\ k e. B ) <-> ( ph /\ y e. B ) ) )
102 61 adantr 
 |-  ( ( k = y /\ u e. A ) -> [_ u / x ]_ C = [_ y / k ]_ [_ u / x ]_ C )
103 102 mpteq2dva 
 |-  ( k = y -> ( u e. A |-> [_ u / x ]_ C ) = ( u e. A |-> [_ y / k ]_ [_ u / x ]_ C ) )
104 103 eleq1d 
 |-  ( k = y -> ( ( u e. A |-> [_ u / x ]_ C ) e. ( A -cn-> CC ) <-> ( u e. A |-> [_ y / k ]_ [_ u / x ]_ C ) e. ( A -cn-> CC ) ) )
105 101 104 imbi12d 
 |-  ( k = y -> ( ( ( ph /\ k e. B ) -> ( u e. A |-> [_ u / x ]_ C ) e. ( A -cn-> CC ) ) <-> ( ( ph /\ y e. B ) -> ( u e. A |-> [_ y / k ]_ [_ u / x ]_ C ) e. ( A -cn-> CC ) ) ) )
106 nfcv 
 |-  F/_ u C
107 106 26 28 cbvmpt 
 |-  ( x e. A |-> C ) = ( u e. A |-> [_ u / x ]_ C )
108 107 4 eqeltrrid 
 |-  ( ( ph /\ k e. B ) -> ( u e. A |-> [_ u / x ]_ C ) e. ( A -cn-> CC ) )
109 100 105 108 chvarfv 
 |-  ( ( ph /\ y e. B ) -> ( u e. A |-> [_ y / k ]_ [_ u / x ]_ C ) e. ( A -cn-> CC ) )
110 64 109 syldan 
 |-  ( ( ph /\ ( z C_ B /\ y e. ( B \ z ) ) ) -> ( u e. A |-> [_ y / k ]_ [_ u / x ]_ C ) e. ( A -cn-> CC ) )
111 110 adantr 
 |-  ( ( ( ph /\ ( z C_ B /\ y e. ( B \ z ) ) ) /\ ( x e. A |-> prod_ k e. z C ) e. ( A -cn-> CC ) ) -> ( u e. A |-> [_ y / k ]_ [_ u / x ]_ C ) e. ( A -cn-> CC ) )
112 94 111 mulcncf 
 |-  ( ( ( ph /\ ( z C_ B /\ y e. ( B \ z ) ) ) /\ ( x e. A |-> prod_ k e. z C ) e. ( A -cn-> CC ) ) -> ( u e. A |-> ( prod_ k e. z [_ u / x ]_ C x. [_ y / k ]_ [_ u / x ]_ C ) ) e. ( A -cn-> CC ) )
113 83 112 eqeltrd 
 |-  ( ( ( ph /\ ( z C_ B /\ y e. ( B \ z ) ) ) /\ ( x e. A |-> prod_ k e. z C ) e. ( A -cn-> CC ) ) -> ( u e. A |-> prod_ k e. ( z u. { y } ) [_ u / x ]_ C ) e. ( A -cn-> CC ) )
114 32 113 eqeltrd 
 |-  ( ( ( ph /\ ( z C_ B /\ y e. ( B \ z ) ) ) /\ ( x e. A |-> prod_ k e. z C ) e. ( A -cn-> CC ) ) -> ( x e. A |-> prod_ k e. ( z u. { y } ) C ) e. ( A -cn-> CC ) )
115 114 ex 
 |-  ( ( ph /\ ( z C_ B /\ y e. ( B \ z ) ) ) -> ( ( x e. A |-> prod_ k e. z C ) e. ( A -cn-> CC ) -> ( x e. A |-> prod_ k e. ( z u. { y } ) C ) e. ( A -cn-> CC ) ) )
116 7 10 13 16 23 115 2 findcard2d 
 |-  ( ph -> ( x e. A |-> prod_ k e. B C ) e. ( A -cn-> CC ) )