Theorem rlmval

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

	Ref	Expression
Assertion	rlmval	$$⊢\mathrm{ringLMod}\left(W\right)=\mathrm{subringAlg}\left(W\right)\left({\mathrm{Base}}_W\right)$$

Proof

Step	Hyp	Ref	Expression
1		fveq2	$$⊢a=W\to \mathrm{subringAlg}\left(a\right)=\mathrm{subringAlg}\left(W\right)$$
2		fveq2	$$⊢a=W\to {\mathrm{Base}}_a={\mathrm{Base}}_W$$
3	1 2	fveq12d	$$⊢a=W\to \mathrm{subringAlg}\left(a\right)\left({\mathrm{Base}}_a\right)=\mathrm{subringAlg}\left(W\right)\left({\mathrm{Base}}_W\right)$$
4		df-rgmod	$$⊢\mathrm{ringLMod}=\left(a\in \mathrm{V}⟼\mathrm{subringAlg}\left(a\right)\left({\mathrm{Base}}_a\right)\right)$$
5		fvex	$$⊢\mathrm{subringAlg}\left(W\right)\left({\mathrm{Base}}_W\right)\in \mathrm{V}$$
6	3 4 5	fvmpt	$$⊢W\in \mathrm{V}\to \mathrm{ringLMod}\left(W\right)=\mathrm{subringAlg}\left(W\right)\left({\mathrm{Base}}_W\right)$$
7		0fv	$$⊢\varnothing \left({\mathrm{Base}}_W\right)=\varnothing$$
8	7	eqcomi	$$⊢\varnothing =\varnothing \left({\mathrm{Base}}_W\right)$$
9		fvprc	$$⊢\neg W\in \mathrm{V}\to \mathrm{ringLMod}\left(W\right)=\varnothing$$
10		fvprc	$$⊢\neg W\in \mathrm{V}\to \mathrm{subringAlg}\left(W\right)=\varnothing$$
11	10	fveq1d	$$⊢\neg W\in \mathrm{V}\to \mathrm{subringAlg}\left(W\right)\left({\mathrm{Base}}_W\right)=\varnothing \left({\mathrm{Base}}_W\right)$$
12	8 9 11	3eqtr4a	$$⊢\neg W\in \mathrm{V}\to \mathrm{ringLMod}\left(W\right)=\mathrm{subringAlg}\left(W\right)\left({\mathrm{Base}}_W\right)$$
13	6 12	pm2.61i	$$⊢\mathrm{ringLMod}\left(W\right)=\mathrm{subringAlg}\left(W\right)\left({\mathrm{Base}}_W\right)$$