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 φ A
fprodcncf.b φ B Fin
fprodcncf.c φ x A k B C
fprodcncf.cn φ k B x A C : A cn
Assertion fprodcncf φ x A k B C : A cn

Proof

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