Theorem xkofvcn

Description: Joint continuity of the function value operation as a function on continuous function spaces. (Compare xkopjcn .) (Contributed by Mario Carneiro, 20-Mar-2015) (Revised by Mario Carneiro, 22-Aug-2015)

	Ref	Expression
Hypotheses	xkofvcn.1	⊢ 𝑋 = ∪ 𝑅
	xkofvcn.2	⊢ 𝐹 = ( 𝑓 ∈ ( 𝑅 Cn 𝑆 ) , 𝑥 ∈ 𝑋 ↦ ( 𝑓 ‘ 𝑥 ) )
Assertion	xkofvcn	⊢ ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ Top ) → 𝐹 ∈ ( ( ( 𝑆 ↑ko 𝑅 ) ×t 𝑅 ) Cn 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		xkofvcn.1	⊢ 𝑋 = ∪ 𝑅
2		xkofvcn.2	⊢ 𝐹 = ( 𝑓 ∈ ( 𝑅 Cn 𝑆 ) , 𝑥 ∈ 𝑋 ↦ ( 𝑓 ‘ 𝑥 ) )
3		nllytop	⊢ ( 𝑅 ∈ 𝑛-Locally Comp → 𝑅 ∈ Top )
4		eqid	⊢ ( 𝑆 ↑ko 𝑅 ) = ( 𝑆 ↑ko 𝑅 )
5	4	xkotopon	⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → ( 𝑆 ↑ko 𝑅 ) ∈ ( TopOn ‘ ( 𝑅 Cn 𝑆 ) ) )
6	3 5	sylan	⊢ ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ Top ) → ( 𝑆 ↑ko 𝑅 ) ∈ ( TopOn ‘ ( 𝑅 Cn 𝑆 ) ) )
7	3	adantr	⊢ ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ Top ) → 𝑅 ∈ Top )
8	1	toptopon	⊢ ( 𝑅 ∈ Top ↔ 𝑅 ∈ ( TopOn ‘ 𝑋 ) )
9	7 8	sylib	⊢ ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ Top ) → 𝑅 ∈ ( TopOn ‘ 𝑋 ) )
10	6 9	cnmpt1st	⊢ ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ Top ) → ( 𝑓 ∈ ( 𝑅 Cn 𝑆 ) , 𝑥 ∈ 𝑋 ↦ 𝑓 ) ∈ ( ( ( 𝑆 ↑ko 𝑅 ) ×t 𝑅 ) Cn ( 𝑆 ↑ko 𝑅 ) ) )
11	6 9	cnmpt2nd	⊢ ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ Top ) → ( 𝑓 ∈ ( 𝑅 Cn 𝑆 ) , 𝑥 ∈ 𝑋 ↦ 𝑥 ) ∈ ( ( ( 𝑆 ↑ko 𝑅 ) ×t 𝑅 ) Cn 𝑅 ) )
12		1on	⊢ 1o ∈ On
13		distopon	⊢ ( 1o ∈ On → 𝒫 1o ∈ ( TopOn ‘ 1o ) )
14	12 13	mp1i	⊢ ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ Top ) → 𝒫 1o ∈ ( TopOn ‘ 1o ) )
15		xkoccn	⊢ ( ( 𝒫 1o ∈ ( TopOn ‘ 1o ) ∧ 𝑅 ∈ ( TopOn ‘ 𝑋 ) ) → ( 𝑦 ∈ 𝑋 ↦ ( 1o × { 𝑦 } ) ) ∈ ( 𝑅 Cn ( 𝑅 ↑ko 𝒫 1o ) ) )
16	14 9 15	syl2anc	⊢ ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ Top ) → ( 𝑦 ∈ 𝑋 ↦ ( 1o × { 𝑦 } ) ) ∈ ( 𝑅 Cn ( 𝑅 ↑ko 𝒫 1o ) ) )
17		sneq	⊢ ( 𝑦 = 𝑥 → { 𝑦 } = { 𝑥 } )
18	17	xpeq2d	⊢ ( 𝑦 = 𝑥 → ( 1o × { 𝑦 } ) = ( 1o × { 𝑥 } ) )
19	6 9 11 9 16 18	cnmpt21	⊢ ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ Top ) → ( 𝑓 ∈ ( 𝑅 Cn 𝑆 ) , 𝑥 ∈ 𝑋 ↦ ( 1o × { 𝑥 } ) ) ∈ ( ( ( 𝑆 ↑ko 𝑅 ) ×t 𝑅 ) Cn ( 𝑅 ↑ko 𝒫 1o ) ) )
20		distop	⊢ ( 1o ∈ On → 𝒫 1o ∈ Top )
21	12 20	mp1i	⊢ ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ Top ) → 𝒫 1o ∈ Top )
22		eqid	⊢ ( 𝑅 ↑ko 𝒫 1o ) = ( 𝑅 ↑ko 𝒫 1o )
23	22	xkotopon	⊢ ( ( 𝒫 1o ∈ Top ∧ 𝑅 ∈ Top ) → ( 𝑅 ↑ko 𝒫 1o ) ∈ ( TopOn ‘ ( 𝒫 1o Cn 𝑅 ) ) )
24	21 7 23	syl2anc	⊢ ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ Top ) → ( 𝑅 ↑ko 𝒫 1o ) ∈ ( TopOn ‘ ( 𝒫 1o Cn 𝑅 ) ) )
25		simpl	⊢ ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ Top ) → 𝑅 ∈ 𝑛-Locally Comp )
26		simpr	⊢ ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ Top ) → 𝑆 ∈ Top )
27		eqid	⊢ ( 𝑔 ∈ ( 𝑅 Cn 𝑆 ) , ℎ ∈ ( 𝒫 1o Cn 𝑅 ) ↦ ( 𝑔 ∘ ℎ ) ) = ( 𝑔 ∈ ( 𝑅 Cn 𝑆 ) , ℎ ∈ ( 𝒫 1o Cn 𝑅 ) ↦ ( 𝑔 ∘ ℎ ) )
28	27	xkococn	⊢ ( ( 𝒫 1o ∈ Top ∧ 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ Top ) → ( 𝑔 ∈ ( 𝑅 Cn 𝑆 ) , ℎ ∈ ( 𝒫 1o Cn 𝑅 ) ↦ ( 𝑔 ∘ ℎ ) ) ∈ ( ( ( 𝑆 ↑ko 𝑅 ) ×t ( 𝑅 ↑ko 𝒫 1o ) ) Cn ( 𝑆 ↑ko 𝒫 1o ) ) )
29	21 25 26 28	syl3anc	⊢ ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ Top ) → ( 𝑔 ∈ ( 𝑅 Cn 𝑆 ) , ℎ ∈ ( 𝒫 1o Cn 𝑅 ) ↦ ( 𝑔 ∘ ℎ ) ) ∈ ( ( ( 𝑆 ↑ko 𝑅 ) ×t ( 𝑅 ↑ko 𝒫 1o ) ) Cn ( 𝑆 ↑ko 𝒫 1o ) ) )
30		coeq1	⊢ ( 𝑔 = 𝑓 → ( 𝑔 ∘ ℎ ) = ( 𝑓 ∘ ℎ ) )
31		coeq2	⊢ ( ℎ = ( 1o × { 𝑥 } ) → ( 𝑓 ∘ ℎ ) = ( 𝑓 ∘ ( 1o × { 𝑥 } ) ) )
32	30 31	sylan9eq	⊢ ( ( 𝑔 = 𝑓 ∧ ℎ = ( 1o × { 𝑥 } ) ) → ( 𝑔 ∘ ℎ ) = ( 𝑓 ∘ ( 1o × { 𝑥 } ) ) )
33	6 9 10 19 6 24 29 32	cnmpt22	⊢ ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ Top ) → ( 𝑓 ∈ ( 𝑅 Cn 𝑆 ) , 𝑥 ∈ 𝑋 ↦ ( 𝑓 ∘ ( 1o × { 𝑥 } ) ) ) ∈ ( ( ( 𝑆 ↑ko 𝑅 ) ×t 𝑅 ) Cn ( 𝑆 ↑ko 𝒫 1o ) ) )
34		eqid	⊢ ( 𝑆 ↑ko 𝒫 1o ) = ( 𝑆 ↑ko 𝒫 1o )
35	34	xkotopon	⊢ ( ( 𝒫 1o ∈ Top ∧ 𝑆 ∈ Top ) → ( 𝑆 ↑ko 𝒫 1o ) ∈ ( TopOn ‘ ( 𝒫 1o Cn 𝑆 ) ) )
36	21 26 35	syl2anc	⊢ ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ Top ) → ( 𝑆 ↑ko 𝒫 1o ) ∈ ( TopOn ‘ ( 𝒫 1o Cn 𝑆 ) ) )
37		0lt1o	⊢ ∅ ∈ 1o
38	37	a1i	⊢ ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ Top ) → ∅ ∈ 1o )
39		unipw	⊢ ∪ 𝒫 1o = 1o
40	39	eqcomi	⊢ 1o = ∪ 𝒫 1o
41	40	xkopjcn	⊢ ( ( 𝒫 1o ∈ Top ∧ 𝑆 ∈ Top ∧ ∅ ∈ 1o ) → ( 𝑔 ∈ ( 𝒫 1o Cn 𝑆 ) ↦ ( 𝑔 ‘ ∅ ) ) ∈ ( ( 𝑆 ↑ko 𝒫 1o ) Cn 𝑆 ) )
42	21 26 38 41	syl3anc	⊢ ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ Top ) → ( 𝑔 ∈ ( 𝒫 1o Cn 𝑆 ) ↦ ( 𝑔 ‘ ∅ ) ) ∈ ( ( 𝑆 ↑ko 𝒫 1o ) Cn 𝑆 ) )
43		fveq1	⊢ ( 𝑔 = ( 𝑓 ∘ ( 1o × { 𝑥 } ) ) → ( 𝑔 ‘ ∅ ) = ( ( 𝑓 ∘ ( 1o × { 𝑥 } ) ) ‘ ∅ ) )
44		vex	⊢ 𝑥 ∈ V
45	44	fconst	⊢ ( 1o × { 𝑥 } ) : 1o ⟶ { 𝑥 }
46		fvco3	⊢ ( ( ( 1o × { 𝑥 } ) : 1o ⟶ { 𝑥 } ∧ ∅ ∈ 1o ) → ( ( 𝑓 ∘ ( 1o × { 𝑥 } ) ) ‘ ∅ ) = ( 𝑓 ‘ ( ( 1o × { 𝑥 } ) ‘ ∅ ) ) )
47	45 37 46	mp2an	⊢ ( ( 𝑓 ∘ ( 1o × { 𝑥 } ) ) ‘ ∅ ) = ( 𝑓 ‘ ( ( 1o × { 𝑥 } ) ‘ ∅ ) )
48	44	fvconst2	⊢ ( ∅ ∈ 1o → ( ( 1o × { 𝑥 } ) ‘ ∅ ) = 𝑥 )
49	37 48	ax-mp	⊢ ( ( 1o × { 𝑥 } ) ‘ ∅ ) = 𝑥
50	49	fveq2i	⊢ ( 𝑓 ‘ ( ( 1o × { 𝑥 } ) ‘ ∅ ) ) = ( 𝑓 ‘ 𝑥 )
51	47 50	eqtri	⊢ ( ( 𝑓 ∘ ( 1o × { 𝑥 } ) ) ‘ ∅ ) = ( 𝑓 ‘ 𝑥 )
52	43 51	eqtrdi	⊢ ( 𝑔 = ( 𝑓 ∘ ( 1o × { 𝑥 } ) ) → ( 𝑔 ‘ ∅ ) = ( 𝑓 ‘ 𝑥 ) )
53	6 9 33 36 42 52	cnmpt21	⊢ ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ Top ) → ( 𝑓 ∈ ( 𝑅 Cn 𝑆 ) , 𝑥 ∈ 𝑋 ↦ ( 𝑓 ‘ 𝑥 ) ) ∈ ( ( ( 𝑆 ↑ko 𝑅 ) ×t 𝑅 ) Cn 𝑆 ) )
54	2 53	eqeltrid	⊢ ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ Top ) → 𝐹 ∈ ( ( ( 𝑆 ↑ko 𝑅 ) ×t 𝑅 ) Cn 𝑆 ) )