Description: The functionalization of the ring multiplication operation is a continuous function in a topological ring. (Contributed by Mario Carneiro, 5-Oct-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | mulrcn.j | |- J = ( TopOpen ` R ) |
|
mulrcn.t | |- T = ( +f ` ( mulGrp ` R ) ) |
||
Assertion | mulrcn | |- ( R e. TopRing -> T e. ( ( J tX J ) Cn J ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mulrcn.j | |- J = ( TopOpen ` R ) |
|
2 | mulrcn.t | |- T = ( +f ` ( mulGrp ` R ) ) |
|
3 | eqid | |- ( mulGrp ` R ) = ( mulGrp ` R ) |
|
4 | 3 | trgtmd | |- ( R e. TopRing -> ( mulGrp ` R ) e. TopMnd ) |
5 | 3 1 | mgptopn | |- J = ( TopOpen ` ( mulGrp ` R ) ) |
6 | 5 2 | tmdcn | |- ( ( mulGrp ` R ) e. TopMnd -> T e. ( ( J tX J ) Cn J ) ) |
7 | 4 6 | syl | |- ( R e. TopRing -> T e. ( ( J tX J ) Cn J ) ) |