Metamath Proof Explorer

Theorem xpstopnlem2

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

Ref Expression
Hypotheses xpstps.t ⊢ 𝑇 = ( 𝑅 ×s 𝑆 )
xpstopn.j ⊢ 𝐽 = ( TopOpen ‘ 𝑅 )
xpstopn.k ⊢ 𝐾 = ( TopOpen ‘ 𝑆 )
xpstopn.o ⊢ 𝑂 = ( TopOpen ‘ 𝑇 )
xpstopnlem.x ⊢ 𝑋 = ( Base ‘ 𝑅 )
xpstopnlem.y ⊢ 𝑌 = ( Base ‘ 𝑆 )
xpstopnlem.f ⊢ 𝐹 = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } )
Assertion xpstopnlem2 ( ( 𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp ) → 𝑂 = ( 𝐽 ×t 𝐾 ) )

Proof

Step Hyp Ref Expression
1 xpstps.t ⊢ 𝑇 = ( 𝑅 ×s 𝑆 )
2 xpstopn.j ⊢ 𝐽 = ( TopOpen ‘ 𝑅 )
3 xpstopn.k ⊢ 𝐾 = ( TopOpen ‘ 𝑆 )
4 xpstopn.o ⊢ 𝑂 = ( TopOpen ‘ 𝑇 )
5 xpstopnlem.x ⊢ 𝑋 = ( Base ‘ 𝑅 )
6 xpstopnlem.y ⊢ 𝑌 = ( Base ‘ 𝑆 )
7 xpstopnlem.f ⊢ 𝐹 = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } )
8 eqid ⊢ ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) = ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } )
9 fvexd ⊢ ( ( 𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp ) → ( Scalar ‘ 𝑅 ) ∈ V )
10 2on ⊢ 2o ∈ On
11 10 a1i ⊢ ( ( 𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp ) → 2o ∈ On )
12 fnpr2o ⊢ ( ( 𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp ) → { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } Fn 2o )
13 eqid ⊢ ( TopOpen ‘ ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ) = ( TopOpen ‘ ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) )
14 8 9 11 12 13 prdstopn ⊢ ( ( 𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp ) → ( TopOpen ‘ ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ) = ( ∏t ‘ ( TopOpen ∘ { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ) )
15 topnfn ⊢ TopOpen Fn V
16 dffn2 ⊢ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } Fn 2o ↔ { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } : 2o ⟶ V )
17 12 16 sylib ⊢ ( ( 𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp ) → { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } : 2o ⟶ V )
18 fnfco ⊢ ( ( TopOpen Fn V ∧ { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } : 2o ⟶ V ) → ( TopOpen ∘ { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) Fn 2o )
19 15 17 18 sylancr ⊢ ( ( 𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp ) → ( TopOpen ∘ { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) Fn 2o )
20 xpsfeq ⊢ ( ( TopOpen ∘ { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) Fn 2o → { ⟨ ∅ , ( ( TopOpen ∘ { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ‘ ∅ ) ⟩ , ⟨ 1o , ( ( TopOpen ∘ { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ‘ 1o ) ⟩ } = ( TopOpen ∘ { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) )
21 19 20 syl ⊢ ( ( 𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp ) → { ⟨ ∅ , ( ( TopOpen ∘ { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ‘ ∅ ) ⟩ , ⟨ 1o , ( ( TopOpen ∘ { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ‘ 1o ) ⟩ } = ( TopOpen ∘ { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) )
22 0ex ⊢ ∅ ∈ V
23 22 prid1 ⊢ ∅ ∈ { ∅ , 1o }
24 df2o3 ⊢ 2o = { ∅ , 1o }
25 23 24 eleqtrri ⊢ ∅ ∈ 2o
26 fvco2 ⊢ ( ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } Fn 2o ∧ ∅ ∈ 2o ) → ( ( TopOpen ∘ { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ‘ ∅ ) = ( TopOpen ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ ∅ ) ) )
27 12 25 26 sylancl ⊢ ( ( 𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp ) → ( ( TopOpen ∘ { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ‘ ∅ ) = ( TopOpen ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ ∅ ) ) )
28 fvpr0o ⊢ ( 𝑅 ∈ TopSp → ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ ∅ ) = 𝑅 )
29 28 adantr ⊢ ( ( 𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp ) → ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ ∅ ) = 𝑅 )
30 29 fveq2d ⊢ ( ( 𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp ) → ( TopOpen ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ ∅ ) ) = ( TopOpen ‘ 𝑅 ) )
31 30 2 eqtr4di ⊢ ( ( 𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp ) → ( TopOpen ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ ∅ ) ) = 𝐽 )
32 27 31 eqtrd ⊢ ( ( 𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp ) → ( ( TopOpen ∘ { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ‘ ∅ ) = 𝐽 )
33 32 opeq2d ⊢ ( ( 𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp ) → ⟨ ∅ , ( ( TopOpen ∘ { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ‘ ∅ ) ⟩ = ⟨ ∅ , 𝐽 ⟩ )
34 1oelpr ⊢ 1o ∈ { ∅ , 1o }
35 34 24 eleqtrri ⊢ 1o ∈ 2o
36 fvco2 ⊢ ( ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } Fn 2o ∧ 1o ∈ 2o ) → ( ( TopOpen ∘ { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ‘ 1o ) = ( TopOpen ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 1o ) ) )
37 12 35 36 sylancl ⊢ ( ( 𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp ) → ( ( TopOpen ∘ { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ‘ 1o ) = ( TopOpen ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 1o ) ) )
38 fvpr1o ⊢ ( 𝑆 ∈ TopSp → ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 1o ) = 𝑆 )
39 38 adantl ⊢ ( ( 𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp ) → ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 1o ) = 𝑆 )
40 39 fveq2d ⊢ ( ( 𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp ) → ( TopOpen ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 1o ) ) = ( TopOpen ‘ 𝑆 ) )
41 40 3 eqtr4di ⊢ ( ( 𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp ) → ( TopOpen ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 1o ) ) = 𝐾 )
42 37 41 eqtrd ⊢ ( ( 𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp ) → ( ( TopOpen ∘ { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ‘ 1o ) = 𝐾 )
43 42 opeq2d ⊢ ( ( 𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp ) → ⟨ 1o , ( ( TopOpen ∘ { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ‘ 1o ) ⟩ = ⟨ 1o , 𝐾 ⟩ )
44 33 43 preq12d ⊢ ( ( 𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp ) → { ⟨ ∅ , ( ( TopOpen ∘ { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ‘ ∅ ) ⟩ , ⟨ 1o , ( ( TopOpen ∘ { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ‘ 1o ) ⟩ } = { ⟨ ∅ , 𝐽 ⟩ , ⟨ 1o , 𝐾 ⟩ } )
45 21 44 eqtr3d ⊢ ( ( 𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp ) → ( TopOpen ∘ { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) = { ⟨ ∅ , 𝐽 ⟩ , ⟨ 1o , 𝐾 ⟩ } )
46 45 fveq2d ⊢ ( ( 𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp ) → ( ∏t ‘ ( TopOpen ∘ { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ) = ( ∏t ‘ { ⟨ ∅ , 𝐽 ⟩ , ⟨ 1o , 𝐾 ⟩ } ) )
47 14 46 eqtrd ⊢ ( ( 𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp ) → ( TopOpen ‘ ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ) = ( ∏t ‘ { ⟨ ∅ , 𝐽 ⟩ , ⟨ 1o , 𝐾 ⟩ } ) )
48 47 oveq1d ⊢ ( ( 𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp ) → ( ( TopOpen ‘ ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ) qTop ◡ 𝐹 ) = ( ( ∏t ‘ { ⟨ ∅ , 𝐽 ⟩ , ⟨ 1o , 𝐾 ⟩ } ) qTop ◡ 𝐹 ) )
49 simpl ⊢ ( ( 𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp ) → 𝑅 ∈ TopSp )
50 simpr ⊢ ( ( 𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp ) → 𝑆 ∈ TopSp )
51 eqid ⊢ ( Scalar ‘ 𝑅 ) = ( Scalar ‘ 𝑅 )
52 1 5 6 49 50 7 51 8 xpsval ⊢ ( ( 𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp ) → 𝑇 = ( ◡ 𝐹 “s ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ) )
53 1 5 6 49 50 7 51 8 xpsrnbas ⊢ ( ( 𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp ) → ran 𝐹 = ( Base ‘ ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ) )
54 7 xpsff1o2 ⊢ 𝐹 : ( 𝑋 × 𝑌 ) –1-1-onto→ ran 𝐹
55 f1ocnv ⊢ ( 𝐹 : ( 𝑋 × 𝑌 ) –1-1-onto→ ran 𝐹 → ◡ 𝐹 : ran 𝐹 –1-1-onto→ ( 𝑋 × 𝑌 ) )
56 54 55 mp1i ⊢ ( ( 𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp ) → ◡ 𝐹 : ran 𝐹 –1-1-onto→ ( 𝑋 × 𝑌 ) )
57 f1ofo ⊢ ( ◡ 𝐹 : ran 𝐹 –1-1-onto→ ( 𝑋 × 𝑌 ) → ◡ 𝐹 : ran 𝐹 –onto→ ( 𝑋 × 𝑌 ) )
58 56 57 syl ⊢ ( ( 𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp ) → ◡ 𝐹 : ran 𝐹 –onto→ ( 𝑋 × 𝑌 ) )
59 ovexd ⊢ ( ( 𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp ) → ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ∈ V )
60 52 53 58 59 13 4 imastopn ⊢ ( ( 𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp ) → 𝑂 = ( ( TopOpen ‘ ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ) qTop ◡ 𝐹 ) )
61 5 2 istps ⊢ ( 𝑅 ∈ TopSp ↔ 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
62 49 61 sylib ⊢ ( ( 𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
63 6 3 istps ⊢ ( 𝑆 ∈ TopSp ↔ 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
64 50 63 sylib ⊢ ( ( 𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp ) → 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
65 7 62 64 xpstopnlem1 ⊢ ( ( 𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp ) → 𝐹 ∈ ( ( 𝐽 ×t 𝐾 ) Homeo ( ∏t ‘ { ⟨ ∅ , 𝐽 ⟩ , ⟨ 1o , 𝐾 ⟩ } ) ) )
66 hmeocnv ⊢ ( 𝐹 ∈ ( ( 𝐽 ×t 𝐾 ) Homeo ( ∏t ‘ { ⟨ ∅ , 𝐽 ⟩ , ⟨ 1o , 𝐾 ⟩ } ) ) → ◡ 𝐹 ∈ ( ( ∏t ‘ { ⟨ ∅ , 𝐽 ⟩ , ⟨ 1o , 𝐾 ⟩ } ) Homeo ( 𝐽 ×t 𝐾 ) ) )
67 hmeoqtop ⊢ ( ◡ 𝐹 ∈ ( ( ∏t ‘ { ⟨ ∅ , 𝐽 ⟩ , ⟨ 1o , 𝐾 ⟩ } ) Homeo ( 𝐽 ×t 𝐾 ) ) → ( 𝐽 ×t 𝐾 ) = ( ( ∏t ‘ { ⟨ ∅ , 𝐽 ⟩ , ⟨ 1o , 𝐾 ⟩ } ) qTop ◡ 𝐹 ) )
68 65 66 67 3syl ⊢ ( ( 𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp ) → ( 𝐽 ×t 𝐾 ) = ( ( ∏t ‘ { ⟨ ∅ , 𝐽 ⟩ , ⟨ 1o , 𝐾 ⟩ } ) qTop ◡ 𝐹 ) )
69 48 60 68 3eqtr4d ⊢ ( ( 𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp ) → 𝑂 = ( 𝐽 ×t 𝐾 ) )