Theorem rrxdim

Description: Dimension of the generalized Euclidean space. (Contributed by Thierry Arnoux, 20-May-2023)

	Ref	Expression
Hypothesis	rrxdim.1
Assertion	rrxdim	$$⊢I\in V\to \dim \left(H\right)=\left|I\right|$$

Proof

Step	Hyp	Ref	Expression
1		rrxdim.1
2	1	rrxval	$$⊢I\in V\to H=\mathrm{toCPreHil}\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)$$
3		eqid	$$⊢\mathrm{toCPreHil}\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)=\mathrm{toCPreHil}\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)$$
4		eqid	$$⊢{\mathrm{Base}}_{\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)}={\mathrm{Base}}_{\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)}$$
5		eqid	$$⊢{\cdot }_{𝑖}\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)={\cdot }_{𝑖}\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)$$
6	3 4 5	tcphval	$$⊢\mathrm{toCPreHil}\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)=\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)\mathrm{toNrmGrp}\left(x\in {\mathrm{Base}}_{\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)}⟼\sqrt{x{\cdot }_{𝑖}\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)x}\right)$$
7	2 6	eqtrdi	$$⊢I\in V\to H=\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)\mathrm{toNrmGrp}\left(x\in {\mathrm{Base}}_{\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)}⟼\sqrt{x{\cdot }_{𝑖}\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)x}\right)$$
8	7	fveq2d	$$⊢I\in V\to \dim \left(H\right)=\dim \left(\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)\mathrm{toNrmGrp}\left(x\in {\mathrm{Base}}_{\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)}⟼\sqrt{x{\cdot }_{𝑖}\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)x}\right)\right)$$
9		resubdrg	$$⊢\left(ℝ\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)\wedge {ℝ}_{\mathrm{fld}}\in \mathrm{DivRing}\right)$$
10	9	simpri	$$⊢{ℝ}_{\mathrm{fld}}\in \mathrm{DivRing}$$
11		eqid	$$⊢{ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I={ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I$$
12	11	frlmlvec	$$⊢\left({ℝ}_{\mathrm{fld}}\in \mathrm{DivRing}\wedge I\in V\right)\to {ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\in \mathrm{LVec}$$
13	10 12	mpan	$$⊢I\in V\to {ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\in \mathrm{LVec}$$
14	4	tcphex	$$⊢\left(x\in {\mathrm{Base}}_{\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)}⟼\sqrt{x{\cdot }_{𝑖}\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)x}\right)\in \mathrm{V}$$
15		eqid	$$⊢\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)\mathrm{toNrmGrp}\left(x\in {\mathrm{Base}}_{\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)}⟼\sqrt{x{\cdot }_{𝑖}\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)x}\right)=\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)\mathrm{toNrmGrp}\left(x\in {\mathrm{Base}}_{\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)}⟼\sqrt{x{\cdot }_{𝑖}\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)x}\right)$$
16	15	tngdim	$$⊢\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\in \mathrm{LVec}\wedge \left(x\in {\mathrm{Base}}_{\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)}⟼\sqrt{x{\cdot }_{𝑖}\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)x}\right)\in \mathrm{V}\right)\to \dim \left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)=\dim \left(\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)\mathrm{toNrmGrp}\left(x\in {\mathrm{Base}}_{\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)}⟼\sqrt{x{\cdot }_{𝑖}\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)x}\right)\right)$$
17	13 14 16	sylancl	$$⊢I\in V\to \dim \left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)=\dim \left(\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)\mathrm{toNrmGrp}\left(x\in {\mathrm{Base}}_{\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)}⟼\sqrt{x{\cdot }_{𝑖}\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)x}\right)\right)$$
18	11	frlmdim	$$⊢\left({ℝ}_{\mathrm{fld}}\in \mathrm{DivRing}\wedge I\in V\right)\to \dim \left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)=\left|I\right|$$
19	10 18	mpan	$$⊢I\in V\to \dim \left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)=\left|I\right|$$
20	8 17 19	3eqtr2d	$$⊢I\in V\to \dim \left(H\right)=\left|I\right|$$