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 )