Step | Hyp | Ref
| Expression |
1 | | prdstgpd.y |
. . 3
⊢ 𝑌 = (𝑆Xs𝑅) |
2 | | prdstgpd.i |
. . 3
⊢ (𝜑 → 𝐼 ∈ 𝑊) |
3 | | prdstgpd.s |
. . 3
⊢ (𝜑 → 𝑆 ∈ 𝑉) |
4 | | prdstgpd.r |
. . . 4
⊢ (𝜑 → 𝑅:𝐼⟶TopGrp) |
5 | | tgpgrp 23229 |
. . . . 5
⊢ (𝑥 ∈ TopGrp → 𝑥 ∈ Grp) |
6 | 5 | ssriv 3925 |
. . . 4
⊢ TopGrp
⊆ Grp |
7 | | fss 6617 |
. . . 4
⊢ ((𝑅:𝐼⟶TopGrp ∧ TopGrp ⊆ Grp)
→ 𝑅:𝐼⟶Grp) |
8 | 4, 6, 7 | sylancl 586 |
. . 3
⊢ (𝜑 → 𝑅:𝐼⟶Grp) |
9 | 1, 2, 3, 8 | prdsgrpd 18685 |
. 2
⊢ (𝜑 → 𝑌 ∈ Grp) |
10 | | tgptmd 23230 |
. . . . 5
⊢ (𝑥 ∈ TopGrp → 𝑥 ∈ TopMnd) |
11 | 10 | ssriv 3925 |
. . . 4
⊢ TopGrp
⊆ TopMnd |
12 | | fss 6617 |
. . . 4
⊢ ((𝑅:𝐼⟶TopGrp ∧ TopGrp ⊆ TopMnd)
→ 𝑅:𝐼⟶TopMnd) |
13 | 4, 11, 12 | sylancl 586 |
. . 3
⊢ (𝜑 → 𝑅:𝐼⟶TopMnd) |
14 | 1, 2, 3, 13 | prdstmdd 23275 |
. 2
⊢ (𝜑 → 𝑌 ∈ TopMnd) |
15 | | eqid 2738 |
. . . 4
⊢
(∏t‘(TopOpen ∘ 𝑅)) = (∏t‘(TopOpen
∘ 𝑅)) |
16 | | eqid 2738 |
. . . . . 6
⊢
(TopOpen‘𝑌) =
(TopOpen‘𝑌) |
17 | | eqid 2738 |
. . . . . 6
⊢
(Base‘𝑌) =
(Base‘𝑌) |
18 | 16, 17 | tmdtopon 23232 |
. . . . 5
⊢ (𝑌 ∈ TopMnd →
(TopOpen‘𝑌) ∈
(TopOn‘(Base‘𝑌))) |
19 | 14, 18 | syl 17 |
. . . 4
⊢ (𝜑 → (TopOpen‘𝑌) ∈
(TopOn‘(Base‘𝑌))) |
20 | | topnfn 17136 |
. . . . . 6
⊢ TopOpen
Fn V |
21 | 4 | ffnd 6601 |
. . . . . . 7
⊢ (𝜑 → 𝑅 Fn 𝐼) |
22 | | dffn2 6602 |
. . . . . . 7
⊢ (𝑅 Fn 𝐼 ↔ 𝑅:𝐼⟶V) |
23 | 21, 22 | sylib 217 |
. . . . . 6
⊢ (𝜑 → 𝑅:𝐼⟶V) |
24 | | fnfco 6639 |
. . . . . 6
⊢ ((TopOpen
Fn V ∧ 𝑅:𝐼⟶V) → (TopOpen
∘ 𝑅) Fn 𝐼) |
25 | 20, 23, 24 | sylancr 587 |
. . . . 5
⊢ (𝜑 → (TopOpen ∘ 𝑅) Fn 𝐼) |
26 | | fvco3 6867 |
. . . . . . . 8
⊢ ((𝑅:𝐼⟶TopGrp ∧ 𝑦 ∈ 𝐼) → ((TopOpen ∘ 𝑅)‘𝑦) = (TopOpen‘(𝑅‘𝑦))) |
27 | 4, 26 | sylan 580 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → ((TopOpen ∘ 𝑅)‘𝑦) = (TopOpen‘(𝑅‘𝑦))) |
28 | 4 | ffvelrnda 6961 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → (𝑅‘𝑦) ∈ TopGrp) |
29 | | eqid 2738 |
. . . . . . . . 9
⊢
(TopOpen‘(𝑅‘𝑦)) = (TopOpen‘(𝑅‘𝑦)) |
30 | | eqid 2738 |
. . . . . . . . 9
⊢
(Base‘(𝑅‘𝑦)) = (Base‘(𝑅‘𝑦)) |
31 | 29, 30 | tgptopon 23233 |
. . . . . . . 8
⊢ ((𝑅‘𝑦) ∈ TopGrp → (TopOpen‘(𝑅‘𝑦)) ∈ (TopOn‘(Base‘(𝑅‘𝑦)))) |
32 | | topontop 22062 |
. . . . . . . 8
⊢
((TopOpen‘(𝑅‘𝑦)) ∈ (TopOn‘(Base‘(𝑅‘𝑦))) → (TopOpen‘(𝑅‘𝑦)) ∈ Top) |
33 | 28, 31, 32 | 3syl 18 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → (TopOpen‘(𝑅‘𝑦)) ∈ Top) |
34 | 27, 33 | eqeltrd 2839 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → ((TopOpen ∘ 𝑅)‘𝑦) ∈ Top) |
35 | 34 | ralrimiva 3103 |
. . . . 5
⊢ (𝜑 → ∀𝑦 ∈ 𝐼 ((TopOpen ∘ 𝑅)‘𝑦) ∈ Top) |
36 | | ffnfv 6992 |
. . . . 5
⊢ ((TopOpen
∘ 𝑅):𝐼⟶Top ↔ ((TopOpen
∘ 𝑅) Fn 𝐼 ∧ ∀𝑦 ∈ 𝐼 ((TopOpen ∘ 𝑅)‘𝑦) ∈ Top)) |
37 | 25, 35, 36 | sylanbrc 583 |
. . . 4
⊢ (𝜑 → (TopOpen ∘ 𝑅):𝐼⟶Top) |
38 | 19 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → (TopOpen‘𝑌) ∈ (TopOn‘(Base‘𝑌))) |
39 | 1, 3, 2, 21, 16 | prdstopn 22779 |
. . . . . . . . . . . 12
⊢ (𝜑 → (TopOpen‘𝑌) =
(∏t‘(TopOpen ∘ 𝑅))) |
40 | 39 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → (TopOpen‘𝑌) = (∏t‘(TopOpen
∘ 𝑅))) |
41 | 40 | eqcomd 2744 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → (∏t‘(TopOpen
∘ 𝑅)) =
(TopOpen‘𝑌)) |
42 | 41, 38 | eqeltrd 2839 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → (∏t‘(TopOpen
∘ 𝑅)) ∈
(TopOn‘(Base‘𝑌))) |
43 | | toponuni 22063 |
. . . . . . . . 9
⊢
((∏t‘(TopOpen ∘ 𝑅)) ∈ (TopOn‘(Base‘𝑌)) → (Base‘𝑌) = ∪
(∏t‘(TopOpen ∘ 𝑅))) |
44 | | mpteq1 5167 |
. . . . . . . . 9
⊢
((Base‘𝑌) =
∪ (∏t‘(TopOpen ∘ 𝑅)) → (𝑥 ∈ (Base‘𝑌) ↦ (𝑥‘𝑦)) = (𝑥 ∈ ∪
(∏t‘(TopOpen ∘ 𝑅)) ↦ (𝑥‘𝑦))) |
45 | 42, 43, 44 | 3syl 18 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → (𝑥 ∈ (Base‘𝑌) ↦ (𝑥‘𝑦)) = (𝑥 ∈ ∪
(∏t‘(TopOpen ∘ 𝑅)) ↦ (𝑥‘𝑦))) |
46 | 2 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → 𝐼 ∈ 𝑊) |
47 | 37 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → (TopOpen ∘ 𝑅):𝐼⟶Top) |
48 | | simpr 485 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → 𝑦 ∈ 𝐼) |
49 | | eqid 2738 |
. . . . . . . . . 10
⊢ ∪ (∏t‘(TopOpen ∘ 𝑅)) = ∪ (∏t‘(TopOpen ∘ 𝑅)) |
50 | 49, 15 | ptpjcn 22762 |
. . . . . . . . 9
⊢ ((𝐼 ∈ 𝑊 ∧ (TopOpen ∘ 𝑅):𝐼⟶Top ∧ 𝑦 ∈ 𝐼) → (𝑥 ∈ ∪
(∏t‘(TopOpen ∘ 𝑅)) ↦ (𝑥‘𝑦)) ∈ ((∏t‘(TopOpen
∘ 𝑅)) Cn ((TopOpen
∘ 𝑅)‘𝑦))) |
51 | 46, 47, 48, 50 | syl3anc 1370 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → (𝑥 ∈ ∪
(∏t‘(TopOpen ∘ 𝑅)) ↦ (𝑥‘𝑦)) ∈ ((∏t‘(TopOpen
∘ 𝑅)) Cn ((TopOpen
∘ 𝑅)‘𝑦))) |
52 | 45, 51 | eqeltrd 2839 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → (𝑥 ∈ (Base‘𝑌) ↦ (𝑥‘𝑦)) ∈ ((∏t‘(TopOpen
∘ 𝑅)) Cn ((TopOpen
∘ 𝑅)‘𝑦))) |
53 | 41, 27 | oveq12d 7293 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → ((∏t‘(TopOpen
∘ 𝑅)) Cn ((TopOpen
∘ 𝑅)‘𝑦)) = ((TopOpen‘𝑌) Cn (TopOpen‘(𝑅‘𝑦)))) |
54 | 52, 53 | eleqtrd 2841 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → (𝑥 ∈ (Base‘𝑌) ↦ (𝑥‘𝑦)) ∈ ((TopOpen‘𝑌) Cn (TopOpen‘(𝑅‘𝑦)))) |
55 | | eqid 2738 |
. . . . . . . 8
⊢
(invg‘(𝑅‘𝑦)) = (invg‘(𝑅‘𝑦)) |
56 | 29, 55 | tgpinv 23236 |
. . . . . . 7
⊢ ((𝑅‘𝑦) ∈ TopGrp →
(invg‘(𝑅‘𝑦)) ∈ ((TopOpen‘(𝑅‘𝑦)) Cn (TopOpen‘(𝑅‘𝑦)))) |
57 | 28, 56 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → (invg‘(𝑅‘𝑦)) ∈ ((TopOpen‘(𝑅‘𝑦)) Cn (TopOpen‘(𝑅‘𝑦)))) |
58 | 38, 54, 57 | cnmpt11f 22815 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → (𝑥 ∈ (Base‘𝑌) ↦ ((invg‘(𝑅‘𝑦))‘(𝑥‘𝑦))) ∈ ((TopOpen‘𝑌) Cn (TopOpen‘(𝑅‘𝑦)))) |
59 | 27 | oveq2d 7291 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → ((TopOpen‘𝑌) Cn ((TopOpen ∘ 𝑅)‘𝑦)) = ((TopOpen‘𝑌) Cn (TopOpen‘(𝑅‘𝑦)))) |
60 | 58, 59 | eleqtrrd 2842 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → (𝑥 ∈ (Base‘𝑌) ↦ ((invg‘(𝑅‘𝑦))‘(𝑥‘𝑦))) ∈ ((TopOpen‘𝑌) Cn ((TopOpen ∘ 𝑅)‘𝑦))) |
61 | 15, 19, 2, 37, 60 | ptcn 22778 |
. . 3
⊢ (𝜑 → (𝑥 ∈ (Base‘𝑌) ↦ (𝑦 ∈ 𝐼 ↦ ((invg‘(𝑅‘𝑦))‘(𝑥‘𝑦)))) ∈ ((TopOpen‘𝑌) Cn (∏t‘(TopOpen
∘ 𝑅)))) |
62 | | eqid 2738 |
. . . . . . 7
⊢
(invg‘𝑌) = (invg‘𝑌) |
63 | 17, 62 | grpinvf 18626 |
. . . . . 6
⊢ (𝑌 ∈ Grp →
(invg‘𝑌):(Base‘𝑌)⟶(Base‘𝑌)) |
64 | 9, 63 | syl 17 |
. . . . 5
⊢ (𝜑 →
(invg‘𝑌):(Base‘𝑌)⟶(Base‘𝑌)) |
65 | 64 | feqmptd 6837 |
. . . 4
⊢ (𝜑 →
(invg‘𝑌) =
(𝑥 ∈ (Base‘𝑌) ↦
((invg‘𝑌)‘𝑥))) |
66 | 2 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑌)) → 𝐼 ∈ 𝑊) |
67 | 3 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑌)) → 𝑆 ∈ 𝑉) |
68 | 8 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑌)) → 𝑅:𝐼⟶Grp) |
69 | | simpr 485 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑌)) → 𝑥 ∈ (Base‘𝑌)) |
70 | 1, 66, 67, 68, 17, 62, 69 | prdsinvgd 18686 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑌)) → ((invg‘𝑌)‘𝑥) = (𝑦 ∈ 𝐼 ↦ ((invg‘(𝑅‘𝑦))‘(𝑥‘𝑦)))) |
71 | 70 | mpteq2dva 5174 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ (Base‘𝑌) ↦ ((invg‘𝑌)‘𝑥)) = (𝑥 ∈ (Base‘𝑌) ↦ (𝑦 ∈ 𝐼 ↦ ((invg‘(𝑅‘𝑦))‘(𝑥‘𝑦))))) |
72 | 65, 71 | eqtrd 2778 |
. . 3
⊢ (𝜑 →
(invg‘𝑌) =
(𝑥 ∈ (Base‘𝑌) ↦ (𝑦 ∈ 𝐼 ↦ ((invg‘(𝑅‘𝑦))‘(𝑥‘𝑦))))) |
73 | 39 | oveq2d 7291 |
. . 3
⊢ (𝜑 → ((TopOpen‘𝑌) Cn (TopOpen‘𝑌)) = ((TopOpen‘𝑌) Cn
(∏t‘(TopOpen ∘ 𝑅)))) |
74 | 61, 72, 73 | 3eltr4d 2854 |
. 2
⊢ (𝜑 →
(invg‘𝑌)
∈ ((TopOpen‘𝑌)
Cn (TopOpen‘𝑌))) |
75 | 16, 62 | istgp 23228 |
. 2
⊢ (𝑌 ∈ TopGrp ↔ (𝑌 ∈ Grp ∧ 𝑌 ∈ TopMnd ∧
(invg‘𝑌)
∈ ((TopOpen‘𝑌)
Cn (TopOpen‘𝑌)))) |
76 | 9, 14, 74, 75 | syl3anbrc 1342 |
1
⊢ (𝜑 → 𝑌 ∈ TopGrp) |