Database
BASIC ALGEBRAIC STRUCTURES
Ideals
The subring algebra; ideals
rlmds
Next ⟩
rlmlmod
Metamath Proof Explorer
Ascii
Unicode
Theorem
rlmds
Description:
Metric component of the ring module.
(Contributed by
Mario Carneiro
, 6-Oct-2015)
Ref
Expression
Assertion
rlmds
⊢
dist
⁡
R
=
dist
⁡
ringLMod
⁡
R
Proof
Step
Hyp
Ref
Expression
1
rlmval
⊢
ringLMod
⁡
R
=
subringAlg
⁡
R
⁡
Base
R
2
1
a1i
⊢
⊤
→
ringLMod
⁡
R
=
subringAlg
⁡
R
⁡
Base
R
3
ssidd
⊢
⊤
→
Base
R
⊆
Base
R
4
2
3
srads
⊢
⊤
→
dist
⁡
R
=
dist
⁡
ringLMod
⁡
R
5
4
mptru
⊢
dist
⁡
R
=
dist
⁡
ringLMod
⁡
R