rrxcph

Description: Generalized Euclidean real spaces are subcomplex pre-Hilbert spaces. (Contributed by Thierry Arnoux, 23-Jun-2019) (Proof shortened by AV, 22-Jul-2019)

	Ref	Expression
Hypotheses	rrxval.r	$⊢ H = I$
	rrxbase.b	$⊢ B = {Base}_{H}$
Assertion	rrxcph	$⊢ I \in V \to H \in CPreHil$

Proof

Step	Hyp	Ref	Expression
1		rrxval.r	$⊢ H = I$
2		rrxbase.b	$⊢ B = {Base}_{H}$
3	1	rrxval	$⊢ I \in V \to H = toCPreHil (ℝ_{fld} freeLMod I)$
4		eqid	$⊢ toCPreHil (ℝ_{fld} freeLMod I) = toCPreHil (ℝ_{fld} freeLMod I)$
5		eqid	$⊢ {Base}_{(ℝ_{fld} freeLMod I)} = {Base}_{(ℝ_{fld} freeLMod I)}$
6		eqid	$⊢ Scalar (ℝ_{fld} freeLMod I) = Scalar (ℝ_{fld} freeLMod I)$
7		eqid	$⊢ ℝ_{fld} freeLMod I = ℝ_{fld} freeLMod I$
8		rebase	$⊢ ℝ = {Base}_{ℝ_{fld}}$
9		remulr	$⊢ \times = \cdot_{ℝ_{fld}}$
10		eqid	$⊢ \cdot_{𝑖} (ℝ_{fld} freeLMod I) = \cdot_{𝑖} (ℝ_{fld} freeLMod I)$
11		eqid	$⊢ 0_{(ℝ_{fld} freeLMod I)} = 0_{(ℝ_{fld} freeLMod I)}$
12		re0g	$⊢ 0 = 0_{ℝ_{fld}}$
13		refldcj	$⊢ * = *_{ℝ_{fld}}$
14		refld	$⊢ ℝ_{fld} \in Field$
15	14	a1i	$⊢ I \in V \to ℝ_{fld} \in Field$
16		fconstmpt	$⊢ I \times \{0\} = (x \in I ⟼ 0)$
17	7 8 5	frlmbasf	$⊢ (I \in V \land f \in {Base}_{(ℝ_{fld} freeLMod I)}) \to f : I ⟶ ℝ$
18	17	ffnd	$⊢ (I \in V \land f \in {Base}_{(ℝ_{fld} freeLMod I)}) \to f Fn I$
19	18	3adant3	$⊢ (I \in V \land f \in {Base}_{(ℝ_{fld} freeLMod I)} \land f \cdot_{𝑖} (ℝ_{fld} freeLMod I) f = 0) \to f Fn I$
20		simpl	$⊢ (I \in V \land f \in {Base}_{(ℝ_{fld} freeLMod I)}) \to I \in V$
21	14	a1i	$⊢ (I \in V \land f \in {Base}_{(ℝ_{fld} freeLMod I)}) \to ℝ_{fld} \in Field$
22		simpr	$⊢ (I \in V \land f \in {Base}_{(ℝ_{fld} freeLMod I)}) \to f \in {Base}_{(ℝ_{fld} freeLMod I)}$
23	7 8 9 5 10	frlmipval	$⊢ ((I \in V \land ℝ_{fld} \in Field) \land (f \in {Base}_{(ℝ_{fld} freeLMod I)} \land f \in {Base}_{(ℝ_{fld} freeLMod I)})) \to f \cdot_{𝑖} (ℝ_{fld} freeLMod I) f = \sum_{ℝ_{fld}} (f \times_{f} f)$
24	20 21 22 22 23	syl22anc	$⊢ (I \in V \land f \in {Base}_{(ℝ_{fld} freeLMod I)}) \to f \cdot_{𝑖} (ℝ_{fld} freeLMod I) f = \sum_{ℝ_{fld}} (f \times_{f} f)$
25		inidm	$⊢ I \cap I = I$
26		eqidd	$⊢ ((I \in V \land f \in {Base}_{(ℝ_{fld} freeLMod I)}) \land x \in I) \to f (x) = f (x)$
27	18 18 20 20 25 26 26	offval	$⊢ (I \in V \land f \in {Base}_{(ℝ_{fld} freeLMod I)}) \to f \times_{f} f = (x \in I ⟼ f (x) f (x))$
28	17	ffvelcdmda	$⊢ ((I \in V \land f \in {Base}_{(ℝ_{fld} freeLMod I)}) \land x \in I) \to f (x) \in ℝ$
29	28 28	remulcld	$⊢ ((I \in V \land f \in {Base}_{(ℝ_{fld} freeLMod I)}) \land x \in I) \to f (x) f (x) \in ℝ$
30	27 29	fmpt3d	$⊢ (I \in V \land f \in {Base}_{(ℝ_{fld} freeLMod I)}) \to (f \times_{f} f) : I ⟶ ℝ$
31		ovexd	$⊢ (I \in V \land f \in {Base}_{(ℝ_{fld} freeLMod I)}) \to f \times_{f} f \in V$
32	30	ffund	$⊢ (I \in V \land f \in {Base}_{(ℝ_{fld} freeLMod I)}) \to Fun (f \times_{f} f)$
33	7 12 5	frlmbasfsupp	$⊢ (I \in V \land f \in {Base}_{(ℝ_{fld} freeLMod I)}) \to {finSupp}_{0} (f)$
34		0red	$⊢ (I \in V \land f \in {Base}_{(ℝ_{fld} freeLMod I)}) \to 0 \in ℝ$
35		simpr	$⊢ ((I \in V \land f \in {Base}_{(ℝ_{fld} freeLMod I)}) \land x \in ℝ) \to x \in ℝ$
36	35	recnd	$⊢ ((I \in V \land f \in {Base}_{(ℝ_{fld} freeLMod I)}) \land x \in ℝ) \to x \in ℂ$
37	36	mul02d	$⊢ ((I \in V \land f \in {Base}_{(ℝ_{fld} freeLMod I)}) \land x \in ℝ) \to 0 \cdot x = 0$
38	20 34 17 17 37	suppofss1d	$⊢ (I \in V \land f \in {Base}_{(ℝ_{fld} freeLMod I)}) \to (f \times_{f} f) supp 0 \subseteq f supp 0$
39		fsuppsssupp	$⊢ ((f \times_{f} f \in V \land Fun (f \times_{f} f)) \land ({finSupp}_{0} (f) \land (f \times_{f} f) supp 0 \subseteq f supp 0)) \to {finSupp}_{0} ((f \times_{f} f))$
40	31 32 33 38 39	syl22anc	$⊢ (I \in V \land f \in {Base}_{(ℝ_{fld} freeLMod I)}) \to {finSupp}_{0} ((f \times_{f} f))$
41		regsumsupp	$⊢ ((f \times_{f} f) : I ⟶ ℝ \land {finSupp}_{0} ((f \times_{f} f)) \land I \in V) \to \sum_{ℝ_{fld}} (f \times_{f} f) = \sum_{x \in (f \times_{f} f) supp 0} (f \times_{f} f) (x)$
42	30 40 20 41	syl3anc	$⊢ (I \in V \land f \in {Base}_{(ℝ_{fld} freeLMod I)}) \to \sum_{ℝ_{fld}} (f \times_{f} f) = \sum_{x \in (f \times_{f} f) supp 0} (f \times_{f} f) (x)$
43		suppssdm	$⊢ f supp 0 \subseteq dom f$
44	43 17	fssdm	$⊢ (I \in V \land f \in {Base}_{(ℝ_{fld} freeLMod I)}) \to f supp 0 \subseteq I$
45	38 44	sstrd	$⊢ (I \in V \land f \in {Base}_{(ℝ_{fld} freeLMod I)}) \to (f \times_{f} f) supp 0 \subseteq I$
46	45	sselda	$⊢ ((I \in V \land f \in {Base}_{(ℝ_{fld} freeLMod I)}) \land x \in {supp}_{0} ((f \times_{f} f))) \to x \in I$
47	18 18 20 20 25 26 26	ofval	$⊢ ((I \in V \land f \in {Base}_{(ℝ_{fld} freeLMod I)}) \land x \in I) \to (f \times_{f} f) (x) = f (x) f (x)$
48	46 47	syldan	$⊢ ((I \in V \land f \in {Base}_{(ℝ_{fld} freeLMod I)}) \land x \in {supp}_{0} ((f \times_{f} f))) \to (f \times_{f} f) (x) = f (x) f (x)$
49	48	sumeq2dv	$⊢ (I \in V \land f \in {Base}_{(ℝ_{fld} freeLMod I)}) \to \sum_{x \in (f \times_{f} f) supp 0} (f \times_{f} f) (x) = \sum_{x \in (f \times_{f} f) supp 0} f (x) f (x)$
50	42 49	eqtrd	$⊢ (I \in V \land f \in {Base}_{(ℝ_{fld} freeLMod I)}) \to \sum_{ℝ_{fld}} (f \times_{f} f) = \sum_{x \in (f \times_{f} f) supp 0} f (x) f (x)$
51	24 50	eqtrd	$⊢ (I \in V \land f \in {Base}_{(ℝ_{fld} freeLMod I)}) \to f \cdot_{𝑖} (ℝ_{fld} freeLMod I) f = \sum_{x \in (f \times_{f} f) supp 0} f (x) f (x)$
52	51	3adant3	$⊢ (I \in V \land f \in {Base}_{(ℝ_{fld} freeLMod I)} \land f \cdot_{𝑖} (ℝ_{fld} freeLMod I) f = 0) \to f \cdot_{𝑖} (ℝ_{fld} freeLMod I) f = \sum_{x \in (f \times_{f} f) supp 0} f (x) f (x)$
53		simp3	$⊢ (I \in V \land f \in {Base}_{(ℝ_{fld} freeLMod I)} \land f \cdot_{𝑖} (ℝ_{fld} freeLMod I) f = 0) \to f \cdot_{𝑖} (ℝ_{fld} freeLMod I) f = 0$
54	52 53	eqtr3d	$⊢ (I \in V \land f \in {Base}_{(ℝ_{fld} freeLMod I)} \land f \cdot_{𝑖} (ℝ_{fld} freeLMod I) f = 0) \to \sum_{x \in (f \times_{f} f) supp 0} f (x) f (x) = 0$
55	33	fsuppimpd	$⊢ (I \in V \land f \in {Base}_{(ℝ_{fld} freeLMod I)}) \to f supp 0 \in Fin$
56	55 38	ssfid	$⊢ (I \in V \land f \in {Base}_{(ℝ_{fld} freeLMod I)}) \to (f \times_{f} f) supp 0 \in Fin$
57	46 29	syldan	$⊢ ((I \in V \land f \in {Base}_{(ℝ_{fld} freeLMod I)}) \land x \in {supp}_{0} ((f \times_{f} f))) \to f (x) f (x) \in ℝ$
58	28	msqge0d	$⊢ ((I \in V \land f \in {Base}_{(ℝ_{fld} freeLMod I)}) \land x \in I) \to 0 \leq f (x) f (x)$
59	46 58	syldan	$⊢ ((I \in V \land f \in {Base}_{(ℝ_{fld} freeLMod I)}) \land x \in {supp}_{0} ((f \times_{f} f))) \to 0 \leq f (x) f (x)$
60	56 57 59	fsum00	$⊢ (I \in V \land f \in {Base}_{(ℝ_{fld} freeLMod I)}) \to (\sum_{x \in (f \times_{f} f) supp 0} f (x) f (x) = 0 \leftrightarrow \forall x \in {supp}_{0} ((f \times_{f} f)) f (x) f (x) = 0)$
61	60	3adant3	$⊢ (I \in V \land f \in {Base}_{(ℝ_{fld} freeLMod I)} \land f \cdot_{𝑖} (ℝ_{fld} freeLMod I) f = 0) \to (\sum_{x \in (f \times_{f} f) supp 0} f (x) f (x) = 0 \leftrightarrow \forall x \in {supp}_{0} ((f \times_{f} f)) f (x) f (x) = 0)$
62	54 61	mpbid	$⊢ (I \in V \land f \in {Base}_{(ℝ_{fld} freeLMod I)} \land f \cdot_{𝑖} (ℝ_{fld} freeLMod I) f = 0) \to \forall x \in {supp}_{0} ((f \times_{f} f)) f (x) f (x) = 0$
63	62	r19.21bi	$⊢ ((I \in V \land f \in {Base}_{(ℝ_{fld} freeLMod I)} \land f \cdot_{𝑖} (ℝ_{fld} freeLMod I) f = 0) \land x \in {supp}_{0} ((f \times_{f} f))) \to f (x) f (x) = 0$
64	63	adantlr	$⊢ (((I \in V \land f \in {Base}_{(ℝ_{fld} freeLMod I)} \land f \cdot_{𝑖} (ℝ_{fld} freeLMod I) f = 0) \land x \in I) \land x \in {supp}_{0} ((f \times_{f} f))) \to f (x) f (x) = 0$
65	28	3adantl3	$⊢ ((I \in V \land f \in {Base}_{(ℝ_{fld} freeLMod I)} \land f \cdot_{𝑖} (ℝ_{fld} freeLMod I) f = 0) \land x \in I) \to f (x) \in ℝ$
66	65	recnd	$⊢ ((I \in V \land f \in {Base}_{(ℝ_{fld} freeLMod I)} \land f \cdot_{𝑖} (ℝ_{fld} freeLMod I) f = 0) \land x \in I) \to f (x) \in ℂ$
67	66 66	mul0ord	$⊢ ((I \in V \land f \in {Base}_{(ℝ_{fld} freeLMod I)} \land f \cdot_{𝑖} (ℝ_{fld} freeLMod I) f = 0) \land x \in I) \to (f (x) f (x) = 0 \leftrightarrow (f (x) = 0 \lor f (x) = 0))$
68	67	adantr	$⊢ (((I \in V \land f \in {Base}_{(ℝ_{fld} freeLMod I)} \land f \cdot_{𝑖} (ℝ_{fld} freeLMod I) f = 0) \land x \in I) \land x \in {supp}_{0} ((f \times_{f} f))) \to (f (x) f (x) = 0 \leftrightarrow (f (x) = 0 \lor f (x) = 0))$
69	64 68	mpbid	$⊢ (((I \in V \land f \in {Base}_{(ℝ_{fld} freeLMod I)} \land f \cdot_{𝑖} (ℝ_{fld} freeLMod I) f = 0) \land x \in I) \land x \in {supp}_{0} ((f \times_{f} f))) \to (f (x) = 0 \lor f (x) = 0)$
70		oridm	$⊢ (f (x) = 0 \lor f (x) = 0) \leftrightarrow f (x) = 0$
71	69 70	sylib	$⊢ (((I \in V \land f \in {Base}_{(ℝ_{fld} freeLMod I)} \land f \cdot_{𝑖} (ℝ_{fld} freeLMod I) f = 0) \land x \in I) \land x \in {supp}_{0} ((f \times_{f} f))) \to f (x) = 0$
72	30	3adant3	$⊢ (I \in V \land f \in {Base}_{(ℝ_{fld} freeLMod I)} \land f \cdot_{𝑖} (ℝ_{fld} freeLMod I) f = 0) \to (f \times_{f} f) : I ⟶ ℝ$
73	72	adantr	$⊢ ((I \in V \land f \in {Base}_{(ℝ_{fld} freeLMod I)} \land f \cdot_{𝑖} (ℝ_{fld} freeLMod I) f = 0) \land x \in I) \to (f \times_{f} f) : I ⟶ ℝ$
74		ssidd	$⊢ ((I \in V \land f \in {Base}_{(ℝ_{fld} freeLMod I)} \land f \cdot_{𝑖} (ℝ_{fld} freeLMod I) f = 0) \land x \in I) \to (f \times_{f} f) supp 0 \subseteq (f \times_{f} f) supp 0$
75		simpl1	$⊢ ((I \in V \land f \in {Base}_{(ℝ_{fld} freeLMod I)} \land f \cdot_{𝑖} (ℝ_{fld} freeLMod I) f = 0) \land x \in I) \to I \in V$
76		0red	$⊢ ((I \in V \land f \in {Base}_{(ℝ_{fld} freeLMod I)} \land f \cdot_{𝑖} (ℝ_{fld} freeLMod I) f = 0) \land x \in I) \to 0 \in ℝ$
77	73 74 75 76	suppssr	$⊢ (((I \in V \land f \in {Base}_{(ℝ_{fld} freeLMod I)} \land f \cdot_{𝑖} (ℝ_{fld} freeLMod I) f = 0) \land x \in I) \land x \in (I ∖ {supp}_{0} ((f \times_{f} f)))) \to (f \times_{f} f) (x) = 0$
78	47	3adantl3	$⊢ ((I \in V \land f \in {Base}_{(ℝ_{fld} freeLMod I)} \land f \cdot_{𝑖} (ℝ_{fld} freeLMod I) f = 0) \land x \in I) \to (f \times_{f} f) (x) = f (x) f (x)$
79	78	eqeq1d	$⊢ ((I \in V \land f \in {Base}_{(ℝ_{fld} freeLMod I)} \land f \cdot_{𝑖} (ℝ_{fld} freeLMod I) f = 0) \land x \in I) \to ((f \times_{f} f) (x) = 0 \leftrightarrow f (x) f (x) = 0)$
80	79 67	bitrd	$⊢ ((I \in V \land f \in {Base}_{(ℝ_{fld} freeLMod I)} \land f \cdot_{𝑖} (ℝ_{fld} freeLMod I) f = 0) \land x \in I) \to ((f \times_{f} f) (x) = 0 \leftrightarrow (f (x) = 0 \lor f (x) = 0))$
81	80 70	bitrdi	$⊢ ((I \in V \land f \in {Base}_{(ℝ_{fld} freeLMod I)} \land f \cdot_{𝑖} (ℝ_{fld} freeLMod I) f = 0) \land x \in I) \to ((f \times_{f} f) (x) = 0 \leftrightarrow f (x) = 0)$
82	81	biimpa	$⊢ (((I \in V \land f \in {Base}_{(ℝ_{fld} freeLMod I)} \land f \cdot_{𝑖} (ℝ_{fld} freeLMod I) f = 0) \land x \in I) \land (f \times_{f} f) (x) = 0) \to f (x) = 0$
83	77 82	syldan	$⊢ (((I \in V \land f \in {Base}_{(ℝ_{fld} freeLMod I)} \land f \cdot_{𝑖} (ℝ_{fld} freeLMod I) f = 0) \land x \in I) \land x \in (I ∖ {supp}_{0} ((f \times_{f} f)))) \to f (x) = 0$
84		undif	$⊢ (f \times_{f} f) supp 0 \subseteq I \leftrightarrow {supp}_{0} ((f \times_{f} f)) \cup (I ∖ {supp}_{0} ((f \times_{f} f))) = I$
85	45 84	sylib	$⊢ (I \in V \land f \in {Base}_{(ℝ_{fld} freeLMod I)}) \to {supp}_{0} ((f \times_{f} f)) \cup (I ∖ {supp}_{0} ((f \times_{f} f))) = I$
86	85	eleq2d	$⊢ (I \in V \land f \in {Base}_{(ℝ_{fld} freeLMod I)}) \to (x \in ({supp}_{0} ((f \times_{f} f)) \cup (I ∖ {supp}_{0} ((f \times_{f} f)))) \leftrightarrow x \in I)$
87	86	3adant3	$⊢ (I \in V \land f \in {Base}_{(ℝ_{fld} freeLMod I)} \land f \cdot_{𝑖} (ℝ_{fld} freeLMod I) f = 0) \to (x \in ({supp}_{0} ((f \times_{f} f)) \cup (I ∖ {supp}_{0} ((f \times_{f} f)))) \leftrightarrow x \in I)$
88	87	biimpar	$⊢ ((I \in V \land f \in {Base}_{(ℝ_{fld} freeLMod I)} \land f \cdot_{𝑖} (ℝ_{fld} freeLMod I) f = 0) \land x \in I) \to x \in ({supp}_{0} ((f \times_{f} f)) \cup (I ∖ {supp}_{0} ((f \times_{f} f))))$
89		elun	$⊢ x \in ({supp}_{0} ((f \times_{f} f)) \cup (I ∖ {supp}_{0} ((f \times_{f} f)))) \leftrightarrow (x \in {supp}_{0} ((f \times_{f} f)) \lor x \in (I ∖ {supp}_{0} ((f \times_{f} f))))$
90	88 89	sylib	$⊢ ((I \in V \land f \in {Base}_{(ℝ_{fld} freeLMod I)} \land f \cdot_{𝑖} (ℝ_{fld} freeLMod I) f = 0) \land x \in I) \to (x \in {supp}_{0} ((f \times_{f} f)) \lor x \in (I ∖ {supp}_{0} ((f \times_{f} f))))$
91	71 83 90	mpjaodan	$⊢ ((I \in V \land f \in {Base}_{(ℝ_{fld} freeLMod I)} \land f \cdot_{𝑖} (ℝ_{fld} freeLMod I) f = 0) \land x \in I) \to f (x) = 0$
92	91	ralrimiva	$⊢ (I \in V \land f \in {Base}_{(ℝ_{fld} freeLMod I)} \land f \cdot_{𝑖} (ℝ_{fld} freeLMod I) f = 0) \to \forall x \in I f (x) = 0$
93		fconstfv	$⊢ f : I ⟶ \{0\} \leftrightarrow (f Fn I \land \forall x \in I f (x) = 0)$
94		c0ex	$⊢ 0 \in V$
95	94	fconst2	$⊢ f : I ⟶ \{0\} \leftrightarrow f = I \times \{0\}$
96	93 95	sylbb1	$⊢ (f Fn I \land \forall x \in I f (x) = 0) \to f = I \times \{0\}$
97	19 92 96	syl2anc	$⊢ (I \in V \land f \in {Base}_{(ℝ_{fld} freeLMod I)} \land f \cdot_{𝑖} (ℝ_{fld} freeLMod I) f = 0) \to f = I \times \{0\}$
98		isfld	$⊢ ℝ_{fld} \in Field \leftrightarrow (ℝ_{fld} \in DivRing \land ℝ_{fld} \in CRing)$
99	14 98	mpbi	$⊢ (ℝ_{fld} \in DivRing \land ℝ_{fld} \in CRing)$
100	99	simpli	$⊢ ℝ_{fld} \in DivRing$
101		drngring	$⊢ ℝ_{fld} \in DivRing \to ℝ_{fld} \in Ring$
102	100 101	ax-mp	$⊢ ℝ_{fld} \in Ring$
103	7 12	frlm0	$⊢ (ℝ_{fld} \in Ring \land I \in V) \to I \times \{0\} = 0_{(ℝ_{fld} freeLMod I)}$
104	102 103	mpan	$⊢ I \in V \to I \times \{0\} = 0_{(ℝ_{fld} freeLMod I)}$
105	104 16	eqtr3di	$⊢ I \in V \to 0_{(ℝ_{fld} freeLMod I)} = (x \in I ⟼ 0)$
106	105	3ad2ant1	$⊢ (I \in V \land f \in {Base}_{(ℝ_{fld} freeLMod I)} \land f \cdot_{𝑖} (ℝ_{fld} freeLMod I) f = 0) \to 0_{(ℝ_{fld} freeLMod I)} = (x \in I ⟼ 0)$
107	16 97 106	3eqtr4a	$⊢ (I \in V \land f \in {Base}_{(ℝ_{fld} freeLMod I)} \land f \cdot_{𝑖} (ℝ_{fld} freeLMod I) f = 0) \to f = 0_{(ℝ_{fld} freeLMod I)}$
108		cjre	$⊢ x \in ℝ \to \overline{x} = x$
109	108	adantl	$⊢ (I \in V \land x \in ℝ) \to \overline{x} = x$
110		id	$⊢ I \in V \to I \in V$
111	7 8 9 5 10 11 12 13 15 107 109 110	frlmphl	$⊢ I \in V \to ℝ_{fld} freeLMod I \in PreHil$
112	7	frlmsca	$⊢ (ℝ_{fld} \in Field \land I \in V) \to ℝ_{fld} = Scalar (ℝ_{fld} freeLMod I)$
113	14 112	mpan	$⊢ I \in V \to ℝ_{fld} = Scalar (ℝ_{fld} freeLMod I)$
114		df-refld	$⊢ ℝ_{fld} = ℂ_{fld} ↾_{𝑠} ℝ$
115	113 114	eqtr3di	$⊢ I \in V \to Scalar (ℝ_{fld} freeLMod I) = ℂ_{fld} ↾_{𝑠} ℝ$
116		simpr1	$⊢ (I \in V \land (f \in ℝ \land f \in ℝ \land 0 \leq f)) \to f \in ℝ$
117		simpr3	$⊢ (I \in V \land (f \in ℝ \land f \in ℝ \land 0 \leq f)) \to 0 \leq f$
118	116 117	resqrtcld	$⊢ (I \in V \land (f \in ℝ \land f \in ℝ \land 0 \leq f)) \to \sqrt{f} \in ℝ$
119	56 57 59	fsumge0	$⊢ (I \in V \land f \in {Base}_{(ℝ_{fld} freeLMod I)}) \to 0 \leq \sum_{x \in (f \times_{f} f) supp 0} f (x) f (x)$
120	119 50	breqtrrd	$⊢ (I \in V \land f \in {Base}_{(ℝ_{fld} freeLMod I)}) \to 0 \leq \sum_{ℝ_{fld}} (f \times_{f} f)$
121	120 24	breqtrrd	$⊢ (I \in V \land f \in {Base}_{(ℝ_{fld} freeLMod I)}) \to 0 \leq f \cdot_{𝑖} (ℝ_{fld} freeLMod I) f$
122	4 5 6 111 115 10 118 121	tcphcph	$⊢ I \in V \to toCPreHil (ℝ_{fld} freeLMod I) \in CPreHil$
123	3 122	eqeltrd	$⊢ I \in V \to H \in CPreHil$

Metamath Proof Explorer

Theorem rrxcph

Proof