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 )