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 Y=S𝑠R
prdstmdd.i φIW
prdstmdd.s φSV
prdstmdd.r φR:ITopMnd
Assertion prdstmdd φYTopMnd

Proof

Step Hyp Ref Expression
1 prdstmdd.y Y=S𝑠R
2 prdstmdd.i φIW
3 prdstmdd.s φSV
4 prdstmdd.r φR:ITopMnd
5 tmdmnd xTopMndxMnd
6 5 ssriv TopMndMnd
7 fss R:ITopMndTopMndMndR:IMnd
8 4 6 7 sylancl φR:IMnd
9 1 2 3 8 prdsmndd φYMnd
10 tmdtps xTopMndxTopSp
11 10 ssriv TopMndTopSp
12 fss R:ITopMndTopMndTopSpR:ITopSp
13 4 11 12 sylancl φR:ITopSp
14 1 3 2 13 prdstps φYTopSp
15 eqid BaseY=BaseY
16 3 3ad2ant1 φfBaseYgBaseYSV
17 2 3ad2ant1 φfBaseYgBaseYIW
18 4 ffnd φRFnI
19 18 3ad2ant1 φfBaseYgBaseYRFnI
20 simp2 φfBaseYgBaseYfBaseY
21 simp3 φfBaseYgBaseYgBaseY
22 eqid +Y=+Y
23 1 15 16 17 19 20 21 22 prdsplusgval φfBaseYgBaseYf+Yg=kIfk+Rkgk
24 23 mpoeq3dva φfBaseY,gBaseYf+Yg=fBaseY,gBaseYkIfk+Rkgk
25 eqid +𝑓Y=+𝑓Y
26 15 22 25 plusffval +𝑓Y=fBaseY,gBaseYf+Yg
27 vex fV
28 vex gV
29 27 28 op1std z=fg1stz=f
30 29 fveq1d z=fg1stzk=fk
31 27 28 op2ndd z=fg2ndz=g
32 31 fveq1d z=fg2ndzk=gk
33 30 32 oveq12d z=fg1stzk+Rk2ndzk=fk+Rkgk
34 33 mpteq2dv z=fgkI1stzk+Rk2ndzk=kIfk+Rkgk
35 34 mpompt zBaseY×BaseYkI1stzk+Rk2ndzk=fBaseY,gBaseYkIfk+Rkgk
36 24 26 35 3eqtr4g φ+𝑓Y=zBaseY×BaseYkI1stzk+Rk2ndzk
37 eqid 𝑡TopOpenR=𝑡TopOpenR
38 eqid TopOpenY=TopOpenY
39 15 38 istps YTopSpTopOpenYTopOnBaseY
40 14 39 sylib φTopOpenYTopOnBaseY
41 txtopon TopOpenYTopOnBaseYTopOpenYTopOnBaseYTopOpenY×tTopOpenYTopOnBaseY×BaseY
42 40 40 41 syl2anc φTopOpenY×tTopOpenYTopOnBaseY×BaseY
43 topnfn TopOpenFnV
44 ssv TopSpV
45 fnssres TopOpenFnVTopSpVTopOpenTopSpFnTopSp
46 43 44 45 mp2an TopOpenTopSpFnTopSp
47 fvres xTopSpTopOpenTopSpx=TopOpenx
48 eqid TopOpenx=TopOpenx
49 48 tpstop xTopSpTopOpenxTop
50 47 49 eqeltrd xTopSpTopOpenTopSpxTop
51 50 rgen xTopSpTopOpenTopSpxTop
52 ffnfv TopOpenTopSp:TopSpTopTopOpenTopSpFnTopSpxTopSpTopOpenTopSpxTop
53 46 51 52 mpbir2an TopOpenTopSp:TopSpTop
54 fco2 TopOpenTopSp:TopSpTopR:ITopSpTopOpenR:ITop
55 53 13 54 sylancr φTopOpenR:ITop
56 33 mpompt zBaseY×BaseY1stzk+Rk2ndzk=fBaseY,gBaseYfk+Rkgk
57 eqid TopOpenRk=TopOpenRk
58 eqid +Rk=+Rk
59 4 ffvelrnda φkIRkTopMnd
60 40 adantr φkITopOpenYTopOnBaseY
61 60 60 cnmpt1st φkIfBaseY,gBaseYfTopOpenY×tTopOpenYCnTopOpenY
62 1 3 2 18 38 prdstopn φTopOpenY=𝑡TopOpenR
63 62 adantr φkITopOpenY=𝑡TopOpenR
64 63 60 eqeltrrd φkI𝑡TopOpenRTopOnBaseY
65 toponuni 𝑡TopOpenRTopOnBaseYBaseY=𝑡TopOpenR
66 64 65 syl φkIBaseY=𝑡TopOpenR
67 66 mpteq1d φkIxBaseYxk=x𝑡TopOpenRxk
68 2 adantr φkIIW
69 55 adantr φkITopOpenR:ITop
70 simpr φkIkI
71 eqid 𝑡TopOpenR=𝑡TopOpenR
72 71 37 ptpjcn IWTopOpenR:ITopkIx𝑡TopOpenRxk𝑡TopOpenRCnTopOpenRk
73 68 69 70 72 syl3anc φkIx𝑡TopOpenRxk𝑡TopOpenRCnTopOpenRk
74 67 73 eqeltrd φkIxBaseYxk𝑡TopOpenRCnTopOpenRk
75 63 eqcomd φkI𝑡TopOpenR=TopOpenY
76 fvco3 R:ITopMndkITopOpenRk=TopOpenRk
77 4 76 sylan φkITopOpenRk=TopOpenRk
78 75 77 oveq12d φkI𝑡TopOpenRCnTopOpenRk=TopOpenYCnTopOpenRk
79 74 78 eleqtrd φkIxBaseYxkTopOpenYCnTopOpenRk
80 fveq1 x=fxk=fk
81 60 60 61 60 79 80 cnmpt21 φkIfBaseY,gBaseYfkTopOpenY×tTopOpenYCnTopOpenRk
82 60 60 cnmpt2nd φkIfBaseY,gBaseYgTopOpenY×tTopOpenYCnTopOpenY
83 fveq1 x=gxk=gk
84 60 60 82 60 79 83 cnmpt21 φkIfBaseY,gBaseYgkTopOpenY×tTopOpenYCnTopOpenRk
85 57 58 59 60 60 81 84 cnmpt2plusg φkIfBaseY,gBaseYfk+RkgkTopOpenY×tTopOpenYCnTopOpenRk
86 77 oveq2d φkITopOpenY×tTopOpenYCnTopOpenRk=TopOpenY×tTopOpenYCnTopOpenRk
87 85 86 eleqtrrd φkIfBaseY,gBaseYfk+RkgkTopOpenY×tTopOpenYCnTopOpenRk
88 56 87 eqeltrid φkIzBaseY×BaseY1stzk+Rk2ndzkTopOpenY×tTopOpenYCnTopOpenRk
89 37 42 2 55 88 ptcn φzBaseY×BaseYkI1stzk+Rk2ndzkTopOpenY×tTopOpenYCn𝑡TopOpenR
90 36 89 eqeltrd φ+𝑓YTopOpenY×tTopOpenYCn𝑡TopOpenR
91 62 oveq2d φTopOpenY×tTopOpenYCnTopOpenY=TopOpenY×tTopOpenYCn𝑡TopOpenR
92 90 91 eleqtrrd φ+𝑓YTopOpenY×tTopOpenYCnTopOpenY
93 25 38 istmd YTopMndYMndYTopSp+𝑓YTopOpenY×tTopOpenYCnTopOpenY
94 9 14 92 93 syl3anbrc φYTopMnd