This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝑆 ) )