This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rlmsca2

Description: Scalars in the ring module. (Contributed by Stefan O'Rear, 1-Apr-2015)

Ref Expression
Assertion rlmsca2 ( I ‘ 𝑅 ) = ( Scalar ‘ ( ringLMod ‘ 𝑅 ) )

Proof

Step Hyp Ref Expression
1 fvi ⊢ ( 𝑅 ∈ V → ( I ‘ 𝑅 ) = 𝑅 )
2 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
3 2 ressid ⊢ ( 𝑅 ∈ V → ( 𝑅 ↾s ( Base ‘ 𝑅 ) ) = 𝑅 )
4 1 3 eqtr4d ⊢ ( 𝑅 ∈ V → ( I ‘ 𝑅 ) = ( 𝑅 ↾s ( Base ‘ 𝑅 ) ) )
5 fvprc ⊢ ( ¬ 𝑅 ∈ V → ( I ‘ 𝑅 ) = ∅ )
6 reldmress ⊢ Rel dom ↾s
7 6 ovprc1 ⊢ ( ¬ 𝑅 ∈ V → ( 𝑅 ↾s ( Base ‘ 𝑅 ) ) = ∅ )
8 5 7 eqtr4d ⊢ ( ¬ 𝑅 ∈ V → ( I ‘ 𝑅 ) = ( 𝑅 ↾s ( Base ‘ 𝑅 ) ) )
9 4 8 pm2.61i ⊢ ( I ‘ 𝑅 ) = ( 𝑅 ↾s ( Base ‘ 𝑅 ) )
10 rlmval ⊢ ( ringLMod ‘ 𝑅 ) = ( ( subringAlg ‘ 𝑅 ) ‘ ( Base ‘ 𝑅 ) )
11 10 a1i ⊢ ( ⊤ → ( ringLMod ‘ 𝑅 ) = ( ( subringAlg ‘ 𝑅 ) ‘ ( Base ‘ 𝑅 ) ) )
12 ssidd ⊢ ( ⊤ → ( Base ‘ 𝑅 ) ⊆ ( Base ‘ 𝑅 ) )
13 11 12 srasca ⊢ ( ⊤ → ( 𝑅 ↾s ( Base ‘ 𝑅 ) ) = ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) )
14 13 mptru ⊢ ( 𝑅 ↾s ( Base ‘ 𝑅 ) ) = ( Scalar ‘ ( ringLMod ‘ 𝑅 ) )
15 9 14 eqtri ⊢ ( I ‘ 𝑅 ) = ( Scalar ‘ ( ringLMod ‘ 𝑅 ) )