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) Avoid ax-mulf . (Revised by GG, 19-Apr-2025)

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 nfv 
 |-  F/ k W e. A
34 10 33 nfan 
 |-  F/ k ( ( ph /\ x e. X ) /\ W e. A )
35 11 nfel1 
 |-  F/ k [_ W / k ]_ B e. CC
36 34 35 nfim 
 |-  F/ k ( ( ( ph /\ x e. X ) /\ W e. A ) -> [_ W / k ]_ B e. CC )
37 eleq1 
 |-  ( k = W -> ( k e. A <-> W e. A ) )
38 37 anbi2d 
 |-  ( k = W -> ( ( ( ph /\ x e. X ) /\ k e. A ) <-> ( ( ph /\ x e. X ) /\ W e. A ) ) )
39 31 eleq1d 
 |-  ( k = W -> ( B e. CC <-> [_ W / k ]_ B e. CC ) )
40 38 39 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 ) ) )
41 36 40 29 vtoclg1f 
 |-  ( W e. A -> ( ( ( ph /\ x e. X ) /\ W e. A ) -> [_ W / k ]_ B e. CC ) )
42 41 anabsi7 
 |-  ( ( ( ph /\ x e. X ) /\ W e. A ) -> [_ W / k ]_ B e. CC )
43 32 42 mpdan 
 |-  ( ( ph /\ x e. X ) -> [_ W / k ]_ B e. CC )
44 10 11 13 14 15 30 31 43 fprodsplitsn 
 |-  ( ( ph /\ x e. X ) -> prod_ k e. ( Z u. { W } ) B = ( prod_ k e. Z B x. [_ W / k ]_ B ) )
45 44 mpteq2dva 
 |-  ( ph -> ( x e. X |-> prod_ k e. ( Z u. { W } ) B ) = ( x e. X |-> ( prod_ k e. Z B x. [_ W / k ]_ B ) ) )
46 7 eldifad 
 |-  ( ph -> W e. A )
47 1 33 nfan 
 |-  F/ k ( ph /\ W e. A )
48 nfcv 
 |-  F/_ k X
49 48 11 nfmpt 
 |-  F/_ k ( x e. X |-> [_ W / k ]_ B )
50 49 nfel1 
 |-  F/ k ( x e. X |-> [_ W / k ]_ B ) e. ( J Cn K )
51 47 50 nfim 
 |-  F/ k ( ( ph /\ W e. A ) -> ( x e. X |-> [_ W / k ]_ B ) e. ( J Cn K ) )
52 37 anbi2d 
 |-  ( k = W -> ( ( ph /\ k e. A ) <-> ( ph /\ W e. A ) ) )
53 31 mpteq2dv 
 |-  ( k = W -> ( x e. X |-> B ) = ( x e. X |-> [_ W / k ]_ B ) )
54 53 eleq1d 
 |-  ( k = W -> ( ( x e. X |-> B ) e. ( J Cn K ) <-> ( x e. X |-> [_ W / k ]_ B ) e. ( J Cn K ) ) )
55 52 54 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 ) ) ) )
56 51 55 5 vtoclg1f 
 |-  ( W e. A -> ( ( ph /\ W e. A ) -> ( x e. X |-> [_ W / k ]_ B ) e. ( J Cn K ) ) )
57 56 anabsi7 
 |-  ( ( ph /\ W e. A ) -> ( x e. X |-> [_ W / k ]_ B ) e. ( J Cn K ) )
58 46 57 mpdan 
 |-  ( ph -> ( x e. X |-> [_ W / k ]_ B ) e. ( J Cn K ) )
59 19 a1i 
 |-  ( ph -> K e. ( TopOn ` CC ) )
60 2 mpomulcn 
 |-  ( u e. CC , v e. CC |-> ( u x. v ) ) e. ( ( K tX K ) Cn K )
61 60 a1i 
 |-  ( ph -> ( u e. CC , v e. CC |-> ( u x. v ) ) e. ( ( K tX K ) Cn K ) )
62 oveq12 
 |-  ( ( u = prod_ k e. Z B /\ v = [_ W / k ]_ B ) -> ( u x. v ) = ( prod_ k e. Z B x. [_ W / k ]_ B ) )
63 3 8 58 59 59 61 62 cnmpt12 
 |-  ( ph -> ( x e. X |-> ( prod_ k e. Z B x. [_ W / k ]_ B ) ) e. ( J Cn K ) )
64 45 63 eqeltrd 
 |-  ( ph -> ( x e. X |-> prod_ k e. ( Z u. { W } ) B ) e. ( J Cn K ) )