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 𝑌 = ( 𝑆 Xs 𝑅 )
prdstgpd.i ( 𝜑𝐼𝑊 )
prdstgpd.s ( 𝜑𝑆𝑉 )
prdstgpd.r ( 𝜑𝑅 : 𝐼 ⟶ TopGrp )
Assertion prdstgpd ( 𝜑𝑌 ∈ TopGrp )

Proof

Step Hyp Ref Expression
1 prdstgpd.y 𝑌 = ( 𝑆 Xs 𝑅 )
2 prdstgpd.i ( 𝜑𝐼𝑊 )
3 prdstgpd.s ( 𝜑𝑆𝑉 )
4 prdstgpd.r ( 𝜑𝑅 : 𝐼 ⟶ TopGrp )
5 tgpgrp ( 𝑥 ∈ TopGrp → 𝑥 ∈ Grp )
6 5 ssriv TopGrp ⊆ Grp
7 fss ( ( 𝑅 : 𝐼 ⟶ TopGrp ∧ TopGrp ⊆ Grp ) → 𝑅 : 𝐼 ⟶ Grp )
8 4 6 7 sylancl ( 𝜑𝑅 : 𝐼 ⟶ Grp )
9 1 2 3 8 prdsgrpd ( 𝜑𝑌 ∈ Grp )
10 tgptmd ( 𝑥 ∈ TopGrp → 𝑥 ∈ TopMnd )
11 10 ssriv TopGrp ⊆ TopMnd
12 fss ( ( 𝑅 : 𝐼 ⟶ TopGrp ∧ TopGrp ⊆ TopMnd ) → 𝑅 : 𝐼 ⟶ TopMnd )
13 4 11 12 sylancl ( 𝜑𝑅 : 𝐼 ⟶ TopMnd )
14 1 2 3 13 prdstmdd ( 𝜑𝑌 ∈ TopMnd )
15 eqid ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) = ( ∏t ‘ ( TopOpen ∘ 𝑅 ) )
16 eqid ( TopOpen ‘ 𝑌 ) = ( TopOpen ‘ 𝑌 )
17 eqid ( Base ‘ 𝑌 ) = ( Base ‘ 𝑌 )
18 16 17 tmdtopon ( 𝑌 ∈ TopMnd → ( TopOpen ‘ 𝑌 ) ∈ ( TopOn ‘ ( Base ‘ 𝑌 ) ) )
19 14 18 syl ( 𝜑 → ( TopOpen ‘ 𝑌 ) ∈ ( TopOn ‘ ( Base ‘ 𝑌 ) ) )
20 topnfn TopOpen Fn V
21 4 ffnd ( 𝜑𝑅 Fn 𝐼 )
22 dffn2 ( 𝑅 Fn 𝐼𝑅 : 𝐼 ⟶ V )
23 21 22 sylib ( 𝜑𝑅 : 𝐼 ⟶ V )
24 fnfco ( ( TopOpen Fn V ∧ 𝑅 : 𝐼 ⟶ V ) → ( TopOpen ∘ 𝑅 ) Fn 𝐼 )
25 20 23 24 sylancr ( 𝜑 → ( TopOpen ∘ 𝑅 ) Fn 𝐼 )
26 fvco3 ( ( 𝑅 : 𝐼 ⟶ TopGrp ∧ 𝑦𝐼 ) → ( ( TopOpen ∘ 𝑅 ) ‘ 𝑦 ) = ( TopOpen ‘ ( 𝑅𝑦 ) ) )
27 4 26 sylan ( ( 𝜑𝑦𝐼 ) → ( ( TopOpen ∘ 𝑅 ) ‘ 𝑦 ) = ( TopOpen ‘ ( 𝑅𝑦 ) ) )
28 4 ffvelrnda ( ( 𝜑𝑦𝐼 ) → ( 𝑅𝑦 ) ∈ TopGrp )
29 eqid ( TopOpen ‘ ( 𝑅𝑦 ) ) = ( TopOpen ‘ ( 𝑅𝑦 ) )
30 eqid ( Base ‘ ( 𝑅𝑦 ) ) = ( Base ‘ ( 𝑅𝑦 ) )
31 29 30 tgptopon ( ( 𝑅𝑦 ) ∈ TopGrp → ( TopOpen ‘ ( 𝑅𝑦 ) ) ∈ ( TopOn ‘ ( Base ‘ ( 𝑅𝑦 ) ) ) )
32 topontop ( ( TopOpen ‘ ( 𝑅𝑦 ) ) ∈ ( TopOn ‘ ( Base ‘ ( 𝑅𝑦 ) ) ) → ( TopOpen ‘ ( 𝑅𝑦 ) ) ∈ Top )
33 28 31 32 3syl ( ( 𝜑𝑦𝐼 ) → ( TopOpen ‘ ( 𝑅𝑦 ) ) ∈ Top )
34 27 33 eqeltrd ( ( 𝜑𝑦𝐼 ) → ( ( TopOpen ∘ 𝑅 ) ‘ 𝑦 ) ∈ Top )
35 34 ralrimiva ( 𝜑 → ∀ 𝑦𝐼 ( ( TopOpen ∘ 𝑅 ) ‘ 𝑦 ) ∈ Top )
36 ffnfv ( ( TopOpen ∘ 𝑅 ) : 𝐼 ⟶ Top ↔ ( ( TopOpen ∘ 𝑅 ) Fn 𝐼 ∧ ∀ 𝑦𝐼 ( ( TopOpen ∘ 𝑅 ) ‘ 𝑦 ) ∈ Top ) )
37 25 35 36 sylanbrc ( 𝜑 → ( TopOpen ∘ 𝑅 ) : 𝐼 ⟶ Top )
38 19 adantr ( ( 𝜑𝑦𝐼 ) → ( TopOpen ‘ 𝑌 ) ∈ ( TopOn ‘ ( Base ‘ 𝑌 ) ) )
39 1 3 2 21 16 prdstopn ( 𝜑 → ( TopOpen ‘ 𝑌 ) = ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) )
40 39 adantr ( ( 𝜑𝑦𝐼 ) → ( TopOpen ‘ 𝑌 ) = ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) )
41 40 eqcomd ( ( 𝜑𝑦𝐼 ) → ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) = ( TopOpen ‘ 𝑌 ) )
42 41 38 eqeltrd ( ( 𝜑𝑦𝐼 ) → ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) ∈ ( TopOn ‘ ( Base ‘ 𝑌 ) ) )
43 toponuni ( ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) ∈ ( TopOn ‘ ( Base ‘ 𝑌 ) ) → ( Base ‘ 𝑌 ) = ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) )
44 mpteq1 ( ( Base ‘ 𝑌 ) = ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) → ( 𝑥 ∈ ( Base ‘ 𝑌 ) ↦ ( 𝑥𝑦 ) ) = ( 𝑥 ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) ↦ ( 𝑥𝑦 ) ) )
45 42 43 44 3syl ( ( 𝜑𝑦𝐼 ) → ( 𝑥 ∈ ( Base ‘ 𝑌 ) ↦ ( 𝑥𝑦 ) ) = ( 𝑥 ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) ↦ ( 𝑥𝑦 ) ) )
46 2 adantr ( ( 𝜑𝑦𝐼 ) → 𝐼𝑊 )
47 37 adantr ( ( 𝜑𝑦𝐼 ) → ( TopOpen ∘ 𝑅 ) : 𝐼 ⟶ Top )
48 simpr ( ( 𝜑𝑦𝐼 ) → 𝑦𝐼 )
49 eqid ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) = ( ∏t ‘ ( TopOpen ∘ 𝑅 ) )
50 49 15 ptpjcn ( ( 𝐼𝑊 ∧ ( TopOpen ∘ 𝑅 ) : 𝐼 ⟶ Top ∧ 𝑦𝐼 ) → ( 𝑥 ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) ↦ ( 𝑥𝑦 ) ) ∈ ( ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) Cn ( ( TopOpen ∘ 𝑅 ) ‘ 𝑦 ) ) )
51 46 47 48 50 syl3anc ( ( 𝜑𝑦𝐼 ) → ( 𝑥 ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) ↦ ( 𝑥𝑦 ) ) ∈ ( ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) Cn ( ( TopOpen ∘ 𝑅 ) ‘ 𝑦 ) ) )
52 45 51 eqeltrd ( ( 𝜑𝑦𝐼 ) → ( 𝑥 ∈ ( Base ‘ 𝑌 ) ↦ ( 𝑥𝑦 ) ) ∈ ( ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) Cn ( ( TopOpen ∘ 𝑅 ) ‘ 𝑦 ) ) )
53 41 27 oveq12d ( ( 𝜑𝑦𝐼 ) → ( ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) Cn ( ( TopOpen ∘ 𝑅 ) ‘ 𝑦 ) ) = ( ( TopOpen ‘ 𝑌 ) Cn ( TopOpen ‘ ( 𝑅𝑦 ) ) ) )
54 52 53 eleqtrd ( ( 𝜑𝑦𝐼 ) → ( 𝑥 ∈ ( Base ‘ 𝑌 ) ↦ ( 𝑥𝑦 ) ) ∈ ( ( TopOpen ‘ 𝑌 ) Cn ( TopOpen ‘ ( 𝑅𝑦 ) ) ) )
55 eqid ( invg ‘ ( 𝑅𝑦 ) ) = ( invg ‘ ( 𝑅𝑦 ) )
56 29 55 tgpinv ( ( 𝑅𝑦 ) ∈ TopGrp → ( invg ‘ ( 𝑅𝑦 ) ) ∈ ( ( TopOpen ‘ ( 𝑅𝑦 ) ) Cn ( TopOpen ‘ ( 𝑅𝑦 ) ) ) )
57 28 56 syl ( ( 𝜑𝑦𝐼 ) → ( invg ‘ ( 𝑅𝑦 ) ) ∈ ( ( TopOpen ‘ ( 𝑅𝑦 ) ) Cn ( TopOpen ‘ ( 𝑅𝑦 ) ) ) )
58 38 54 57 cnmpt11f ( ( 𝜑𝑦𝐼 ) → ( 𝑥 ∈ ( Base ‘ 𝑌 ) ↦ ( ( invg ‘ ( 𝑅𝑦 ) ) ‘ ( 𝑥𝑦 ) ) ) ∈ ( ( TopOpen ‘ 𝑌 ) Cn ( TopOpen ‘ ( 𝑅𝑦 ) ) ) )
59 27 oveq2d ( ( 𝜑𝑦𝐼 ) → ( ( TopOpen ‘ 𝑌 ) Cn ( ( TopOpen ∘ 𝑅 ) ‘ 𝑦 ) ) = ( ( TopOpen ‘ 𝑌 ) Cn ( TopOpen ‘ ( 𝑅𝑦 ) ) ) )
60 58 59 eleqtrrd ( ( 𝜑𝑦𝐼 ) → ( 𝑥 ∈ ( Base ‘ 𝑌 ) ↦ ( ( invg ‘ ( 𝑅𝑦 ) ) ‘ ( 𝑥𝑦 ) ) ) ∈ ( ( TopOpen ‘ 𝑌 ) Cn ( ( TopOpen ∘ 𝑅 ) ‘ 𝑦 ) ) )
61 15 19 2 37 60 ptcn ( 𝜑 → ( 𝑥 ∈ ( Base ‘ 𝑌 ) ↦ ( 𝑦𝐼 ↦ ( ( invg ‘ ( 𝑅𝑦 ) ) ‘ ( 𝑥𝑦 ) ) ) ) ∈ ( ( TopOpen ‘ 𝑌 ) Cn ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) ) )
62 eqid ( invg𝑌 ) = ( invg𝑌 )
63 17 62 grpinvf ( 𝑌 ∈ Grp → ( invg𝑌 ) : ( Base ‘ 𝑌 ) ⟶ ( Base ‘ 𝑌 ) )
64 9 63 syl ( 𝜑 → ( invg𝑌 ) : ( Base ‘ 𝑌 ) ⟶ ( Base ‘ 𝑌 ) )
65 64 feqmptd ( 𝜑 → ( invg𝑌 ) = ( 𝑥 ∈ ( Base ‘ 𝑌 ) ↦ ( ( invg𝑌 ) ‘ 𝑥 ) ) )
66 2 adantr ( ( 𝜑𝑥 ∈ ( Base ‘ 𝑌 ) ) → 𝐼𝑊 )
67 3 adantr ( ( 𝜑𝑥 ∈ ( Base ‘ 𝑌 ) ) → 𝑆𝑉 )
68 8 adantr ( ( 𝜑𝑥 ∈ ( Base ‘ 𝑌 ) ) → 𝑅 : 𝐼 ⟶ Grp )
69 simpr ( ( 𝜑𝑥 ∈ ( Base ‘ 𝑌 ) ) → 𝑥 ∈ ( Base ‘ 𝑌 ) )
70 1 66 67 68 17 62 69 prdsinvgd ( ( 𝜑𝑥 ∈ ( Base ‘ 𝑌 ) ) → ( ( invg𝑌 ) ‘ 𝑥 ) = ( 𝑦𝐼 ↦ ( ( invg ‘ ( 𝑅𝑦 ) ) ‘ ( 𝑥𝑦 ) ) ) )
71 70 mpteq2dva ( 𝜑 → ( 𝑥 ∈ ( Base ‘ 𝑌 ) ↦ ( ( invg𝑌 ) ‘ 𝑥 ) ) = ( 𝑥 ∈ ( Base ‘ 𝑌 ) ↦ ( 𝑦𝐼 ↦ ( ( invg ‘ ( 𝑅𝑦 ) ) ‘ ( 𝑥𝑦 ) ) ) ) )
72 65 71 eqtrd ( 𝜑 → ( invg𝑌 ) = ( 𝑥 ∈ ( Base ‘ 𝑌 ) ↦ ( 𝑦𝐼 ↦ ( ( invg ‘ ( 𝑅𝑦 ) ) ‘ ( 𝑥𝑦 ) ) ) ) )
73 39 oveq2d ( 𝜑 → ( ( TopOpen ‘ 𝑌 ) Cn ( TopOpen ‘ 𝑌 ) ) = ( ( TopOpen ‘ 𝑌 ) Cn ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) ) )
74 61 72 73 3eltr4d ( 𝜑 → ( invg𝑌 ) ∈ ( ( TopOpen ‘ 𝑌 ) Cn ( TopOpen ‘ 𝑌 ) ) )
75 16 62 istgp ( 𝑌 ∈ TopGrp ↔ ( 𝑌 ∈ Grp ∧ 𝑌 ∈ TopMnd ∧ ( invg𝑌 ) ∈ ( ( TopOpen ‘ 𝑌 ) Cn ( TopOpen ‘ 𝑌 ) ) ) )
76 9 14 74 75 syl3anbrc ( 𝜑𝑌 ∈ TopGrp )