Theorem rlmval2

Description: Value of the ring module extended. (Contributed by AV, 2-Dec-2018) (Revised by Thierry Arnoux, 16-Jun-2019)

	Ref	Expression
Assertion	rlmval2	$$⊢W\in X\to \mathrm{ringLMod}\left(W\right)=\left(\left(W\mathrm{sSet}⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),W⟩\right)\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},{\cdot }_W⟩\right)\mathrm{sSet}⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),{\cdot }_W⟩$$

Proof

Step	Hyp	Ref	Expression
1		rlmval	$$⊢\mathrm{ringLMod}\left(W\right)=\mathrm{subringAlg}\left(W\right)\left({\mathrm{Base}}_W\right)$$
2	1	a1i	$$⊢W\in X\to \mathrm{ringLMod}\left(W\right)=\mathrm{subringAlg}\left(W\right)\left({\mathrm{Base}}_W\right)$$
3		ssid	$$⊢{\mathrm{Base}}_W\subseteq {\mathrm{Base}}_W$$
4		sraval	$$⊢\left(W\in X\wedge {\mathrm{Base}}_W\subseteq {\mathrm{Base}}_W\right)\to \mathrm{subringAlg}\left(W\right)\left({\mathrm{Base}}_W\right)=\left(\left(W\mathrm{sSet}⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),W{\upharpoonright }_{𝑠}{\mathrm{Base}}_W⟩\right)\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},{\cdot }_W⟩\right)\mathrm{sSet}⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),{\cdot }_W⟩$$
5	3 4	mpan2	$$⊢W\in X\to \mathrm{subringAlg}\left(W\right)\left({\mathrm{Base}}_W\right)=\left(\left(W\mathrm{sSet}⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),W{\upharpoonright }_{𝑠}{\mathrm{Base}}_W⟩\right)\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},{\cdot }_W⟩\right)\mathrm{sSet}⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),{\cdot }_W⟩$$
6		eqid	$$⊢{\mathrm{Base}}_W={\mathrm{Base}}_W$$
7	6	ressid	$$⊢W\in X\to W{\upharpoonright }_{𝑠}{\mathrm{Base}}_W=W$$
8	7	opeq2d	$$⊢W\in X\to ⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),W{\upharpoonright }_{𝑠}{\mathrm{Base}}_W⟩=⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),W⟩$$
9	8	oveq2d	$$⊢W\in X\to W\mathrm{sSet}⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),W{\upharpoonright }_{𝑠}{\mathrm{Base}}_W⟩=W\mathrm{sSet}⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),W⟩$$
10	9	oveq1d	$$⊢W\in X\to \left(W\mathrm{sSet}⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),W{\upharpoonright }_{𝑠}{\mathrm{Base}}_W⟩\right)\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},{\cdot }_W⟩=\left(W\mathrm{sSet}⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),W⟩\right)\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},{\cdot }_W⟩$$
11	10	oveq1d	$$⊢W\in X\to \left(\left(W\mathrm{sSet}⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),W{\upharpoonright }_{𝑠}{\mathrm{Base}}_W⟩\right)\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},{\cdot }_W⟩\right)\mathrm{sSet}⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),{\cdot }_W⟩=\left(\left(W\mathrm{sSet}⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),W⟩\right)\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},{\cdot }_W⟩\right)\mathrm{sSet}⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),{\cdot }_W⟩$$
12	2 5 11	3eqtrd	$$⊢W\in X\to \mathrm{ringLMod}\left(W\right)=\left(\left(W\mathrm{sSet}⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),W⟩\right)\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},{\cdot }_W⟩\right)\mathrm{sSet}⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),{\cdot }_W⟩$$