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 ⊢ ( 𝜑 → 𝐴 ⊆ ℂ )
fprodcncf.b ⊢ ( 𝜑 → 𝐵 ∈ Fin )
fprodcncf.c ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ) → 𝐶 ∈ ℂ )
fprodcncf.cn ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ ( 𝐴 –cn→ ℂ ) )
Assertion fprodcncf ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ∏ 𝑘 ∈ 𝐵 𝐶 ) ∈ ( 𝐴 –cn→ ℂ ) )

Proof

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