Metamath Proof Explorer

Theorem xpstopnlem2

Description: Lemma for xpstopn . (Contributed by Mario Carneiro, 27-Aug-2015)

Ref Expression
Hypotheses xpstps.t ${⊢}{T}={R}{×}_{𝑠}{S}$
xpstopn.j ${⊢}{J}=\mathrm{TopOpen}\left({R}\right)$
xpstopn.k ${⊢}{K}=\mathrm{TopOpen}\left({S}\right)$
xpstopn.o ${⊢}{O}=\mathrm{TopOpen}\left({T}\right)$
xpstopnlem.x ${⊢}{X}={\mathrm{Base}}_{{R}}$
xpstopnlem.y ${⊢}{Y}={\mathrm{Base}}_{{S}}$
xpstopnlem.f ${⊢}{F}=\left({x}\in {X},{y}\in {Y}⟼\left\{⟨\varnothing ,{x}⟩,⟨{1}_{𝑜},{y}⟩\right\}\right)$
Assertion xpstopnlem2 ${⊢}\left({R}\in \mathrm{TopSp}\wedge {S}\in \mathrm{TopSp}\right)\to {O}={J}{×}_{t}{K}$

Proof

Step Hyp Ref Expression
1 xpstps.t ${⊢}{T}={R}{×}_{𝑠}{S}$
2 xpstopn.j ${⊢}{J}=\mathrm{TopOpen}\left({R}\right)$
3 xpstopn.k ${⊢}{K}=\mathrm{TopOpen}\left({S}\right)$
4 xpstopn.o ${⊢}{O}=\mathrm{TopOpen}\left({T}\right)$
5 xpstopnlem.x ${⊢}{X}={\mathrm{Base}}_{{R}}$
6 xpstopnlem.y ${⊢}{Y}={\mathrm{Base}}_{{S}}$
7 xpstopnlem.f ${⊢}{F}=\left({x}\in {X},{y}\in {Y}⟼\left\{⟨\varnothing ,{x}⟩,⟨{1}_{𝑜},{y}⟩\right\}\right)$
8 eqid ${⊢}\mathrm{Scalar}\left({R}\right){⨉}_{𝑠}\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}=\mathrm{Scalar}\left({R}\right){⨉}_{𝑠}\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}$
9 fvexd ${⊢}\left({R}\in \mathrm{TopSp}\wedge {S}\in \mathrm{TopSp}\right)\to \mathrm{Scalar}\left({R}\right)\in \mathrm{V}$
10 2on ${⊢}{2}_{𝑜}\in \mathrm{On}$
11 10 a1i ${⊢}\left({R}\in \mathrm{TopSp}\wedge {S}\in \mathrm{TopSp}\right)\to {2}_{𝑜}\in \mathrm{On}$
12 fnpr2o ${⊢}\left({R}\in \mathrm{TopSp}\wedge {S}\in \mathrm{TopSp}\right)\to \left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}Fn{2}_{𝑜}$
13 eqid ${⊢}\mathrm{TopOpen}\left(\mathrm{Scalar}\left({R}\right){⨉}_{𝑠}\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\right)=\mathrm{TopOpen}\left(\mathrm{Scalar}\left({R}\right){⨉}_{𝑠}\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\right)$
14 8 9 11 12 13 prdstopn ${⊢}\left({R}\in \mathrm{TopSp}\wedge {S}\in \mathrm{TopSp}\right)\to \mathrm{TopOpen}\left(\mathrm{Scalar}\left({R}\right){⨉}_{𝑠}\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\right)={\prod }_{𝑡}\left(\mathrm{TopOpen}\circ \left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\right)$
15 topnfn ${⊢}\mathrm{TopOpen}Fn\mathrm{V}$
16 dffn2 ${⊢}\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}Fn{2}_{𝑜}↔\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}:{2}_{𝑜}⟶\mathrm{V}$
17 12 16 sylib ${⊢}\left({R}\in \mathrm{TopSp}\wedge {S}\in \mathrm{TopSp}\right)\to \left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}:{2}_{𝑜}⟶\mathrm{V}$
18 fnfco ${⊢}\left(\mathrm{TopOpen}Fn\mathrm{V}\wedge \left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}:{2}_{𝑜}⟶\mathrm{V}\right)\to \left(\mathrm{TopOpen}\circ \left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\right)Fn{2}_{𝑜}$
19 15 17 18 sylancr ${⊢}\left({R}\in \mathrm{TopSp}\wedge {S}\in \mathrm{TopSp}\right)\to \left(\mathrm{TopOpen}\circ \left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\right)Fn{2}_{𝑜}$
20 xpsfeq ${⊢}\left(\mathrm{TopOpen}\circ \left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\right)Fn{2}_{𝑜}\to \left\{⟨\varnothing ,\left(\mathrm{TopOpen}\circ \left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\right)\left(\varnothing \right)⟩,⟨{1}_{𝑜},\left(\mathrm{TopOpen}\circ \left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\right)\left({1}_{𝑜}\right)⟩\right\}=\mathrm{TopOpen}\circ \left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}$
21 19 20 syl ${⊢}\left({R}\in \mathrm{TopSp}\wedge {S}\in \mathrm{TopSp}\right)\to \left\{⟨\varnothing ,\left(\mathrm{TopOpen}\circ \left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\right)\left(\varnothing \right)⟩,⟨{1}_{𝑜},\left(\mathrm{TopOpen}\circ \left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\right)\left({1}_{𝑜}\right)⟩\right\}=\mathrm{TopOpen}\circ \left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}$
22 0ex ${⊢}\varnothing \in \mathrm{V}$
23 22 prid1 ${⊢}\varnothing \in \left\{\varnothing ,{1}_{𝑜}\right\}$
24 df2o3 ${⊢}{2}_{𝑜}=\left\{\varnothing ,{1}_{𝑜}\right\}$
25 23 24 eleqtrri ${⊢}\varnothing \in {2}_{𝑜}$
26 fvco2 ${⊢}\left(\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}Fn{2}_{𝑜}\wedge \varnothing \in {2}_{𝑜}\right)\to \left(\mathrm{TopOpen}\circ \left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\right)\left(\varnothing \right)=\mathrm{TopOpen}\left(\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\left(\varnothing \right)\right)$
27 12 25 26 sylancl ${⊢}\left({R}\in \mathrm{TopSp}\wedge {S}\in \mathrm{TopSp}\right)\to \left(\mathrm{TopOpen}\circ \left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\right)\left(\varnothing \right)=\mathrm{TopOpen}\left(\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\left(\varnothing \right)\right)$
28 fvpr0o ${⊢}{R}\in \mathrm{TopSp}\to \left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\left(\varnothing \right)={R}$
29 28 adantr ${⊢}\left({R}\in \mathrm{TopSp}\wedge {S}\in \mathrm{TopSp}\right)\to \left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\left(\varnothing \right)={R}$
30 29 fveq2d ${⊢}\left({R}\in \mathrm{TopSp}\wedge {S}\in \mathrm{TopSp}\right)\to \mathrm{TopOpen}\left(\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\left(\varnothing \right)\right)=\mathrm{TopOpen}\left({R}\right)$
31 30 2 syl6eqr ${⊢}\left({R}\in \mathrm{TopSp}\wedge {S}\in \mathrm{TopSp}\right)\to \mathrm{TopOpen}\left(\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\left(\varnothing \right)\right)={J}$
32 27 31 eqtrd ${⊢}\left({R}\in \mathrm{TopSp}\wedge {S}\in \mathrm{TopSp}\right)\to \left(\mathrm{TopOpen}\circ \left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\right)\left(\varnothing \right)={J}$
33 32 opeq2d ${⊢}\left({R}\in \mathrm{TopSp}\wedge {S}\in \mathrm{TopSp}\right)\to ⟨\varnothing ,\left(\mathrm{TopOpen}\circ \left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\right)\left(\varnothing \right)⟩=⟨\varnothing ,{J}⟩$
34 1oex ${⊢}{1}_{𝑜}\in \mathrm{V}$
35 34 prid2 ${⊢}{1}_{𝑜}\in \left\{\varnothing ,{1}_{𝑜}\right\}$
36 35 24 eleqtrri ${⊢}{1}_{𝑜}\in {2}_{𝑜}$
37 fvco2 ${⊢}\left(\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}Fn{2}_{𝑜}\wedge {1}_{𝑜}\in {2}_{𝑜}\right)\to \left(\mathrm{TopOpen}\circ \left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\right)\left({1}_{𝑜}\right)=\mathrm{TopOpen}\left(\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\left({1}_{𝑜}\right)\right)$
38 12 36 37 sylancl ${⊢}\left({R}\in \mathrm{TopSp}\wedge {S}\in \mathrm{TopSp}\right)\to \left(\mathrm{TopOpen}\circ \left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\right)\left({1}_{𝑜}\right)=\mathrm{TopOpen}\left(\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\left({1}_{𝑜}\right)\right)$
39 fvpr1o ${⊢}{S}\in \mathrm{TopSp}\to \left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\left({1}_{𝑜}\right)={S}$
40 39 adantl ${⊢}\left({R}\in \mathrm{TopSp}\wedge {S}\in \mathrm{TopSp}\right)\to \left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\left({1}_{𝑜}\right)={S}$
41 40 fveq2d ${⊢}\left({R}\in \mathrm{TopSp}\wedge {S}\in \mathrm{TopSp}\right)\to \mathrm{TopOpen}\left(\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\left({1}_{𝑜}\right)\right)=\mathrm{TopOpen}\left({S}\right)$
42 41 3 syl6eqr ${⊢}\left({R}\in \mathrm{TopSp}\wedge {S}\in \mathrm{TopSp}\right)\to \mathrm{TopOpen}\left(\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\left({1}_{𝑜}\right)\right)={K}$
43 38 42 eqtrd ${⊢}\left({R}\in \mathrm{TopSp}\wedge {S}\in \mathrm{TopSp}\right)\to \left(\mathrm{TopOpen}\circ \left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\right)\left({1}_{𝑜}\right)={K}$
44 43 opeq2d ${⊢}\left({R}\in \mathrm{TopSp}\wedge {S}\in \mathrm{TopSp}\right)\to ⟨{1}_{𝑜},\left(\mathrm{TopOpen}\circ \left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\right)\left({1}_{𝑜}\right)⟩=⟨{1}_{𝑜},{K}⟩$
45 33 44 preq12d ${⊢}\left({R}\in \mathrm{TopSp}\wedge {S}\in \mathrm{TopSp}\right)\to \left\{⟨\varnothing ,\left(\mathrm{TopOpen}\circ \left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\right)\left(\varnothing \right)⟩,⟨{1}_{𝑜},\left(\mathrm{TopOpen}\circ \left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\right)\left({1}_{𝑜}\right)⟩\right\}=\left\{⟨\varnothing ,{J}⟩,⟨{1}_{𝑜},{K}⟩\right\}$
46 21 45 eqtr3d ${⊢}\left({R}\in \mathrm{TopSp}\wedge {S}\in \mathrm{TopSp}\right)\to \mathrm{TopOpen}\circ \left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}=\left\{⟨\varnothing ,{J}⟩,⟨{1}_{𝑜},{K}⟩\right\}$
47 46 fveq2d ${⊢}\left({R}\in \mathrm{TopSp}\wedge {S}\in \mathrm{TopSp}\right)\to {\prod }_{𝑡}\left(\mathrm{TopOpen}\circ \left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\right)={\prod }_{𝑡}\left(\left\{⟨\varnothing ,{J}⟩,⟨{1}_{𝑜},{K}⟩\right\}\right)$
48 14 47 eqtrd ${⊢}\left({R}\in \mathrm{TopSp}\wedge {S}\in \mathrm{TopSp}\right)\to \mathrm{TopOpen}\left(\mathrm{Scalar}\left({R}\right){⨉}_{𝑠}\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\right)={\prod }_{𝑡}\left(\left\{⟨\varnothing ,{J}⟩,⟨{1}_{𝑜},{K}⟩\right\}\right)$
49 48 oveq1d ${⊢}\left({R}\in \mathrm{TopSp}\wedge {S}\in \mathrm{TopSp}\right)\to \mathrm{TopOpen}\left(\mathrm{Scalar}\left({R}\right){⨉}_{𝑠}\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\right)\mathrm{qTop}{{F}}^{-1}={\prod }_{𝑡}\left(\left\{⟨\varnothing ,{J}⟩,⟨{1}_{𝑜},{K}⟩\right\}\right)\mathrm{qTop}{{F}}^{-1}$
50 simpl ${⊢}\left({R}\in \mathrm{TopSp}\wedge {S}\in \mathrm{TopSp}\right)\to {R}\in \mathrm{TopSp}$
51 simpr ${⊢}\left({R}\in \mathrm{TopSp}\wedge {S}\in \mathrm{TopSp}\right)\to {S}\in \mathrm{TopSp}$
52 eqid ${⊢}\mathrm{Scalar}\left({R}\right)=\mathrm{Scalar}\left({R}\right)$
53 1 5 6 50 51 7 52 8 xpsval ${⊢}\left({R}\in \mathrm{TopSp}\wedge {S}\in \mathrm{TopSp}\right)\to {T}={{F}}^{-1}{“}_{𝑠}\left(\mathrm{Scalar}\left({R}\right){⨉}_{𝑠}\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\right)$
54 1 5 6 50 51 7 52 8 xpsrnbas ${⊢}\left({R}\in \mathrm{TopSp}\wedge {S}\in \mathrm{TopSp}\right)\to \mathrm{ran}{F}={\mathrm{Base}}_{\left(\mathrm{Scalar}\left({R}\right){⨉}_{𝑠}\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\right)}$
55 7 xpsff1o2 ${⊢}{F}:{X}×{Y}\underset{1-1 onto}{⟶}\mathrm{ran}{F}$
56 f1ocnv ${⊢}{F}:{X}×{Y}\underset{1-1 onto}{⟶}\mathrm{ran}{F}\to {{F}}^{-1}:\mathrm{ran}{F}\underset{1-1 onto}{⟶}{X}×{Y}$
57 55 56 mp1i ${⊢}\left({R}\in \mathrm{TopSp}\wedge {S}\in \mathrm{TopSp}\right)\to {{F}}^{-1}:\mathrm{ran}{F}\underset{1-1 onto}{⟶}{X}×{Y}$
58 f1ofo ${⊢}{{F}}^{-1}:\mathrm{ran}{F}\underset{1-1 onto}{⟶}{X}×{Y}\to {{F}}^{-1}:\mathrm{ran}{F}\underset{onto}{⟶}{X}×{Y}$
59 57 58 syl ${⊢}\left({R}\in \mathrm{TopSp}\wedge {S}\in \mathrm{TopSp}\right)\to {{F}}^{-1}:\mathrm{ran}{F}\underset{onto}{⟶}{X}×{Y}$
60 ovexd ${⊢}\left({R}\in \mathrm{TopSp}\wedge {S}\in \mathrm{TopSp}\right)\to \mathrm{Scalar}\left({R}\right){⨉}_{𝑠}\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\in \mathrm{V}$
61 53 54 59 60 13 4 imastopn ${⊢}\left({R}\in \mathrm{TopSp}\wedge {S}\in \mathrm{TopSp}\right)\to {O}=\mathrm{TopOpen}\left(\mathrm{Scalar}\left({R}\right){⨉}_{𝑠}\left\{⟨\varnothing ,{R}⟩,⟨{1}_{𝑜},{S}⟩\right\}\right)\mathrm{qTop}{{F}}^{-1}$
62 5 2 istps ${⊢}{R}\in \mathrm{TopSp}↔{J}\in \mathrm{TopOn}\left({X}\right)$
63 50 62 sylib ${⊢}\left({R}\in \mathrm{TopSp}\wedge {S}\in \mathrm{TopSp}\right)\to {J}\in \mathrm{TopOn}\left({X}\right)$
64 6 3 istps ${⊢}{S}\in \mathrm{TopSp}↔{K}\in \mathrm{TopOn}\left({Y}\right)$
65 51 64 sylib ${⊢}\left({R}\in \mathrm{TopSp}\wedge {S}\in \mathrm{TopSp}\right)\to {K}\in \mathrm{TopOn}\left({Y}\right)$
66 7 63 65 xpstopnlem1 ${⊢}\left({R}\in \mathrm{TopSp}\wedge {S}\in \mathrm{TopSp}\right)\to {F}\in \left(\left({J}{×}_{t}{K}\right)\mathrm{Homeo}{\prod }_{𝑡}\left(\left\{⟨\varnothing ,{J}⟩,⟨{1}_{𝑜},{K}⟩\right\}\right)\right)$
67 hmeocnv ${⊢}{F}\in \left(\left({J}{×}_{t}{K}\right)\mathrm{Homeo}{\prod }_{𝑡}\left(\left\{⟨\varnothing ,{J}⟩,⟨{1}_{𝑜},{K}⟩\right\}\right)\right)\to {{F}}^{-1}\in \left({\prod }_{𝑡}\left(\left\{⟨\varnothing ,{J}⟩,⟨{1}_{𝑜},{K}⟩\right\}\right)\mathrm{Homeo}\left({J}{×}_{t}{K}\right)\right)$
68 hmeoqtop ${⊢}{{F}}^{-1}\in \left({\prod }_{𝑡}\left(\left\{⟨\varnothing ,{J}⟩,⟨{1}_{𝑜},{K}⟩\right\}\right)\mathrm{Homeo}\left({J}{×}_{t}{K}\right)\right)\to {J}{×}_{t}{K}={\prod }_{𝑡}\left(\left\{⟨\varnothing ,{J}⟩,⟨{1}_{𝑜},{K}⟩\right\}\right)\mathrm{qTop}{{F}}^{-1}$
69 66 67 68 3syl ${⊢}\left({R}\in \mathrm{TopSp}\wedge {S}\in \mathrm{TopSp}\right)\to {J}{×}_{t}{K}={\prod }_{𝑡}\left(\left\{⟨\varnothing ,{J}⟩,⟨{1}_{𝑜},{K}⟩\right\}\right)\mathrm{qTop}{{F}}^{-1}$
70 49 61 69 3eqtr4d ${⊢}\left({R}\in \mathrm{TopSp}\wedge {S}\in \mathrm{TopSp}\right)\to {O}={J}{×}_{t}{K}$