Theorem rrx0

Description: The zero ("origin") in a generalized real Euclidean space. (Contributed by AV, 11-Feb-2023)

	Ref	Expression
Hypotheses	rrxsca.r
	rrx0.0	$$⊢\underset{\dot{}}{0}=I\times \left\{0\right\}$$
Assertion	rrx0	$$⊢I\in V\to 0_H=\underset{\dot{}}{0}$$

Proof

Step	Hyp	Ref	Expression
1		rrxsca.r
2		rrx0.0	$$⊢\underset{\dot{}}{0}=I\times \left\{0\right\}$$
3	1	rrxval	$$⊢I\in V\to H=\mathrm{toCPreHil}\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)$$
4	3	fveq2d	$$⊢I\in V\to 0_H=0_{\mathrm{toCPreHil}\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)}$$
5		eqid	$$⊢\mathrm{toCPreHil}\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)=\mathrm{toCPreHil}\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)$$
6		eqid	$$⊢{\mathrm{Base}}_{\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)}={\mathrm{Base}}_{\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)}$$
7		eqid	$$⊢{\cdot }_{𝑖}\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)={\cdot }_{𝑖}\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)$$
8	5 6 7	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)$$
9	8	a1i	$$⊢I\in V\to \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)$$
10	9	fveq2d	$$⊢I\in V\to 0_{\mathrm{toCPreHil}\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)}=0_{\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)}$$
11		fvexd	$$⊢I\in V\to {\mathrm{Base}}_{\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)}\in \mathrm{V}$$
12	11	mptexd	$$⊢I\in V\to \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}$$
13		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)$$
14		eqid	$$⊢0_{\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)}=0_{\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)}$$
15	13 14	tng0	$$⊢\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}\to 0_{\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)}=0_{\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)}$$
16	12 15	syl	$$⊢I\in V\to 0_{\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)}=0_{\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		refld	$$⊢{ℝ}_{\mathrm{fld}}\in \mathrm{Field}$$
18		isfld	$$⊢{ℝ}_{\mathrm{fld}}\in \mathrm{Field}\leftrightarrow \left({ℝ}_{\mathrm{fld}}\in \mathrm{DivRing}\wedge {ℝ}_{\mathrm{fld}}\in \mathrm{CRing}\right)$$
19		drngring	$$⊢{ℝ}_{\mathrm{fld}}\in \mathrm{DivRing}\to {ℝ}_{\mathrm{fld}}\in \mathrm{Ring}$$
20	19	adantr	$$⊢\left({ℝ}_{\mathrm{fld}}\in \mathrm{DivRing}\wedge {ℝ}_{\mathrm{fld}}\in \mathrm{CRing}\right)\to {ℝ}_{\mathrm{fld}}\in \mathrm{Ring}$$
21	18 20	sylbi	$$⊢{ℝ}_{\mathrm{fld}}\in \mathrm{Field}\to {ℝ}_{\mathrm{fld}}\in \mathrm{Ring}$$
22	17 21	ax-mp	$$⊢{ℝ}_{\mathrm{fld}}\in \mathrm{Ring}$$
23		eqid	$$⊢{ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I={ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I$$
24		re0g	$$⊢0=0_{{ℝ}_{\mathrm{fld}}}$$
25	23 24	frlm0	$$⊢\left({ℝ}_{\mathrm{fld}}\in \mathrm{Ring}\wedge I\in V\right)\to I\times \left\{0\right\}=0_{\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)}$$
26	22 25	mpan	$$⊢I\in V\to I\times \left\{0\right\}=0_{\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)}$$
27	2 26	eqtr2id	$$⊢I\in V\to 0_{\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)}=\underset{\dot{}}{0}$$
28	10 16 27	3eqtr2d	$$⊢I\in V\to 0_{\mathrm{toCPreHil}\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)}=\underset{\dot{}}{0}$$
29	4 28	eqtrd	$$⊢I\in V\to 0_H=\underset{\dot{}}{0}$$