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 )