Proof of Theorem xpstopnlem2
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | eqid 2736 | . . . . 5
⊢
((Scalar‘𝑅)Xs{〈∅, 𝑅〉, 〈1o, 𝑆〉}) = ((Scalar‘𝑅)Xs{〈∅, 𝑅〉, 〈1o, 𝑆〉}) | 
| 2 |  | fvexd 6920 | . . . . 5
⊢ ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) →
(Scalar‘𝑅) ∈
V) | 
| 3 |  | 2on 8521 | . . . . . 6
⊢
2o ∈ On | 
| 4 | 3 | a1i 11 | . . . . 5
⊢ ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) →
2o ∈ On) | 
| 5 |  | fnpr2o 17603 | . . . . 5
⊢ ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) →
{〈∅, 𝑅〉,
〈1o, 𝑆〉} Fn 2o) | 
| 6 |  | eqid 2736 | . . . . 5
⊢
(TopOpen‘((Scalar‘𝑅)Xs{〈∅, 𝑅〉, 〈1o, 𝑆〉})) =
(TopOpen‘((Scalar‘𝑅)Xs{〈∅, 𝑅〉, 〈1o, 𝑆〉})) | 
| 7 | 1, 2, 4, 5, 6 | prdstopn 23637 | . . . 4
⊢ ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) →
(TopOpen‘((Scalar‘𝑅)Xs{〈∅, 𝑅〉, 〈1o, 𝑆〉})) =
(∏t‘(TopOpen ∘ {〈∅, 𝑅〉, 〈1o, 𝑆〉}))) | 
| 8 |  | topnfn 17471 | . . . . . . . 8
⊢ TopOpen
Fn V | 
| 9 |  | dffn2 6737 | . . . . . . . . 9
⊢
({〈∅, 𝑅〉, 〈1o, 𝑆〉} Fn 2o ↔
{〈∅, 𝑅〉,
〈1o, 𝑆〉}:2o⟶V) | 
| 10 | 5, 9 | sylib 218 | . . . . . . . 8
⊢ ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) →
{〈∅, 𝑅〉,
〈1o, 𝑆〉}:2o⟶V) | 
| 11 |  | fnfco 6772 | . . . . . . . 8
⊢ ((TopOpen
Fn V ∧ {〈∅, 𝑅〉, 〈1o, 𝑆〉}:2o⟶V)
→ (TopOpen ∘ {〈∅, 𝑅〉, 〈1o, 𝑆〉}) Fn
2o) | 
| 12 | 8, 10, 11 | sylancr 587 | . . . . . . 7
⊢ ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) → (TopOpen
∘ {〈∅, 𝑅〉, 〈1o, 𝑆〉}) Fn
2o) | 
| 13 |  | xpsfeq 17609 | . . . . . . 7
⊢ ((TopOpen
∘ {〈∅, 𝑅〉, 〈1o, 𝑆〉}) Fn 2o →
{〈∅, ((TopOpen ∘ {〈∅, 𝑅〉, 〈1o, 𝑆〉})‘∅)〉,
〈1o, ((TopOpen ∘ {〈∅, 𝑅〉, 〈1o, 𝑆〉})‘1o)〉} =
(TopOpen ∘ {〈∅, 𝑅〉, 〈1o, 𝑆〉})) | 
| 14 | 12, 13 | syl 17 | . . . . . 6
⊢ ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) →
{〈∅, ((TopOpen ∘ {〈∅, 𝑅〉, 〈1o, 𝑆〉})‘∅)〉,
〈1o, ((TopOpen ∘ {〈∅, 𝑅〉, 〈1o, 𝑆〉})‘1o)〉} =
(TopOpen ∘ {〈∅, 𝑅〉, 〈1o, 𝑆〉})) | 
| 15 |  | 0ex 5306 | . . . . . . . . . . . 12
⊢ ∅
∈ V | 
| 16 | 15 | prid1 4761 | . . . . . . . . . . 11
⊢ ∅
∈ {∅, 1o} | 
| 17 |  | df2o3 8515 | . . . . . . . . . . 11
⊢
2o = {∅, 1o} | 
| 18 | 16, 17 | eleqtrri 2839 | . . . . . . . . . 10
⊢ ∅
∈ 2o | 
| 19 |  | fvco2 7005 | . . . . . . . . . 10
⊢
(({〈∅, 𝑅〉, 〈1o, 𝑆〉} Fn 2o ∧
∅ ∈ 2o) → ((TopOpen ∘ {〈∅, 𝑅〉, 〈1o,
𝑆〉})‘∅) =
(TopOpen‘({〈∅, 𝑅〉, 〈1o, 𝑆〉}‘∅))) | 
| 20 | 5, 18, 19 | sylancl 586 | . . . . . . . . 9
⊢ ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) → ((TopOpen
∘ {〈∅, 𝑅〉, 〈1o, 𝑆〉})‘∅) =
(TopOpen‘({〈∅, 𝑅〉, 〈1o, 𝑆〉}‘∅))) | 
| 21 |  | fvpr0o 17605 | . . . . . . . . . . . 12
⊢ (𝑅 ∈ TopSp →
({〈∅, 𝑅〉,
〈1o, 𝑆〉}‘∅) = 𝑅) | 
| 22 | 21 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) →
({〈∅, 𝑅〉,
〈1o, 𝑆〉}‘∅) = 𝑅) | 
| 23 | 22 | fveq2d 6909 | . . . . . . . . . 10
⊢ ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) →
(TopOpen‘({〈∅, 𝑅〉, 〈1o, 𝑆〉}‘∅)) =
(TopOpen‘𝑅)) | 
| 24 |  | xpstopn.j | . . . . . . . . . 10
⊢ 𝐽 = (TopOpen‘𝑅) | 
| 25 | 23, 24 | eqtr4di 2794 | . . . . . . . . 9
⊢ ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) →
(TopOpen‘({〈∅, 𝑅〉, 〈1o, 𝑆〉}‘∅)) = 𝐽) | 
| 26 | 20, 25 | eqtrd 2776 | . . . . . . . 8
⊢ ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) → ((TopOpen
∘ {〈∅, 𝑅〉, 〈1o, 𝑆〉})‘∅) = 𝐽) | 
| 27 | 26 | opeq2d 4879 | . . . . . . 7
⊢ ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) →
〈∅, ((TopOpen ∘ {〈∅, 𝑅〉, 〈1o, 𝑆〉})‘∅)〉 =
〈∅, 𝐽〉) | 
| 28 |  | 1oex 8517 | . . . . . . . . . . . 12
⊢
1o ∈ V | 
| 29 | 28 | prid2 4762 | . . . . . . . . . . 11
⊢
1o ∈ {∅, 1o} | 
| 30 | 29, 17 | eleqtrri 2839 | . . . . . . . . . 10
⊢
1o ∈ 2o | 
| 31 |  | fvco2 7005 | . . . . . . . . . 10
⊢
(({〈∅, 𝑅〉, 〈1o, 𝑆〉} Fn 2o ∧
1o ∈ 2o) → ((TopOpen ∘ {〈∅,
𝑅〉,
〈1o, 𝑆〉})‘1o) =
(TopOpen‘({〈∅, 𝑅〉, 〈1o, 𝑆〉}‘1o))) | 
| 32 | 5, 30, 31 | sylancl 586 | . . . . . . . . 9
⊢ ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) → ((TopOpen
∘ {〈∅, 𝑅〉, 〈1o, 𝑆〉})‘1o) =
(TopOpen‘({〈∅, 𝑅〉, 〈1o, 𝑆〉}‘1o))) | 
| 33 |  | fvpr1o 17606 | . . . . . . . . . . . 12
⊢ (𝑆 ∈ TopSp →
({〈∅, 𝑅〉,
〈1o, 𝑆〉}‘1o) = 𝑆) | 
| 34 | 33 | adantl 481 | . . . . . . . . . . 11
⊢ ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) →
({〈∅, 𝑅〉,
〈1o, 𝑆〉}‘1o) = 𝑆) | 
| 35 | 34 | fveq2d 6909 | . . . . . . . . . 10
⊢ ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) →
(TopOpen‘({〈∅, 𝑅〉, 〈1o, 𝑆〉}‘1o)) =
(TopOpen‘𝑆)) | 
| 36 |  | xpstopn.k | . . . . . . . . . 10
⊢ 𝐾 = (TopOpen‘𝑆) | 
| 37 | 35, 36 | eqtr4di 2794 | . . . . . . . . 9
⊢ ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) →
(TopOpen‘({〈∅, 𝑅〉, 〈1o, 𝑆〉}‘1o)) =
𝐾) | 
| 38 | 32, 37 | eqtrd 2776 | . . . . . . . 8
⊢ ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) → ((TopOpen
∘ {〈∅, 𝑅〉, 〈1o, 𝑆〉})‘1o) =
𝐾) | 
| 39 | 38 | opeq2d 4879 | . . . . . . 7
⊢ ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) →
〈1o, ((TopOpen ∘ {〈∅, 𝑅〉, 〈1o, 𝑆〉})‘1o)〉 =
〈1o, 𝐾〉) | 
| 40 | 27, 39 | preq12d 4740 | . . . . . 6
⊢ ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) →
{〈∅, ((TopOpen ∘ {〈∅, 𝑅〉, 〈1o, 𝑆〉})‘∅)〉,
〈1o, ((TopOpen ∘ {〈∅, 𝑅〉, 〈1o, 𝑆〉})‘1o)〉} =
{〈∅, 𝐽〉,
〈1o, 𝐾〉}) | 
| 41 | 14, 40 | eqtr3d 2778 | . . . . 5
⊢ ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) → (TopOpen
∘ {〈∅, 𝑅〉, 〈1o, 𝑆〉}) = {〈∅, 𝐽〉, 〈1o,
𝐾〉}) | 
| 42 | 41 | fveq2d 6909 | . . . 4
⊢ ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) →
(∏t‘(TopOpen ∘ {〈∅, 𝑅〉, 〈1o, 𝑆〉})) =
(∏t‘{〈∅, 𝐽〉, 〈1o, 𝐾〉})) | 
| 43 | 7, 42 | eqtrd 2776 | . . 3
⊢ ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) →
(TopOpen‘((Scalar‘𝑅)Xs{〈∅, 𝑅〉, 〈1o, 𝑆〉})) =
(∏t‘{〈∅, 𝐽〉, 〈1o, 𝐾〉})) | 
| 44 | 43 | oveq1d 7447 | . 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 482 | . . . 4
⊢ ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) → 𝑅 ∈ TopSp) | 
| 49 |  | simpr 484 | . . . 4
⊢ ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) → 𝑆 ∈ TopSp) | 
| 50 |  | xpstopnlem.f | . . . 4
⊢ 𝐹 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉}) | 
| 51 |  | eqid 2736 | . . . 4
⊢
(Scalar‘𝑅) =
(Scalar‘𝑅) | 
| 52 | 45, 46, 47, 48, 49, 50, 51, 1 | xpsval 17616 | . . 3
⊢ ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) → 𝑇 = (◡𝐹 “s
((Scalar‘𝑅)Xs{〈∅, 𝑅〉, 〈1o,
𝑆〉}))) | 
| 53 | 45, 46, 47, 48, 49, 50, 51, 1 | xpsrnbas 17617 | . . 3
⊢ ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) → ran 𝐹 =
(Base‘((Scalar‘𝑅)Xs{〈∅, 𝑅〉, 〈1o, 𝑆〉}))) | 
| 54 | 50 | xpsff1o2 17615 | . . . . 5
⊢ 𝐹:(𝑋 × 𝑌)–1-1-onto→ran
𝐹 | 
| 55 |  | f1ocnv 6859 | . . . . 5
⊢ (𝐹:(𝑋 × 𝑌)–1-1-onto→ran
𝐹 → ◡𝐹:ran 𝐹–1-1-onto→(𝑋 × 𝑌)) | 
| 56 | 54, 55 | mp1i 13 | . . . 4
⊢ ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) → ◡𝐹:ran 𝐹–1-1-onto→(𝑋 × 𝑌)) | 
| 57 |  | f1ofo 6854 | . . . 4
⊢ (◡𝐹:ran 𝐹–1-1-onto→(𝑋 × 𝑌) → ◡𝐹:ran 𝐹–onto→(𝑋 × 𝑌)) | 
| 58 | 56, 57 | syl 17 | . . 3
⊢ ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) → ◡𝐹:ran 𝐹–onto→(𝑋 × 𝑌)) | 
| 59 |  | ovexd 7467 | . . 3
⊢ ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) →
((Scalar‘𝑅)Xs{〈∅, 𝑅〉, 〈1o,
𝑆〉}) ∈
V) | 
| 60 |  | xpstopn.o | . . 3
⊢ 𝑂 = (TopOpen‘𝑇) | 
| 61 | 52, 53, 58, 59, 6, 60 | imastopn 23729 | . 2
⊢ ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) → 𝑂 =
((TopOpen‘((Scalar‘𝑅)Xs{〈∅, 𝑅〉, 〈1o, 𝑆〉})) qTop ◡𝐹)) | 
| 62 | 46, 24 | istps 22941 | . . . . 5
⊢ (𝑅 ∈ TopSp ↔ 𝐽 ∈ (TopOn‘𝑋)) | 
| 63 | 48, 62 | sylib 218 | . . . 4
⊢ ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) → 𝐽 ∈ (TopOn‘𝑋)) | 
| 64 | 47, 36 | istps 22941 | . . . . 5
⊢ (𝑆 ∈ TopSp ↔ 𝐾 ∈ (TopOn‘𝑌)) | 
| 65 | 49, 64 | sylib 218 | . . . 4
⊢ ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) → 𝐾 ∈ (TopOn‘𝑌)) | 
| 66 | 50, 63, 65 | xpstopnlem1 23818 | . . 3
⊢ ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) → 𝐹 ∈ ((𝐽 ×t 𝐾)Homeo(∏t‘{〈∅,
𝐽〉, 〈1o,
𝐾〉}))) | 
| 67 |  | hmeocnv 23771 | . . 3
⊢ (𝐹 ∈ ((𝐽 ×t 𝐾)Homeo(∏t‘{〈∅,
𝐽〉, 〈1o,
𝐾〉})) → ◡𝐹 ∈
((∏t‘{〈∅, 𝐽〉, 〈1o, 𝐾〉})Homeo(𝐽 ×t 𝐾))) | 
| 68 |  | hmeoqtop 23784 | . . 3
⊢ (◡𝐹 ∈
((∏t‘{〈∅, 𝐽〉, 〈1o, 𝐾〉})Homeo(𝐽 ×t 𝐾)) → (𝐽 ×t 𝐾) =
((∏t‘{〈∅, 𝐽〉, 〈1o, 𝐾〉}) qTop ◡𝐹)) | 
| 69 | 66, 67, 68 | 3syl 18 | . 2
⊢ ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) → (𝐽 ×t 𝐾) =
((∏t‘{〈∅, 𝐽〉, 〈1o, 𝐾〉}) qTop ◡𝐹)) | 
| 70 | 44, 61, 69 | 3eqtr4d 2786 | 1
⊢ ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) → 𝑂 = (𝐽 ×t 𝐾)) |