Proof of Theorem xpstopnlem2
Step | Hyp | Ref
| Expression |
1 | | eqid 2610 |
. . . . 5
⊢
((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})) = ((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})) |
2 | | fvex 6113 |
. . . . . 6
⊢
(Scalar‘𝑅)
∈ V |
3 | 2 | a1i 11 |
. . . . 5
⊢ ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) →
(Scalar‘𝑅) ∈
V) |
4 | | 2on 7455 |
. . . . . 6
⊢
2𝑜 ∈ On |
5 | 4 | a1i 11 |
. . . . 5
⊢ ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) →
2𝑜 ∈ On) |
6 | | xpscfn 16042 |
. . . . 5
⊢ ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) → ◡({𝑅} +𝑐 {𝑆}) Fn
2𝑜) |
7 | | eqid 2610 |
. . . . 5
⊢
(TopOpen‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆}))) = (TopOpen‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆}))) |
8 | 1, 3, 5, 6, 7 | prdstopn 21241 |
. . . 4
⊢ ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) →
(TopOpen‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆}))) = (∏t‘(TopOpen
∘ ◡({𝑅} +𝑐 {𝑆})))) |
9 | | topnfn 15909 |
. . . . . . . 8
⊢ TopOpen
Fn V |
10 | | dffn2 5960 |
. . . . . . . . 9
⊢ (◡({𝑅} +𝑐 {𝑆}) Fn 2𝑜 ↔ ◡({𝑅} +𝑐 {𝑆}):2𝑜⟶V) |
11 | 6, 10 | sylib 207 |
. . . . . . . 8
⊢ ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) → ◡({𝑅} +𝑐 {𝑆}):2𝑜⟶V) |
12 | | fnfco 5982 |
. . . . . . . 8
⊢ ((TopOpen
Fn V ∧ ◡({𝑅} +𝑐 {𝑆}):2𝑜⟶V) →
(TopOpen ∘ ◡({𝑅} +𝑐 {𝑆})) Fn
2𝑜) |
13 | 9, 11, 12 | sylancr 694 |
. . . . . . 7
⊢ ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) → (TopOpen
∘ ◡({𝑅} +𝑐 {𝑆})) Fn
2𝑜) |
14 | | xpsfeq 16047 |
. . . . . . 7
⊢ ((TopOpen
∘ ◡({𝑅} +𝑐 {𝑆})) Fn 2𝑜 → ◡({((TopOpen ∘ ◡({𝑅} +𝑐 {𝑆}))‘∅)} +𝑐
{((TopOpen ∘ ◡({𝑅} +𝑐 {𝑆}))‘1𝑜)}) =
(TopOpen ∘ ◡({𝑅} +𝑐 {𝑆}))) |
15 | 13, 14 | syl 17 |
. . . . . 6
⊢ ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) → ◡({((TopOpen ∘ ◡({𝑅} +𝑐 {𝑆}))‘∅)} +𝑐
{((TopOpen ∘ ◡({𝑅} +𝑐 {𝑆}))‘1𝑜)}) =
(TopOpen ∘ ◡({𝑅} +𝑐 {𝑆}))) |
16 | | 0ex 4718 |
. . . . . . . . . . . . 13
⊢ ∅
∈ V |
17 | 16 | prid1 4241 |
. . . . . . . . . . . 12
⊢ ∅
∈ {∅, 1𝑜} |
18 | | df2o3 7460 |
. . . . . . . . . . . 12
⊢
2𝑜 = {∅,
1𝑜} |
19 | 17, 18 | eleqtrri 2687 |
. . . . . . . . . . 11
⊢ ∅
∈ 2𝑜 |
20 | | fvco2 6183 |
. . . . . . . . . . 11
⊢ ((◡({𝑅} +𝑐 {𝑆}) Fn 2𝑜 ∧ ∅
∈ 2𝑜) → ((TopOpen ∘ ◡({𝑅} +𝑐 {𝑆}))‘∅) = (TopOpen‘(◡({𝑅} +𝑐 {𝑆})‘∅))) |
21 | 6, 19, 20 | sylancl 693 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) → ((TopOpen
∘ ◡({𝑅} +𝑐 {𝑆}))‘∅) = (TopOpen‘(◡({𝑅} +𝑐 {𝑆})‘∅))) |
22 | | xpsc0 16043 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ TopSp → (◡({𝑅} +𝑐 {𝑆})‘∅) = 𝑅) |
23 | 22 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) → (◡({𝑅} +𝑐 {𝑆})‘∅) = 𝑅) |
24 | 23 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) →
(TopOpen‘(◡({𝑅} +𝑐 {𝑆})‘∅)) = (TopOpen‘𝑅)) |
25 | | xpstopn.j |
. . . . . . . . . . 11
⊢ 𝐽 = (TopOpen‘𝑅) |
26 | 24, 25 | syl6eqr 2662 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) →
(TopOpen‘(◡({𝑅} +𝑐 {𝑆})‘∅)) = 𝐽) |
27 | 21, 26 | eqtrd 2644 |
. . . . . . . . 9
⊢ ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) → ((TopOpen
∘ ◡({𝑅} +𝑐 {𝑆}))‘∅) = 𝐽) |
28 | 27 | sneqd 4137 |
. . . . . . . 8
⊢ ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) → {((TopOpen
∘ ◡({𝑅} +𝑐 {𝑆}))‘∅)} = {𝐽}) |
29 | | 1on 7454 |
. . . . . . . . . . . . . 14
⊢
1𝑜 ∈ On |
30 | 29 | elexi 3186 |
. . . . . . . . . . . . 13
⊢
1𝑜 ∈ V |
31 | 30 | prid2 4242 |
. . . . . . . . . . . 12
⊢
1𝑜 ∈ {∅,
1𝑜} |
32 | 31, 18 | eleqtrri 2687 |
. . . . . . . . . . 11
⊢
1𝑜 ∈ 2𝑜 |
33 | | fvco2 6183 |
. . . . . . . . . . 11
⊢ ((◡({𝑅} +𝑐 {𝑆}) Fn 2𝑜 ∧
1𝑜 ∈ 2𝑜) → ((TopOpen ∘
◡({𝑅} +𝑐 {𝑆}))‘1𝑜) =
(TopOpen‘(◡({𝑅} +𝑐 {𝑆})‘1𝑜))) |
34 | 6, 32, 33 | sylancl 693 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) → ((TopOpen
∘ ◡({𝑅} +𝑐 {𝑆}))‘1𝑜) =
(TopOpen‘(◡({𝑅} +𝑐 {𝑆})‘1𝑜))) |
35 | | xpsc1 16044 |
. . . . . . . . . . . . 13
⊢ (𝑆 ∈ TopSp → (◡({𝑅} +𝑐 {𝑆})‘1𝑜) = 𝑆) |
36 | 35 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) → (◡({𝑅} +𝑐 {𝑆})‘1𝑜) = 𝑆) |
37 | 36 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) →
(TopOpen‘(◡({𝑅} +𝑐 {𝑆})‘1𝑜)) =
(TopOpen‘𝑆)) |
38 | | xpstopn.k |
. . . . . . . . . . 11
⊢ 𝐾 = (TopOpen‘𝑆) |
39 | 37, 38 | syl6eqr 2662 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) →
(TopOpen‘(◡({𝑅} +𝑐 {𝑆})‘1𝑜)) = 𝐾) |
40 | 34, 39 | eqtrd 2644 |
. . . . . . . . 9
⊢ ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) → ((TopOpen
∘ ◡({𝑅} +𝑐 {𝑆}))‘1𝑜) = 𝐾) |
41 | 40 | sneqd 4137 |
. . . . . . . 8
⊢ ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) → {((TopOpen
∘ ◡({𝑅} +𝑐 {𝑆}))‘1𝑜)} = {𝐾}) |
42 | 28, 41 | oveq12d 6567 |
. . . . . . 7
⊢ ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) →
({((TopOpen ∘ ◡({𝑅} +𝑐 {𝑆}))‘∅)}
+𝑐 {((TopOpen ∘ ◡({𝑅} +𝑐 {𝑆}))‘1𝑜)}) = ({𝐽} +𝑐 {𝐾})) |
43 | 42 | cnveqd 5220 |
. . . . . 6
⊢ ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) → ◡({((TopOpen ∘ ◡({𝑅} +𝑐 {𝑆}))‘∅)} +𝑐
{((TopOpen ∘ ◡({𝑅} +𝑐 {𝑆}))‘1𝑜)}) = ◡({𝐽} +𝑐 {𝐾})) |
44 | 15, 43 | eqtr3d 2646 |
. . . . 5
⊢ ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) → (TopOpen
∘ ◡({𝑅} +𝑐 {𝑆})) = ◡({𝐽} +𝑐 {𝐾})) |
45 | 44 | fveq2d 6107 |
. . . 4
⊢ ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) →
(∏t‘(TopOpen ∘ ◡({𝑅} +𝑐 {𝑆}))) = (∏t‘◡({𝐽} +𝑐 {𝐾}))) |
46 | 8, 45 | eqtrd 2644 |
. . 3
⊢ ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) →
(TopOpen‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆}))) = (∏t‘◡({𝐽} +𝑐 {𝐾}))) |
47 | 46 | oveq1d 6564 |
. 2
⊢ ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) →
((TopOpen‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆}))) qTop ◡𝐹) = ((∏t‘◡({𝐽} +𝑐 {𝐾})) qTop ◡𝐹)) |
48 | | xpstps.t |
. . . 4
⊢ 𝑇 = (𝑅 ×s 𝑆) |
49 | | xpstopnlem.x |
. . . 4
⊢ 𝑋 = (Base‘𝑅) |
50 | | xpstopnlem.y |
. . . 4
⊢ 𝑌 = (Base‘𝑆) |
51 | | simpl 472 |
. . . 4
⊢ ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) → 𝑅 ∈ TopSp) |
52 | | simpr 476 |
. . . 4
⊢ ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) → 𝑆 ∈ TopSp) |
53 | | xpstopnlem.f |
. . . 4
⊢ 𝐹 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) |
54 | | eqid 2610 |
. . . 4
⊢
(Scalar‘𝑅) =
(Scalar‘𝑅) |
55 | 48, 49, 50, 51, 52, 53, 54, 1 | xpsval 16055 |
. . 3
⊢ ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) → 𝑇 = (◡𝐹 “s
((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})))) |
56 | 48, 49, 50, 51, 52, 53, 54, 1 | xpslem 16056 |
. . 3
⊢ ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) → ran 𝐹 =
(Base‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})))) |
57 | 53 | xpsff1o2 16054 |
. . . . 5
⊢ 𝐹:(𝑋 × 𝑌)–1-1-onto→ran
𝐹 |
58 | | f1ocnv 6062 |
. . . . 5
⊢ (𝐹:(𝑋 × 𝑌)–1-1-onto→ran
𝐹 → ◡𝐹:ran 𝐹–1-1-onto→(𝑋 × 𝑌)) |
59 | 57, 58 | mp1i 13 |
. . . 4
⊢ ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) → ◡𝐹:ran 𝐹–1-1-onto→(𝑋 × 𝑌)) |
60 | | f1ofo 6057 |
. . . 4
⊢ (◡𝐹:ran 𝐹–1-1-onto→(𝑋 × 𝑌) → ◡𝐹:ran 𝐹–onto→(𝑋 × 𝑌)) |
61 | 59, 60 | syl 17 |
. . 3
⊢ ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) → ◡𝐹:ran 𝐹–onto→(𝑋 × 𝑌)) |
62 | | ovex 6577 |
. . . 4
⊢
((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})) ∈ V |
63 | 62 | a1i 11 |
. . 3
⊢ ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) →
((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})) ∈ V) |
64 | | xpstopn.o |
. . 3
⊢ 𝑂 = (TopOpen‘𝑇) |
65 | 55, 56, 61, 63, 7, 64 | imastopn 21333 |
. 2
⊢ ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) → 𝑂 =
((TopOpen‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆}))) qTop ◡𝐹)) |
66 | 49, 25 | istps 20551 |
. . . . 5
⊢ (𝑅 ∈ TopSp ↔ 𝐽 ∈ (TopOn‘𝑋)) |
67 | 51, 66 | sylib 207 |
. . . 4
⊢ ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) → 𝐽 ∈ (TopOn‘𝑋)) |
68 | 50, 38 | istps 20551 |
. . . . 5
⊢ (𝑆 ∈ TopSp ↔ 𝐾 ∈ (TopOn‘𝑌)) |
69 | 52, 68 | sylib 207 |
. . . 4
⊢ ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) → 𝐾 ∈ (TopOn‘𝑌)) |
70 | 53, 67, 69 | xpstopnlem1 21422 |
. . 3
⊢ ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) → 𝐹 ∈ ((𝐽 ×t 𝐾)Homeo(∏t‘◡({𝐽} +𝑐 {𝐾})))) |
71 | | hmeocnv 21375 |
. . 3
⊢ (𝐹 ∈ ((𝐽 ×t 𝐾)Homeo(∏t‘◡({𝐽} +𝑐 {𝐾}))) → ◡𝐹 ∈ ((∏t‘◡({𝐽} +𝑐 {𝐾}))Homeo(𝐽 ×t 𝐾))) |
72 | | hmeoqtop 21388 |
. . 3
⊢ (◡𝐹 ∈ ((∏t‘◡({𝐽} +𝑐 {𝐾}))Homeo(𝐽 ×t 𝐾)) → (𝐽 ×t 𝐾) = ((∏t‘◡({𝐽} +𝑐 {𝐾})) qTop ◡𝐹)) |
73 | 70, 71, 72 | 3syl 18 |
. 2
⊢ ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) → (𝐽 ×t 𝐾) =
((∏t‘◡({𝐽} +𝑐 {𝐾})) qTop ◡𝐹)) |
74 | 47, 65, 73 | 3eqtr4d 2654 |
1
⊢ ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) → 𝑂 = (𝐽 ×t 𝐾)) |