rrxmval - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > rrxmval		Structured version Visualization version GIF version

Theorem rrxmval 24597

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

**Hypotheses**
Ref	Expression
rrxmval.1	⊢ 𝑋 = {ℎ ∈ (ℝ ↑_m 𝐼) ∣ ℎ finSupp 0}
rrxmval.d	⊢ 𝐷 = (dist‘(ℝ^‘𝐼))

**Assertion**
Ref	Expression
rrxmval	⊢ ((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) → (𝐹𝐷𝐺) = (√‘Σ𝑘 ∈ ((𝐹 supp 0) ∪ (𝐺 supp 0))(((𝐹‘𝑘) − (𝐺‘𝑘))↑2)))

Distinct variable groups: ℎ,𝐹,𝑘 ℎ,𝐺,𝑘 ℎ,𝐼,𝑘 ℎ,𝑉,𝑘 𝑘,𝑋 Allowed substitution hints: 𝐷(ℎ,𝑘) 𝑋(ℎ)

Proof of Theorem rrxmval Dummy variables 𝑓 𝑔 𝑥 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		rrxmval.d	. . . . 5 ⊢ 𝐷 = (dist‘(ℝ^‘𝐼))
2		eqid 2733	. . . . . 6 ⊢ (ℝ^‘𝐼) = (ℝ^‘𝐼)
3		eqid 2733	. . . . . 6 ⊢ (Base‘(ℝ^‘𝐼)) = (Base‘(ℝ^‘𝐼))
4	2, 3	rrxds 24585	. . . . 5 ⊢ (𝐼 ∈ 𝑉 → (𝑓 ∈ (Base‘(ℝ^‘𝐼)), 𝑔 ∈ (Base‘(ℝ^‘𝐼)) ↦ (√‘(ℝ_fld Σ_g (𝑥 ∈ 𝐼 ↦ (((𝑓‘𝑥) − (𝑔‘𝑥))↑2))))) = (dist‘(ℝ^‘𝐼)))
5	1, 4	eqtr4id 2792	. . . 4 ⊢ (𝐼 ∈ 𝑉 → 𝐷 = (𝑓 ∈ (Base‘(ℝ^‘𝐼)), 𝑔 ∈ (Base‘(ℝ^‘𝐼)) ↦ (√‘(ℝ_fld Σ_g (𝑥 ∈ 𝐼 ↦ (((𝑓‘𝑥) − (𝑔‘𝑥))↑2))))))
6		rrxmval.1	. . . . . 6 ⊢ 𝑋 = {ℎ ∈ (ℝ ↑_m 𝐼) ∣ ℎ finSupp 0}
7	2, 3	rrxbase 24580	. . . . . 6 ⊢ (𝐼 ∈ 𝑉 → (Base‘(ℝ^‘𝐼)) = {ℎ ∈ (ℝ ↑_m 𝐼) ∣ ℎ finSupp 0})
8	6, 7	eqtr4id 2792	. . . . 5 ⊢ (𝐼 ∈ 𝑉 → 𝑋 = (Base‘(ℝ^‘𝐼)))
9		mpoeq12 7368	. . . . 5 ⊢ ((𝑋 = (Base‘(ℝ^‘𝐼)) ∧ 𝑋 = (Base‘(ℝ^‘𝐼))) → (𝑓 ∈ 𝑋, 𝑔 ∈ 𝑋 ↦ (√‘(ℝ_fld Σ_g (𝑥 ∈ 𝐼 ↦ (((𝑓‘𝑥) − (𝑔‘𝑥))↑2))))) = (𝑓 ∈ (Base‘(ℝ^‘𝐼)), 𝑔 ∈ (Base‘(ℝ^‘𝐼)) ↦ (√‘(ℝ_fld Σ_g (𝑥 ∈ 𝐼 ↦ (((𝑓‘𝑥) − (𝑔‘𝑥))↑2))))))
10	8, 8, 9	syl2anc 583	. . . 4 ⊢ (𝐼 ∈ 𝑉 → (𝑓 ∈ 𝑋, 𝑔 ∈ 𝑋 ↦ (√‘(ℝ_fld Σ_g (𝑥 ∈ 𝐼 ↦ (((𝑓‘𝑥) − (𝑔‘𝑥))↑2))))) = (𝑓 ∈ (Base‘(ℝ^‘𝐼)), 𝑔 ∈ (Base‘(ℝ^‘𝐼)) ↦ (√‘(ℝ_fld Σ_g (𝑥 ∈ 𝐼 ↦ (((𝑓‘𝑥) − (𝑔‘𝑥))↑2))))))
11	5, 10	eqtr4d 2776	. . 3 ⊢ (𝐼 ∈ 𝑉 → 𝐷 = (𝑓 ∈ 𝑋, 𝑔 ∈ 𝑋 ↦ (√‘(ℝ_fld Σ_g (𝑥 ∈ 𝐼 ↦ (((𝑓‘𝑥) − (𝑔‘𝑥))↑2))))))
12	11	3ad2ant1 1131	. 2 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) → 𝐷 = (𝑓 ∈ 𝑋, 𝑔 ∈ 𝑋 ↦ (√‘(ℝ_fld Σ_g (𝑥 ∈ 𝐼 ↦ (((𝑓‘𝑥) − (𝑔‘𝑥))↑2))))))
13		simprl 767	. . . . . . . . 9 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑓 = 𝐹 ∧ 𝑔 = 𝐺)) → 𝑓 = 𝐹)
14	13	fveq1d 6794	. . . . . . . 8 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑓 = 𝐹 ∧ 𝑔 = 𝐺)) → (𝑓‘𝑥) = (𝐹‘𝑥))
15		simprr 769	. . . . . . . . 9 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑓 = 𝐹 ∧ 𝑔 = 𝐺)) → 𝑔 = 𝐺)
16	15	fveq1d 6794	. . . . . . . 8 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑓 = 𝐹 ∧ 𝑔 = 𝐺)) → (𝑔‘𝑥) = (𝐺‘𝑥))
17	14, 16	oveq12d 7313	. . . . . . 7 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑓 = 𝐹 ∧ 𝑔 = 𝐺)) → ((𝑓‘𝑥) − (𝑔‘𝑥)) = ((𝐹‘𝑥) − (𝐺‘𝑥)))
18	17	oveq1d 7310	. . . . . 6 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑓 = 𝐹 ∧ 𝑔 = 𝐺)) → (((𝑓‘𝑥) − (𝑔‘𝑥))↑2) = (((𝐹‘𝑥) − (𝐺‘𝑥))↑2))
19	18	mpteq2dv 5179	. . . . 5 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑓 = 𝐹 ∧ 𝑔 = 𝐺)) → (𝑥 ∈ 𝐼 ↦ (((𝑓‘𝑥) − (𝑔‘𝑥))↑2)) = (𝑥 ∈ 𝐼 ↦ (((𝐹‘𝑥) − (𝐺‘𝑥))↑2)))
20	19	oveq2d 7311	. . . 4 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑓 = 𝐹 ∧ 𝑔 = 𝐺)) → (ℝ_fld Σ_g (𝑥 ∈ 𝐼 ↦ (((𝑓‘𝑥) − (𝑔‘𝑥))↑2))) = (ℝ_fld Σ_g (𝑥 ∈ 𝐼 ↦ (((𝐹‘𝑥) − (𝐺‘𝑥))↑2))))
21		simp2 1135	. . . . . . . . . . . 12 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) → 𝐹 ∈ 𝑋)
22	6, 21	rrxf 24593	. . . . . . . . . . 11 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) → 𝐹:𝐼⟶ℝ)
23	22	ffvelcdmda 6981	. . . . . . . . . 10 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ 𝑥 ∈ 𝐼) → (𝐹‘𝑥) ∈ ℝ)
24		simp3 1136	. . . . . . . . . . . 12 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) → 𝐺 ∈ 𝑋)
25	6, 24	rrxf 24593	. . . . . . . . . . 11 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) → 𝐺:𝐼⟶ℝ)
26	25	ffvelcdmda 6981	. . . . . . . . . 10 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ 𝑥 ∈ 𝐼) → (𝐺‘𝑥) ∈ ℝ)
27	23, 26	resubcld 11431	. . . . . . . . 9 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ 𝑥 ∈ 𝐼) → ((𝐹‘𝑥) − (𝐺‘𝑥)) ∈ ℝ)
28	27	resqcld 13993	. . . . . . . 8 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ 𝑥 ∈ 𝐼) → (((𝐹‘𝑥) − (𝐺‘𝑥))↑2) ∈ ℝ)
29	28	fmpttd 7009	. . . . . . 7 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) → (𝑥 ∈ 𝐼 ↦ (((𝐹‘𝑥) − (𝐺‘𝑥))↑2)):𝐼⟶ℝ)
30	6, 21	rrxfsupp 24594	. . . . . . . . . 10 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) → (𝐹 supp 0) ∈ Fin)
31	6, 24	rrxfsupp 24594	. . . . . . . . . 10 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) → (𝐺 supp 0) ∈ Fin)
32		unfi 8980	. . . . . . . . . 10 ⊢ (((𝐹 supp 0) ∈ Fin ∧ (𝐺 supp 0) ∈ Fin) → ((𝐹 supp 0) ∪ (𝐺 supp 0)) ∈ Fin)
33	30, 31, 32	syl2anc 583	. . . . . . . . 9 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) → ((𝐹 supp 0) ∪ (𝐺 supp 0)) ∈ Fin)
34	6	rrxmvallem 24596	. . . . . . . . 9 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) → ((𝑥 ∈ 𝐼 ↦ (((𝐹‘𝑥) − (𝐺‘𝑥))↑2)) supp 0) ⊆ ((𝐹 supp 0) ∪ (𝐺 supp 0)))
35	33, 34	ssfid 9070	. . . . . . . 8 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) → ((𝑥 ∈ 𝐼 ↦ (((𝐹‘𝑥) − (𝐺‘𝑥))↑2)) supp 0) ∈ Fin)
36		mptexg 7117	. . . . . . . . . 10 ⊢ (𝐼 ∈ 𝑉 → (𝑥 ∈ 𝐼 ↦ (((𝐹‘𝑥) − (𝐺‘𝑥))↑2)) ∈ V)
37		funmpt 6489	. . . . . . . . . . 11 ⊢ Fun (𝑥 ∈ 𝐼 ↦ (((𝐹‘𝑥) − (𝐺‘𝑥))↑2))
38		0cn 10995	. . . . . . . . . . 11 ⊢ 0 ∈ ℂ
39		funisfsupp 9161	. . . . . . . . . . 11 ⊢ ((Fun (𝑥 ∈ 𝐼 ↦ (((𝐹‘𝑥) − (𝐺‘𝑥))↑2)) ∧ (𝑥 ∈ 𝐼 ↦ (((𝐹‘𝑥) − (𝐺‘𝑥))↑2)) ∈ V ∧ 0 ∈ ℂ) → ((𝑥 ∈ 𝐼 ↦ (((𝐹‘𝑥) − (𝐺‘𝑥))↑2)) finSupp 0 ↔ ((𝑥 ∈ 𝐼 ↦ (((𝐹‘𝑥) − (𝐺‘𝑥))↑2)) supp 0) ∈ Fin))
40	37, 38, 39	mp3an13 1450	. . . . . . . . . 10 ⊢ ((𝑥 ∈ 𝐼 ↦ (((𝐹‘𝑥) − (𝐺‘𝑥))↑2)) ∈ V → ((𝑥 ∈ 𝐼 ↦ (((𝐹‘𝑥) − (𝐺‘𝑥))↑2)) finSupp 0 ↔ ((𝑥 ∈ 𝐼 ↦ (((𝐹‘𝑥) − (𝐺‘𝑥))↑2)) supp 0) ∈ Fin))
41	36, 40	syl 17	. . . . . . . . 9 ⊢ (𝐼 ∈ 𝑉 → ((𝑥 ∈ 𝐼 ↦ (((𝐹‘𝑥) − (𝐺‘𝑥))↑2)) finSupp 0 ↔ ((𝑥 ∈ 𝐼 ↦ (((𝐹‘𝑥) − (𝐺‘𝑥))↑2)) supp 0) ∈ Fin))
42	41	3ad2ant1 1131	. . . . . . . 8 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) → ((𝑥 ∈ 𝐼 ↦ (((𝐹‘𝑥) − (𝐺‘𝑥))↑2)) finSupp 0 ↔ ((𝑥 ∈ 𝐼 ↦ (((𝐹‘𝑥) − (𝐺‘𝑥))↑2)) supp 0) ∈ Fin))
43	35, 42	mpbird 256	. . . . . . 7 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) → (𝑥 ∈ 𝐼 ↦ (((𝐹‘𝑥) − (𝐺‘𝑥))↑2)) finSupp 0)
44		simp1 1134	. . . . . . 7 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) → 𝐼 ∈ 𝑉)
45		regsumsupp 20855	. . . . . . 7 ⊢ (((𝑥 ∈ 𝐼 ↦ (((𝐹‘𝑥) − (𝐺‘𝑥))↑2)):𝐼⟶ℝ ∧ (𝑥 ∈ 𝐼 ↦ (((𝐹‘𝑥) − (𝐺‘𝑥))↑2)) finSupp 0 ∧ 𝐼 ∈ 𝑉) → (ℝ_fld Σ_g (𝑥 ∈ 𝐼 ↦ (((𝐹‘𝑥) − (𝐺‘𝑥))↑2))) = Σ𝑘 ∈ ((𝑥 ∈ 𝐼 ↦ (((𝐹‘𝑥) − (𝐺‘𝑥))↑2)) supp 0)((𝑥 ∈ 𝐼 ↦ (((𝐹‘𝑥) − (𝐺‘𝑥))↑2))‘𝑘))
46	29, 43, 44, 45	syl3anc 1369	. . . . . 6 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) → (ℝ_fld Σ_g (𝑥 ∈ 𝐼 ↦ (((𝐹‘𝑥) − (𝐺‘𝑥))↑2))) = Σ𝑘 ∈ ((𝑥 ∈ 𝐼 ↦ (((𝐹‘𝑥) − (𝐺‘𝑥))↑2)) supp 0)((𝑥 ∈ 𝐼 ↦ (((𝐹‘𝑥) − (𝐺‘𝑥))↑2))‘𝑘))
47		suppssdm 8013	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ 𝐼 ↦ (((𝐹‘𝑥) − (𝐺‘𝑥))↑2)) supp 0) ⊆ dom (𝑥 ∈ 𝐼 ↦ (((𝐹‘𝑥) − (𝐺‘𝑥))↑2))
48		eqid 2733	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ 𝐼 ↦ (((𝐹‘𝑥) − (𝐺‘𝑥))↑2)) = (𝑥 ∈ 𝐼 ↦ (((𝐹‘𝑥) − (𝐺‘𝑥))↑2))
49	48	dmmptss 6148	. . . . . . . . . . 11 ⊢ dom (𝑥 ∈ 𝐼 ↦ (((𝐹‘𝑥) − (𝐺‘𝑥))↑2)) ⊆ 𝐼
50	47, 49	sstri 3932	. . . . . . . . . 10 ⊢ ((𝑥 ∈ 𝐼 ↦ (((𝐹‘𝑥) − (𝐺‘𝑥))↑2)) supp 0) ⊆ 𝐼
51	50	a1i 11	. . . . . . . . 9 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) → ((𝑥 ∈ 𝐼 ↦ (((𝐹‘𝑥) − (𝐺‘𝑥))↑2)) supp 0) ⊆ 𝐼)
52	51	sselda 3923	. . . . . . . 8 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ 𝑘 ∈ ((𝑥 ∈ 𝐼 ↦ (((𝐹‘𝑥) − (𝐺‘𝑥))↑2)) supp 0)) → 𝑘 ∈ 𝐼)
53		eqidd 2734	. . . . . . . . . 10 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ 𝑘 ∈ 𝐼) → (𝑥 ∈ 𝐼 ↦ (((𝐹‘𝑥) − (𝐺‘𝑥))↑2)) = (𝑥 ∈ 𝐼 ↦ (((𝐹‘𝑥) − (𝐺‘𝑥))↑2)))
54		simpr 484	. . . . . . . . . . . . 13 ⊢ ((((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ 𝑘 ∈ 𝐼) ∧ 𝑥 = 𝑘) → 𝑥 = 𝑘)
55	54	fveq2d 6796	. . . . . . . . . . . 12 ⊢ ((((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ 𝑘 ∈ 𝐼) ∧ 𝑥 = 𝑘) → (𝐹‘𝑥) = (𝐹‘𝑘))
56	54	fveq2d 6796	. . . . . . . . . . . 12 ⊢ ((((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ 𝑘 ∈ 𝐼) ∧ 𝑥 = 𝑘) → (𝐺‘𝑥) = (𝐺‘𝑘))
57	55, 56	oveq12d 7313	. . . . . . . . . . 11 ⊢ ((((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ 𝑘 ∈ 𝐼) ∧ 𝑥 = 𝑘) → ((𝐹‘𝑥) − (𝐺‘𝑥)) = ((𝐹‘𝑘) − (𝐺‘𝑘)))
58	57	oveq1d 7310	. . . . . . . . . 10 ⊢ ((((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ 𝑘 ∈ 𝐼) ∧ 𝑥 = 𝑘) → (((𝐹‘𝑥) − (𝐺‘𝑥))↑2) = (((𝐹‘𝑘) − (𝐺‘𝑘))↑2))
59		simpr 484	. . . . . . . . . 10 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ 𝑘 ∈ 𝐼) → 𝑘 ∈ 𝐼)
60		ovexd 7330	. . . . . . . . . 10 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ 𝑘 ∈ 𝐼) → (((𝐹‘𝑘) − (𝐺‘𝑘))↑2) ∈ V)
61	53, 58, 59, 60	fvmptd 6902	. . . . . . . . 9 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ 𝑘 ∈ 𝐼) → ((𝑥 ∈ 𝐼 ↦ (((𝐹‘𝑥) − (𝐺‘𝑥))↑2))‘𝑘) = (((𝐹‘𝑘) − (𝐺‘𝑘))↑2))
62	61	eqcomd 2739	. . . . . . . 8 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ 𝑘 ∈ 𝐼) → (((𝐹‘𝑘) − (𝐺‘𝑘))↑2) = ((𝑥 ∈ 𝐼 ↦ (((𝐹‘𝑥) − (𝐺‘𝑥))↑2))‘𝑘))
63	52, 62	syldan 590	. . . . . . 7 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ 𝑘 ∈ ((𝑥 ∈ 𝐼 ↦ (((𝐹‘𝑥) − (𝐺‘𝑥))↑2)) supp 0)) → (((𝐹‘𝑘) − (𝐺‘𝑘))↑2) = ((𝑥 ∈ 𝐼 ↦ (((𝐹‘𝑥) − (𝐺‘𝑥))↑2))‘𝑘))
64	63	sumeq2dv 15443	. . . . . 6 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) → Σ𝑘 ∈ ((𝑥 ∈ 𝐼 ↦ (((𝐹‘𝑥) − (𝐺‘𝑥))↑2)) supp 0)(((𝐹‘𝑘) − (𝐺‘𝑘))↑2) = Σ𝑘 ∈ ((𝑥 ∈ 𝐼 ↦ (((𝐹‘𝑥) − (𝐺‘𝑥))↑2)) supp 0)((𝑥 ∈ 𝐼 ↦ (((𝐹‘𝑥) − (𝐺‘𝑥))↑2))‘𝑘))
65	46, 64	eqtr4d 2776	. . . . 5 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) → (ℝ_fld Σ_g (𝑥 ∈ 𝐼 ↦ (((𝐹‘𝑥) − (𝐺‘𝑥))↑2))) = Σ𝑘 ∈ ((𝑥 ∈ 𝐼 ↦ (((𝐹‘𝑥) − (𝐺‘𝑥))↑2)) supp 0)(((𝐹‘𝑘) − (𝐺‘𝑘))↑2))
66	65	adantr 480	. . . 4 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑓 = 𝐹 ∧ 𝑔 = 𝐺)) → (ℝ_fld Σ_g (𝑥 ∈ 𝐼 ↦ (((𝐹‘𝑥) − (𝐺‘𝑥))↑2))) = Σ𝑘 ∈ ((𝑥 ∈ 𝐼 ↦ (((𝐹‘𝑥) − (𝐺‘𝑥))↑2)) supp 0)(((𝐹‘𝑘) − (𝐺‘𝑘))↑2))
67	22	ffvelcdmda 6981	. . . . . . . . . 10 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ 𝑘 ∈ 𝐼) → (𝐹‘𝑘) ∈ ℝ)
68	67	recnd 11031	. . . . . . . . 9 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ 𝑘 ∈ 𝐼) → (𝐹‘𝑘) ∈ ℂ)
69	25	ffvelcdmda 6981	. . . . . . . . . 10 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ 𝑘 ∈ 𝐼) → (𝐺‘𝑘) ∈ ℝ)
70	69	recnd 11031	. . . . . . . . 9 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ 𝑘 ∈ 𝐼) → (𝐺‘𝑘) ∈ ℂ)
71	68, 70	subcld 11360	. . . . . . . 8 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ 𝑘 ∈ 𝐼) → ((𝐹‘𝑘) − (𝐺‘𝑘)) ∈ ℂ)
72	71	sqcld 13890	. . . . . . 7 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ 𝑘 ∈ 𝐼) → (((𝐹‘𝑘) − (𝐺‘𝑘))↑2) ∈ ℂ)
73	52, 72	syldan 590	. . . . . 6 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ 𝑘 ∈ ((𝑥 ∈ 𝐼 ↦ (((𝐹‘𝑥) − (𝐺‘𝑥))↑2)) supp 0)) → (((𝐹‘𝑘) − (𝐺‘𝑘))↑2) ∈ ℂ)
74	6, 21	rrxsuppss 24595	. . . . . . . . . . 11 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) → (𝐹 supp 0) ⊆ 𝐼)
75	6, 24	rrxsuppss 24595	. . . . . . . . . . 11 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) → (𝐺 supp 0) ⊆ 𝐼)
76	74, 75	unssd 4123	. . . . . . . . . 10 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) → ((𝐹 supp 0) ∪ (𝐺 supp 0)) ⊆ 𝐼)
77	76	ssdifssd 4080	. . . . . . . . 9 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) → (((𝐹 supp 0) ∪ (𝐺 supp 0)) ∖ ((𝑥 ∈ 𝐼 ↦ (((𝐹‘𝑥) − (𝐺‘𝑥))↑2)) supp 0)) ⊆ 𝐼)
78	77	sselda 3923	. . . . . . . 8 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ 𝑘 ∈ (((𝐹 supp 0) ∪ (𝐺 supp 0)) ∖ ((𝑥 ∈ 𝐼 ↦ (((𝐹‘𝑥) − (𝐺‘𝑥))↑2)) supp 0))) → 𝑘 ∈ 𝐼)
79	78, 62	syldan 590	. . . . . . 7 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ 𝑘 ∈ (((𝐹 supp 0) ∪ (𝐺 supp 0)) ∖ ((𝑥 ∈ 𝐼 ↦ (((𝐹‘𝑥) − (𝐺‘𝑥))↑2)) supp 0))) → (((𝐹‘𝑘) − (𝐺‘𝑘))↑2) = ((𝑥 ∈ 𝐼 ↦ (((𝐹‘𝑥) − (𝐺‘𝑥))↑2))‘𝑘))
80	76	ssdifd 4078	. . . . . . . . 9 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) → (((𝐹 supp 0) ∪ (𝐺 supp 0)) ∖ ((𝑥 ∈ 𝐼 ↦ (((𝐹‘𝑥) − (𝐺‘𝑥))↑2)) supp 0)) ⊆ (𝐼 ∖ ((𝑥 ∈ 𝐼 ↦ (((𝐹‘𝑥) − (𝐺‘𝑥))↑2)) supp 0)))
81	80	sselda 3923	. . . . . . . 8 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ 𝑘 ∈ (((𝐹 supp 0) ∪ (𝐺 supp 0)) ∖ ((𝑥 ∈ 𝐼 ↦ (((𝐹‘𝑥) − (𝐺‘𝑥))↑2)) supp 0))) → 𝑘 ∈ (𝐼 ∖ ((𝑥 ∈ 𝐼 ↦ (((𝐹‘𝑥) − (𝐺‘𝑥))↑2)) supp 0)))
82		ssidd 3946	. . . . . . . . 9 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) → ((𝑥 ∈ 𝐼 ↦ (((𝐹‘𝑥) − (𝐺‘𝑥))↑2)) supp 0) ⊆ ((𝑥 ∈ 𝐼 ↦ (((𝐹‘𝑥) − (𝐺‘𝑥))↑2)) supp 0))
83		0cnd 10996	. . . . . . . . 9 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) → 0 ∈ ℂ)
84	29, 82, 44, 83	suppssr 8032	. . . . . . . 8 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ 𝑘 ∈ (𝐼 ∖ ((𝑥 ∈ 𝐼 ↦ (((𝐹‘𝑥) − (𝐺‘𝑥))↑2)) supp 0))) → ((𝑥 ∈ 𝐼 ↦ (((𝐹‘𝑥) − (𝐺‘𝑥))↑2))‘𝑘) = 0)
85	81, 84	syldan 590	. . . . . . 7 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ 𝑘 ∈ (((𝐹 supp 0) ∪ (𝐺 supp 0)) ∖ ((𝑥 ∈ 𝐼 ↦ (((𝐹‘𝑥) − (𝐺‘𝑥))↑2)) supp 0))) → ((𝑥 ∈ 𝐼 ↦ (((𝐹‘𝑥) − (𝐺‘𝑥))↑2))‘𝑘) = 0)
86	79, 85	eqtrd 2773	. . . . . 6 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ 𝑘 ∈ (((𝐹 supp 0) ∪ (𝐺 supp 0)) ∖ ((𝑥 ∈ 𝐼 ↦ (((𝐹‘𝑥) − (𝐺‘𝑥))↑2)) supp 0))) → (((𝐹‘𝑘) − (𝐺‘𝑘))↑2) = 0)
87	34, 73, 86, 33	fsumss 15465	. . . . 5 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) → Σ𝑘 ∈ ((𝑥 ∈ 𝐼 ↦ (((𝐹‘𝑥) − (𝐺‘𝑥))↑2)) supp 0)(((𝐹‘𝑘) − (𝐺‘𝑘))↑2) = Σ𝑘 ∈ ((𝐹 supp 0) ∪ (𝐺 supp 0))(((𝐹‘𝑘) − (𝐺‘𝑘))↑2))
88	87	adantr 480	. . . 4 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑓 = 𝐹 ∧ 𝑔 = 𝐺)) → Σ𝑘 ∈ ((𝑥 ∈ 𝐼 ↦ (((𝐹‘𝑥) − (𝐺‘𝑥))↑2)) supp 0)(((𝐹‘𝑘) − (𝐺‘𝑘))↑2) = Σ𝑘 ∈ ((𝐹 supp 0) ∪ (𝐺 supp 0))(((𝐹‘𝑘) − (𝐺‘𝑘))↑2))
89	20, 66, 88	3eqtrd 2777	. . 3 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑓 = 𝐹 ∧ 𝑔 = 𝐺)) → (ℝ_fld Σ_g (𝑥 ∈ 𝐼 ↦ (((𝑓‘𝑥) − (𝑔‘𝑥))↑2))) = Σ𝑘 ∈ ((𝐹 supp 0) ∪ (𝐺 supp 0))(((𝐹‘𝑘) − (𝐺‘𝑘))↑2))
90	89	fveq2d 6796	. 2 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑓 = 𝐹 ∧ 𝑔 = 𝐺)) → (√‘(ℝ_fld Σ_g (𝑥 ∈ 𝐼 ↦ (((𝑓‘𝑥) − (𝑔‘𝑥))↑2)))) = (√‘Σ𝑘 ∈ ((𝐹 supp 0) ∪ (𝐺 supp 0))(((𝐹‘𝑘) − (𝐺‘𝑘))↑2)))
91		fvexd 6807	. 2 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) → (√‘Σ𝑘 ∈ ((𝐹 supp 0) ∪ (𝐺 supp 0))(((𝐹‘𝑘) − (𝐺‘𝑘))↑2)) ∈ V)
92	12, 90, 21, 24, 91	ovmpod 7445	1 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) → (𝐹𝐷𝐺) = (√‘Σ𝑘 ∈ ((𝐹 supp 0) ∪ (𝐺 supp 0))(((𝐹‘𝑘) − (𝐺‘𝑘))↑2)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 395 ∧ w3a 1085 = wceq 1537 ∈ wcel 2101 {crab 3221 Vcvv 3434 ∖ cdif 3886 ∪ cun 3887 ⊆ wss 3889 class class class wbr 5077 ↦ cmpt 5160 dom cdm 5591 Fun wfun 6441 ⟶wf 6443 ‘cfv 6447 (class class class)co 7295 ∈ cmpo 7297 supp csupp 7997 ↑_m cmap 8635 Fincfn 8753 finSupp cfsupp 9156 ℂcc 10897 ℝcr 10898 0cc0 10899 − cmin 11233 2c2 12056 ↑cexp 13810 √csqrt 14972 Σcsu 15425 Basecbs 16940 distcds 16999 Σ_g cgsu 17179 ℝ_fldcrefld 20837 ℝ^crrx 24575

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1793 ax-4 1807 ax-5 1909 ax-6 1967 ax-7 2007 ax-8 2103 ax-9 2111 ax-10 2132 ax-11 2149 ax-12 2166 ax-ext 2704 ax-rep 5212 ax-sep 5226 ax-nul 5233 ax-pow 5291 ax-pr 5355 ax-un 7608 ax-inf2 9427 ax-cnex 10955 ax-resscn 10956 ax-1cn 10957 ax-icn 10958 ax-addcl 10959 ax-addrcl 10960 ax-mulcl 10961 ax-mulrcl 10962 ax-mulcom 10963 ax-addass 10964 ax-mulass 10965 ax-distr 10966 ax-i2m1 10967 ax-1ne0 10968 ax-1rid 10969 ax-rnegex 10970 ax-rrecex 10971 ax-cnre 10972 ax-pre-lttri 10973 ax-pre-lttrn 10974 ax-pre-ltadd 10975 ax-pre-mulgt0 10976 ax-pre-sup 10977 ax-addf 10978 ax-mulf 10979

This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3or 1086 df-3an 1087 df-tru 1540 df-fal 1550 df-ex 1778 df-nf 1782 df-sb 2063 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2884 df-ne 2939 df-nel 3045 df-ral 3060 df-rex 3069 df-rmo 3222 df-reu 3223 df-rab 3224 df-v 3436 df-sbc 3719 df-csb 3835 df-dif 3892 df-un 3894 df-in 3896 df-ss 3906 df-pss 3908 df-nul 4260 df-if 4463 df-pw 4538 df-sn 4565 df-pr 4567 df-tp 4569 df-op 4571 df-uni 4842 df-int 4883 df-iun 4929 df-br 5078 df-opab 5140 df-mpt 5161 df-tr 5195 df-id 5491 df-eprel 5497 df-po 5505 df-so 5506 df-fr 5546 df-se 5547 df-we 5548 df-xp 5597 df-rel 5598 df-cnv 5599 df-co 5600 df-dm 5601 df-rn 5602 df-res 5603 df-ima 5604 df-pred 6206 df-ord 6273 df-on 6274 df-lim 6275 df-suc 6276 df-iota 6399 df-fun 6449 df-fn 6450 df-f 6451 df-f1 6452 df-fo 6453 df-f1o 6454 df-fv 6455 df-isom 6456 df-riota 7252 df-ov 7298 df-oprab 7299 df-mpo 7300 df-of 7553 df-om 7733 df-1st 7851 df-2nd 7852 df-supp 7998 df-tpos 8062 df-frecs 8117 df-wrecs 8148 df-recs 8222 df-rdg 8261 df-1o 8317 df-er 8518 df-map 8637 df-ixp 8706 df-en 8754 df-dom 8755 df-sdom 8756 df-fin 8757 df-fsupp 9157 df-sup 9229 df-oi 9297 df-card 9725 df-pnf 11039 df-mnf 11040 df-xr 11041 df-ltxr 11042 df-le 11043 df-sub 11235 df-neg 11236 df-div 11661 df-nn 12002 df-2 12064 df-3 12065 df-4 12066 df-5 12067 df-6 12068 df-7 12069 df-8 12070 df-9 12071 df-n0 12262 df-z 12348 df-dec 12466 df-uz 12611 df-rp 12759 df-fz 13268 df-fzo 13411 df-seq 13750 df-exp 13811 df-hash 14073 df-cj 14838 df-re 14839 df-im 14840 df-sqrt 14974 df-abs 14975 df-clim 15225 df-sum 15426 df-struct 16876 df-sets 16893 df-slot 16911 df-ndx 16923 df-base 16941 df-ress 16970 df-plusg 17003 df-mulr 17004 df-starv 17005 df-sca 17006 df-vsca 17007 df-ip 17008 df-tset 17009 df-ple 17010 df-ds 17012 df-unif 17013 df-hom 17014 df-cco 17015 df-0g 17180 df-gsum 17181 df-prds 17186 df-pws 17188 df-mgm 18354 df-sgrp 18403 df-mnd 18414 df-mhm 18458 df-grp 18608 df-minusg 18609 df-sbg 18610 df-subg 18780 df-ghm 18860 df-cntz 18951 df-cmn 19416 df-abl 19417 df-mgp 19749 df-ur 19766 df-ring 19813 df-cring 19814 df-oppr 19890 df-dvdsr 19911 df-unit 19912 df-invr 19942 df-dvr 19953 df-rnghom 19987 df-drng 20021 df-field 20022 df-subrg 20050 df-staf 20133 df-srng 20134 df-lmod 20153 df-lss 20222 df-sra 20462 df-rgmod 20463 df-cnfld 20626 df-refld 20838 df-dsmm 20967 df-frlm 20982 df-nm 23766 df-tng 23768 df-tcph 24361 df-rrx 24577

This theorem is referenced by: rrxmfval 24598 rrxmet 24600 rrxdstprj1 24601

W3C validator