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 ) ) )