rrxds - Metamath Proof Explorer

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

Theorem rrxds 22989

Description: The distance over generalized Euclidean spaces. Compare with df-rrn 32795. (Contributed by Thierry Arnoux, 20-Jun-2019.) (Proof shortened by AV, 20-Jul-2019.)

**Hypotheses**
Ref	Expression
rrxval.r	⊢ 𝐻 = (ℝ^‘𝐼)
rrxbase.b	⊢ 𝐵 = (Base‘𝐻)

**Assertion**
Ref	Expression
rrxds	⊢ (𝐼 ∈ 𝑉 → (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (√‘(ℝ_fld Σ_g (𝑥 ∈ 𝐼 ↦ (((𝑓‘𝑥) − (𝑔‘𝑥))↑2))))) = (dist‘𝐻))

Distinct variable groups: 𝑓,𝑔,𝑥,𝐵 𝑓,𝐼,𝑔,𝑥 𝑓,𝑉,𝑔,𝑥 Allowed substitution hints: 𝐻(𝑥,𝑓,𝑔)

Proof of Theorem rrxds Dummy variable ℎ is distinct from all other variables.

Step	Hyp	Ref	Expression
1		rrxval.r	. . . 4 ⊢ 𝐻 = (ℝ^‘𝐼)
2	1	rrxval 22983	. . 3 ⊢ (𝐼 ∈ 𝑉 → 𝐻 = (toℂHil‘(ℝ_fld freeLMod 𝐼)))
3	2	fveq2d 6107	. 2 ⊢ (𝐼 ∈ 𝑉 → (dist‘𝐻) = (dist‘(toℂHil‘(ℝ_fld freeLMod 𝐼))))
4		recrng 19786	. . . . 5 ⊢ ℝ_fld ∈ *-Ring
5		srngring 18675	. . . . 5 ⊢ (ℝ_fld ∈ *-Ring → ℝ_fld ∈ Ring)
6	4, 5	ax-mp 5	. . . 4 ⊢ ℝ_fld ∈ Ring
7		eqid 2610	. . . . 5 ⊢ (ℝ_fld freeLMod 𝐼) = (ℝ_fld freeLMod 𝐼)
8	7	frlmlmod 19912	. . . 4 ⊢ ((ℝ_fld ∈ Ring ∧ 𝐼 ∈ 𝑉) → (ℝ_fld freeLMod 𝐼) ∈ LMod)
9	6, 8	mpan 702	. . 3 ⊢ (𝐼 ∈ 𝑉 → (ℝ_fld freeLMod 𝐼) ∈ LMod)
10		lmodgrp 18693	. . 3 ⊢ ((ℝ_fld freeLMod 𝐼) ∈ LMod → (ℝ_fld freeLMod 𝐼) ∈ Grp)
11		eqid 2610	. . . 4 ⊢ (toℂHil‘(ℝ_fld freeLMod 𝐼)) = (toℂHil‘(ℝ_fld freeLMod 𝐼))
12		eqid 2610	. . . 4 ⊢ (norm‘(toℂHil‘(ℝ_fld freeLMod 𝐼))) = (norm‘(toℂHil‘(ℝ_fld freeLMod 𝐼)))
13		eqid 2610	. . . 4 ⊢ (-_g‘(ℝ_fld freeLMod 𝐼)) = (-_g‘(ℝ_fld freeLMod 𝐼))
14	11, 12, 13	tchds 22838	. . 3 ⊢ ((ℝ_fld freeLMod 𝐼) ∈ Grp → ((norm‘(toℂHil‘(ℝ_fld freeLMod 𝐼))) ∘ (-_g‘(ℝ_fld freeLMod 𝐼))) = (dist‘(toℂHil‘(ℝ_fld freeLMod 𝐼))))
15	9, 10, 14	3syl 18	. 2 ⊢ (𝐼 ∈ 𝑉 → ((norm‘(toℂHil‘(ℝ_fld freeLMod 𝐼))) ∘ (-_g‘(ℝ_fld freeLMod 𝐼))) = (dist‘(toℂHil‘(ℝ_fld freeLMod 𝐼))))
16		eqid 2610	. . . . . . . 8 ⊢ (Base‘(ℝ_fld freeLMod 𝐼)) = (Base‘(ℝ_fld freeLMod 𝐼))
17	16, 13	grpsubf 17317	. . . . . . 7 ⊢ ((ℝ_fld freeLMod 𝐼) ∈ Grp → (-_g‘(ℝ_fld freeLMod 𝐼)):((Base‘(ℝ_fld freeLMod 𝐼)) × (Base‘(ℝ_fld freeLMod 𝐼)))⟶(Base‘(ℝ_fld freeLMod 𝐼)))
18	9, 10, 17	3syl 18	. . . . . 6 ⊢ (𝐼 ∈ 𝑉 → (-_g‘(ℝ_fld freeLMod 𝐼)):((Base‘(ℝ_fld freeLMod 𝐼)) × (Base‘(ℝ_fld freeLMod 𝐼)))⟶(Base‘(ℝ_fld freeLMod 𝐼)))
19		rrxbase.b	. . . . . . . . . 10 ⊢ 𝐵 = (Base‘𝐻)
20	1, 19	rrxbase 22984	. . . . . . . . 9 ⊢ (𝐼 ∈ 𝑉 → 𝐵 = {ℎ ∈ (ℝ ↑_𝑚 𝐼) ∣ ℎ finSupp 0})
21		rebase 19771	. . . . . . . . . . 11 ⊢ ℝ = (Base‘ℝ_fld)
22		re0g 19777	. . . . . . . . . . 11 ⊢ 0 = (0_g‘ℝ_fld)
23		eqid 2610	. . . . . . . . . . 11 ⊢ {ℎ ∈ (ℝ ↑_𝑚 𝐼) ∣ ℎ finSupp 0} = {ℎ ∈ (ℝ ↑_𝑚 𝐼) ∣ ℎ finSupp 0}
24	7, 21, 22, 23	frlmbas 19918	. . . . . . . . . 10 ⊢ ((ℝ_fld ∈ Ring ∧ 𝐼 ∈ 𝑉) → {ℎ ∈ (ℝ ↑_𝑚 𝐼) ∣ ℎ finSupp 0} = (Base‘(ℝ_fld freeLMod 𝐼)))
25	6, 24	mpan 702	. . . . . . . . 9 ⊢ (𝐼 ∈ 𝑉 → {ℎ ∈ (ℝ ↑_𝑚 𝐼) ∣ ℎ finSupp 0} = (Base‘(ℝ_fld freeLMod 𝐼)))
26	20, 25	eqtrd 2644	. . . . . . . 8 ⊢ (𝐼 ∈ 𝑉 → 𝐵 = (Base‘(ℝ_fld freeLMod 𝐼)))
27	26	sqxpeqd 5065	. . . . . . 7 ⊢ (𝐼 ∈ 𝑉 → (𝐵 × 𝐵) = ((Base‘(ℝ_fld freeLMod 𝐼)) × (Base‘(ℝ_fld freeLMod 𝐼))))
28	27, 26	feq23d 5953	. . . . . 6 ⊢ (𝐼 ∈ 𝑉 → ((-_g‘(ℝ_fld freeLMod 𝐼)):(𝐵 × 𝐵)⟶𝐵 ↔ (-_g‘(ℝ_fld freeLMod 𝐼)):((Base‘(ℝ_fld freeLMod 𝐼)) × (Base‘(ℝ_fld freeLMod 𝐼)))⟶(Base‘(ℝ_fld freeLMod 𝐼))))
29	18, 28	mpbird 246	. . . . 5 ⊢ (𝐼 ∈ 𝑉 → (-_g‘(ℝ_fld freeLMod 𝐼)):(𝐵 × 𝐵)⟶𝐵)
30	29	fovrnda 6703	. . . 4 ⊢ ((𝐼 ∈ 𝑉 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (𝑓(-_g‘(ℝ_fld freeLMod 𝐼))𝑔) ∈ 𝐵)
31		ffn 5958	. . . . . 6 ⊢ ((-_g‘(ℝ_fld freeLMod 𝐼)):(𝐵 × 𝐵)⟶𝐵 → (-_g‘(ℝ_fld freeLMod 𝐼)) Fn (𝐵 × 𝐵))
32	29, 31	syl 17	. . . . 5 ⊢ (𝐼 ∈ 𝑉 → (-_g‘(ℝ_fld freeLMod 𝐼)) Fn (𝐵 × 𝐵))
33		fnov 6666	. . . . 5 ⊢ ((-_g‘(ℝ_fld freeLMod 𝐼)) Fn (𝐵 × 𝐵) ↔ (-_g‘(ℝ_fld freeLMod 𝐼)) = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑓(-_g‘(ℝ_fld freeLMod 𝐼))𝑔)))
34	32, 33	sylib 207	. . . 4 ⊢ (𝐼 ∈ 𝑉 → (-_g‘(ℝ_fld freeLMod 𝐼)) = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑓(-_g‘(ℝ_fld freeLMod 𝐼))𝑔)))
35	1, 19	rrxnm 22987	. . . . 5 ⊢ (𝐼 ∈ 𝑉 → (ℎ ∈ 𝐵 ↦ (√‘(ℝ_fld Σ_g (𝑥 ∈ 𝐼 ↦ ((ℎ‘𝑥)↑2))))) = (norm‘𝐻))
36	2	fveq2d 6107	. . . . 5 ⊢ (𝐼 ∈ 𝑉 → (norm‘𝐻) = (norm‘(toℂHil‘(ℝ_fld freeLMod 𝐼))))
37	35, 36	eqtr2d 2645	. . . 4 ⊢ (𝐼 ∈ 𝑉 → (norm‘(toℂHil‘(ℝ_fld freeLMod 𝐼))) = (ℎ ∈ 𝐵 ↦ (√‘(ℝ_fld Σ_g (𝑥 ∈ 𝐼 ↦ ((ℎ‘𝑥)↑2))))))
38		fveq1 6102	. . . . . . . 8 ⊢ (ℎ = (𝑓(-_g‘(ℝ_fld freeLMod 𝐼))𝑔) → (ℎ‘𝑥) = ((𝑓(-_g‘(ℝ_fld freeLMod 𝐼))𝑔)‘𝑥))
39	38	oveq1d 6564	. . . . . . 7 ⊢ (ℎ = (𝑓(-_g‘(ℝ_fld freeLMod 𝐼))𝑔) → ((ℎ‘𝑥)↑2) = (((𝑓(-_g‘(ℝ_fld freeLMod 𝐼))𝑔)‘𝑥)↑2))
40	39	mpteq2dv 4673	. . . . . 6 ⊢ (ℎ = (𝑓(-_g‘(ℝ_fld freeLMod 𝐼))𝑔) → (𝑥 ∈ 𝐼 ↦ ((ℎ‘𝑥)↑2)) = (𝑥 ∈ 𝐼 ↦ (((𝑓(-_g‘(ℝ_fld freeLMod 𝐼))𝑔)‘𝑥)↑2)))
41	40	oveq2d 6565	. . . . 5 ⊢ (ℎ = (𝑓(-_g‘(ℝ_fld freeLMod 𝐼))𝑔) → (ℝ_fld Σ_g (𝑥 ∈ 𝐼 ↦ ((ℎ‘𝑥)↑2))) = (ℝ_fld Σ_g (𝑥 ∈ 𝐼 ↦ (((𝑓(-_g‘(ℝ_fld freeLMod 𝐼))𝑔)‘𝑥)↑2))))
42	41	fveq2d 6107	. . . 4 ⊢ (ℎ = (𝑓(-_g‘(ℝ_fld freeLMod 𝐼))𝑔) → (√‘(ℝ_fld Σ_g (𝑥 ∈ 𝐼 ↦ ((ℎ‘𝑥)↑2)))) = (√‘(ℝ_fld Σ_g (𝑥 ∈ 𝐼 ↦ (((𝑓(-_g‘(ℝ_fld freeLMod 𝐼))𝑔)‘𝑥)↑2)))))
43	30, 34, 37, 42	fmpt2co 7147	. . 3 ⊢ (𝐼 ∈ 𝑉 → ((norm‘(toℂHil‘(ℝ_fld freeLMod 𝐼))) ∘ (-_g‘(ℝ_fld freeLMod 𝐼))) = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (√‘(ℝ_fld Σ_g (𝑥 ∈ 𝐼 ↦ (((𝑓(-_g‘(ℝ_fld freeLMod 𝐼))𝑔)‘𝑥)↑2))))))
44		simp1 1054	. . . . . . . . . . . . . 14 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) → 𝐼 ∈ 𝑉)
45		simprl 790	. . . . . . . . . . . . . . . 16 ⊢ ((𝐼 ∈ 𝑉 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → 𝑓 ∈ 𝐵)
46	26	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝐼 ∈ 𝑉 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → 𝐵 = (Base‘(ℝ_fld freeLMod 𝐼)))
47	45, 46	eleqtrd 2690	. . . . . . . . . . . . . . 15 ⊢ ((𝐼 ∈ 𝑉 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)))
48	47	3impb 1252	. . . . . . . . . . . . . 14 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) → 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)))
49	7, 21, 16	frlmbasmap 19922	. . . . . . . . . . . . . 14 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) → 𝑓 ∈ (ℝ ↑_𝑚 𝐼))
50	44, 48, 49	syl2anc 691	. . . . . . . . . . . . 13 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) → 𝑓 ∈ (ℝ ↑_𝑚 𝐼))
51		elmapi 7765	. . . . . . . . . . . . 13 ⊢ (𝑓 ∈ (ℝ ↑_𝑚 𝐼) → 𝑓:𝐼⟶ℝ)
52	50, 51	syl 17	. . . . . . . . . . . 12 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) → 𝑓:𝐼⟶ℝ)
53		ffn 5958	. . . . . . . . . . . 12 ⊢ (𝑓:𝐼⟶ℝ → 𝑓 Fn 𝐼)
54	52, 53	syl 17	. . . . . . . . . . 11 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) → 𝑓 Fn 𝐼)
55		simprr 792	. . . . . . . . . . . . . . . 16 ⊢ ((𝐼 ∈ 𝑉 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → 𝑔 ∈ 𝐵)
56	55, 46	eleqtrd 2690	. . . . . . . . . . . . . . 15 ⊢ ((𝐼 ∈ 𝑉 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → 𝑔 ∈ (Base‘(ℝ_fld freeLMod 𝐼)))
57	56	3impb 1252	. . . . . . . . . . . . . 14 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) → 𝑔 ∈ (Base‘(ℝ_fld freeLMod 𝐼)))
58	7, 21, 16	frlmbasmap 19922	. . . . . . . . . . . . . 14 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑔 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) → 𝑔 ∈ (ℝ ↑_𝑚 𝐼))
59	44, 57, 58	syl2anc 691	. . . . . . . . . . . . 13 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) → 𝑔 ∈ (ℝ ↑_𝑚 𝐼))
60		elmapi 7765	. . . . . . . . . . . . 13 ⊢ (𝑔 ∈ (ℝ ↑_𝑚 𝐼) → 𝑔:𝐼⟶ℝ)
61	59, 60	syl 17	. . . . . . . . . . . 12 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) → 𝑔:𝐼⟶ℝ)
62		ffn 5958	. . . . . . . . . . . 12 ⊢ (𝑔:𝐼⟶ℝ → 𝑔 Fn 𝐼)
63	61, 62	syl 17	. . . . . . . . . . 11 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) → 𝑔 Fn 𝐼)
64		inidm 3784	. . . . . . . . . . 11 ⊢ (𝐼 ∩ 𝐼) = 𝐼
65		eqidd 2611	. . . . . . . . . . 11 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) ∧ 𝑥 ∈ 𝐼) → (𝑓‘𝑥) = (𝑓‘𝑥))
66		eqidd 2611	. . . . . . . . . . 11 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) ∧ 𝑥 ∈ 𝐼) → (𝑔‘𝑥) = (𝑔‘𝑥))
67	54, 63, 44, 44, 64, 65, 66	offval 6802	. . . . . . . . . 10 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) → (𝑓 ∘_𝑓 (-_g‘ℝ_fld)𝑔) = (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(-_g‘ℝ_fld)(𝑔‘𝑥))))
68	6	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝐼 ∈ 𝑉 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → ℝ_fld ∈ Ring)
69		simpl 472	. . . . . . . . . . . 12 ⊢ ((𝐼 ∈ 𝑉 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → 𝐼 ∈ 𝑉)
70		eqid 2610	. . . . . . . . . . . 12 ⊢ (-_g‘ℝ_fld) = (-_g‘ℝ_fld)
71	7, 16, 68, 69, 47, 56, 70, 13	frlmsubgval 19927	. . . . . . . . . . 11 ⊢ ((𝐼 ∈ 𝑉 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (𝑓(-_g‘(ℝ_fld freeLMod 𝐼))𝑔) = (𝑓 ∘_𝑓 (-_g‘ℝ_fld)𝑔))
72	71	3impb 1252	. . . . . . . . . 10 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) → (𝑓(-_g‘(ℝ_fld freeLMod 𝐼))𝑔) = (𝑓 ∘_𝑓 (-_g‘ℝ_fld)𝑔))
73	52	ffvelrnda 6267	. . . . . . . . . . . 12 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) ∧ 𝑥 ∈ 𝐼) → (𝑓‘𝑥) ∈ ℝ)
74	61	ffvelrnda 6267	. . . . . . . . . . . 12 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) ∧ 𝑥 ∈ 𝐼) → (𝑔‘𝑥) ∈ ℝ)
75	70	resubgval 19774	. . . . . . . . . . . 12 ⊢ (((𝑓‘𝑥) ∈ ℝ ∧ (𝑔‘𝑥) ∈ ℝ) → ((𝑓‘𝑥) − (𝑔‘𝑥)) = ((𝑓‘𝑥)(-_g‘ℝ_fld)(𝑔‘𝑥)))
76	73, 74, 75	syl2anc 691	. . . . . . . . . . 11 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) ∧ 𝑥 ∈ 𝐼) → ((𝑓‘𝑥) − (𝑔‘𝑥)) = ((𝑓‘𝑥)(-_g‘ℝ_fld)(𝑔‘𝑥)))
77	76	mpteq2dva 4672	. . . . . . . . . 10 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) → (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥) − (𝑔‘𝑥))) = (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(-_g‘ℝ_fld)(𝑔‘𝑥))))
78	67, 72, 77	3eqtr4d 2654	. . . . . . . . 9 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) → (𝑓(-_g‘(ℝ_fld freeLMod 𝐼))𝑔) = (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥) − (𝑔‘𝑥))))
79	73, 74	resubcld 10337	. . . . . . . . 9 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) ∧ 𝑥 ∈ 𝐼) → ((𝑓‘𝑥) − (𝑔‘𝑥)) ∈ ℝ)
80	78, 79	fvmpt2d 6202	. . . . . . . 8 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) ∧ 𝑥 ∈ 𝐼) → ((𝑓(-_g‘(ℝ_fld freeLMod 𝐼))𝑔)‘𝑥) = ((𝑓‘𝑥) − (𝑔‘𝑥)))
81	80	oveq1d 6564	. . . . . . 7 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) ∧ 𝑥 ∈ 𝐼) → (((𝑓(-_g‘(ℝ_fld freeLMod 𝐼))𝑔)‘𝑥)↑2) = (((𝑓‘𝑥) − (𝑔‘𝑥))↑2))
82	81	mpteq2dva 4672	. . . . . 6 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) → (𝑥 ∈ 𝐼 ↦ (((𝑓(-_g‘(ℝ_fld freeLMod 𝐼))𝑔)‘𝑥)↑2)) = (𝑥 ∈ 𝐼 ↦ (((𝑓‘𝑥) − (𝑔‘𝑥))↑2)))
83	82	oveq2d 6565	. . . . 5 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) → (ℝ_fld Σ_g (𝑥 ∈ 𝐼 ↦ (((𝑓(-_g‘(ℝ_fld freeLMod 𝐼))𝑔)‘𝑥)↑2))) = (ℝ_fld Σ_g (𝑥 ∈ 𝐼 ↦ (((𝑓‘𝑥) − (𝑔‘𝑥))↑2))))
84	83	fveq2d 6107	. . . 4 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) → (√‘(ℝ_fld Σ_g (𝑥 ∈ 𝐼 ↦ (((𝑓(-_g‘(ℝ_fld freeLMod 𝐼))𝑔)‘𝑥)↑2)))) = (√‘(ℝ_fld Σ_g (𝑥 ∈ 𝐼 ↦ (((𝑓‘𝑥) − (𝑔‘𝑥))↑2)))))
85	84	mpt2eq3dva 6617	. . 3 ⊢ (𝐼 ∈ 𝑉 → (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (√‘(ℝ_fld Σ_g (𝑥 ∈ 𝐼 ↦ (((𝑓(-_g‘(ℝ_fld freeLMod 𝐼))𝑔)‘𝑥)↑2))))) = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (√‘(ℝ_fld Σ_g (𝑥 ∈ 𝐼 ↦ (((𝑓‘𝑥) − (𝑔‘𝑥))↑2))))))
86	43, 85	eqtrd 2644	. 2 ⊢ (𝐼 ∈ 𝑉 → ((norm‘(toℂHil‘(ℝ_fld freeLMod 𝐼))) ∘ (-_g‘(ℝ_fld freeLMod 𝐼))) = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (√‘(ℝ_fld Σ_g (𝑥 ∈ 𝐼 ↦ (((𝑓‘𝑥) − (𝑔‘𝑥))↑2))))))
87	3, 15, 86	3eqtr2rd 2651	1 ⊢ (𝐼 ∈ 𝑉 → (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (√‘(ℝ_fld Σ_g (𝑥 ∈ 𝐼 ↦ (((𝑓‘𝑥) − (𝑔‘𝑥))↑2))))) = (dist‘𝐻))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 383 ∧ w3a 1031 = wceq 1475 ∈ wcel 1977 {crab 2900 class class class wbr 4583 ↦ cmpt 4643 × cxp 5036 ∘ ccom 5042 Fn wfn 5799 ⟶wf 5800 ‘cfv 5804 (class class class)co 6549 ↦ cmpt2 6551 ∘_𝑓 cof 6793 ↑_𝑚 cmap 7744 finSupp cfsupp 8158 ℝcr 9814 0cc0 9815 − cmin 10145 2c2 10947 ↑cexp 12722 √csqrt 13821 Basecbs 15695 distcds 15777 Σ_g cgsu 15924 Grpcgrp 17245 -_gcsg 17247 Ringcrg 18370 *-Ringcsr 18667 LModclmod 18686 ℝ_fldcrefld 19769 freeLMod cfrlm 19909 normcnm 22191 toℂHilctch 22775 ℝ^crrx 22979

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-8 1979 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-rep 4699 ax-sep 4709 ax-nul 4717 ax-pow 4769 ax-pr 4833 ax-un 6847 ax-cnex 9871 ax-resscn 9872 ax-1cn 9873 ax-icn 9874 ax-addcl 9875 ax-addrcl 9876 ax-mulcl 9877 ax-mulrcl 9878 ax-mulcom 9879 ax-addass 9880 ax-mulass 9881 ax-distr 9882 ax-i2m1 9883 ax-1ne0 9884 ax-1rid 9885 ax-rnegex 9886 ax-rrecex 9887 ax-cnre 9888 ax-pre-lttri 9889 ax-pre-lttrn 9890 ax-pre-ltadd 9891 ax-pre-mulgt0 9892 ax-pre-sup 9893 ax-addf 9894 ax-mulf 9895

This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3or 1032 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-eu 2462 df-mo 2463 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ne 2782 df-nel 2783 df-ral 2901 df-rex 2902 df-reu 2903 df-rmo 2904 df-rab 2905 df-v 3175 df-sbc 3403 df-csb 3500 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-pss 3556 df-nul 3875 df-if 4037 df-pw 4110 df-sn 4126 df-pr 4128 df-tp 4130 df-op 4132 df-uni 4373 df-int 4411 df-iun 4457 df-br 4584 df-opab 4644 df-mpt 4645 df-tr 4681 df-eprel 4949 df-id 4953 df-po 4959 df-so 4960 df-fr 4997 df-we 4999 df-xp 5044 df-rel 5045 df-cnv 5046 df-co 5047 df-dm 5048 df-rn 5049 df-res 5050 df-ima 5051 df-pred 5597 df-ord 5643 df-on 5644 df-lim 5645 df-suc 5646 df-iota 5768 df-fun 5806 df-fn 5807 df-f 5808 df-f1 5809 df-fo 5810 df-f1o 5811 df-fv 5812 df-riota 6511 df-ov 6552 df-oprab 6553 df-mpt2 6554 df-of 6795 df-om 6958 df-1st 7059 df-2nd 7060 df-supp 7183 df-tpos 7239 df-wrecs 7294 df-recs 7355 df-rdg 7393 df-1o 7447 df-oadd 7451 df-er 7629 df-map 7746 df-ixp 7795 df-en 7842 df-dom 7843 df-sdom 7844 df-fin 7845 df-fsupp 8159 df-sup 8231 df-pnf 9955 df-mnf 9956 df-xr 9957 df-ltxr 9958 df-le 9959 df-sub 10147 df-neg 10148 df-div 10564 df-nn 10898 df-2 10956 df-3 10957 df-4 10958 df-5 10959 df-6 10960 df-7 10961 df-8 10962 df-9 10963 df-n0 11170 df-z 11255 df-dec 11370 df-uz 11564 df-rp 11709 df-fz 12198 df-seq 12664 df-exp 12723 df-cj 13687 df-re 13688 df-im 13689 df-sqrt 13823 df-abs 13824 df-struct 15697 df-ndx 15698 df-slot 15699 df-base 15700 df-sets 15701 df-ress 15702 df-plusg 15781 df-mulr 15782 df-starv 15783 df-sca 15784 df-vsca 15785 df-ip 15786 df-tset 15787 df-ple 15788 df-ds 15791 df-unif 15792 df-hom 15793 df-cco 15794 df-0g 15925 df-prds 15931 df-pws 15933 df-mgm 17065 df-sgrp 17107 df-mnd 17118 df-mhm 17158 df-grp 17248 df-minusg 17249 df-sbg 17250 df-subg 17414 df-ghm 17481 df-cmn 18018 df-mgp 18313 df-ur 18325 df-ring 18372 df-cring 18373 df-oppr 18446 df-dvdsr 18464 df-unit 18465 df-invr 18495 df-dvr 18506 df-rnghom 18538 df-drng 18572 df-field 18573 df-subrg 18601 df-staf 18668 df-srng 18669 df-lmod 18688 df-lss 18754 df-sra 18993 df-rgmod 18994 df-cnfld 19568 df-refld 19770 df-dsmm 19895 df-frlm 19910 df-nm 22197 df-tng 22199 df-tch 22777 df-rrx 22981

This theorem is referenced by: rrxmval 22996 rrxmfval 22997 rrxtopn 39177 rrxdsfi 39181

W3C validator