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

Metamath Proof Explorer

Definition df-rgmod

Description: Any ring can be regarded as a left algebra over itself. The function ringLMod associates with any ring the left algebra consisting in the ring itself regarded as a left algebra over itself. It has an inner product which is simply the ring product. (Contributed by Stefan O'Rear, 6-Dec-2014)

Ref Expression
Assertion df-rgmod ringLMod = ( 𝑤 ∈ V ↦ ( ( subringAlg ‘ 𝑤 ) ‘ ( Base ‘ 𝑤 ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 crglmod ⊢ ringLMod
1 vw ⊢ 𝑤
2 cvv ⊢ V
3 csra ⊢ subringAlg
4 1 cv ⊢ 𝑤
5 4 3 cfv ⊢ ( subringAlg ‘ 𝑤 )
6 cbs ⊢ Base
7 4 6 cfv ⊢ ( Base ‘ 𝑤 )
8 7 5 cfv ⊢ ( ( subringAlg ‘ 𝑤 ) ‘ ( Base ‘ 𝑤 ) )
9 1 2 8 cmpt ⊢ ( 𝑤 ∈ V ↦ ( ( subringAlg ‘ 𝑤 ) ‘ ( Base ‘ 𝑤 ) ) )
10 0 9 wceq ⊢ ringLMod = ( 𝑤 ∈ V ↦ ( ( subringAlg ‘ 𝑤 ) ‘ ( Base ‘ 𝑤 ) ) )