Metamath Proof Explorer


Theorem prdstgpd

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

Ref Expression
Hypotheses prdstgpd.y
|- Y = ( S Xs_ R )
prdstgpd.i
|- ( ph -> I e. W )
prdstgpd.s
|- ( ph -> S e. V )
prdstgpd.r
|- ( ph -> R : I --> TopGrp )
Assertion prdstgpd
|- ( ph -> Y e. TopGrp )

Proof

Step Hyp Ref Expression
1 prdstgpd.y
 |-  Y = ( S Xs_ R )
2 prdstgpd.i
 |-  ( ph -> I e. W )
3 prdstgpd.s
 |-  ( ph -> S e. V )
4 prdstgpd.r
 |-  ( ph -> R : I --> TopGrp )
5 tgpgrp
 |-  ( x e. TopGrp -> x e. Grp )
6 5 ssriv
 |-  TopGrp C_ Grp
7 fss
 |-  ( ( R : I --> TopGrp /\ TopGrp C_ Grp ) -> R : I --> Grp )
8 4 6 7 sylancl
 |-  ( ph -> R : I --> Grp )
9 1 2 3 8 prdsgrpd
 |-  ( ph -> Y e. Grp )
10 tgptmd
 |-  ( x e. TopGrp -> x e. TopMnd )
11 10 ssriv
 |-  TopGrp C_ TopMnd
12 fss
 |-  ( ( R : I --> TopGrp /\ TopGrp C_ TopMnd ) -> R : I --> TopMnd )
13 4 11 12 sylancl
 |-  ( ph -> R : I --> TopMnd )
14 1 2 3 13 prdstmdd
 |-  ( ph -> Y e. TopMnd )
15 eqid
 |-  ( Xt_ ` ( TopOpen o. R ) ) = ( Xt_ ` ( TopOpen o. R ) )
16 eqid
 |-  ( TopOpen ` Y ) = ( TopOpen ` Y )
17 eqid
 |-  ( Base ` Y ) = ( Base ` Y )
18 16 17 tmdtopon
 |-  ( Y e. TopMnd -> ( TopOpen ` Y ) e. ( TopOn ` ( Base ` Y ) ) )
19 14 18 syl
 |-  ( ph -> ( TopOpen ` Y ) e. ( TopOn ` ( Base ` Y ) ) )
20 topnfn
 |-  TopOpen Fn _V
21 4 ffnd
 |-  ( ph -> R Fn I )
22 dffn2
 |-  ( R Fn I <-> R : I --> _V )
23 21 22 sylib
 |-  ( ph -> R : I --> _V )
24 fnfco
 |-  ( ( TopOpen Fn _V /\ R : I --> _V ) -> ( TopOpen o. R ) Fn I )
25 20 23 24 sylancr
 |-  ( ph -> ( TopOpen o. R ) Fn I )
26 fvco3
 |-  ( ( R : I --> TopGrp /\ y e. I ) -> ( ( TopOpen o. R ) ` y ) = ( TopOpen ` ( R ` y ) ) )
27 4 26 sylan
 |-  ( ( ph /\ y e. I ) -> ( ( TopOpen o. R ) ` y ) = ( TopOpen ` ( R ` y ) ) )
28 4 ffvelrnda
 |-  ( ( ph /\ y e. I ) -> ( R ` y ) e. TopGrp )
29 eqid
 |-  ( TopOpen ` ( R ` y ) ) = ( TopOpen ` ( R ` y ) )
30 eqid
 |-  ( Base ` ( R ` y ) ) = ( Base ` ( R ` y ) )
31 29 30 tgptopon
 |-  ( ( R ` y ) e. TopGrp -> ( TopOpen ` ( R ` y ) ) e. ( TopOn ` ( Base ` ( R ` y ) ) ) )
32 topontop
 |-  ( ( TopOpen ` ( R ` y ) ) e. ( TopOn ` ( Base ` ( R ` y ) ) ) -> ( TopOpen ` ( R ` y ) ) e. Top )
33 28 31 32 3syl
 |-  ( ( ph /\ y e. I ) -> ( TopOpen ` ( R ` y ) ) e. Top )
34 27 33 eqeltrd
 |-  ( ( ph /\ y e. I ) -> ( ( TopOpen o. R ) ` y ) e. Top )
35 34 ralrimiva
 |-  ( ph -> A. y e. I ( ( TopOpen o. R ) ` y ) e. Top )
36 ffnfv
 |-  ( ( TopOpen o. R ) : I --> Top <-> ( ( TopOpen o. R ) Fn I /\ A. y e. I ( ( TopOpen o. R ) ` y ) e. Top ) )
37 25 35 36 sylanbrc
 |-  ( ph -> ( TopOpen o. R ) : I --> Top )
38 19 adantr
 |-  ( ( ph /\ y e. I ) -> ( TopOpen ` Y ) e. ( TopOn ` ( Base ` Y ) ) )
39 1 3 2 21 16 prdstopn
 |-  ( ph -> ( TopOpen ` Y ) = ( Xt_ ` ( TopOpen o. R ) ) )
40 39 adantr
 |-  ( ( ph /\ y e. I ) -> ( TopOpen ` Y ) = ( Xt_ ` ( TopOpen o. R ) ) )
41 40 eqcomd
 |-  ( ( ph /\ y e. I ) -> ( Xt_ ` ( TopOpen o. R ) ) = ( TopOpen ` Y ) )
42 41 38 eqeltrd
 |-  ( ( ph /\ y e. I ) -> ( Xt_ ` ( TopOpen o. R ) ) e. ( TopOn ` ( Base ` Y ) ) )
43 toponuni
 |-  ( ( Xt_ ` ( TopOpen o. R ) ) e. ( TopOn ` ( Base ` Y ) ) -> ( Base ` Y ) = U. ( Xt_ ` ( TopOpen o. R ) ) )
44 mpteq1
 |-  ( ( Base ` Y ) = U. ( Xt_ ` ( TopOpen o. R ) ) -> ( x e. ( Base ` Y ) |-> ( x ` y ) ) = ( x e. U. ( Xt_ ` ( TopOpen o. R ) ) |-> ( x ` y ) ) )
45 42 43 44 3syl
 |-  ( ( ph /\ y e. I ) -> ( x e. ( Base ` Y ) |-> ( x ` y ) ) = ( x e. U. ( Xt_ ` ( TopOpen o. R ) ) |-> ( x ` y ) ) )
46 2 adantr
 |-  ( ( ph /\ y e. I ) -> I e. W )
47 37 adantr
 |-  ( ( ph /\ y e. I ) -> ( TopOpen o. R ) : I --> Top )
48 simpr
 |-  ( ( ph /\ y e. I ) -> y e. I )
49 eqid
 |-  U. ( Xt_ ` ( TopOpen o. R ) ) = U. ( Xt_ ` ( TopOpen o. R ) )
50 49 15 ptpjcn
 |-  ( ( I e. W /\ ( TopOpen o. R ) : I --> Top /\ y e. I ) -> ( x e. U. ( Xt_ ` ( TopOpen o. R ) ) |-> ( x ` y ) ) e. ( ( Xt_ ` ( TopOpen o. R ) ) Cn ( ( TopOpen o. R ) ` y ) ) )
51 46 47 48 50 syl3anc
 |-  ( ( ph /\ y e. I ) -> ( x e. U. ( Xt_ ` ( TopOpen o. R ) ) |-> ( x ` y ) ) e. ( ( Xt_ ` ( TopOpen o. R ) ) Cn ( ( TopOpen o. R ) ` y ) ) )
52 45 51 eqeltrd
 |-  ( ( ph /\ y e. I ) -> ( x e. ( Base ` Y ) |-> ( x ` y ) ) e. ( ( Xt_ ` ( TopOpen o. R ) ) Cn ( ( TopOpen o. R ) ` y ) ) )
53 41 27 oveq12d
 |-  ( ( ph /\ y e. I ) -> ( ( Xt_ ` ( TopOpen o. R ) ) Cn ( ( TopOpen o. R ) ` y ) ) = ( ( TopOpen ` Y ) Cn ( TopOpen ` ( R ` y ) ) ) )
54 52 53 eleqtrd
 |-  ( ( ph /\ y e. I ) -> ( x e. ( Base ` Y ) |-> ( x ` y ) ) e. ( ( TopOpen ` Y ) Cn ( TopOpen ` ( R ` y ) ) ) )
55 eqid
 |-  ( invg ` ( R ` y ) ) = ( invg ` ( R ` y ) )
56 29 55 tgpinv
 |-  ( ( R ` y ) e. TopGrp -> ( invg ` ( R ` y ) ) e. ( ( TopOpen ` ( R ` y ) ) Cn ( TopOpen ` ( R ` y ) ) ) )
57 28 56 syl
 |-  ( ( ph /\ y e. I ) -> ( invg ` ( R ` y ) ) e. ( ( TopOpen ` ( R ` y ) ) Cn ( TopOpen ` ( R ` y ) ) ) )
58 38 54 57 cnmpt11f
 |-  ( ( ph /\ y e. I ) -> ( x e. ( Base ` Y ) |-> ( ( invg ` ( R ` y ) ) ` ( x ` y ) ) ) e. ( ( TopOpen ` Y ) Cn ( TopOpen ` ( R ` y ) ) ) )
59 27 oveq2d
 |-  ( ( ph /\ y e. I ) -> ( ( TopOpen ` Y ) Cn ( ( TopOpen o. R ) ` y ) ) = ( ( TopOpen ` Y ) Cn ( TopOpen ` ( R ` y ) ) ) )
60 58 59 eleqtrrd
 |-  ( ( ph /\ y e. I ) -> ( x e. ( Base ` Y ) |-> ( ( invg ` ( R ` y ) ) ` ( x ` y ) ) ) e. ( ( TopOpen ` Y ) Cn ( ( TopOpen o. R ) ` y ) ) )
61 15 19 2 37 60 ptcn
 |-  ( ph -> ( x e. ( Base ` Y ) |-> ( y e. I |-> ( ( invg ` ( R ` y ) ) ` ( x ` y ) ) ) ) e. ( ( TopOpen ` Y ) Cn ( Xt_ ` ( TopOpen o. R ) ) ) )
62 eqid
 |-  ( invg ` Y ) = ( invg ` Y )
63 17 62 grpinvf
 |-  ( Y e. Grp -> ( invg ` Y ) : ( Base ` Y ) --> ( Base ` Y ) )
64 9 63 syl
 |-  ( ph -> ( invg ` Y ) : ( Base ` Y ) --> ( Base ` Y ) )
65 64 feqmptd
 |-  ( ph -> ( invg ` Y ) = ( x e. ( Base ` Y ) |-> ( ( invg ` Y ) ` x ) ) )
66 2 adantr
 |-  ( ( ph /\ x e. ( Base ` Y ) ) -> I e. W )
67 3 adantr
 |-  ( ( ph /\ x e. ( Base ` Y ) ) -> S e. V )
68 8 adantr
 |-  ( ( ph /\ x e. ( Base ` Y ) ) -> R : I --> Grp )
69 simpr
 |-  ( ( ph /\ x e. ( Base ` Y ) ) -> x e. ( Base ` Y ) )
70 1 66 67 68 17 62 69 prdsinvgd
 |-  ( ( ph /\ x e. ( Base ` Y ) ) -> ( ( invg ` Y ) ` x ) = ( y e. I |-> ( ( invg ` ( R ` y ) ) ` ( x ` y ) ) ) )
71 70 mpteq2dva
 |-  ( ph -> ( x e. ( Base ` Y ) |-> ( ( invg ` Y ) ` x ) ) = ( x e. ( Base ` Y ) |-> ( y e. I |-> ( ( invg ` ( R ` y ) ) ` ( x ` y ) ) ) ) )
72 65 71 eqtrd
 |-  ( ph -> ( invg ` Y ) = ( x e. ( Base ` Y ) |-> ( y e. I |-> ( ( invg ` ( R ` y ) ) ` ( x ` y ) ) ) ) )
73 39 oveq2d
 |-  ( ph -> ( ( TopOpen ` Y ) Cn ( TopOpen ` Y ) ) = ( ( TopOpen ` Y ) Cn ( Xt_ ` ( TopOpen o. R ) ) ) )
74 61 72 73 3eltr4d
 |-  ( ph -> ( invg ` Y ) e. ( ( TopOpen ` Y ) Cn ( TopOpen ` Y ) ) )
75 16 62 istgp
 |-  ( Y e. TopGrp <-> ( Y e. Grp /\ Y e. TopMnd /\ ( invg ` Y ) e. ( ( TopOpen ` Y ) Cn ( TopOpen ` Y ) ) ) )
76 9 14 74 75 syl3anbrc
 |-  ( ph -> Y e. TopGrp )