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

Metamath Proof Explorer

Theorem rrxmval

Description: The value of the Euclidean metric. Compare with rrnmval . (Contributed by Thierry Arnoux, 30-Jun-2019)

Ref Expression
Hypotheses rrxmval.1 ⊢ 𝑋 = { ℎ ∈ ( ℝ ↑m 𝐼 ) ∣ ℎ finSupp 0 }
rrxmval.d ⊢ 𝐷 = ( dist ‘ ( ℝ^ ‘ 𝐼 ) )
Assertion rrxmval ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) → ( 𝐹 𝐷 𝐺 ) = ( √ ‘ Σ 𝑘 ∈ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) ) )

Proof

Step Hyp Ref Expression
1 rrxmval.1 ⊢ 𝑋 = { ℎ ∈ ( ℝ ↑m 𝐼 ) ∣ ℎ finSupp 0 }
2 rrxmval.d ⊢ 𝐷 = ( dist ‘ ( ℝ^ ‘ 𝐼 ) )
3 eqid ⊢ ( ℝ^ ‘ 𝐼 ) = ( ℝ^ ‘ 𝐼 )
4 eqid ⊢ ( Base ‘ ( ℝ^ ‘ 𝐼 ) ) = ( Base ‘ ( ℝ^ ‘ 𝐼 ) )
5 3 4 rrxds ⊢ ( 𝐼 ∈ 𝑉 → ( 𝑓 ∈ ( Base ‘ ( ℝ^ ‘ 𝐼 ) ) , 𝑔 ∈ ( Base ‘ ( ℝ^ ‘ 𝐼 ) ) ↦ ( √ ‘ ( ℝfld Σg ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝑓 ‘ 𝑥 ) − ( 𝑔 ‘ 𝑥 ) ) ↑ 2 ) ) ) ) ) = ( dist ‘ ( ℝ^ ‘ 𝐼 ) ) )
6 2 5 eqtr4id ⊢ ( 𝐼 ∈ 𝑉 → 𝐷 = ( 𝑓 ∈ ( Base ‘ ( ℝ^ ‘ 𝐼 ) ) , 𝑔 ∈ ( Base ‘ ( ℝ^ ‘ 𝐼 ) ) ↦ ( √ ‘ ( ℝfld Σg ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝑓 ‘ 𝑥 ) − ( 𝑔 ‘ 𝑥 ) ) ↑ 2 ) ) ) ) ) )
7 3 4 rrxbase ⊢ ( 𝐼 ∈ 𝑉 → ( Base ‘ ( ℝ^ ‘ 𝐼 ) ) = { ℎ ∈ ( ℝ ↑m 𝐼 ) ∣ ℎ finSupp 0 } )
8 1 7 eqtr4id ⊢ ( 𝐼 ∈ 𝑉 → 𝑋 = ( Base ‘ ( ℝ^ ‘ 𝐼 ) ) )
9 mpoeq12 ⊢ ( ( 𝑋 = ( Base ‘ ( ℝ^ ‘ 𝐼 ) ) ∧ 𝑋 = ( Base ‘ ( ℝ^ ‘ 𝐼 ) ) ) → ( 𝑓 ∈ 𝑋 , 𝑔 ∈ 𝑋 ↦ ( √ ‘ ( ℝfld Σg ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝑓 ‘ 𝑥 ) − ( 𝑔 ‘ 𝑥 ) ) ↑ 2 ) ) ) ) ) = ( 𝑓 ∈ ( Base ‘ ( ℝ^ ‘ 𝐼 ) ) , 𝑔 ∈ ( Base ‘ ( ℝ^ ‘ 𝐼 ) ) ↦ ( √ ‘ ( ℝfld Σg ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝑓 ‘ 𝑥 ) − ( 𝑔 ‘ 𝑥 ) ) ↑ 2 ) ) ) ) ) )
10 8 8 9 syl2anc ⊢ ( 𝐼 ∈ 𝑉 → ( 𝑓 ∈ 𝑋 , 𝑔 ∈ 𝑋 ↦ ( √ ‘ ( ℝfld Σg ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝑓 ‘ 𝑥 ) − ( 𝑔 ‘ 𝑥 ) ) ↑ 2 ) ) ) ) ) = ( 𝑓 ∈ ( Base ‘ ( ℝ^ ‘ 𝐼 ) ) , 𝑔 ∈ ( Base ‘ ( ℝ^ ‘ 𝐼 ) ) ↦ ( √ ‘ ( ℝfld Σg ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝑓 ‘ 𝑥 ) − ( 𝑔 ‘ 𝑥 ) ) ↑ 2 ) ) ) ) ) )
11 6 10 eqtr4d ⊢ ( 𝐼 ∈ 𝑉 → 𝐷 = ( 𝑓 ∈ 𝑋 , 𝑔 ∈ 𝑋 ↦ ( √ ‘ ( ℝfld Σg ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝑓 ‘ 𝑥 ) − ( 𝑔 ‘ 𝑥 ) ) ↑ 2 ) ) ) ) ) )
12 11 3ad2ant1 ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) → 𝐷 = ( 𝑓 ∈ 𝑋 , 𝑔 ∈ 𝑋 ↦ ( √ ‘ ( ℝfld Σg ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝑓 ‘ 𝑥 ) − ( 𝑔 ‘ 𝑥 ) ) ↑ 2 ) ) ) ) ) )
13 simprl ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) ) → 𝑓 = 𝐹 )
14 13 fveq1d ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) ) → ( 𝑓 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
15 simprr ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) ) → 𝑔 = 𝐺 )
16 15 fveq1d ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) ) → ( 𝑔 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) )
17 14 16 oveq12d ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) ) → ( ( 𝑓 ‘ 𝑥 ) − ( 𝑔 ‘ 𝑥 ) ) = ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) )
18 17 oveq1d ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) ) → ( ( ( 𝑓 ‘ 𝑥 ) − ( 𝑔 ‘ 𝑥 ) ) ↑ 2 ) = ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ↑ 2 ) )
19 18 mpteq2dv ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) ) → ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝑓 ‘ 𝑥 ) − ( 𝑔 ‘ 𝑥 ) ) ↑ 2 ) ) = ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ↑ 2 ) ) )
20 19 oveq2d ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) ) → ( ℝfld Σg ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝑓 ‘ 𝑥 ) − ( 𝑔 ‘ 𝑥 ) ) ↑ 2 ) ) ) = ( ℝfld Σg ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ↑ 2 ) ) ) )
21 simp2 ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) → 𝐹 ∈ 𝑋 )
22 1 21 rrxf ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) → 𝐹 : 𝐼 ⟶ ℝ )
23 22 ffvelcdmda ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
24 simp3 ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) → 𝐺 ∈ 𝑋 )
25 1 24 rrxf ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) → 𝐺 : 𝐼 ⟶ ℝ )
26 25 ffvelcdmda ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝐺 ‘ 𝑥 ) ∈ ℝ )
27 23 26 resubcld ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ∈ ℝ )
28 27 resqcld ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ 𝑥 ∈ 𝐼 ) → ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ↑ 2 ) ∈ ℝ )
29 28 fmpttd ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) → ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ↑ 2 ) ) : 𝐼 ⟶ ℝ )
30 1 21 rrxfsupp ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) → ( 𝐹 supp 0 ) ∈ Fin )
31 1 24 rrxfsupp ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) → ( 𝐺 supp 0 ) ∈ Fin )
32 unfi ⊢ ( ( ( 𝐹 supp 0 ) ∈ Fin ∧ ( 𝐺 supp 0 ) ∈ Fin ) → ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ∈ Fin )
33 30 31 32 syl2anc ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) → ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ∈ Fin )
34 1 rrxmvallem ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) → ( ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ↑ 2 ) ) supp 0 ) ⊆ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) )
35 33 34 ssfid ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) → ( ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ↑ 2 ) ) supp 0 ) ∈ Fin )
36 mptexg ⊢ ( 𝐼 ∈ 𝑉 → ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ↑ 2 ) ) ∈ V )
37 funmpt ⊢ Fun ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ↑ 2 ) )
38 0cn ⊢ 0 ∈ ℂ
39 funisfsupp ⊢ ( ( Fun ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ↑ 2 ) ) ∧ ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ↑ 2 ) ) ∈ V ∧ 0 ∈ ℂ ) → ( ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ↑ 2 ) ) finSupp 0 ↔ ( ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ↑ 2 ) ) supp 0 ) ∈ Fin ) )
40 37 38 39 mp3an13 ⊢ ( ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ↑ 2 ) ) ∈ V → ( ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ↑ 2 ) ) finSupp 0 ↔ ( ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ↑ 2 ) ) supp 0 ) ∈ Fin ) )
41 36 40 syl ⊢ ( 𝐼 ∈ 𝑉 → ( ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ↑ 2 ) ) finSupp 0 ↔ ( ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ↑ 2 ) ) supp 0 ) ∈ Fin ) )
42 41 3ad2ant1 ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) → ( ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ↑ 2 ) ) finSupp 0 ↔ ( ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ↑ 2 ) ) supp 0 ) ∈ Fin ) )
43 35 42 mpbird ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) → ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ↑ 2 ) ) finSupp 0 )
44 simp1 ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) → 𝐼 ∈ 𝑉 )
45 regsumsupp ⊢ ( ( ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ↑ 2 ) ) : 𝐼 ⟶ ℝ ∧ ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ↑ 2 ) ) finSupp 0 ∧ 𝐼 ∈ 𝑉 ) → ( ℝfld Σg ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ↑ 2 ) ) ) = Σ 𝑘 ∈ ( ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ↑ 2 ) ) supp 0 ) ( ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ↑ 2 ) ) ‘ 𝑘 ) )
46 29 43 44 45 syl3anc ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) → ( ℝfld Σg ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ↑ 2 ) ) ) = Σ 𝑘 ∈ ( ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ↑ 2 ) ) supp 0 ) ( ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ↑ 2 ) ) ‘ 𝑘 ) )
47 suppssdm ⊢ ( ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ↑ 2 ) ) supp 0 ) ⊆ dom ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ↑ 2 ) )
48 eqid ⊢ ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ↑ 2 ) ) = ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ↑ 2 ) )
49 48 dmmptss ⊢ dom ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ↑ 2 ) ) ⊆ 𝐼
50 47 49 sstri ⊢ ( ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ↑ 2 ) ) supp 0 ) ⊆ 𝐼
51 50 a1i ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) → ( ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ↑ 2 ) ) supp 0 ) ⊆ 𝐼 )
52 51 sselda ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ 𝑘 ∈ ( ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ↑ 2 ) ) supp 0 ) ) → 𝑘 ∈ 𝐼 )
53 eqidd ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐼 ) → ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ↑ 2 ) ) = ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ↑ 2 ) ) )
54 simpr ⊢ ( ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐼 ) ∧ 𝑥 = 𝑘 ) → 𝑥 = 𝑘 )
55 54 fveq2d ⊢ ( ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐼 ) ∧ 𝑥 = 𝑘 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑘 ) )
56 54 fveq2d ⊢ ( ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐼 ) ∧ 𝑥 = 𝑘 ) → ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑘 ) )
57 55 56 oveq12d ⊢ ( ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐼 ) ∧ 𝑥 = 𝑘 ) → ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) = ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) )
58 57 oveq1d ⊢ ( ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐼 ) ∧ 𝑥 = 𝑘 ) → ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ↑ 2 ) = ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) )
59 simpr ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐼 ) → 𝑘 ∈ 𝐼 )
60 ovexd ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐼 ) → ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) ∈ V )
61 53 58 59 60 fvmptd ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐼 ) → ( ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ↑ 2 ) ) ‘ 𝑘 ) = ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) )
62 61 eqcomd ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐼 ) → ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) = ( ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ↑ 2 ) ) ‘ 𝑘 ) )
63 52 62 syldan ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ 𝑘 ∈ ( ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ↑ 2 ) ) supp 0 ) ) → ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) = ( ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ↑ 2 ) ) ‘ 𝑘 ) )
64 63 sumeq2dv ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) → Σ 𝑘 ∈ ( ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ↑ 2 ) ) supp 0 ) ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) = Σ 𝑘 ∈ ( ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ↑ 2 ) ) supp 0 ) ( ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ↑ 2 ) ) ‘ 𝑘 ) )
65 46 64 eqtr4d ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) → ( ℝfld Σg ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ↑ 2 ) ) ) = Σ 𝑘 ∈ ( ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ↑ 2 ) ) supp 0 ) ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) )
66 65 adantr ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) ) → ( ℝfld Σg ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ↑ 2 ) ) ) = Σ 𝑘 ∈ ( ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ↑ 2 ) ) supp 0 ) ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) )
67 22 ffvelcdmda ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐼 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
68 67 recnd ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐼 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
69 25 ffvelcdmda ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐼 ) → ( 𝐺 ‘ 𝑘 ) ∈ ℝ )
70 69 recnd ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐼 ) → ( 𝐺 ‘ 𝑘 ) ∈ ℂ )
71 68 70 subcld ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐼 ) → ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ∈ ℂ )
72 71 sqcld ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐼 ) → ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) ∈ ℂ )
73 52 72 syldan ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ 𝑘 ∈ ( ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ↑ 2 ) ) supp 0 ) ) → ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) ∈ ℂ )
74 1 21 rrxsuppss ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) → ( 𝐹 supp 0 ) ⊆ 𝐼 )
75 1 24 rrxsuppss ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) → ( 𝐺 supp 0 ) ⊆ 𝐼 )
76 74 75 unssd ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) → ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ⊆ 𝐼 )
77 76 ssdifssd ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) → ( ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ∖ ( ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ↑ 2 ) ) supp 0 ) ) ⊆ 𝐼 )
78 77 sselda ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ 𝑘 ∈ ( ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ∖ ( ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ↑ 2 ) ) supp 0 ) ) ) → 𝑘 ∈ 𝐼 )
79 78 62 syldan ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ 𝑘 ∈ ( ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ∖ ( ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ↑ 2 ) ) supp 0 ) ) ) → ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) = ( ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ↑ 2 ) ) ‘ 𝑘 ) )
80 76 ssdifd ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) → ( ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ∖ ( ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ↑ 2 ) ) supp 0 ) ) ⊆ ( 𝐼 ∖ ( ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ↑ 2 ) ) supp 0 ) ) )
81 80 sselda ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ 𝑘 ∈ ( ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ∖ ( ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ↑ 2 ) ) supp 0 ) ) ) → 𝑘 ∈ ( 𝐼 ∖ ( ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ↑ 2 ) ) supp 0 ) ) )
82 ssidd ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) → ( ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ↑ 2 ) ) supp 0 ) ⊆ ( ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ↑ 2 ) ) supp 0 ) )
83 0cnd ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) → 0 ∈ ℂ )
84 29 82 44 83 suppssr ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ 𝑘 ∈ ( 𝐼 ∖ ( ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ↑ 2 ) ) supp 0 ) ) ) → ( ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ↑ 2 ) ) ‘ 𝑘 ) = 0 )
85 81 84 syldan ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ 𝑘 ∈ ( ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ∖ ( ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ↑ 2 ) ) supp 0 ) ) ) → ( ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ↑ 2 ) ) ‘ 𝑘 ) = 0 )
86 79 85 eqtrd ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ 𝑘 ∈ ( ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ∖ ( ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ↑ 2 ) ) supp 0 ) ) ) → ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) = 0 )
87 34 73 86 33 fsumss ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) → Σ 𝑘 ∈ ( ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ↑ 2 ) ) supp 0 ) ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) = Σ 𝑘 ∈ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) )
88 87 adantr ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) ) → Σ 𝑘 ∈ ( ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ↑ 2 ) ) supp 0 ) ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) = Σ 𝑘 ∈ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) )
89 20 66 88 3eqtrd ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) ) → ( ℝfld Σg ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝑓 ‘ 𝑥 ) − ( 𝑔 ‘ 𝑥 ) ) ↑ 2 ) ) ) = Σ 𝑘 ∈ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) )
90 89 fveq2d ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) ) → ( √ ‘ ( ℝfld Σg ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝑓 ‘ 𝑥 ) − ( 𝑔 ‘ 𝑥 ) ) ↑ 2 ) ) ) ) = ( √ ‘ Σ 𝑘 ∈ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) ) )
91 fvexd ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) → ( √ ‘ Σ 𝑘 ∈ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) ) ∈ V )
92 12 90 21 24 91 ovmpod ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) → ( 𝐹 𝐷 𝐺 ) = ( √ ‘ Σ 𝑘 ∈ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) ) )