Theorem rrxprds

Description: Expand the definition of the generalized real Euclidean spaces. (Contributed by Thierry Arnoux, 16-Jun-2019)

	Ref	Expression
Hypotheses	rrxval.r
	rrxbase.b	$$⊢B={\mathrm{Base}}_H$$
Assertion	rrxprds	$$⊢I\in V\to H=\mathrm{toCPreHil}\left(\left({ℝ}_{\mathrm{fld}}{⨉}_{𝑠}\left(I\times \left\{\mathrm{subringAlg}\left({ℝ}_{\mathrm{fld}}\right)\left(ℝ\right)\right\}\right)\right){\upharpoonright }_{𝑠}B\right)$$

Proof

Step	Hyp	Ref	Expression
1		rrxval.r
2		rrxbase.b	$$⊢B={\mathrm{Base}}_H$$
3	1	rrxval	$$⊢I\in V\to H=\mathrm{toCPreHil}\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)$$
4		refld	$$⊢{ℝ}_{\mathrm{fld}}\in \mathrm{Field}$$
5		eqid	$$⊢{ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I={ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I$$
6		eqid	$$⊢{\mathrm{Base}}_{\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)}={\mathrm{Base}}_{\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)}$$
7	5 6	frlmpws	$$⊢\left({ℝ}_{\mathrm{fld}}\in \mathrm{Field}\wedge I\in V\right)\to {ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I=\left(\mathrm{ringLMod}\left({ℝ}_{\mathrm{fld}}\right){\uparrow }_{𝑠}I\right){\upharpoonright }_{𝑠}{\mathrm{Base}}_{\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)}$$
8	4 7	mpan	$$⊢I\in V\to {ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I=\left(\mathrm{ringLMod}\left({ℝ}_{\mathrm{fld}}\right){\uparrow }_{𝑠}I\right){\upharpoonright }_{𝑠}{\mathrm{Base}}_{\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)}$$
9		fvex	$$⊢\mathrm{subringAlg}\left({ℝ}_{\mathrm{fld}}\right)\left(ℝ\right)\in \mathrm{V}$$
10		rlmval	$$⊢\mathrm{ringLMod}\left({ℝ}_{\mathrm{fld}}\right)=\mathrm{subringAlg}\left({ℝ}_{\mathrm{fld}}\right)\left({\mathrm{Base}}_{{ℝ}_{\mathrm{fld}}}\right)$$
11		rebase	$$⊢ℝ={\mathrm{Base}}_{{ℝ}_{\mathrm{fld}}}$$
12	11	fveq2i	$$⊢\mathrm{subringAlg}\left({ℝ}_{\mathrm{fld}}\right)\left(ℝ\right)=\mathrm{subringAlg}\left({ℝ}_{\mathrm{fld}}\right)\left({\mathrm{Base}}_{{ℝ}_{\mathrm{fld}}}\right)$$
13	10 12	eqtr4i	$$⊢\mathrm{ringLMod}\left({ℝ}_{\mathrm{fld}}\right)=\mathrm{subringAlg}\left({ℝ}_{\mathrm{fld}}\right)\left(ℝ\right)$$
14	13	oveq1i	$$⊢\mathrm{ringLMod}\left({ℝ}_{\mathrm{fld}}\right){\uparrow }_{𝑠}I=\mathrm{subringAlg}\left({ℝ}_{\mathrm{fld}}\right)\left(ℝ\right){\uparrow }_{𝑠}I$$
15	11	ressid	$$⊢{ℝ}_{\mathrm{fld}}\in \mathrm{Field}\to {ℝ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}ℝ={ℝ}_{\mathrm{fld}}$$
16	4 15	ax-mp	$$⊢{ℝ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}ℝ={ℝ}_{\mathrm{fld}}$$
17		eqidd	$$⊢\top \to \mathrm{subringAlg}\left({ℝ}_{\mathrm{fld}}\right)\left(ℝ\right)=\mathrm{subringAlg}\left({ℝ}_{\mathrm{fld}}\right)\left(ℝ\right)$$
18	11	eqimssi	$$⊢ℝ\subseteq {\mathrm{Base}}_{{ℝ}_{\mathrm{fld}}}$$
19	18	a1i	$$⊢\top \to ℝ\subseteq {\mathrm{Base}}_{{ℝ}_{\mathrm{fld}}}$$
20	17 19	srasca	$$⊢\top \to {ℝ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}ℝ=\mathrm{Scalar}\left(\mathrm{subringAlg}\left({ℝ}_{\mathrm{fld}}\right)\left(ℝ\right)\right)$$
21	20	mptru	$$⊢{ℝ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}ℝ=\mathrm{Scalar}\left(\mathrm{subringAlg}\left({ℝ}_{\mathrm{fld}}\right)\left(ℝ\right)\right)$$
22	16 21	eqtr3i	$$⊢{ℝ}_{\mathrm{fld}}=\mathrm{Scalar}\left(\mathrm{subringAlg}\left({ℝ}_{\mathrm{fld}}\right)\left(ℝ\right)\right)$$
23	14 22	pwsval	$$⊢\left(\mathrm{subringAlg}\left({ℝ}_{\mathrm{fld}}\right)\left(ℝ\right)\in \mathrm{V}\wedge I\in V\right)\to \mathrm{ringLMod}\left({ℝ}_{\mathrm{fld}}\right){\uparrow }_{𝑠}I={ℝ}_{\mathrm{fld}}{⨉}_{𝑠}\left(I\times \left\{\mathrm{subringAlg}\left({ℝ}_{\mathrm{fld}}\right)\left(ℝ\right)\right\}\right)$$
24	9 23	mpan	$$⊢I\in V\to \mathrm{ringLMod}\left({ℝ}_{\mathrm{fld}}\right){\uparrow }_{𝑠}I={ℝ}_{\mathrm{fld}}{⨉}_{𝑠}\left(I\times \left\{\mathrm{subringAlg}\left({ℝ}_{\mathrm{fld}}\right)\left(ℝ\right)\right\}\right)$$
25	24	eqcomd	$$⊢I\in V\to {ℝ}_{\mathrm{fld}}{⨉}_{𝑠}\left(I\times \left\{\mathrm{subringAlg}\left({ℝ}_{\mathrm{fld}}\right)\left(ℝ\right)\right\}\right)=\mathrm{ringLMod}\left({ℝ}_{\mathrm{fld}}\right){\uparrow }_{𝑠}I$$
26	3	fveq2d	$$⊢I\in V\to {\mathrm{Base}}_H={\mathrm{Base}}_{\mathrm{toCPreHil}\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)}$$
27		eqid	$$⊢\mathrm{toCPreHil}\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)=\mathrm{toCPreHil}\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)$$
28	27 6	tcphbas	$$⊢{\mathrm{Base}}_{\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)}={\mathrm{Base}}_{\mathrm{toCPreHil}\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)}$$
29	26 2 28	3eqtr4g	$$⊢I\in V\to B={\mathrm{Base}}_{\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)}$$
30	25 29	oveq12d	$$⊢I\in V\to \left({ℝ}_{\mathrm{fld}}{⨉}_{𝑠}\left(I\times \left\{\mathrm{subringAlg}\left({ℝ}_{\mathrm{fld}}\right)\left(ℝ\right)\right\}\right)\right){\upharpoonright }_{𝑠}B=\left(\mathrm{ringLMod}\left({ℝ}_{\mathrm{fld}}\right){\uparrow }_{𝑠}I\right){\upharpoonright }_{𝑠}{\mathrm{Base}}_{\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)}$$
31	8 30	eqtr4d	$$⊢I\in V\to {ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I=\left({ℝ}_{\mathrm{fld}}{⨉}_{𝑠}\left(I\times \left\{\mathrm{subringAlg}\left({ℝ}_{\mathrm{fld}}\right)\left(ℝ\right)\right\}\right)\right){\upharpoonright }_{𝑠}B$$
32	31	fveq2d	$$⊢I\in V\to \mathrm{toCPreHil}\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)=\mathrm{toCPreHil}\left(\left({ℝ}_{\mathrm{fld}}{⨉}_{𝑠}\left(I\times \left\{\mathrm{subringAlg}\left({ℝ}_{\mathrm{fld}}\right)\left(ℝ\right)\right\}\right)\right){\upharpoonright }_{𝑠}B\right)$$
33	3 32	eqtrd	$$⊢I\in V\to H=\mathrm{toCPreHil}\left(\left({ℝ}_{\mathrm{fld}}{⨉}_{𝑠}\left(I\times \left\{\mathrm{subringAlg}\left({ℝ}_{\mathrm{fld}}\right)\left(ℝ\right)\right\}\right)\right){\upharpoonright }_{𝑠}B\right)$$