This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-rrx

Description: Define the function associating with a set the free real vector space on that set, equipped with the natural inner product and norm. This is the direct sum of copies of the field of real numbers indexed by that set. We call it here a "generalized real Euclidean space", but note that it need not be complete (for instance if the given set is infinite countable). (Contributed by Thierry Arnoux, 16-Jun-2019)

		Ref	Expression
	Assertion	df-rrx	⊢ ℝ^ = ( 𝑖 ∈ V ↦ ( toℂPreHil ‘ ( ℝ_fld freeLMod 𝑖 ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		crrx	⊢ ℝ^
1		vi	⊢ 𝑖
2		cvv	⊢ V
3		ctcph	⊢ toℂPreHil
4		crefld	⊢ ℝ_fld
5		cfrlm	⊢ freeLMod
6	1	cv	⊢ 𝑖
7	4 6 5	co	⊢ ( ℝ_fld freeLMod 𝑖 )
8	7 3	cfv	⊢ ( toℂPreHil ‘ ( ℝ_fld freeLMod 𝑖 ) )
9	1 2 8	cmpt	⊢ ( 𝑖 ∈ V ↦ ( toℂPreHil ‘ ( ℝ_fld freeLMod 𝑖 ) ) )
10	0 9	wceq	⊢ ℝ^ = ( 𝑖 ∈ V ↦ ( toℂPreHil ‘ ( ℝ_fld freeLMod 𝑖 ) ) )