Metamath Proof Explorer

Theorem fprodcnlem

Description: A finite product of functions to complex numbers from a common topological space is continuous. Induction step. (Contributed by Glauco Siliprandi, 8-Apr-2021)

Ref Expression
Hypotheses fprodcnlem.1 
|- F/ k ph
fprodcnlem.k 
|- K = ( TopOpen ` CCfld )
fprodcnlem.j 
|- ( ph -> J e. ( TopOn ` X ) )
fprodcnlem.a 
|- ( ph -> A e. Fin )
fprodcnlem.b 
|- ( ( ph /\ k e. A ) -> ( x e. X |-> B ) e. ( J Cn K ) )
fprodcnlem.z 
|- ( ph -> Z C_ A )
fprodcnlem.w 
|- ( ph -> W e. ( A \ Z ) )
fprodcnlem.p 
|- ( ph -> ( x e. X |-> prod_ k e. Z B ) e. ( J Cn K ) )
Assertion fprodcnlem 
|- ( ph -> ( x e. X |-> prod_ k e. ( Z u. { W } ) B ) e. ( J Cn K ) )

Proof

Step Hyp Ref Expression
1 fprodcnlem.1 
 |-  F/ k ph
2 fprodcnlem.k 
 |-  K = ( TopOpen ` CCfld )
3 fprodcnlem.j 
 |-  ( ph -> J e. ( TopOn ` X ) )
4 fprodcnlem.a 
 |-  ( ph -> A e. Fin )
5 fprodcnlem.b 
 |-  ( ( ph /\ k e. A ) -> ( x e. X |-> B ) e. ( J Cn K ) )
6 fprodcnlem.z 
 |-  ( ph -> Z C_ A )
7 fprodcnlem.w 
 |-  ( ph -> W e. ( A \ Z ) )
8 fprodcnlem.p 
 |-  ( ph -> ( x e. X |-> prod_ k e. Z B ) e. ( J Cn K ) )
9 nfv 
 |-  F/ k x e. X
10 1 9 nfan 
 |-  F/ k ( ph /\ x e. X )
11 nfcsb1v 
 |-  F/_ k [_ W / k ]_ B
12 4 6 ssfid 
 |-  ( ph -> Z e. Fin )
13 12 adantr 
 |-  ( ( ph /\ x e. X ) -> Z e. Fin )
14 7 adantr 
 |-  ( ( ph /\ x e. X ) -> W e. ( A \ Z ) )
15 14 eldifbd 
 |-  ( ( ph /\ x e. X ) -> -. W e. Z )
16 6 sselda 
 |-  ( ( ph /\ k e. Z ) -> k e. A )
17 16 adantlr 
 |-  ( ( ( ph /\ x e. X ) /\ k e. Z ) -> k e. A )
18 3 adantr 
 |-  ( ( ph /\ k e. A ) -> J e. ( TopOn ` X ) )
19 2 cnfldtopon 
 |-  K e. ( TopOn ` CC )
20 19 a1i 
 |-  ( ( ph /\ k e. A ) -> K e. ( TopOn ` CC ) )
21 cnf2 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` CC ) /\ ( x e. X |-> B ) e. ( J Cn K ) ) -> ( x e. X |-> B ) : X --> CC )
22 18 20 5 21 syl3anc 
 |-  ( ( ph /\ k e. A ) -> ( x e. X |-> B ) : X --> CC )
23 eqid 
 |-  ( x e. X |-> B ) = ( x e. X |-> B )
24 23 fmpt 
 |-  ( A. x e. X B e. CC <-> ( x e. X |-> B ) : X --> CC )
25 22 24 sylibr 
 |-  ( ( ph /\ k e. A ) -> A. x e. X B e. CC )
26 25 adantlr 
 |-  ( ( ( ph /\ x e. X ) /\ k e. A ) -> A. x e. X B e. CC )
27 simplr 
 |-  ( ( ( ph /\ x e. X ) /\ k e. A ) -> x e. X )
28 rspa 
 |-  ( ( A. x e. X B e. CC /\ x e. X ) -> B e. CC )
29 26 27 28 syl2anc 
 |-  ( ( ( ph /\ x e. X ) /\ k e. A ) -> B e. CC )
30 17 29 syldan 
 |-  ( ( ( ph /\ x e. X ) /\ k e. Z ) -> B e. CC )
31 csbeq1a 
 |-  ( k = W -> B = [_ W / k ]_ B )
32 14 eldifad 
 |-  ( ( ph /\ x e. X ) -> W e. A )
33 simpr 
 |-  ( ( ( ph /\ x e. X ) /\ W e. A ) -> W e. A )
34 nfcv 
 |-  F/_ k W
35 nfv 
 |-  F/ k W e. A
36 10 35 nfan 
 |-  F/ k ( ( ph /\ x e. X ) /\ W e. A )
37 11 nfel1 
 |-  F/ k [_ W / k ]_ B e. CC
38 36 37 nfim 
 |-  F/ k ( ( ( ph /\ x e. X ) /\ W e. A ) -> [_ W / k ]_ B e. CC )
39 eleq1 
 |-  ( k = W -> ( k e. A <-> W e. A ) )
40 39 anbi2d 
 |-  ( k = W -> ( ( ( ph /\ x e. X ) /\ k e. A ) <-> ( ( ph /\ x e. X ) /\ W e. A ) ) )
41 31 eleq1d 
 |-  ( k = W -> ( B e. CC <-> [_ W / k ]_ B e. CC ) )
42 40 41 imbi12d 
 |-  ( k = W -> ( ( ( ( ph /\ x e. X ) /\ k e. A ) -> B e. CC ) <-> ( ( ( ph /\ x e. X ) /\ W e. A ) -> [_ W / k ]_ B e. CC ) ) )
43 34 38 42 29 vtoclgf 
 |-  ( W e. A -> ( ( ( ph /\ x e. X ) /\ W e. A ) -> [_ W / k ]_ B e. CC ) )
44 33 43 mpcom 
 |-  ( ( ( ph /\ x e. X ) /\ W e. A ) -> [_ W / k ]_ B e. CC )
45 32 44 mpdan 
 |-  ( ( ph /\ x e. X ) -> [_ W / k ]_ B e. CC )
46 10 11 13 14 15 30 31 45 fprodsplitsn 
 |-  ( ( ph /\ x e. X ) -> prod_ k e. ( Z u. { W } ) B = ( prod_ k e. Z B x. [_ W / k ]_ B ) )
47 46 mpteq2dva 
 |-  ( ph -> ( x e. X |-> prod_ k e. ( Z u. { W } ) B ) = ( x e. X |-> ( prod_ k e. Z B x. [_ W / k ]_ B ) ) )
48 7 eldifad 
 |-  ( ph -> W e. A )
49 1 35 nfan 
 |-  F/ k ( ph /\ W e. A )
50 nfcv 
 |-  F/_ k X
51 50 11 nfmpt 
 |-  F/_ k ( x e. X |-> [_ W / k ]_ B )
52 nfcv 
 |-  F/_ k ( J Cn K )
53 51 52 nfel 
 |-  F/ k ( x e. X |-> [_ W / k ]_ B ) e. ( J Cn K )
54 49 53 nfim 
 |-  F/ k ( ( ph /\ W e. A ) -> ( x e. X |-> [_ W / k ]_ B ) e. ( J Cn K ) )
55 39 anbi2d 
 |-  ( k = W -> ( ( ph /\ k e. A ) <-> ( ph /\ W e. A ) ) )
56 31 mpteq2dv 
 |-  ( k = W -> ( x e. X |-> B ) = ( x e. X |-> [_ W / k ]_ B ) )
57 56 eleq1d 
 |-  ( k = W -> ( ( x e. X |-> B ) e. ( J Cn K ) <-> ( x e. X |-> [_ W / k ]_ B ) e. ( J Cn K ) ) )
58 55 57 imbi12d 
 |-  ( k = W -> ( ( ( ph /\ k e. A ) -> ( x e. X |-> B ) e. ( J Cn K ) ) <-> ( ( ph /\ W e. A ) -> ( x e. X |-> [_ W / k ]_ B ) e. ( J Cn K ) ) ) )
59 5 idi 
 |-  ( ( ph /\ k e. A ) -> ( x e. X |-> B ) e. ( J Cn K ) )
60 34 54 58 59 vtoclgf 
 |-  ( W e. A -> ( ( ph /\ W e. A ) -> ( x e. X |-> [_ W / k ]_ B ) e. ( J Cn K ) ) )
61 60 anabsi7 
 |-  ( ( ph /\ W e. A ) -> ( x e. X |-> [_ W / k ]_ B ) e. ( J Cn K ) )
62 48 61 mpdan 
 |-  ( ph -> ( x e. X |-> [_ W / k ]_ B ) e. ( J Cn K ) )
63 2 mulcn 
 |-  x. e. ( ( K tX K ) Cn K )
64 63 a1i 
 |-  ( ph -> x. e. ( ( K tX K ) Cn K ) )
65 3 8 62 64 cnmpt12f 
 |-  ( ph -> ( x e. X |-> ( prod_ k e. Z B x. [_ W / k ]_ B ) ) e. ( J Cn K ) )
66 47 65 eqeltrd 
 |-  ( ph -> ( x e. X |-> prod_ k e. ( Z u. { W } ) B ) e. ( J Cn K ) )