Database
BASIC ALGEBRAIC STRUCTURES
Ideals
The subring algebra; ideals
rlmsca2
Next ⟩
rlmvsca
Metamath Proof Explorer
Ascii
Unicode
Theorem
rlmsca2
Description:
Scalars in the ring module.
(Contributed by
Stefan O'Rear
, 1-Apr-2015)
Ref
Expression
Assertion
rlmsca2
⊢
I
⁡
R
=
Scalar
⁡
ringLMod
⁡
R
Proof
Step
Hyp
Ref
Expression
1
fvi
⊢
R
∈
V
→
I
⁡
R
=
R
2
eqid
⊢
Base
R
=
Base
R
3
2
ressid
⊢
R
∈
V
→
R
↾
𝑠
Base
R
=
R
4
1
3
eqtr4d
⊢
R
∈
V
→
I
⁡
R
=
R
↾
𝑠
Base
R
5
fvprc
⊢
¬
R
∈
V
→
I
⁡
R
=
∅
6
reldmress
⊢
Rel
⁡
dom
⁡
↾
𝑠
7
6
ovprc1
⊢
¬
R
∈
V
→
R
↾
𝑠
Base
R
=
∅
8
5
7
eqtr4d
⊢
¬
R
∈
V
→
I
⁡
R
=
R
↾
𝑠
Base
R
9
4
8
pm2.61i
⊢
I
⁡
R
=
R
↾
𝑠
Base
R
10
rlmval
⊢
ringLMod
⁡
R
=
subringAlg
⁡
R
⁡
Base
R
11
10
a1i
⊢
⊤
→
ringLMod
⁡
R
=
subringAlg
⁡
R
⁡
Base
R
12
ssidd
⊢
⊤
→
Base
R
⊆
Base
R
13
11
12
srasca
⊢
⊤
→
R
↾
𝑠
Base
R
=
Scalar
⁡
ringLMod
⁡
R
14
13
mptru
⊢
R
↾
𝑠
Base
R
=
Scalar
⁡
ringLMod
⁡
R
15
9
14
eqtri
⊢
I
⁡
R
=
Scalar
⁡
ringLMod
⁡
R