Description: Topology of the multiplication group. (Contributed by Mario Carneiro, 5-Oct-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | mgpbas.1 | ⊢ 𝑀 = ( mulGrp ‘ 𝑅 ) | |
mgptopn.2 | ⊢ 𝐽 = ( TopOpen ‘ 𝑅 ) | ||
Assertion | mgptopn | ⊢ 𝐽 = ( TopOpen ‘ 𝑀 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mgpbas.1 | ⊢ 𝑀 = ( mulGrp ‘ 𝑅 ) | |
2 | mgptopn.2 | ⊢ 𝐽 = ( TopOpen ‘ 𝑅 ) | |
3 | eqid | ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 ) | |
4 | eqid | ⊢ ( TopSet ‘ 𝑅 ) = ( TopSet ‘ 𝑅 ) | |
5 | 3 4 | topnval | ⊢ ( ( TopSet ‘ 𝑅 ) ↾t ( Base ‘ 𝑅 ) ) = ( TopOpen ‘ 𝑅 ) |
6 | 1 3 | mgpbas | ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑀 ) |
7 | 1 | mgptset | ⊢ ( TopSet ‘ 𝑅 ) = ( TopSet ‘ 𝑀 ) |
8 | 6 7 | topnval | ⊢ ( ( TopSet ‘ 𝑅 ) ↾t ( Base ‘ 𝑅 ) ) = ( TopOpen ‘ 𝑀 ) |
9 | 2 5 8 | 3eqtr2i | ⊢ 𝐽 = ( TopOpen ‘ 𝑀 ) |