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 ‘ 𝑊 ) )