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

Metamath Proof Explorer

Theorem rlmval

Description: Value of the ring module. (Contributed by Stefan O'Rear, 31-Mar-2015)

Ref Expression
Assertion rlmval ( ringLMod ‘ 𝑊 ) = ( ( subringAlg ‘ 𝑊 ) ‘ ( Base ‘ 𝑊 ) )

Proof

Step Hyp Ref Expression
1 fveq2 ⊢ ( 𝑎 = 𝑊 → ( subringAlg ‘ 𝑎 ) = ( subringAlg ‘ 𝑊 ) )
2 fveq2 ⊢ ( 𝑎 = 𝑊 → ( Base ‘ 𝑎 ) = ( Base ‘ 𝑊 ) )
3 1 2 fveq12d ⊢ ( 𝑎 = 𝑊 → ( ( subringAlg ‘ 𝑎 ) ‘ ( Base ‘ 𝑎 ) ) = ( ( subringAlg ‘ 𝑊 ) ‘ ( Base ‘ 𝑊 ) ) )
4 df-rgmod ⊢ ringLMod = ( 𝑎 ∈ V ↦ ( ( subringAlg ‘ 𝑎 ) ‘ ( Base ‘ 𝑎 ) ) )
5 fvex ⊢ ( ( subringAlg ‘ 𝑊 ) ‘ ( Base ‘ 𝑊 ) ) ∈ V
6 3 4 5 fvmpt ⊢ ( 𝑊 ∈ V → ( ringLMod ‘ 𝑊 ) = ( ( subringAlg ‘ 𝑊 ) ‘ ( Base ‘ 𝑊 ) ) )
7 0fv ⊢ ( ∅ ‘ ( Base ‘ 𝑊 ) ) = ∅
8 7 eqcomi ⊢ ∅ = ( ∅ ‘ ( Base ‘ 𝑊 ) )
9 fvprc ⊢ ( ¬ 𝑊 ∈ V → ( ringLMod ‘ 𝑊 ) = ∅ )
10 fvprc ⊢ ( ¬ 𝑊 ∈ V → ( subringAlg ‘ 𝑊 ) = ∅ )
11 10 fveq1d ⊢ ( ¬ 𝑊 ∈ V → ( ( subringAlg ‘ 𝑊 ) ‘ ( Base ‘ 𝑊 ) ) = ( ∅ ‘ ( Base ‘ 𝑊 ) ) )
12 8 9 11 3eqtr4a ⊢ ( ¬ 𝑊 ∈ V → ( ringLMod ‘ 𝑊 ) = ( ( subringAlg ‘ 𝑊 ) ‘ ( Base ‘ 𝑊 ) ) )
13 6 12 pm2.61i ⊢ ( ringLMod ‘ 𝑊 ) = ( ( subringAlg ‘ 𝑊 ) ‘ ( Base ‘ 𝑊 ) )