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→ ℂ ) )