rrnval

Description: The n-dimensional Euclidean space. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 13-Sep-2015)

		Ref	Expression
	Hypothesis	rrnval.1	⊢ 𝑋 = ( ℝ ↑_m 𝐼 )
	Assertion	rrnval	⊢ ( 𝐼 ∈ Fin → ( ℝⁿ ‘ 𝐼 ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		rrnval.1	⊢ 𝑋 = ( ℝ ↑_m 𝐼 )
2		oveq2	⊢ ( 𝑖 = 𝐼 → ( ℝ ↑_m 𝑖 ) = ( ℝ ↑_m 𝐼 ) )
3	2 1	eqtr4di	⊢ ( 𝑖 = 𝐼 → ( ℝ ↑_m 𝑖 ) = 𝑋 )
4		sumeq1	⊢ ( 𝑖 = 𝐼 → Σ 𝑘 ∈ 𝑖 ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) = Σ 𝑘 ∈ 𝐼 ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) )
5	4	fveq2d	⊢ ( 𝑖 = 𝐼 → ( √ ‘ Σ 𝑘 ∈ 𝑖 ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) ) = ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) ) )
6	3 3 5	mpoeq123dv	⊢ ( 𝑖 = 𝐼 → ( 𝑥 ∈ ( ℝ ↑_m 𝑖 ) , 𝑦 ∈ ( ℝ ↑_m 𝑖 ) ↦ ( √ ‘ Σ 𝑘 ∈ 𝑖 ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) ) ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) ) ) )
7		df-rrn	⊢ ℝⁿ = ( 𝑖 ∈ Fin ↦ ( 𝑥 ∈ ( ℝ ↑_m 𝑖 ) , 𝑦 ∈ ( ℝ ↑_m 𝑖 ) ↦ ( √ ‘ Σ 𝑘 ∈ 𝑖 ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) ) ) )
8		fvrn0	⊢ ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) ) ∈ ( ran √ ∪ { ∅ } )
9	8	rgen2w	⊢ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) ) ∈ ( ran √ ∪ { ∅ } )
10		eqid	⊢ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) ) ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) ) )
11	10	fmpo	⊢ ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) ) ∈ ( ran √ ∪ { ∅ } ) ↔ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) ) ) : ( 𝑋 × 𝑋 ) ⟶ ( ran √ ∪ { ∅ } ) )
12	9 11	mpbi	⊢ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) ) ) : ( 𝑋 × 𝑋 ) ⟶ ( ran √ ∪ { ∅ } )
13		ovex	⊢ ( ℝ ↑_m 𝐼 ) ∈ V
14	1 13	eqeltri	⊢ 𝑋 ∈ V
15	14 14	xpex	⊢ ( 𝑋 × 𝑋 ) ∈ V
16		cnex	⊢ ℂ ∈ V
17		sqrtf	⊢ √ : ℂ ⟶ ℂ
18		frn	⊢ ( √ : ℂ ⟶ ℂ → ran √ ⊆ ℂ )
19	17 18	ax-mp	⊢ ran √ ⊆ ℂ
20	16 19	ssexi	⊢ ran √ ∈ V
21		p0ex	⊢ { ∅ } ∈ V
22	20 21	unex	⊢ ( ran √ ∪ { ∅ } ) ∈ V
23		fex2	⊢ ( ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) ) ) : ( 𝑋 × 𝑋 ) ⟶ ( ran √ ∪ { ∅ } ) ∧ ( 𝑋 × 𝑋 ) ∈ V ∧ ( ran √ ∪ { ∅ } ) ∈ V ) → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) ) ) ∈ V )
24	12 15 22 23	mp3an	⊢ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) ) ) ∈ V
25	6 7 24	fvmpt	⊢ ( 𝐼 ∈ Fin → ( ℝⁿ ‘ 𝐼 ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝑥 ‘ 𝑘 ) − ( 𝑦 ‘ 𝑘 ) ) ↑ 2 ) ) ) )

Metamath Proof Explorer

Theorem rrnval

Proof