MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  xpstopnlem2 Structured version   Visualization version   GIF version

Theorem xpstopnlem2 22354
Description: Lemma for xpstopn 22355. (Contributed by Mario Carneiro, 27-Aug-2015.)
Hypotheses
Ref Expression
xpstps.t 𝑇 = (𝑅 ×s 𝑆)
xpstopn.j 𝐽 = (TopOpen‘𝑅)
xpstopn.k 𝐾 = (TopOpen‘𝑆)
xpstopn.o 𝑂 = (TopOpen‘𝑇)
xpstopnlem.x 𝑋 = (Base‘𝑅)
xpstopnlem.y 𝑌 = (Base‘𝑆)
xpstopnlem.f 𝐹 = (𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})
Assertion
Ref Expression
xpstopnlem2 ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) → 𝑂 = (𝐽 ×t 𝐾))
Distinct variable groups:   𝑥,𝑦,𝐽   𝑥,𝐾,𝑦   𝑥,𝑅,𝑦   𝑥,𝑆,𝑦   𝑥,𝑋,𝑦   𝑥,𝑌,𝑦
Allowed substitution hints:   𝑇(𝑥,𝑦)   𝐹(𝑥,𝑦)   𝑂(𝑥,𝑦)

Proof of Theorem xpstopnlem2
StepHypRef Expression
1 eqid 2826 . . . . 5 ((Scalar‘𝑅)Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}) = ((Scalar‘𝑅)Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩})
2 fvexd 6684 . . . . 5 ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) → (Scalar‘𝑅) ∈ V)
3 2on 8107 . . . . . 6 2o ∈ On
43a1i 11 . . . . 5 ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) → 2o ∈ On)
5 fnpr2o 16825 . . . . 5 ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) → {⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩} Fn 2o)
6 eqid 2826 . . . . 5 (TopOpen‘((Scalar‘𝑅)Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩})) = (TopOpen‘((Scalar‘𝑅)Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}))
71, 2, 4, 5, 6prdstopn 22171 . . . 4 ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) → (TopOpen‘((Scalar‘𝑅)Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩})) = (∏t‘(TopOpen ∘ {⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩})))
8 topnfn 16694 . . . . . . . 8 TopOpen Fn V
9 dffn2 6515 . . . . . . . . 9 ({⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩} Fn 2o ↔ {⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}:2o⟶V)
105, 9sylib 219 . . . . . . . 8 ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) → {⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}:2o⟶V)
11 fnfco 6542 . . . . . . . 8 ((TopOpen Fn V ∧ {⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}:2o⟶V) → (TopOpen ∘ {⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}) Fn 2o)
128, 10, 11sylancr 587 . . . . . . 7 ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) → (TopOpen ∘ {⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}) Fn 2o)
13 xpsfeq 16831 . . . . . . 7 ((TopOpen ∘ {⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}) Fn 2o → {⟨∅, ((TopOpen ∘ {⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩})‘∅)⟩, ⟨1o, ((TopOpen ∘ {⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩})‘1o)⟩} = (TopOpen ∘ {⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}))
1412, 13syl 17 . . . . . 6 ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) → {⟨∅, ((TopOpen ∘ {⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩})‘∅)⟩, ⟨1o, ((TopOpen ∘ {⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩})‘1o)⟩} = (TopOpen ∘ {⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}))
15 0ex 5208 . . . . . . . . . . . 12 ∅ ∈ V
1615prid1 4697 . . . . . . . . . . 11 ∅ ∈ {∅, 1o}
17 df2o3 8113 . . . . . . . . . . 11 2o = {∅, 1o}
1816, 17eleqtrri 2917 . . . . . . . . . 10 ∅ ∈ 2o
19 fvco2 6757 . . . . . . . . . 10 (({⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩} Fn 2o ∧ ∅ ∈ 2o) → ((TopOpen ∘ {⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩})‘∅) = (TopOpen‘({⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}‘∅)))
205, 18, 19sylancl 586 . . . . . . . . 9 ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) → ((TopOpen ∘ {⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩})‘∅) = (TopOpen‘({⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}‘∅)))
21 fvpr0o 16827 . . . . . . . . . . . 12 (𝑅 ∈ TopSp → ({⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}‘∅) = 𝑅)
2221adantr 481 . . . . . . . . . . 11 ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) → ({⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}‘∅) = 𝑅)
2322fveq2d 6673 . . . . . . . . . 10 ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) → (TopOpen‘({⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}‘∅)) = (TopOpen‘𝑅))
24 xpstopn.j . . . . . . . . . 10 𝐽 = (TopOpen‘𝑅)
2523, 24syl6eqr 2879 . . . . . . . . 9 ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) → (TopOpen‘({⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}‘∅)) = 𝐽)
2620, 25eqtrd 2861 . . . . . . . 8 ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) → ((TopOpen ∘ {⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩})‘∅) = 𝐽)
2726opeq2d 4809 . . . . . . 7 ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) → ⟨∅, ((TopOpen ∘ {⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩})‘∅)⟩ = ⟨∅, 𝐽⟩)
28 1oex 8106 . . . . . . . . . . . 12 1o ∈ V
2928prid2 4698 . . . . . . . . . . 11 1o ∈ {∅, 1o}
3029, 17eleqtrri 2917 . . . . . . . . . 10 1o ∈ 2o
31 fvco2 6757 . . . . . . . . . 10 (({⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩} Fn 2o ∧ 1o ∈ 2o) → ((TopOpen ∘ {⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩})‘1o) = (TopOpen‘({⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}‘1o)))
325, 30, 31sylancl 586 . . . . . . . . 9 ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) → ((TopOpen ∘ {⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩})‘1o) = (TopOpen‘({⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}‘1o)))
33 fvpr1o 16828 . . . . . . . . . . . 12 (𝑆 ∈ TopSp → ({⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}‘1o) = 𝑆)
3433adantl 482 . . . . . . . . . . 11 ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) → ({⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}‘1o) = 𝑆)
3534fveq2d 6673 . . . . . . . . . 10 ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) → (TopOpen‘({⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}‘1o)) = (TopOpen‘𝑆))
36 xpstopn.k . . . . . . . . . 10 𝐾 = (TopOpen‘𝑆)
3735, 36syl6eqr 2879 . . . . . . . . 9 ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) → (TopOpen‘({⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}‘1o)) = 𝐾)
3832, 37eqtrd 2861 . . . . . . . 8 ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) → ((TopOpen ∘ {⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩})‘1o) = 𝐾)
3938opeq2d 4809 . . . . . . 7 ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) → ⟨1o, ((TopOpen ∘ {⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩})‘1o)⟩ = ⟨1o, 𝐾⟩)
4027, 39preq12d 4676 . . . . . 6 ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) → {⟨∅, ((TopOpen ∘ {⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩})‘∅)⟩, ⟨1o, ((TopOpen ∘ {⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩})‘1o)⟩} = {⟨∅, 𝐽⟩, ⟨1o, 𝐾⟩})
4114, 40eqtr3d 2863 . . . . 5 ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) → (TopOpen ∘ {⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}) = {⟨∅, 𝐽⟩, ⟨1o, 𝐾⟩})
4241fveq2d 6673 . . . 4 ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) → (∏t‘(TopOpen ∘ {⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩})) = (∏t‘{⟨∅, 𝐽⟩, ⟨1o, 𝐾⟩}))
437, 42eqtrd 2861 . . 3 ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) → (TopOpen‘((Scalar‘𝑅)Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩})) = (∏t‘{⟨∅, 𝐽⟩, ⟨1o, 𝐾⟩}))
4443oveq1d 7165 . 2 ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) → ((TopOpen‘((Scalar‘𝑅)Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩})) qTop 𝐹) = ((∏t‘{⟨∅, 𝐽⟩, ⟨1o, 𝐾⟩}) qTop 𝐹))
45 xpstps.t . . . 4 𝑇 = (𝑅 ×s 𝑆)
46 xpstopnlem.x . . . 4 𝑋 = (Base‘𝑅)
47 xpstopnlem.y . . . 4 𝑌 = (Base‘𝑆)
48 simpl 483 . . . 4 ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) → 𝑅 ∈ TopSp)
49 simpr 485 . . . 4 ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) → 𝑆 ∈ TopSp)
50 xpstopnlem.f . . . 4 𝐹 = (𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})
51 eqid 2826 . . . 4 (Scalar‘𝑅) = (Scalar‘𝑅)
5245, 46, 47, 48, 49, 50, 51, 1xpsval 16838 . . 3 ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) → 𝑇 = (𝐹s ((Scalar‘𝑅)Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩})))
5345, 46, 47, 48, 49, 50, 51, 1xpsrnbas 16839 . . 3 ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) → ran 𝐹 = (Base‘((Scalar‘𝑅)Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩})))
5450xpsff1o2 16837 . . . . 5 𝐹:(𝑋 × 𝑌)–1-1-onto→ran 𝐹
55 f1ocnv 6626 . . . . 5 (𝐹:(𝑋 × 𝑌)–1-1-onto→ran 𝐹𝐹:ran 𝐹1-1-onto→(𝑋 × 𝑌))
5654, 55mp1i 13 . . . 4 ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) → 𝐹:ran 𝐹1-1-onto→(𝑋 × 𝑌))
57 f1ofo 6621 . . . 4 (𝐹:ran 𝐹1-1-onto→(𝑋 × 𝑌) → 𝐹:ran 𝐹onto→(𝑋 × 𝑌))
5856, 57syl 17 . . 3 ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) → 𝐹:ran 𝐹onto→(𝑋 × 𝑌))
59 ovexd 7185 . . 3 ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) → ((Scalar‘𝑅)Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}) ∈ V)
60 xpstopn.o . . 3 𝑂 = (TopOpen‘𝑇)
6152, 53, 58, 59, 6, 60imastopn 22263 . 2 ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) → 𝑂 = ((TopOpen‘((Scalar‘𝑅)Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩})) qTop 𝐹))
6246, 24istps 21477 . . . . 5 (𝑅 ∈ TopSp ↔ 𝐽 ∈ (TopOn‘𝑋))
6348, 62sylib 219 . . . 4 ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) → 𝐽 ∈ (TopOn‘𝑋))
6447, 36istps 21477 . . . . 5 (𝑆 ∈ TopSp ↔ 𝐾 ∈ (TopOn‘𝑌))
6549, 64sylib 219 . . . 4 ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) → 𝐾 ∈ (TopOn‘𝑌))
6650, 63, 65xpstopnlem1 22352 . . 3 ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) → 𝐹 ∈ ((𝐽 ×t 𝐾)Homeo(∏t‘{⟨∅, 𝐽⟩, ⟨1o, 𝐾⟩})))
67 hmeocnv 22305 . . 3 (𝐹 ∈ ((𝐽 ×t 𝐾)Homeo(∏t‘{⟨∅, 𝐽⟩, ⟨1o, 𝐾⟩})) → 𝐹 ∈ ((∏t‘{⟨∅, 𝐽⟩, ⟨1o, 𝐾⟩})Homeo(𝐽 ×t 𝐾)))
68 hmeoqtop 22318 . . 3 (𝐹 ∈ ((∏t‘{⟨∅, 𝐽⟩, ⟨1o, 𝐾⟩})Homeo(𝐽 ×t 𝐾)) → (𝐽 ×t 𝐾) = ((∏t‘{⟨∅, 𝐽⟩, ⟨1o, 𝐾⟩}) qTop 𝐹))
6966, 67, 683syl 18 . 2 ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) → (𝐽 ×t 𝐾) = ((∏t‘{⟨∅, 𝐽⟩, ⟨1o, 𝐾⟩}) qTop 𝐹))
7044, 61, 693eqtr4d 2871 1 ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) → 𝑂 = (𝐽 ×t 𝐾))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1530  wcel 2107  Vcvv 3500  c0 4295  {cpr 4566  cop 4570   × cxp 5552  ccnv 5553  ran crn 5555  ccom 5558  Oncon0 6190   Fn wfn 6349  wf 6350  ontowfo 6352  1-1-ontowf1o 6353  cfv 6354  (class class class)co 7150  cmpo 7152  1oc1o 8091  2oc2o 8092  Basecbs 16478  Scalarcsca 16563  TopOpenctopn 16690  tcpt 16707  Xscprds 16714   qTop cqtop 16771   ×s cxps 16774  TopOnctopon 21453  TopSpctps 21475   ×t ctx 22103  Homeochmeo 22296
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798  ax-rep 5187  ax-sep 5200  ax-nul 5207  ax-pow 5263  ax-pr 5326  ax-un 7455  ax-cnex 10587  ax-resscn 10588  ax-1cn 10589  ax-icn 10590  ax-addcl 10591  ax-addrcl 10592  ax-mulcl 10593  ax-mulrcl 10594  ax-mulcom 10595  ax-addass 10596  ax-mulass 10597  ax-distr 10598  ax-i2m1 10599  ax-1ne0 10600  ax-1rid 10601  ax-rnegex 10602  ax-rrecex 10603  ax-cnre 10604  ax-pre-lttri 10605  ax-pre-lttrn 10606  ax-pre-ltadd 10607  ax-pre-mulgt0 10608
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3or 1082  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2620  df-eu 2652  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-ne 3022  df-nel 3129  df-ral 3148  df-rex 3149  df-reu 3150  df-rab 3152  df-v 3502  df-sbc 3777  df-csb 3888  df-dif 3943  df-un 3945  df-in 3947  df-ss 3956  df-pss 3958  df-nul 4296  df-if 4471  df-pw 4544  df-sn 4565  df-pr 4567  df-tp 4569  df-op 4571  df-uni 4838  df-int 4875  df-iun 4919  df-iin 4920  df-br 5064  df-opab 5126  df-mpt 5144  df-tr 5170  df-id 5459  df-eprel 5464  df-po 5473  df-so 5474  df-fr 5513  df-we 5515  df-xp 5560  df-rel 5561  df-cnv 5562  df-co 5563  df-dm 5564  df-rn 5565  df-res 5566  df-ima 5567  df-pred 6147  df-ord 6193  df-on 6194  df-lim 6195  df-suc 6196  df-iota 6313  df-fun 6356  df-fn 6357  df-f 6358  df-f1 6359  df-fo 6360  df-f1o 6361  df-fv 6362  df-riota 7108  df-ov 7153  df-oprab 7154  df-mpo 7155  df-om 7574  df-1st 7685  df-2nd 7686  df-wrecs 7943  df-recs 8004  df-rdg 8042  df-1o 8098  df-2o 8099  df-oadd 8102  df-er 8284  df-map 8403  df-ixp 8456  df-en 8504  df-dom 8505  df-sdom 8506  df-fin 8507  df-fi 8869  df-sup 8900  df-inf 8901  df-pnf 10671  df-mnf 10672  df-xr 10673  df-ltxr 10674  df-le 10675  df-sub 10866  df-neg 10867  df-nn 11633  df-2 11694  df-3 11695  df-4 11696  df-5 11697  df-6 11698  df-7 11699  df-8 11700  df-9 11701  df-n0 11892  df-z 11976  df-dec 12093  df-uz 12238  df-fz 12888  df-struct 16480  df-ndx 16481  df-slot 16482  df-base 16484  df-plusg 16573  df-mulr 16574  df-sca 16576  df-vsca 16577  df-ip 16578  df-tset 16579  df-ple 16580  df-ds 16582  df-hom 16584  df-cco 16585  df-rest 16691  df-topn 16692  df-topgen 16712  df-pt 16713  df-prds 16716  df-qtop 16775  df-imas 16776  df-xps 16778  df-top 21437  df-topon 21454  df-topsp 21476  df-bases 21489  df-cn 21770  df-cnp 21771  df-tx 22105  df-hmeo 22298
This theorem is referenced by:  xpstopn  22355
  Copyright terms: Public domain W3C validator