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 Xs_ R )
prdstmdd.i
|- ( ph -> I e. W )
prdstmdd.s
|- ( ph -> S e. V )
prdstmdd.r
|- ( ph -> R : I --> TopMnd )
Assertion prdstmdd
|- ( ph -> Y e. TopMnd )

Proof

Step Hyp Ref Expression
1 prdstmdd.y
 |-  Y = ( S Xs_ R )
2 prdstmdd.i
 |-  ( ph -> I e. W )
3 prdstmdd.s
 |-  ( ph -> S e. V )
4 prdstmdd.r
 |-  ( ph -> R : I --> TopMnd )
5 tmdmnd
 |-  ( x e. TopMnd -> x e. Mnd )
6 5 ssriv
 |-  TopMnd C_ Mnd
7 fss
 |-  ( ( R : I --> TopMnd /\ TopMnd C_ Mnd ) -> R : I --> Mnd )
8 4 6 7 sylancl
 |-  ( ph -> R : I --> Mnd )
9 1 2 3 8 prdsmndd
 |-  ( ph -> Y e. Mnd )
10 tmdtps
 |-  ( x e. TopMnd -> x e. TopSp )
11 10 ssriv
 |-  TopMnd C_ TopSp
12 fss
 |-  ( ( R : I --> TopMnd /\ TopMnd C_ TopSp ) -> R : I --> TopSp )
13 4 11 12 sylancl
 |-  ( ph -> R : I --> TopSp )
14 1 3 2 13 prdstps
 |-  ( ph -> Y e. TopSp )
15 eqid
 |-  ( Base ` Y ) = ( Base ` Y )
16 3 3ad2ant1
 |-  ( ( ph /\ f e. ( Base ` Y ) /\ g e. ( Base ` Y ) ) -> S e. V )
17 2 3ad2ant1
 |-  ( ( ph /\ f e. ( Base ` Y ) /\ g e. ( Base ` Y ) ) -> I e. W )
18 4 ffnd
 |-  ( ph -> R Fn I )
19 18 3ad2ant1
 |-  ( ( ph /\ f e. ( Base ` Y ) /\ g e. ( Base ` Y ) ) -> R Fn I )
20 simp2
 |-  ( ( ph /\ f e. ( Base ` Y ) /\ g e. ( Base ` Y ) ) -> f e. ( Base ` Y ) )
21 simp3
 |-  ( ( ph /\ f e. ( Base ` Y ) /\ g e. ( Base ` Y ) ) -> g e. ( Base ` Y ) )
22 eqid
 |-  ( +g ` Y ) = ( +g ` Y )
23 1 15 16 17 19 20 21 22 prdsplusgval
 |-  ( ( ph /\ f e. ( Base ` Y ) /\ g e. ( Base ` Y ) ) -> ( f ( +g ` Y ) g ) = ( k e. I |-> ( ( f ` k ) ( +g ` ( R ` k ) ) ( g ` k ) ) ) )
24 23 mpoeq3dva
 |-  ( ph -> ( f e. ( Base ` Y ) , g e. ( Base ` Y ) |-> ( f ( +g ` Y ) g ) ) = ( f e. ( Base ` Y ) , g e. ( Base ` Y ) |-> ( k e. I |-> ( ( f ` k ) ( +g ` ( R ` k ) ) ( g ` k ) ) ) ) )
25 eqid
 |-  ( +f ` Y ) = ( +f ` Y )
26 15 22 25 plusffval
 |-  ( +f ` Y ) = ( f e. ( Base ` Y ) , g e. ( Base ` Y ) |-> ( f ( +g ` Y ) g ) )
27 vex
 |-  f e. _V
28 vex
 |-  g e. _V
29 27 28 op1std
 |-  ( z = <. f , g >. -> ( 1st ` z ) = f )
30 29 fveq1d
 |-  ( z = <. f , g >. -> ( ( 1st ` z ) ` k ) = ( f ` k ) )
31 27 28 op2ndd
 |-  ( z = <. f , g >. -> ( 2nd ` z ) = g )
32 31 fveq1d
 |-  ( z = <. f , g >. -> ( ( 2nd ` z ) ` k ) = ( g ` k ) )
33 30 32 oveq12d
 |-  ( z = <. f , g >. -> ( ( ( 1st ` z ) ` k ) ( +g ` ( R ` k ) ) ( ( 2nd ` z ) ` k ) ) = ( ( f ` k ) ( +g ` ( R ` k ) ) ( g ` k ) ) )
34 33 mpteq2dv
 |-  ( z = <. f , g >. -> ( k e. I |-> ( ( ( 1st ` z ) ` k ) ( +g ` ( R ` k ) ) ( ( 2nd ` z ) ` k ) ) ) = ( k e. I |-> ( ( f ` k ) ( +g ` ( R ` k ) ) ( g ` k ) ) ) )
35 34 mpompt
 |-  ( z e. ( ( Base ` Y ) X. ( Base ` Y ) ) |-> ( k e. I |-> ( ( ( 1st ` z ) ` k ) ( +g ` ( R ` k ) ) ( ( 2nd ` z ) ` k ) ) ) ) = ( f e. ( Base ` Y ) , g e. ( Base ` Y ) |-> ( k e. I |-> ( ( f ` k ) ( +g ` ( R ` k ) ) ( g ` k ) ) ) )
36 24 26 35 3eqtr4g
 |-  ( ph -> ( +f ` Y ) = ( z e. ( ( Base ` Y ) X. ( Base ` Y ) ) |-> ( k e. I |-> ( ( ( 1st ` z ) ` k ) ( +g ` ( R ` k ) ) ( ( 2nd ` z ) ` k ) ) ) ) )
37 eqid
 |-  ( Xt_ ` ( TopOpen o. R ) ) = ( Xt_ ` ( TopOpen o. R ) )
38 eqid
 |-  ( TopOpen ` Y ) = ( TopOpen ` Y )
39 15 38 istps
 |-  ( Y e. TopSp <-> ( TopOpen ` Y ) e. ( TopOn ` ( Base ` Y ) ) )
40 14 39 sylib
 |-  ( ph -> ( TopOpen ` Y ) e. ( TopOn ` ( Base ` Y ) ) )
41 txtopon
 |-  ( ( ( TopOpen ` Y ) e. ( TopOn ` ( Base ` Y ) ) /\ ( TopOpen ` Y ) e. ( TopOn ` ( Base ` Y ) ) ) -> ( ( TopOpen ` Y ) tX ( TopOpen ` Y ) ) e. ( TopOn ` ( ( Base ` Y ) X. ( Base ` Y ) ) ) )
42 40 40 41 syl2anc
 |-  ( ph -> ( ( TopOpen ` Y ) tX ( TopOpen ` Y ) ) e. ( TopOn ` ( ( Base ` Y ) X. ( Base ` Y ) ) ) )
43 topnfn
 |-  TopOpen Fn _V
44 ssv
 |-  TopSp C_ _V
45 fnssres
 |-  ( ( TopOpen Fn _V /\ TopSp C_ _V ) -> ( TopOpen |` TopSp ) Fn TopSp )
46 43 44 45 mp2an
 |-  ( TopOpen |` TopSp ) Fn TopSp
47 fvres
 |-  ( x e. TopSp -> ( ( TopOpen |` TopSp ) ` x ) = ( TopOpen ` x ) )
48 eqid
 |-  ( TopOpen ` x ) = ( TopOpen ` x )
49 48 tpstop
 |-  ( x e. TopSp -> ( TopOpen ` x ) e. Top )
50 47 49 eqeltrd
 |-  ( x e. TopSp -> ( ( TopOpen |` TopSp ) ` x ) e. Top )
51 50 rgen
 |-  A. x e. TopSp ( ( TopOpen |` TopSp ) ` x ) e. Top
52 ffnfv
 |-  ( ( TopOpen |` TopSp ) : TopSp --> Top <-> ( ( TopOpen |` TopSp ) Fn TopSp /\ A. x e. TopSp ( ( TopOpen |` TopSp ) ` x ) e. Top ) )
53 46 51 52 mpbir2an
 |-  ( TopOpen |` TopSp ) : TopSp --> Top
54 fco2
 |-  ( ( ( TopOpen |` TopSp ) : TopSp --> Top /\ R : I --> TopSp ) -> ( TopOpen o. R ) : I --> Top )
55 53 13 54 sylancr
 |-  ( ph -> ( TopOpen o. R ) : I --> Top )
56 33 mpompt
 |-  ( z e. ( ( Base ` Y ) X. ( Base ` Y ) ) |-> ( ( ( 1st ` z ) ` k ) ( +g ` ( R ` k ) ) ( ( 2nd ` z ) ` k ) ) ) = ( f e. ( Base ` Y ) , g e. ( Base ` Y ) |-> ( ( f ` k ) ( +g ` ( R ` k ) ) ( g ` k ) ) )
57 eqid
 |-  ( TopOpen ` ( R ` k ) ) = ( TopOpen ` ( R ` k ) )
58 eqid
 |-  ( +g ` ( R ` k ) ) = ( +g ` ( R ` k ) )
59 4 ffvelrnda
 |-  ( ( ph /\ k e. I ) -> ( R ` k ) e. TopMnd )
60 40 adantr
 |-  ( ( ph /\ k e. I ) -> ( TopOpen ` Y ) e. ( TopOn ` ( Base ` Y ) ) )
61 60 60 cnmpt1st
 |-  ( ( ph /\ k e. I ) -> ( f e. ( Base ` Y ) , g e. ( Base ` Y ) |-> f ) e. ( ( ( TopOpen ` Y ) tX ( TopOpen ` Y ) ) Cn ( TopOpen ` Y ) ) )
62 1 3 2 18 38 prdstopn
 |-  ( ph -> ( TopOpen ` Y ) = ( Xt_ ` ( TopOpen o. R ) ) )
63 62 adantr
 |-  ( ( ph /\ k e. I ) -> ( TopOpen ` Y ) = ( Xt_ ` ( TopOpen o. R ) ) )
64 63 60 eqeltrrd
 |-  ( ( ph /\ k e. I ) -> ( Xt_ ` ( TopOpen o. R ) ) e. ( TopOn ` ( Base ` Y ) ) )
65 toponuni
 |-  ( ( Xt_ ` ( TopOpen o. R ) ) e. ( TopOn ` ( Base ` Y ) ) -> ( Base ` Y ) = U. ( Xt_ ` ( TopOpen o. R ) ) )
66 64 65 syl
 |-  ( ( ph /\ k e. I ) -> ( Base ` Y ) = U. ( Xt_ ` ( TopOpen o. R ) ) )
67 66 mpteq1d
 |-  ( ( ph /\ k e. I ) -> ( x e. ( Base ` Y ) |-> ( x ` k ) ) = ( x e. U. ( Xt_ ` ( TopOpen o. R ) ) |-> ( x ` k ) ) )
68 2 adantr
 |-  ( ( ph /\ k e. I ) -> I e. W )
69 55 adantr
 |-  ( ( ph /\ k e. I ) -> ( TopOpen o. R ) : I --> Top )
70 simpr
 |-  ( ( ph /\ k e. I ) -> k e. I )
71 eqid
 |-  U. ( Xt_ ` ( TopOpen o. R ) ) = U. ( Xt_ ` ( TopOpen o. R ) )
72 71 37 ptpjcn
 |-  ( ( I e. W /\ ( TopOpen o. R ) : I --> Top /\ k e. I ) -> ( x e. U. ( Xt_ ` ( TopOpen o. R ) ) |-> ( x ` k ) ) e. ( ( Xt_ ` ( TopOpen o. R ) ) Cn ( ( TopOpen o. R ) ` k ) ) )
73 68 69 70 72 syl3anc
 |-  ( ( ph /\ k e. I ) -> ( x e. U. ( Xt_ ` ( TopOpen o. R ) ) |-> ( x ` k ) ) e. ( ( Xt_ ` ( TopOpen o. R ) ) Cn ( ( TopOpen o. R ) ` k ) ) )
74 67 73 eqeltrd
 |-  ( ( ph /\ k e. I ) -> ( x e. ( Base ` Y ) |-> ( x ` k ) ) e. ( ( Xt_ ` ( TopOpen o. R ) ) Cn ( ( TopOpen o. R ) ` k ) ) )
75 63 eqcomd
 |-  ( ( ph /\ k e. I ) -> ( Xt_ ` ( TopOpen o. R ) ) = ( TopOpen ` Y ) )
76 fvco3
 |-  ( ( R : I --> TopMnd /\ k e. I ) -> ( ( TopOpen o. R ) ` k ) = ( TopOpen ` ( R ` k ) ) )
77 4 76 sylan
 |-  ( ( ph /\ k e. I ) -> ( ( TopOpen o. R ) ` k ) = ( TopOpen ` ( R ` k ) ) )
78 75 77 oveq12d
 |-  ( ( ph /\ k e. I ) -> ( ( Xt_ ` ( TopOpen o. R ) ) Cn ( ( TopOpen o. R ) ` k ) ) = ( ( TopOpen ` Y ) Cn ( TopOpen ` ( R ` k ) ) ) )
79 74 78 eleqtrd
 |-  ( ( ph /\ k e. I ) -> ( x e. ( Base ` Y ) |-> ( x ` k ) ) e. ( ( TopOpen ` Y ) Cn ( TopOpen ` ( R ` k ) ) ) )
80 fveq1
 |-  ( x = f -> ( x ` k ) = ( f ` k ) )
81 60 60 61 60 79 80 cnmpt21
 |-  ( ( ph /\ k e. I ) -> ( f e. ( Base ` Y ) , g e. ( Base ` Y ) |-> ( f ` k ) ) e. ( ( ( TopOpen ` Y ) tX ( TopOpen ` Y ) ) Cn ( TopOpen ` ( R ` k ) ) ) )
82 60 60 cnmpt2nd
 |-  ( ( ph /\ k e. I ) -> ( f e. ( Base ` Y ) , g e. ( Base ` Y ) |-> g ) e. ( ( ( TopOpen ` Y ) tX ( TopOpen ` Y ) ) Cn ( TopOpen ` Y ) ) )
83 fveq1
 |-  ( x = g -> ( x ` k ) = ( g ` k ) )
84 60 60 82 60 79 83 cnmpt21
 |-  ( ( ph /\ k e. I ) -> ( f e. ( Base ` Y ) , g e. ( Base ` Y ) |-> ( g ` k ) ) e. ( ( ( TopOpen ` Y ) tX ( TopOpen ` Y ) ) Cn ( TopOpen ` ( R ` k ) ) ) )
85 57 58 59 60 60 81 84 cnmpt2plusg
 |-  ( ( ph /\ k e. I ) -> ( f e. ( Base ` Y ) , g e. ( Base ` Y ) |-> ( ( f ` k ) ( +g ` ( R ` k ) ) ( g ` k ) ) ) e. ( ( ( TopOpen ` Y ) tX ( TopOpen ` Y ) ) Cn ( TopOpen ` ( R ` k ) ) ) )
86 77 oveq2d
 |-  ( ( ph /\ k e. I ) -> ( ( ( TopOpen ` Y ) tX ( TopOpen ` Y ) ) Cn ( ( TopOpen o. R ) ` k ) ) = ( ( ( TopOpen ` Y ) tX ( TopOpen ` Y ) ) Cn ( TopOpen ` ( R ` k ) ) ) )
87 85 86 eleqtrrd
 |-  ( ( ph /\ k e. I ) -> ( f e. ( Base ` Y ) , g e. ( Base ` Y ) |-> ( ( f ` k ) ( +g ` ( R ` k ) ) ( g ` k ) ) ) e. ( ( ( TopOpen ` Y ) tX ( TopOpen ` Y ) ) Cn ( ( TopOpen o. R ) ` k ) ) )
88 56 87 eqeltrid
 |-  ( ( ph /\ k e. I ) -> ( z e. ( ( Base ` Y ) X. ( Base ` Y ) ) |-> ( ( ( 1st ` z ) ` k ) ( +g ` ( R ` k ) ) ( ( 2nd ` z ) ` k ) ) ) e. ( ( ( TopOpen ` Y ) tX ( TopOpen ` Y ) ) Cn ( ( TopOpen o. R ) ` k ) ) )
89 37 42 2 55 88 ptcn
 |-  ( ph -> ( z e. ( ( Base ` Y ) X. ( Base ` Y ) ) |-> ( k e. I |-> ( ( ( 1st ` z ) ` k ) ( +g ` ( R ` k ) ) ( ( 2nd ` z ) ` k ) ) ) ) e. ( ( ( TopOpen ` Y ) tX ( TopOpen ` Y ) ) Cn ( Xt_ ` ( TopOpen o. R ) ) ) )
90 36 89 eqeltrd
 |-  ( ph -> ( +f ` Y ) e. ( ( ( TopOpen ` Y ) tX ( TopOpen ` Y ) ) Cn ( Xt_ ` ( TopOpen o. R ) ) ) )
91 62 oveq2d
 |-  ( ph -> ( ( ( TopOpen ` Y ) tX ( TopOpen ` Y ) ) Cn ( TopOpen ` Y ) ) = ( ( ( TopOpen ` Y ) tX ( TopOpen ` Y ) ) Cn ( Xt_ ` ( TopOpen o. R ) ) ) )
92 90 91 eleqtrrd
 |-  ( ph -> ( +f ` Y ) e. ( ( ( TopOpen ` Y ) tX ( TopOpen ` Y ) ) Cn ( TopOpen ` Y ) ) )
93 25 38 istmd
 |-  ( Y e. TopMnd <-> ( Y e. Mnd /\ Y e. TopSp /\ ( +f ` Y ) e. ( ( ( TopOpen ` Y ) tX ( TopOpen ` Y ) ) Cn ( TopOpen ` Y ) ) ) )
94 9 14 92 93 syl3anbrc
 |-  ( ph -> Y e. TopMnd )