rrxnm

Description: The norm of the generalized real Euclidean spaces. (Contributed by Thierry Arnoux, 16-Jun-2019)

	Ref	Expression
Hypotheses	rrxval.r	$⊢ H = I$
	rrxbase.b	$⊢ B = {Base}_{H}$
Assertion	rrxnm	$⊢ I \in V \to (f \in B ⟼ \sqrt{\underset{x \in I}{\sum_{ℝ_{fld}}} {f (x)}^{2}}) = norm (H)$

Proof

Step	Hyp	Ref	Expression
1		rrxval.r	$⊢ H = I$
2		rrxbase.b	$⊢ B = {Base}_{H}$
3		recrng	$⊢ ℝ_{fld} \in *-Ring$
4		srngring	$⊢ ℝ_{fld} \in *-Ring \to ℝ_{fld} \in Ring$
5	3 4	ax-mp	$⊢ ℝ_{fld} \in Ring$
6		eqid	$⊢ ℝ_{fld} freeLMod I = ℝ_{fld} freeLMod I$
7	6	frlmlmod	$⊢ (ℝ_{fld} \in Ring \land I \in V) \to ℝ_{fld} freeLMod I \in LMod$
8	5 7	mpan	$⊢ I \in V \to ℝ_{fld} freeLMod I \in LMod$
9		lmodgrp	$⊢ ℝ_{fld} freeLMod I \in LMod \to ℝ_{fld} freeLMod I \in Grp$
10		eqid	$⊢ toCPreHil (ℝ_{fld} freeLMod I) = toCPreHil (ℝ_{fld} freeLMod I)$
11		eqid	$⊢ norm (toCPreHil (ℝ_{fld} freeLMod I)) = norm (toCPreHil (ℝ_{fld} freeLMod I))$
12		eqid	$⊢ {Base}_{(ℝ_{fld} freeLMod I)} = {Base}_{(ℝ_{fld} freeLMod I)}$
13		eqid	$⊢ \cdot_{𝑖} (ℝ_{fld} freeLMod I) = \cdot_{𝑖} (ℝ_{fld} freeLMod I)$
14	10 11 12 13	tchnmfval	$⊢ ℝ_{fld} freeLMod I \in Grp \to norm (toCPreHil (ℝ_{fld} freeLMod I)) = (f \in {Base}_{(ℝ_{fld} freeLMod I)} ⟼ \sqrt{f \cdot_{𝑖} (ℝ_{fld} freeLMod I) f})$
15	8 9 14	3syl	$⊢ I \in V \to norm (toCPreHil (ℝ_{fld} freeLMod I)) = (f \in {Base}_{(ℝ_{fld} freeLMod I)} ⟼ \sqrt{f \cdot_{𝑖} (ℝ_{fld} freeLMod I) f})$
16	1	rrxval	$⊢ I \in V \to H = toCPreHil (ℝ_{fld} freeLMod I)$
17	16	fveq2d	$⊢ I \in V \to norm (H) = norm (toCPreHil (ℝ_{fld} freeLMod I))$
18	16	fveq2d	$⊢ I \in V \to {Base}_{H} = {Base}_{toCPreHil (ℝ_{fld} freeLMod I)}$
19	10 12	tcphbas	$⊢ {Base}_{(ℝ_{fld} freeLMod I)} = {Base}_{toCPreHil (ℝ_{fld} freeLMod I)}$
20	18 2 19	3eqtr4g	$⊢ I \in V \to B = {Base}_{(ℝ_{fld} freeLMod I)}$
21	1 2	rrxbase	$⊢ I \in V \to B = \{f \in (ℝ^{I}) \| {finSupp}_{0} (f)\}$
22		ssrab2	$⊢ \{f \in (ℝ^{I}) \| {finSupp}_{0} (f)\} \subseteq ℝ^{I}$
23	21 22	eqsstrdi	$⊢ I \in V \to B \subseteq ℝ^{I}$
24	23	sselda	$⊢ (I \in V \land f \in B) \to f \in (ℝ^{I})$
25	16	fveq2d	$⊢ I \in V \to \cdot_{𝑖} (H) = \cdot_{𝑖} (toCPreHil (ℝ_{fld} freeLMod I))$
26	1 2	rrxip	$⊢ I \in V \to (h \in (ℝ^{I}), g \in (ℝ^{I}) ⟼ \underset{x \in I}{\sum_{ℝ_{fld}}} h (x) g (x)) = \cdot_{𝑖} (H)$
27	10 13	tcphip	$⊢ \cdot_{𝑖} (ℝ_{fld} freeLMod I) = \cdot_{𝑖} (toCPreHil (ℝ_{fld} freeLMod I))$
28	27	a1i	$⊢ I \in V \to \cdot_{𝑖} (ℝ_{fld} freeLMod I) = \cdot_{𝑖} (toCPreHil (ℝ_{fld} freeLMod I))$
29	25 26 28	3eqtr4rd	$⊢ I \in V \to \cdot_{𝑖} (ℝ_{fld} freeLMod I) = (h \in (ℝ^{I}), g \in (ℝ^{I}) ⟼ \underset{x \in I}{\sum_{ℝ_{fld}}} h (x) g (x))$
30	29	adantr	$⊢ (I \in V \land f \in (ℝ^{I})) \to \cdot_{𝑖} (ℝ_{fld} freeLMod I) = (h \in (ℝ^{I}), g \in (ℝ^{I}) ⟼ \underset{x \in I}{\sum_{ℝ_{fld}}} h (x) g (x))$
31		simprl	$⊢ ((I \in V \land f \in (ℝ^{I})) \land (h = f \land g = f)) \to h = f$
32	31	fveq1d	$⊢ ((I \in V \land f \in (ℝ^{I})) \land (h = f \land g = f)) \to h (x) = f (x)$
33		simprr	$⊢ ((I \in V \land f \in (ℝ^{I})) \land (h = f \land g = f)) \to g = f$
34	33	fveq1d	$⊢ ((I \in V \land f \in (ℝ^{I})) \land (h = f \land g = f)) \to g (x) = f (x)$
35	32 34	oveq12d	$⊢ ((I \in V \land f \in (ℝ^{I})) \land (h = f \land g = f)) \to h (x) g (x) = f (x) f (x)$
36	35	adantr	$⊢ (((I \in V \land f \in (ℝ^{I})) \land (h = f \land g = f)) \land x \in I) \to h (x) g (x) = f (x) f (x)$
37		elmapi	$⊢ f \in (ℝ^{I}) \to f : I ⟶ ℝ$
38	37	adantl	$⊢ (I \in V \land f \in (ℝ^{I})) \to f : I ⟶ ℝ$
39	38	ffvelrnda	$⊢ ((I \in V \land f \in (ℝ^{I})) \land x \in I) \to f (x) \in ℝ$
40	39	recnd	$⊢ ((I \in V \land f \in (ℝ^{I})) \land x \in I) \to f (x) \in ℂ$
41	40	adantlr	$⊢ (((I \in V \land f \in (ℝ^{I})) \land (h = f \land g = f)) \land x \in I) \to f (x) \in ℂ$
42	41	sqvald	$⊢ (((I \in V \land f \in (ℝ^{I})) \land (h = f \land g = f)) \land x \in I) \to {f (x)}^{2} = f (x) f (x)$
43	36 42	eqtr4d	$⊢ (((I \in V \land f \in (ℝ^{I})) \land (h = f \land g = f)) \land x \in I) \to h (x) g (x) = {f (x)}^{2}$
44	43	mpteq2dva	$⊢ ((I \in V \land f \in (ℝ^{I})) \land (h = f \land g = f)) \to (x \in I ⟼ h (x) g (x)) = (x \in I ⟼ {f (x)}^{2})$
45	44	oveq2d	$⊢ ((I \in V \land f \in (ℝ^{I})) \land (h = f \land g = f)) \to \underset{x \in I}{\sum_{ℝ_{fld}}} h (x) g (x) = \underset{x \in I}{\sum_{ℝ_{fld}}} {f (x)}^{2}$
46		simpr	$⊢ (I \in V \land f \in (ℝ^{I})) \to f \in (ℝ^{I})$
47		ovexd	$⊢ (I \in V \land f \in (ℝ^{I})) \to \underset{x \in I}{\sum_{ℝ_{fld}}} {f (x)}^{2} \in V$
48	30 45 46 46 47	ovmpod	$⊢ (I \in V \land f \in (ℝ^{I})) \to f \cdot_{𝑖} (ℝ_{fld} freeLMod I) f = \underset{x \in I}{\sum_{ℝ_{fld}}} {f (x)}^{2}$
49	24 48	syldan	$⊢ (I \in V \land f \in B) \to f \cdot_{𝑖} (ℝ_{fld} freeLMod I) f = \underset{x \in I}{\sum_{ℝ_{fld}}} {f (x)}^{2}$
50	49	eqcomd	$⊢ (I \in V \land f \in B) \to \underset{x \in I}{\sum_{ℝ_{fld}}} {f (x)}^{2} = f \cdot_{𝑖} (ℝ_{fld} freeLMod I) f$
51	50	fveq2d	$⊢ (I \in V \land f \in B) \to \sqrt{\underset{x \in I}{\sum_{ℝ_{fld}}} {f (x)}^{2}} = \sqrt{f \cdot_{𝑖} (ℝ_{fld} freeLMod I) f}$
52	20 51	mpteq12dva	$⊢ I \in V \to (f \in B ⟼ \sqrt{\underset{x \in I}{\sum_{ℝ_{fld}}} {f (x)}^{2}}) = (f \in {Base}_{(ℝ_{fld} freeLMod I)} ⟼ \sqrt{f \cdot_{𝑖} (ℝ_{fld} freeLMod I) f})$
53	15 17 52	3eqtr4rd	$⊢ I \in V \to (f \in B ⟼ \sqrt{\underset{x \in I}{\sum_{ℝ_{fld}}} {f (x)}^{2}}) = norm (H)$

Metamath Proof Explorer

Theorem rrxnm

Proof