Theorem frlmsca

Description: The ring of scalars of a free module. (Contributed by Stefan O'Rear, 1-Feb-2015)

	Ref	Expression
Hypothesis	frlmval.f	$$⊢F=R\mathrm{freeLMod}I$$
Assertion	frlmsca	$$⊢\left(R\in V\wedge I\in W\right)\to R=\mathrm{Scalar}\left(F\right)$$

Proof

Step	Hyp	Ref	Expression
1		frlmval.f	$$⊢F=R\mathrm{freeLMod}I$$
2		fvex	$$⊢\mathrm{ringLMod}\left(R\right)\in \mathrm{V}$$
3		eqid	$$⊢\mathrm{ringLMod}\left(R\right){\uparrow }_{𝑠}I=\mathrm{ringLMod}\left(R\right){\uparrow }_{𝑠}I$$
4		eqid	$$⊢\mathrm{Scalar}\left(\mathrm{ringLMod}\left(R\right)\right)=\mathrm{Scalar}\left(\mathrm{ringLMod}\left(R\right)\right)$$
5	3 4	pwssca	$$⊢\left(\mathrm{ringLMod}\left(R\right)\in \mathrm{V}\wedge I\in W\right)\to \mathrm{Scalar}\left(\mathrm{ringLMod}\left(R\right)\right)=\mathrm{Scalar}\left(\mathrm{ringLMod}\left(R\right){\uparrow }_{𝑠}I\right)$$
6	2 5	mpan	$$⊢I\in W\to \mathrm{Scalar}\left(\mathrm{ringLMod}\left(R\right)\right)=\mathrm{Scalar}\left(\mathrm{ringLMod}\left(R\right){\uparrow }_{𝑠}I\right)$$
7	6	adantl	$$⊢\left(R\in V\wedge I\in W\right)\to \mathrm{Scalar}\left(\mathrm{ringLMod}\left(R\right)\right)=\mathrm{Scalar}\left(\mathrm{ringLMod}\left(R\right){\uparrow }_{𝑠}I\right)$$
8		fvex	$$⊢{\mathrm{Base}}_F\in \mathrm{V}$$
9		eqid	$$⊢\left(\mathrm{ringLMod}\left(R\right){\uparrow }_{𝑠}I\right){\upharpoonright }_{𝑠}{\mathrm{Base}}_F=\left(\mathrm{ringLMod}\left(R\right){\uparrow }_{𝑠}I\right){\upharpoonright }_{𝑠}{\mathrm{Base}}_F$$
10		eqid	$$⊢\mathrm{Scalar}\left(\mathrm{ringLMod}\left(R\right){\uparrow }_{𝑠}I\right)=\mathrm{Scalar}\left(\mathrm{ringLMod}\left(R\right){\uparrow }_{𝑠}I\right)$$
11	9 10	resssca	$$⊢{\mathrm{Base}}_F\in \mathrm{V}\to \mathrm{Scalar}\left(\mathrm{ringLMod}\left(R\right){\uparrow }_{𝑠}I\right)=\mathrm{Scalar}\left(\left(\mathrm{ringLMod}\left(R\right){\uparrow }_{𝑠}I\right){\upharpoonright }_{𝑠}{\mathrm{Base}}_F\right)$$
12	8 11	ax-mp	$$⊢\mathrm{Scalar}\left(\mathrm{ringLMod}\left(R\right){\uparrow }_{𝑠}I\right)=\mathrm{Scalar}\left(\left(\mathrm{ringLMod}\left(R\right){\uparrow }_{𝑠}I\right){\upharpoonright }_{𝑠}{\mathrm{Base}}_F\right)$$
13	7 12	eqtrdi	$$⊢\left(R\in V\wedge I\in W\right)\to \mathrm{Scalar}\left(\mathrm{ringLMod}\left(R\right)\right)=\mathrm{Scalar}\left(\left(\mathrm{ringLMod}\left(R\right){\uparrow }_{𝑠}I\right){\upharpoonright }_{𝑠}{\mathrm{Base}}_F\right)$$
14		rlmsca	$$⊢R\in V\to R=\mathrm{Scalar}\left(\mathrm{ringLMod}\left(R\right)\right)$$
15	14	adantr	$$⊢\left(R\in V\wedge I\in W\right)\to R=\mathrm{Scalar}\left(\mathrm{ringLMod}\left(R\right)\right)$$
16		eqid	$$⊢{\mathrm{Base}}_F={\mathrm{Base}}_F$$
17	1 16	frlmpws	$$⊢\left(R\in V\wedge I\in W\right)\to F=\left(\mathrm{ringLMod}\left(R\right){\uparrow }_{𝑠}I\right){\upharpoonright }_{𝑠}{\mathrm{Base}}_F$$
18	17	fveq2d	$$⊢\left(R\in V\wedge I\in W\right)\to \mathrm{Scalar}\left(F\right)=\mathrm{Scalar}\left(\left(\mathrm{ringLMod}\left(R\right){\uparrow }_{𝑠}I\right){\upharpoonright }_{𝑠}{\mathrm{Base}}_F\right)$$
19	13 15 18	3eqtr4d	$$⊢\left(R\in V\wedge I\in W\right)\to R=\mathrm{Scalar}\left(F\right)$$