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 1oex ⊢ 1o ∈ V
35 34 prid2 ⊢ 1o ∈ { ∅ , 1o }
36 35 24 eleqtrri ⊢ 1o ∈ 2o
37 fvco2 ⊢ ( ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } Fn 2o ∧ 1o ∈ 2o ) → ( ( TopOpen ∘ { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ‘ 1o ) = ( TopOpen ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 1o ) ) )
38 12 36 37 sylancl ⊢ ( ( 𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp ) → ( ( TopOpen ∘ { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ‘ 1o ) = ( TopOpen ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 1o ) ) )
39 fvpr1o ⊢ ( 𝑆 ∈ TopSp → ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 1o ) = 𝑆 )
40 39 adantl ⊢ ( ( 𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp ) → ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 1o ) = 𝑆 )
41 40 fveq2d ⊢ ( ( 𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp ) → ( TopOpen ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 1o ) ) = ( TopOpen ‘ 𝑆 ) )
42 41 3 eqtr4di ⊢ ( ( 𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp ) → ( TopOpen ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 1o ) ) = 𝐾 )
43 38 42 eqtrd ⊢ ( ( 𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp ) → ( ( TopOpen ∘ { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ‘ 1o ) = 𝐾 )
44 43 opeq2d ⊢ ( ( 𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp ) → ⟨ 1o , ( ( TopOpen ∘ { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ‘ 1o ) ⟩ = ⟨ 1o , 𝐾 ⟩ )
45 33 44 preq12d ⊢ ( ( 𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp ) → { ⟨ ∅ , ( ( TopOpen ∘ { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ‘ ∅ ) ⟩ , ⟨ 1o , ( ( TopOpen ∘ { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ‘ 1o ) ⟩ } = { ⟨ ∅ , 𝐽 ⟩ , ⟨ 1o , 𝐾 ⟩ } )
46 21 45 eqtr3d ⊢ ( ( 𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp ) → ( TopOpen ∘ { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) = { ⟨ ∅ , 𝐽 ⟩ , ⟨ 1o , 𝐾 ⟩ } )
47 46 fveq2d ⊢ ( ( 𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp ) → ( ∏t ‘ ( TopOpen ∘ { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ) = ( ∏t ‘ { ⟨ ∅ , 𝐽 ⟩ , ⟨ 1o , 𝐾 ⟩ } ) )
48 14 47 eqtrd ⊢ ( ( 𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp ) → ( TopOpen ‘ ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ) = ( ∏t ‘ { ⟨ ∅ , 𝐽 ⟩ , ⟨ 1o , 𝐾 ⟩ } ) )
49 48 oveq1d ⊢ ( ( 𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp ) → ( ( TopOpen ‘ ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ) qTop ◡ 𝐹 ) = ( ( ∏t ‘ { ⟨ ∅ , 𝐽 ⟩ , ⟨ 1o , 𝐾 ⟩ } ) qTop ◡ 𝐹 ) )
50 simpl ⊢ ( ( 𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp ) → 𝑅 ∈ TopSp )
51 simpr ⊢ ( ( 𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp ) → 𝑆 ∈ TopSp )
52 eqid ⊢ ( Scalar ‘ 𝑅 ) = ( Scalar ‘ 𝑅 )
53 1 5 6 50 51 7 52 8 xpsval ⊢ ( ( 𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp ) → 𝑇 = ( ◡ 𝐹 “s ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ) )
54 1 5 6 50 51 7 52 8 xpsrnbas ⊢ ( ( 𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp ) → ran 𝐹 = ( Base ‘ ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ) )
55 7 xpsff1o2 ⊢ 𝐹 : ( 𝑋 × 𝑌 ) –1-1-onto→ ran 𝐹
56 f1ocnv ⊢ ( 𝐹 : ( 𝑋 × 𝑌 ) –1-1-onto→ ran 𝐹 → ◡ 𝐹 : ran 𝐹 –1-1-onto→ ( 𝑋 × 𝑌 ) )
57 55 56 mp1i ⊢ ( ( 𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp ) → ◡ 𝐹 : ran 𝐹 –1-1-onto→ ( 𝑋 × 𝑌 ) )
58 f1ofo ⊢ ( ◡ 𝐹 : ran 𝐹 –1-1-onto→ ( 𝑋 × 𝑌 ) → ◡ 𝐹 : ran 𝐹 –onto→ ( 𝑋 × 𝑌 ) )
59 57 58 syl ⊢ ( ( 𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp ) → ◡ 𝐹 : ran 𝐹 –onto→ ( 𝑋 × 𝑌 ) )
60 ovexd ⊢ ( ( 𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp ) → ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ∈ V )
61 53 54 59 60 13 4 imastopn ⊢ ( ( 𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp ) → 𝑂 = ( ( TopOpen ‘ ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ) qTop ◡ 𝐹 ) )
62 5 2 istps ⊢ ( 𝑅 ∈ TopSp ↔ 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
63 50 62 sylib ⊢ ( ( 𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
64 6 3 istps ⊢ ( 𝑆 ∈ TopSp ↔ 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
65 51 64 sylib ⊢ ( ( 𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp ) → 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
66 7 63 65 xpstopnlem1 ⊢ ( ( 𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp ) → 𝐹 ∈ ( ( 𝐽 ×t 𝐾 ) Homeo ( ∏t ‘ { ⟨ ∅ , 𝐽 ⟩ , ⟨ 1o , 𝐾 ⟩ } ) ) )
67 hmeocnv ⊢ ( 𝐹 ∈ ( ( 𝐽 ×t 𝐾 ) Homeo ( ∏t ‘ { ⟨ ∅ , 𝐽 ⟩ , ⟨ 1o , 𝐾 ⟩ } ) ) → ◡ 𝐹 ∈ ( ( ∏t ‘ { ⟨ ∅ , 𝐽 ⟩ , ⟨ 1o , 𝐾 ⟩ } ) Homeo ( 𝐽 ×t 𝐾 ) ) )
68 hmeoqtop ⊢ ( ◡ 𝐹 ∈ ( ( ∏t ‘ { ⟨ ∅ , 𝐽 ⟩ , ⟨ 1o , 𝐾 ⟩ } ) Homeo ( 𝐽 ×t 𝐾 ) ) → ( 𝐽 ×t 𝐾 ) = ( ( ∏t ‘ { ⟨ ∅ , 𝐽 ⟩ , ⟨ 1o , 𝐾 ⟩ } ) qTop ◡ 𝐹 ) )
69 66 67 68 3syl ⊢ ( ( 𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp ) → ( 𝐽 ×t 𝐾 ) = ( ( ∏t ‘ { ⟨ ∅ , 𝐽 ⟩ , ⟨ 1o , 𝐾 ⟩ } ) qTop ◡ 𝐹 ) )
70 49 61 69 3eqtr4d ⊢ ( ( 𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp ) → 𝑂 = ( 𝐽 ×t 𝐾 ) )