Metamath Proof Explorer


Theorem prdstmdd

Description: The product of a family of topological monoids is a topological monoid. (Contributed by Mario Carneiro, 22-Sep-2015)

Ref Expression
Hypotheses prdstmdd.y 𝑌 = ( 𝑆 Xs 𝑅 )
prdstmdd.i ( 𝜑𝐼𝑊 )
prdstmdd.s ( 𝜑𝑆𝑉 )
prdstmdd.r ( 𝜑𝑅 : 𝐼 ⟶ TopMnd )
Assertion prdstmdd ( 𝜑𝑌 ∈ TopMnd )

Proof

Step Hyp Ref Expression
1 prdstmdd.y 𝑌 = ( 𝑆 Xs 𝑅 )
2 prdstmdd.i ( 𝜑𝐼𝑊 )
3 prdstmdd.s ( 𝜑𝑆𝑉 )
4 prdstmdd.r ( 𝜑𝑅 : 𝐼 ⟶ TopMnd )
5 tmdmnd ( 𝑥 ∈ TopMnd → 𝑥 ∈ Mnd )
6 5 ssriv TopMnd ⊆ Mnd
7 fss ( ( 𝑅 : 𝐼 ⟶ TopMnd ∧ TopMnd ⊆ Mnd ) → 𝑅 : 𝐼 ⟶ Mnd )
8 4 6 7 sylancl ( 𝜑𝑅 : 𝐼 ⟶ Mnd )
9 1 2 3 8 prdsmndd ( 𝜑𝑌 ∈ Mnd )
10 tmdtps ( 𝑥 ∈ TopMnd → 𝑥 ∈ TopSp )
11 10 ssriv TopMnd ⊆ TopSp
12 fss ( ( 𝑅 : 𝐼 ⟶ TopMnd ∧ TopMnd ⊆ TopSp ) → 𝑅 : 𝐼 ⟶ TopSp )
13 4 11 12 sylancl ( 𝜑𝑅 : 𝐼 ⟶ TopSp )
14 1 3 2 13 prdstps ( 𝜑𝑌 ∈ TopSp )
15 eqid ( Base ‘ 𝑌 ) = ( Base ‘ 𝑌 )
16 3 3ad2ant1 ( ( 𝜑𝑓 ∈ ( Base ‘ 𝑌 ) ∧ 𝑔 ∈ ( Base ‘ 𝑌 ) ) → 𝑆𝑉 )
17 2 3ad2ant1 ( ( 𝜑𝑓 ∈ ( Base ‘ 𝑌 ) ∧ 𝑔 ∈ ( Base ‘ 𝑌 ) ) → 𝐼𝑊 )
18 4 ffnd ( 𝜑𝑅 Fn 𝐼 )
19 18 3ad2ant1 ( ( 𝜑𝑓 ∈ ( Base ‘ 𝑌 ) ∧ 𝑔 ∈ ( Base ‘ 𝑌 ) ) → 𝑅 Fn 𝐼 )
20 simp2 ( ( 𝜑𝑓 ∈ ( Base ‘ 𝑌 ) ∧ 𝑔 ∈ ( Base ‘ 𝑌 ) ) → 𝑓 ∈ ( Base ‘ 𝑌 ) )
21 simp3 ( ( 𝜑𝑓 ∈ ( Base ‘ 𝑌 ) ∧ 𝑔 ∈ ( Base ‘ 𝑌 ) ) → 𝑔 ∈ ( Base ‘ 𝑌 ) )
22 eqid ( +g𝑌 ) = ( +g𝑌 )
23 1 15 16 17 19 20 21 22 prdsplusgval ( ( 𝜑𝑓 ∈ ( Base ‘ 𝑌 ) ∧ 𝑔 ∈ ( Base ‘ 𝑌 ) ) → ( 𝑓 ( +g𝑌 ) 𝑔 ) = ( 𝑘𝐼 ↦ ( ( 𝑓𝑘 ) ( +g ‘ ( 𝑅𝑘 ) ) ( 𝑔𝑘 ) ) ) )
24 23 mpoeq3dva ( 𝜑 → ( 𝑓 ∈ ( Base ‘ 𝑌 ) , 𝑔 ∈ ( Base ‘ 𝑌 ) ↦ ( 𝑓 ( +g𝑌 ) 𝑔 ) ) = ( 𝑓 ∈ ( Base ‘ 𝑌 ) , 𝑔 ∈ ( Base ‘ 𝑌 ) ↦ ( 𝑘𝐼 ↦ ( ( 𝑓𝑘 ) ( +g ‘ ( 𝑅𝑘 ) ) ( 𝑔𝑘 ) ) ) ) )
25 eqid ( +𝑓𝑌 ) = ( +𝑓𝑌 )
26 15 22 25 plusffval ( +𝑓𝑌 ) = ( 𝑓 ∈ ( Base ‘ 𝑌 ) , 𝑔 ∈ ( Base ‘ 𝑌 ) ↦ ( 𝑓 ( +g𝑌 ) 𝑔 ) )
27 vex 𝑓 ∈ V
28 vex 𝑔 ∈ V
29 27 28 op1std ( 𝑧 = ⟨ 𝑓 , 𝑔 ⟩ → ( 1st𝑧 ) = 𝑓 )
30 29 fveq1d ( 𝑧 = ⟨ 𝑓 , 𝑔 ⟩ → ( ( 1st𝑧 ) ‘ 𝑘 ) = ( 𝑓𝑘 ) )
31 27 28 op2ndd ( 𝑧 = ⟨ 𝑓 , 𝑔 ⟩ → ( 2nd𝑧 ) = 𝑔 )
32 31 fveq1d ( 𝑧 = ⟨ 𝑓 , 𝑔 ⟩ → ( ( 2nd𝑧 ) ‘ 𝑘 ) = ( 𝑔𝑘 ) )
33 30 32 oveq12d ( 𝑧 = ⟨ 𝑓 , 𝑔 ⟩ → ( ( ( 1st𝑧 ) ‘ 𝑘 ) ( +g ‘ ( 𝑅𝑘 ) ) ( ( 2nd𝑧 ) ‘ 𝑘 ) ) = ( ( 𝑓𝑘 ) ( +g ‘ ( 𝑅𝑘 ) ) ( 𝑔𝑘 ) ) )
34 33 mpteq2dv ( 𝑧 = ⟨ 𝑓 , 𝑔 ⟩ → ( 𝑘𝐼 ↦ ( ( ( 1st𝑧 ) ‘ 𝑘 ) ( +g ‘ ( 𝑅𝑘 ) ) ( ( 2nd𝑧 ) ‘ 𝑘 ) ) ) = ( 𝑘𝐼 ↦ ( ( 𝑓𝑘 ) ( +g ‘ ( 𝑅𝑘 ) ) ( 𝑔𝑘 ) ) ) )
35 34 mpompt ( 𝑧 ∈ ( ( Base ‘ 𝑌 ) × ( Base ‘ 𝑌 ) ) ↦ ( 𝑘𝐼 ↦ ( ( ( 1st𝑧 ) ‘ 𝑘 ) ( +g ‘ ( 𝑅𝑘 ) ) ( ( 2nd𝑧 ) ‘ 𝑘 ) ) ) ) = ( 𝑓 ∈ ( Base ‘ 𝑌 ) , 𝑔 ∈ ( Base ‘ 𝑌 ) ↦ ( 𝑘𝐼 ↦ ( ( 𝑓𝑘 ) ( +g ‘ ( 𝑅𝑘 ) ) ( 𝑔𝑘 ) ) ) )
36 24 26 35 3eqtr4g ( 𝜑 → ( +𝑓𝑌 ) = ( 𝑧 ∈ ( ( Base ‘ 𝑌 ) × ( Base ‘ 𝑌 ) ) ↦ ( 𝑘𝐼 ↦ ( ( ( 1st𝑧 ) ‘ 𝑘 ) ( +g ‘ ( 𝑅𝑘 ) ) ( ( 2nd𝑧 ) ‘ 𝑘 ) ) ) ) )
37 eqid ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) = ( ∏t ‘ ( TopOpen ∘ 𝑅 ) )
38 eqid ( TopOpen ‘ 𝑌 ) = ( TopOpen ‘ 𝑌 )
39 15 38 istps ( 𝑌 ∈ TopSp ↔ ( TopOpen ‘ 𝑌 ) ∈ ( TopOn ‘ ( Base ‘ 𝑌 ) ) )
40 14 39 sylib ( 𝜑 → ( TopOpen ‘ 𝑌 ) ∈ ( TopOn ‘ ( Base ‘ 𝑌 ) ) )
41 txtopon ( ( ( TopOpen ‘ 𝑌 ) ∈ ( TopOn ‘ ( Base ‘ 𝑌 ) ) ∧ ( TopOpen ‘ 𝑌 ) ∈ ( TopOn ‘ ( Base ‘ 𝑌 ) ) ) → ( ( TopOpen ‘ 𝑌 ) ×t ( TopOpen ‘ 𝑌 ) ) ∈ ( TopOn ‘ ( ( Base ‘ 𝑌 ) × ( Base ‘ 𝑌 ) ) ) )
42 40 40 41 syl2anc ( 𝜑 → ( ( TopOpen ‘ 𝑌 ) ×t ( TopOpen ‘ 𝑌 ) ) ∈ ( TopOn ‘ ( ( Base ‘ 𝑌 ) × ( Base ‘ 𝑌 ) ) ) )
43 topnfn TopOpen Fn V
44 ssv TopSp ⊆ V
45 fnssres ( ( TopOpen Fn V ∧ TopSp ⊆ V ) → ( TopOpen ↾ TopSp ) Fn TopSp )
46 43 44 45 mp2an ( TopOpen ↾ TopSp ) Fn TopSp
47 fvres ( 𝑥 ∈ TopSp → ( ( TopOpen ↾ TopSp ) ‘ 𝑥 ) = ( TopOpen ‘ 𝑥 ) )
48 eqid ( TopOpen ‘ 𝑥 ) = ( TopOpen ‘ 𝑥 )
49 48 tpstop ( 𝑥 ∈ TopSp → ( TopOpen ‘ 𝑥 ) ∈ Top )
50 47 49 eqeltrd ( 𝑥 ∈ TopSp → ( ( TopOpen ↾ TopSp ) ‘ 𝑥 ) ∈ Top )
51 50 rgen 𝑥 ∈ TopSp ( ( TopOpen ↾ TopSp ) ‘ 𝑥 ) ∈ Top
52 ffnfv ( ( TopOpen ↾ TopSp ) : TopSp ⟶ Top ↔ ( ( TopOpen ↾ TopSp ) Fn TopSp ∧ ∀ 𝑥 ∈ TopSp ( ( TopOpen ↾ TopSp ) ‘ 𝑥 ) ∈ Top ) )
53 46 51 52 mpbir2an ( TopOpen ↾ TopSp ) : TopSp ⟶ Top
54 fco2 ( ( ( TopOpen ↾ TopSp ) : TopSp ⟶ Top ∧ 𝑅 : 𝐼 ⟶ TopSp ) → ( TopOpen ∘ 𝑅 ) : 𝐼 ⟶ Top )
55 53 13 54 sylancr ( 𝜑 → ( TopOpen ∘ 𝑅 ) : 𝐼 ⟶ Top )
56 33 mpompt ( 𝑧 ∈ ( ( Base ‘ 𝑌 ) × ( Base ‘ 𝑌 ) ) ↦ ( ( ( 1st𝑧 ) ‘ 𝑘 ) ( +g ‘ ( 𝑅𝑘 ) ) ( ( 2nd𝑧 ) ‘ 𝑘 ) ) ) = ( 𝑓 ∈ ( Base ‘ 𝑌 ) , 𝑔 ∈ ( Base ‘ 𝑌 ) ↦ ( ( 𝑓𝑘 ) ( +g ‘ ( 𝑅𝑘 ) ) ( 𝑔𝑘 ) ) )
57 eqid ( TopOpen ‘ ( 𝑅𝑘 ) ) = ( TopOpen ‘ ( 𝑅𝑘 ) )
58 eqid ( +g ‘ ( 𝑅𝑘 ) ) = ( +g ‘ ( 𝑅𝑘 ) )
59 4 ffvelrnda ( ( 𝜑𝑘𝐼 ) → ( 𝑅𝑘 ) ∈ TopMnd )
60 40 adantr ( ( 𝜑𝑘𝐼 ) → ( TopOpen ‘ 𝑌 ) ∈ ( TopOn ‘ ( Base ‘ 𝑌 ) ) )
61 60 60 cnmpt1st ( ( 𝜑𝑘𝐼 ) → ( 𝑓 ∈ ( Base ‘ 𝑌 ) , 𝑔 ∈ ( Base ‘ 𝑌 ) ↦ 𝑓 ) ∈ ( ( ( TopOpen ‘ 𝑌 ) ×t ( TopOpen ‘ 𝑌 ) ) Cn ( TopOpen ‘ 𝑌 ) ) )
62 1 3 2 18 38 prdstopn ( 𝜑 → ( TopOpen ‘ 𝑌 ) = ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) )
63 62 adantr ( ( 𝜑𝑘𝐼 ) → ( TopOpen ‘ 𝑌 ) = ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) )
64 63 60 eqeltrrd ( ( 𝜑𝑘𝐼 ) → ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) ∈ ( TopOn ‘ ( Base ‘ 𝑌 ) ) )
65 toponuni ( ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) ∈ ( TopOn ‘ ( Base ‘ 𝑌 ) ) → ( Base ‘ 𝑌 ) = ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) )
66 64 65 syl ( ( 𝜑𝑘𝐼 ) → ( Base ‘ 𝑌 ) = ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) )
67 66 mpteq1d ( ( 𝜑𝑘𝐼 ) → ( 𝑥 ∈ ( Base ‘ 𝑌 ) ↦ ( 𝑥𝑘 ) ) = ( 𝑥 ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) ↦ ( 𝑥𝑘 ) ) )
68 2 adantr ( ( 𝜑𝑘𝐼 ) → 𝐼𝑊 )
69 55 adantr ( ( 𝜑𝑘𝐼 ) → ( TopOpen ∘ 𝑅 ) : 𝐼 ⟶ Top )
70 simpr ( ( 𝜑𝑘𝐼 ) → 𝑘𝐼 )
71 eqid ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) = ( ∏t ‘ ( TopOpen ∘ 𝑅 ) )
72 71 37 ptpjcn ( ( 𝐼𝑊 ∧ ( TopOpen ∘ 𝑅 ) : 𝐼 ⟶ Top ∧ 𝑘𝐼 ) → ( 𝑥 ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) ↦ ( 𝑥𝑘 ) ) ∈ ( ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) Cn ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ) )
73 68 69 70 72 syl3anc ( ( 𝜑𝑘𝐼 ) → ( 𝑥 ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) ↦ ( 𝑥𝑘 ) ) ∈ ( ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) Cn ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ) )
74 67 73 eqeltrd ( ( 𝜑𝑘𝐼 ) → ( 𝑥 ∈ ( Base ‘ 𝑌 ) ↦ ( 𝑥𝑘 ) ) ∈ ( ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) Cn ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ) )
75 63 eqcomd ( ( 𝜑𝑘𝐼 ) → ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) = ( TopOpen ‘ 𝑌 ) )
76 fvco3 ( ( 𝑅 : 𝐼 ⟶ TopMnd ∧ 𝑘𝐼 ) → ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) = ( TopOpen ‘ ( 𝑅𝑘 ) ) )
77 4 76 sylan ( ( 𝜑𝑘𝐼 ) → ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) = ( TopOpen ‘ ( 𝑅𝑘 ) ) )
78 75 77 oveq12d ( ( 𝜑𝑘𝐼 ) → ( ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) Cn ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ) = ( ( TopOpen ‘ 𝑌 ) Cn ( TopOpen ‘ ( 𝑅𝑘 ) ) ) )
79 74 78 eleqtrd ( ( 𝜑𝑘𝐼 ) → ( 𝑥 ∈ ( Base ‘ 𝑌 ) ↦ ( 𝑥𝑘 ) ) ∈ ( ( TopOpen ‘ 𝑌 ) Cn ( TopOpen ‘ ( 𝑅𝑘 ) ) ) )
80 fveq1 ( 𝑥 = 𝑓 → ( 𝑥𝑘 ) = ( 𝑓𝑘 ) )
81 60 60 61 60 79 80 cnmpt21 ( ( 𝜑𝑘𝐼 ) → ( 𝑓 ∈ ( Base ‘ 𝑌 ) , 𝑔 ∈ ( Base ‘ 𝑌 ) ↦ ( 𝑓𝑘 ) ) ∈ ( ( ( TopOpen ‘ 𝑌 ) ×t ( TopOpen ‘ 𝑌 ) ) Cn ( TopOpen ‘ ( 𝑅𝑘 ) ) ) )
82 60 60 cnmpt2nd ( ( 𝜑𝑘𝐼 ) → ( 𝑓 ∈ ( Base ‘ 𝑌 ) , 𝑔 ∈ ( Base ‘ 𝑌 ) ↦ 𝑔 ) ∈ ( ( ( TopOpen ‘ 𝑌 ) ×t ( TopOpen ‘ 𝑌 ) ) Cn ( TopOpen ‘ 𝑌 ) ) )
83 fveq1 ( 𝑥 = 𝑔 → ( 𝑥𝑘 ) = ( 𝑔𝑘 ) )
84 60 60 82 60 79 83 cnmpt21 ( ( 𝜑𝑘𝐼 ) → ( 𝑓 ∈ ( Base ‘ 𝑌 ) , 𝑔 ∈ ( Base ‘ 𝑌 ) ↦ ( 𝑔𝑘 ) ) ∈ ( ( ( TopOpen ‘ 𝑌 ) ×t ( TopOpen ‘ 𝑌 ) ) Cn ( TopOpen ‘ ( 𝑅𝑘 ) ) ) )
85 57 58 59 60 60 81 84 cnmpt2plusg ( ( 𝜑𝑘𝐼 ) → ( 𝑓 ∈ ( Base ‘ 𝑌 ) , 𝑔 ∈ ( Base ‘ 𝑌 ) ↦ ( ( 𝑓𝑘 ) ( +g ‘ ( 𝑅𝑘 ) ) ( 𝑔𝑘 ) ) ) ∈ ( ( ( TopOpen ‘ 𝑌 ) ×t ( TopOpen ‘ 𝑌 ) ) Cn ( TopOpen ‘ ( 𝑅𝑘 ) ) ) )
86 77 oveq2d ( ( 𝜑𝑘𝐼 ) → ( ( ( TopOpen ‘ 𝑌 ) ×t ( TopOpen ‘ 𝑌 ) ) Cn ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ) = ( ( ( TopOpen ‘ 𝑌 ) ×t ( TopOpen ‘ 𝑌 ) ) Cn ( TopOpen ‘ ( 𝑅𝑘 ) ) ) )
87 85 86 eleqtrrd ( ( 𝜑𝑘𝐼 ) → ( 𝑓 ∈ ( Base ‘ 𝑌 ) , 𝑔 ∈ ( Base ‘ 𝑌 ) ↦ ( ( 𝑓𝑘 ) ( +g ‘ ( 𝑅𝑘 ) ) ( 𝑔𝑘 ) ) ) ∈ ( ( ( TopOpen ‘ 𝑌 ) ×t ( TopOpen ‘ 𝑌 ) ) Cn ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ) )
88 56 87 eqeltrid ( ( 𝜑𝑘𝐼 ) → ( 𝑧 ∈ ( ( Base ‘ 𝑌 ) × ( Base ‘ 𝑌 ) ) ↦ ( ( ( 1st𝑧 ) ‘ 𝑘 ) ( +g ‘ ( 𝑅𝑘 ) ) ( ( 2nd𝑧 ) ‘ 𝑘 ) ) ) ∈ ( ( ( TopOpen ‘ 𝑌 ) ×t ( TopOpen ‘ 𝑌 ) ) Cn ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ) )
89 37 42 2 55 88 ptcn ( 𝜑 → ( 𝑧 ∈ ( ( Base ‘ 𝑌 ) × ( Base ‘ 𝑌 ) ) ↦ ( 𝑘𝐼 ↦ ( ( ( 1st𝑧 ) ‘ 𝑘 ) ( +g ‘ ( 𝑅𝑘 ) ) ( ( 2nd𝑧 ) ‘ 𝑘 ) ) ) ) ∈ ( ( ( TopOpen ‘ 𝑌 ) ×t ( TopOpen ‘ 𝑌 ) ) Cn ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) ) )
90 36 89 eqeltrd ( 𝜑 → ( +𝑓𝑌 ) ∈ ( ( ( TopOpen ‘ 𝑌 ) ×t ( TopOpen ‘ 𝑌 ) ) Cn ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) ) )
91 62 oveq2d ( 𝜑 → ( ( ( TopOpen ‘ 𝑌 ) ×t ( TopOpen ‘ 𝑌 ) ) Cn ( TopOpen ‘ 𝑌 ) ) = ( ( ( TopOpen ‘ 𝑌 ) ×t ( TopOpen ‘ 𝑌 ) ) Cn ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) ) )
92 90 91 eleqtrrd ( 𝜑 → ( +𝑓𝑌 ) ∈ ( ( ( TopOpen ‘ 𝑌 ) ×t ( TopOpen ‘ 𝑌 ) ) Cn ( TopOpen ‘ 𝑌 ) ) )
93 25 38 istmd ( 𝑌 ∈ TopMnd ↔ ( 𝑌 ∈ Mnd ∧ 𝑌 ∈ TopSp ∧ ( +𝑓𝑌 ) ∈ ( ( ( TopOpen ‘ 𝑌 ) ×t ( TopOpen ‘ 𝑌 ) ) Cn ( TopOpen ‘ 𝑌 ) ) ) )
94 9 14 92 93 syl3anbrc ( 𝜑𝑌 ∈ TopMnd )