rlmval

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

		Ref	Expression
	Assertion	rlmval	$⊢ ringLMod (W) = subringAlg (W) ({Base}_{W})$

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

Metamath Proof Explorer