rrxcph - Metamath Proof Explorer

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

Theorem rrxcph 25512

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

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

**Assertion**
Ref	Expression
rrxcph	⊢ (𝐼 ∈ 𝑉 → 𝐻 ∈ ℂPreHil)

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

Step	Hyp	Ref	Expression
1		rrxval.r	. . 3 ⊢ 𝐻 = (ℝ^‘𝐼)
2	1	rrxval 25507	. 2 ⊢ (𝐼 ∈ 𝑉 → 𝐻 = (toℂPreHil‘(ℝ_fld freeLMod 𝐼)))
3		eqid 2765	. . 3 ⊢ (toℂPreHil‘(ℝ_fld freeLMod 𝐼)) = (toℂPreHil‘(ℝ_fld freeLMod 𝐼))
4		eqid 2765	. . 3 ⊢ (Base‘(ℝ_fld freeLMod 𝐼)) = (Base‘(ℝ_fld freeLMod 𝐼))
5		eqid 2765	. . 3 ⊢ (Scalar‘(ℝ_fld freeLMod 𝐼)) = (Scalar‘(ℝ_fld freeLMod 𝐼))
6		eqid 2765	. . . 4 ⊢ (ℝ_fld freeLMod 𝐼) = (ℝ_fld freeLMod 𝐼)
7		rebase 21716	. . . 4 ⊢ ℝ = (Base‘ℝ_fld)
8		remulr 21721	. . . 4 ⊢ · = (._r‘ℝ_fld)
9		eqid 2765	. . . 4 ⊢ (·_𝑖‘(ℝ_fld freeLMod 𝐼)) = (·_𝑖‘(ℝ_fld freeLMod 𝐼))
10		eqid 2765	. . . 4 ⊢ (0_g‘(ℝ_fld freeLMod 𝐼)) = (0_g‘(ℝ_fld freeLMod 𝐼))
11		re0g 21722	. . . 4 ⊢ 0 = (0_g‘ℝ_fld)
12		refldcj 21730	. . . 4 ⊢ ∗ = (*_𝑟‘ℝ_fld)
13		refld 21729	. . . . 5 ⊢ ℝ_fld ∈ Field
14	13	a1i 11	. . . 4 ⊢ (𝐼 ∈ 𝑉 → ℝ_fld ∈ Field)
15		fconstmpt 5714	. . . . 5 ⊢ (𝐼 × {0}) = (𝑥 ∈ 𝐼 ↦ 0)
16	6, 7, 4	frlmbasf 21870	. . . . . . . 8 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) → 𝑓:𝐼⟶ℝ)
17	16	ffnd 6696	. . . . . . 7 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) → 𝑓 Fn 𝐼)
18	17	3adant3 1148	. . . . . 6 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) → 𝑓 Fn 𝐼)
19		simpl 487	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) → 𝐼 ∈ 𝑉)
20	13	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) → ℝ_fld ∈ Field)
21		simpr 489	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) → 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)))
22	6, 7, 8, 4, 9	frlmipval 21889	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐼 ∈ 𝑉 ∧ ℝ_fld ∈ Field) ∧ (𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)))) → (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = (ℝ_fld Σ_g (𝑓 ∘_f · 𝑓)))
23	19, 20, 21, 21, 22	syl22anc 851	. . . . . . . . . . . . . . . 16 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) → (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = (ℝ_fld Σ_g (𝑓 ∘_f · 𝑓)))
24		inidm 4181	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐼 ∩ 𝐼) = 𝐼
25		eqidd 2766	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) ∧ 𝑥 ∈ 𝐼) → (𝑓‘𝑥) = (𝑓‘𝑥))
26	17, 17, 19, 19, 24, 25, 25	offval 7673	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) → (𝑓 ∘_f · 𝑓) = (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥) · (𝑓‘𝑥))))
27	16	ffvelcdmda 7069	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) ∧ 𝑥 ∈ 𝐼) → (𝑓‘𝑥) ∈ ℝ)
28	27, 27	remulcld 11227	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) ∧ 𝑥 ∈ 𝐼) → ((𝑓‘𝑥) · (𝑓‘𝑥)) ∈ ℝ)
29	26, 28	fmpt3d 7101	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) → (𝑓 ∘_f · 𝑓):𝐼⟶ℝ)
30		ovexd 7435	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) → (𝑓 ∘_f · 𝑓) ∈ V)
31	29	ffund 6700	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) → Fun (𝑓 ∘_f · 𝑓))
32	6, 11, 4	frlmbasfsupp 21868	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) → 𝑓 finSupp 0)
33		0red 11199	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) → 0 ∈ ℝ)
34		simpr 489	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℝ)
35	34	recnd 11225	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℂ)
36	35	mul02d 11396	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) ∧ 𝑥 ∈ ℝ) → (0 · 𝑥) = 0)
37	19, 33, 16, 16, 36	suppofss1d 8188	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) → ((𝑓 ∘_f · 𝑓) supp 0) ⊆ (𝑓 supp 0))
38		fsuppsssupp 9329	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑓 ∘_f · 𝑓) ∈ V ∧ Fun (𝑓 ∘_f · 𝑓)) ∧ (𝑓 finSupp 0 ∧ ((𝑓 ∘_f · 𝑓) supp 0) ⊆ (𝑓 supp 0))) → (𝑓 ∘_f · 𝑓) finSupp 0)
39	30, 31, 32, 37, 38	syl22anc 851	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) → (𝑓 ∘_f · 𝑓) finSupp 0)
40		regsumsupp 21732	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑓 ∘_f · 𝑓):𝐼⟶ℝ ∧ (𝑓 ∘_f · 𝑓) finSupp 0 ∧ 𝐼 ∈ 𝑉) → (ℝ_fld Σ_g (𝑓 ∘_f · 𝑓)) = Σ𝑥 ∈ ((𝑓 ∘_f · 𝑓) supp 0)((𝑓 ∘_f · 𝑓)‘𝑥))
41	29, 39, 19, 40	syl3anc 1394	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) → (ℝ_fld Σ_g (𝑓 ∘_f · 𝑓)) = Σ𝑥 ∈ ((𝑓 ∘_f · 𝑓) supp 0)((𝑓 ∘_f · 𝑓)‘𝑥))
42		suppssdm 8161	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑓 supp 0) ⊆ dom 𝑓
43	42, 16	fssdm 6715	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) → (𝑓 supp 0) ⊆ 𝐼)
44	37, 43	sstrd 3949	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) → ((𝑓 ∘_f · 𝑓) supp 0) ⊆ 𝐼)
45	44	sselda 3939	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) ∧ 𝑥 ∈ ((𝑓 ∘_f · 𝑓) supp 0)) → 𝑥 ∈ 𝐼)
46	17, 17, 19, 19, 24, 25, 25	ofval 7675	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) ∧ 𝑥 ∈ 𝐼) → ((𝑓 ∘_f · 𝑓)‘𝑥) = ((𝑓‘𝑥) · (𝑓‘𝑥)))
47	45, 46	syldan 602	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) ∧ 𝑥 ∈ ((𝑓 ∘_f · 𝑓) supp 0)) → ((𝑓 ∘_f · 𝑓)‘𝑥) = ((𝑓‘𝑥) · (𝑓‘𝑥)))
48	47	sumeq2dv 15743	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) → Σ𝑥 ∈ ((𝑓 ∘_f · 𝑓) supp 0)((𝑓 ∘_f · 𝑓)‘𝑥) = Σ𝑥 ∈ ((𝑓 ∘_f · 𝑓) supp 0)((𝑓‘𝑥) · (𝑓‘𝑥)))
49	41, 48	eqtrd 2800	. . . . . . . . . . . . . . . 16 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) → (ℝ_fld Σ_g (𝑓 ∘_f · 𝑓)) = Σ𝑥 ∈ ((𝑓 ∘_f · 𝑓) supp 0)((𝑓‘𝑥) · (𝑓‘𝑥)))
50	23, 49	eqtrd 2800	. . . . . . . . . . . . . . 15 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) → (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = Σ𝑥 ∈ ((𝑓 ∘_f · 𝑓) supp 0)((𝑓‘𝑥) · (𝑓‘𝑥)))
51	50	3adant3 1148	. . . . . . . . . . . . . 14 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) → (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = Σ𝑥 ∈ ((𝑓 ∘_f · 𝑓) supp 0)((𝑓‘𝑥) · (𝑓‘𝑥)))
52		simp3 1154	. . . . . . . . . . . . . 14 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) → (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0)
53	51, 52	eqtr3d 2802	. . . . . . . . . . . . 13 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) → Σ𝑥 ∈ ((𝑓 ∘_f · 𝑓) supp 0)((𝑓‘𝑥) · (𝑓‘𝑥)) = 0)
54	32	fsuppimpd 9317	. . . . . . . . . . . . . . . 16 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) → (𝑓 supp 0) ∈ Fin)
55	54, 37	ssfid 9217	. . . . . . . . . . . . . . 15 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) → ((𝑓 ∘_f · 𝑓) supp 0) ∈ Fin)
56	45, 28	syldan 602	. . . . . . . . . . . . . . 15 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) ∧ 𝑥 ∈ ((𝑓 ∘_f · 𝑓) supp 0)) → ((𝑓‘𝑥) · (𝑓‘𝑥)) ∈ ℝ)
57	27	msqge0d 11770	. . . . . . . . . . . . . . . 16 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) ∧ 𝑥 ∈ 𝐼) → 0 ≤ ((𝑓‘𝑥) · (𝑓‘𝑥)))
58	45, 57	syldan 602	. . . . . . . . . . . . . . 15 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) ∧ 𝑥 ∈ ((𝑓 ∘_f · 𝑓) supp 0)) → 0 ≤ ((𝑓‘𝑥) · (𝑓‘𝑥)))
59	55, 56, 58	fsum00 15840	. . . . . . . . . . . . . 14 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) → (Σ𝑥 ∈ ((𝑓 ∘_f · 𝑓) supp 0)((𝑓‘𝑥) · (𝑓‘𝑥)) = 0 ↔ ∀𝑥 ∈ ((𝑓 ∘_f · 𝑓) supp 0)((𝑓‘𝑥) · (𝑓‘𝑥)) = 0))
60	59	3adant3 1148	. . . . . . . . . . . . 13 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) → (Σ𝑥 ∈ ((𝑓 ∘_f · 𝑓) supp 0)((𝑓‘𝑥) · (𝑓‘𝑥)) = 0 ↔ ∀𝑥 ∈ ((𝑓 ∘_f · 𝑓) supp 0)((𝑓‘𝑥) · (𝑓‘𝑥)) = 0))
61	53, 60	mpbid 235	. . . . . . . . . . . 12 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) → ∀𝑥 ∈ ((𝑓 ∘_f · 𝑓) supp 0)((𝑓‘𝑥) · (𝑓‘𝑥)) = 0)
62	61	r19.21bi 3257	. . . . . . . . . . 11 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ ((𝑓 ∘_f · 𝑓) supp 0)) → ((𝑓‘𝑥) · (𝑓‘𝑥)) = 0)
63	62	adantlr 727	. . . . . . . . . 10 ⊢ ((((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼) ∧ 𝑥 ∈ ((𝑓 ∘_f · 𝑓) supp 0)) → ((𝑓‘𝑥) · (𝑓‘𝑥)) = 0)
64	27	3adantl3 1185	. . . . . . . . . . . . 13 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼) → (𝑓‘𝑥) ∈ ℝ)
65	64	recnd 11225	. . . . . . . . . . . 12 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼) → (𝑓‘𝑥) ∈ ℂ)
66	65, 65	mul0ord 11850	. . . . . . . . . . 11 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼) → (((𝑓‘𝑥) · (𝑓‘𝑥)) = 0 ↔ ((𝑓‘𝑥) = 0 ∨ (𝑓‘𝑥) = 0)))
67	66	adantr 485	. . . . . . . . . 10 ⊢ ((((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼) ∧ 𝑥 ∈ ((𝑓 ∘_f · 𝑓) supp 0)) → (((𝑓‘𝑥) · (𝑓‘𝑥)) = 0 ↔ ((𝑓‘𝑥) = 0 ∨ (𝑓‘𝑥) = 0)))
68	63, 67	mpbid 235	. . . . . . . . 9 ⊢ ((((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼) ∧ 𝑥 ∈ ((𝑓 ∘_f · 𝑓) supp 0)) → ((𝑓‘𝑥) = 0 ∨ (𝑓‘𝑥) = 0))
69		oridm 917	. . . . . . . . 9 ⊢ (((𝑓‘𝑥) = 0 ∨ (𝑓‘𝑥) = 0) ↔ (𝑓‘𝑥) = 0)
70	68, 69	sylib 221	. . . . . . . 8 ⊢ ((((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼) ∧ 𝑥 ∈ ((𝑓 ∘_f · 𝑓) supp 0)) → (𝑓‘𝑥) = 0)
71	29	3adant3 1148	. . . . . . . . . . 11 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) → (𝑓 ∘_f · 𝑓):𝐼⟶ℝ)
72	71	adantr 485	. . . . . . . . . 10 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼) → (𝑓 ∘_f · 𝑓):𝐼⟶ℝ)
73		ssidd 3962	. . . . . . . . . 10 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼) → ((𝑓 ∘_f · 𝑓) supp 0) ⊆ ((𝑓 ∘_f · 𝑓) supp 0))
74		simpl1 1208	. . . . . . . . . 10 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼) → 𝐼 ∈ 𝑉)
75		0red 11199	. . . . . . . . . 10 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼) → 0 ∈ ℝ)
76	72, 73, 74, 75	suppssr 8179	. . . . . . . . 9 ⊢ ((((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼) ∧ 𝑥 ∈ (𝐼 ∖ ((𝑓 ∘_f · 𝑓) supp 0))) → ((𝑓 ∘_f · 𝑓)‘𝑥) = 0)
77	46	3adantl3 1185	. . . . . . . . . . . . 13 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼) → ((𝑓 ∘_f · 𝑓)‘𝑥) = ((𝑓‘𝑥) · (𝑓‘𝑥)))
78	77	eqeq1d 2767	. . . . . . . . . . . 12 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼) → (((𝑓 ∘_f · 𝑓)‘𝑥) = 0 ↔ ((𝑓‘𝑥) · (𝑓‘𝑥)) = 0))
79	78, 66	bitrd 282	. . . . . . . . . . 11 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼) → (((𝑓 ∘_f · 𝑓)‘𝑥) = 0 ↔ ((𝑓‘𝑥) = 0 ∨ (𝑓‘𝑥) = 0)))
80	79, 69	bitrdi 290	. . . . . . . . . 10 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼) → (((𝑓 ∘_f · 𝑓)‘𝑥) = 0 ↔ (𝑓‘𝑥) = 0))
81	80	biimpa 481	. . . . . . . . 9 ⊢ ((((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼) ∧ ((𝑓 ∘_f · 𝑓)‘𝑥) = 0) → (𝑓‘𝑥) = 0)
82	76, 81	syldan 602	. . . . . . . 8 ⊢ ((((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼) ∧ 𝑥 ∈ (𝐼 ∖ ((𝑓 ∘_f · 𝑓) supp 0))) → (𝑓‘𝑥) = 0)
83		undif 4439	. . . . . . . . . . . . 13 ⊢ (((𝑓 ∘_f · 𝑓) supp 0) ⊆ 𝐼 ↔ (((𝑓 ∘_f · 𝑓) supp 0) ∪ (𝐼 ∖ ((𝑓 ∘_f · 𝑓) supp 0))) = 𝐼)
84	44, 83	sylib 221	. . . . . . . . . . . 12 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) → (((𝑓 ∘_f · 𝑓) supp 0) ∪ (𝐼 ∖ ((𝑓 ∘_f · 𝑓) supp 0))) = 𝐼)
85	84	eleq2d 2851	. . . . . . . . . . 11 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) → (𝑥 ∈ (((𝑓 ∘_f · 𝑓) supp 0) ∪ (𝐼 ∖ ((𝑓 ∘_f · 𝑓) supp 0))) ↔ 𝑥 ∈ 𝐼))
86	85	3adant3 1148	. . . . . . . . . 10 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) → (𝑥 ∈ (((𝑓 ∘_f · 𝑓) supp 0) ∪ (𝐼 ∖ ((𝑓 ∘_f · 𝑓) supp 0))) ↔ 𝑥 ∈ 𝐼))
87	86	biimpar 482	. . . . . . . . 9 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼) → 𝑥 ∈ (((𝑓 ∘_f · 𝑓) supp 0) ∪ (𝐼 ∖ ((𝑓 ∘_f · 𝑓) supp 0))))
88		elun 4109	. . . . . . . . 9 ⊢ (𝑥 ∈ (((𝑓 ∘_f · 𝑓) supp 0) ∪ (𝐼 ∖ ((𝑓 ∘_f · 𝑓) supp 0))) ↔ (𝑥 ∈ ((𝑓 ∘_f · 𝑓) supp 0) ∨ 𝑥 ∈ (𝐼 ∖ ((𝑓 ∘_f · 𝑓) supp 0))))
89	87, 88	sylib 221	. . . . . . . 8 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼) → (𝑥 ∈ ((𝑓 ∘_f · 𝑓) supp 0) ∨ 𝑥 ∈ (𝐼 ∖ ((𝑓 ∘_f · 𝑓) supp 0))))
90	70, 82, 89	mpjaodan 973	. . . . . . 7 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼) → (𝑓‘𝑥) = 0)
91	90	ralrimiva 3157	. . . . . 6 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) → ∀𝑥 ∈ 𝐼 (𝑓‘𝑥) = 0)
92		fconstfv 7200	. . . . . . 7 ⊢ (𝑓:𝐼⟶{0} ↔ (𝑓 Fn 𝐼 ∧ ∀𝑥 ∈ 𝐼 (𝑓‘𝑥) = 0))
93		c0ex 11188	. . . . . . . 8 ⊢ 0 ∈ V
94	93	fconst2 7193	. . . . . . 7 ⊢ (𝑓:𝐼⟶{0} ↔ 𝑓 = (𝐼 × {0}))
95	92, 94	sylbb1 240	. . . . . 6 ⊢ ((𝑓 Fn 𝐼 ∧ ∀𝑥 ∈ 𝐼 (𝑓‘𝑥) = 0) → 𝑓 = (𝐼 × {0}))
96	18, 91, 95	syl2anc 595	. . . . 5 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) → 𝑓 = (𝐼 × {0}))
97		isfld 20815	. . . . . . . . . . 11 ⊢ (ℝ_fld ∈ Field ↔ (ℝ_fld ∈ DivRing ∧ ℝ_fld ∈ CRing))
98	13, 97	mpbi 233	. . . . . . . . . 10 ⊢ (ℝ_fld ∈ DivRing ∧ ℝ_fld ∈ CRing)
99	98	simpli 488	. . . . . . . . 9 ⊢ ℝ_fld ∈ DivRing
100		drngring 20811	. . . . . . . . 9 ⊢ (ℝ_fld ∈ DivRing → ℝ_fld ∈ Ring)
101	99, 100	ax-mp 5	. . . . . . . 8 ⊢ ℝ_fld ∈ Ring
102	6, 11	frlm0 21864	. . . . . . . 8 ⊢ ((ℝ_fld ∈ Ring ∧ 𝐼 ∈ 𝑉) → (𝐼 × {0}) = (0_g‘(ℝ_fld freeLMod 𝐼)))
103	101, 102	mpan 702	. . . . . . 7 ⊢ (𝐼 ∈ 𝑉 → (𝐼 × {0}) = (0_g‘(ℝ_fld freeLMod 𝐼)))
104	103, 15	eqtr3di 2815	. . . . . 6 ⊢ (𝐼 ∈ 𝑉 → (0_g‘(ℝ_fld freeLMod 𝐼)) = (𝑥 ∈ 𝐼 ↦ 0))
105	104	3ad2ant1 1149	. . . . 5 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) → (0_g‘(ℝ_fld freeLMod 𝐼)) = (𝑥 ∈ 𝐼 ↦ 0))
106	15, 96, 105	3eqtr4a 2826	. . . 4 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) → 𝑓 = (0_g‘(ℝ_fld freeLMod 𝐼)))
107		cjre 15180	. . . . 5 ⊢ (𝑥 ∈ ℝ → (∗‘𝑥) = 𝑥)
108	107	adantl 486	. . . 4 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ ℝ) → (∗‘𝑥) = 𝑥)
109		id 23	. . . 4 ⊢ (𝐼 ∈ 𝑉 → 𝐼 ∈ 𝑉)
110	6, 7, 8, 4, 9, 10, 11, 12, 14, 106, 108, 109	frlmphl 21891	. . 3 ⊢ (𝐼 ∈ 𝑉 → (ℝ_fld freeLMod 𝐼) ∈ PreHil)
111	6	frlmsca 21863	. . . . 5 ⊢ ((ℝ_fld ∈ Field ∧ 𝐼 ∈ 𝑉) → ℝ_fld = (Scalar‘(ℝ_fld freeLMod 𝐼)))
112	13, 111	mpan 702	. . . 4 ⊢ (𝐼 ∈ 𝑉 → ℝ_fld = (Scalar‘(ℝ_fld freeLMod 𝐼)))
113		df-refld 21715	. . . 4 ⊢ ℝ_fld = (ℂ_fld ↾_s ℝ)
114	112, 113	eqtr3di 2815	. . 3 ⊢ (𝐼 ∈ 𝑉 → (Scalar‘(ℝ_fld freeLMod 𝐼)) = (ℂ_fld ↾_s ℝ))
115		simpr1 1211	. . . 4 ⊢ ((𝐼 ∈ 𝑉 ∧ (𝑓 ∈ ℝ ∧ 𝑓 ∈ ℝ ∧ 0 ≤ 𝑓)) → 𝑓 ∈ ℝ)
116		simpr3 1213	. . . 4 ⊢ ((𝐼 ∈ 𝑉 ∧ (𝑓 ∈ ℝ ∧ 𝑓 ∈ ℝ ∧ 0 ≤ 𝑓)) → 0 ≤ 𝑓)
117	115, 116	resqrtcld 15459	. . 3 ⊢ ((𝐼 ∈ 𝑉 ∧ (𝑓 ∈ ℝ ∧ 𝑓 ∈ ℝ ∧ 0 ≤ 𝑓)) → (√‘𝑓) ∈ ℝ)
118	55, 56, 58	fsumge0 15837	. . . . 5 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) → 0 ≤ Σ𝑥 ∈ ((𝑓 ∘_f · 𝑓) supp 0)((𝑓‘𝑥) · (𝑓‘𝑥)))
119	118, 49	breqtrrd 5133	. . . 4 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) → 0 ≤ (ℝ_fld Σ_g (𝑓 ∘_f · 𝑓)))
120	119, 23	breqtrrd 5133	. . 3 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) → 0 ≤ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓))
121	3, 4, 5, 110, 114, 9, 117, 120	tcphcph 25357	. 2 ⊢ (𝐼 ∈ 𝑉 → (toℂPreHil‘(ℝ_fld freeLMod 𝐼)) ∈ ℂPreHil)
122	2, 121	eqeltrd 2865	1 ⊢ (𝐼 ∈ 𝑉 → 𝐻 ∈ ℂPreHil)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 209 ∧ wa 400 ∨ wo 860 ∧ w3a 1101 = wceq 1563 ∈ wcel 2145 ∀wral 3079 Vcvv 3457 ∖ cdif 3904 ∪ cun 3905 ⊆ wss 3907 {csn 4585 class class class wbr 5105 ↦ cmpt 5186 × cxp 5650 Fun wfun 6519 Fn wfn 6520 ⟶wf 6521 ‘cfv 6525 (class class class)co 7400 ∘_f cof 7662 supp csupp 8144 finSupp cfsupp 9309 ℝcr 11087 0cc0 11088 · cmul 11093 ≤ cle 11232 ∗ccj 15137 Σcsu 15727 Basecbs 17259 ↾_s cress 17280 Scalarcsca 17303 ·_𝑖cip 17305 0_gc0g 17482 Σ_g cgsu 17483 Ringcrg 20306 CRingccrg 20307 DivRingcdr 20804 Fieldcfield 20805 ℂ_fldccnfld 21482 ℝ_fldcrefld 21714 freeLMod cfrlm 21856 ℂPreHilccph 25286 toℂPreHilctcph 25287 ℝ^crrx 25503

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1818 ax-4 1832 ax-5 1933 ax-6 1990 ax-7 2031 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2215 ax-ext 2737 ax-rep 5232 ax-sep 5251 ax-nul 5261 ax-pow 5327 ax-pr 5395 ax-un 7722 ax-inf2 9598 ax-cnex 11144 ax-resscn 11145 ax-1cn 11146 ax-icn 11147 ax-addcl 11148 ax-addrcl 11149 ax-mulcl 11150 ax-mulrcl 11151 ax-mulcom 11152 ax-addass 11153 ax-mulass 11154 ax-distr 11155 ax-i2m1 11156 ax-1ne0 11157 ax-1rid 11158 ax-rnegex 11159 ax-rrecex 11160 ax-cnre 11161 ax-pre-lttri 11162 ax-pre-lttrn 11163 ax-pre-ltadd 11164 ax-pre-mulgt0 11165 ax-pre-sup 11166 ax-addf 11167 ax-mulf 11168

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1102 df-3an 1103 df-tru 1566 df-fal 1576 df-ex 1803 df-nf 1807 df-sb 2094 df-mo 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ne 2961 df-nel 3065 df-ral 3080 df-rex 3090 df-rmo 3370 df-reu 3371 df-rab 3418 df-v 3459 df-sbc 3748 df-csb 3856 df-dif 3910 df-un 3912 df-in 3914 df-ss 3924 df-pss 3927 df-nul 4289 df-if 4484 df-pw 4560 df-sn 4586 df-pr 4588 df-tp 4590 df-op 4592 df-uni 4869 df-int 4909 df-iun 4954 df-br 5106 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5547 df-eprel 5552 df-po 5560 df-so 5561 df-fr 5605 df-se 5606 df-we 5607 df-xp 5658 df-rel 5659 df-cnv 5660 df-co 5661 df-dm 5662 df-rn 5663 df-res 5664 df-ima 5665 df-pred 6292 df-ord 6353 df-on 6354 df-lim 6355 df-suc 6356 df-iota 6481 df-fun 6527 df-fn 6528 df-f 6529 df-f1 6530 df-fo 6531 df-f1o 6532 df-fv 6533 df-isom 6534 df-riota 7357 df-ov 7403 df-oprab 7404 df-mpo 7405 df-of 7664 df-om 7851 df-1st 7974 df-2nd 7975 df-supp 8145 df-tpos 8210 df-frecs 8266 df-wrecs 8297 df-recs 8346 df-rdg 8385 df-1o 8441 df-er 8682 df-map 8814 df-ixp 8884 df-en 8932 df-dom 8933 df-sdom 8934 df-fin 8935 df-fsupp 9310 df-sup 9390 df-inf 9391 df-oi 9460 df-card 9913 df-pnf 11233 df-mnf 11234 df-xr 11235 df-ltxr 11236 df-le 11237 df-sub 11431 df-neg 11432 df-div 11860 df-nn 12225 df-2 12294 df-3 12295 df-4 12296 df-5 12297 df-6 12298 df-7 12299 df-8 12300 df-9 12301 df-n0 12496 df-z 12583 df-dec 12703 df-uz 12854 df-q 12964 df-rp 13008 df-xneg 13128 df-xadd 13129 df-xmul 13130 df-ico 13369 df-fz 13527 df-fzo 13674 df-seq 14029 df-exp 14089 df-hash 14358 df-cj 15140 df-re 15141 df-im 15142 df-sqrt 15276 df-abs 15277 df-clim 15529 df-sum 15728 df-struct 17197 df-sets 17214 df-slot 17232 df-ndx 17244 df-base 17260 df-ress 17281 df-plusg 17313 df-mulr 17314 df-starv 17315 df-sca 17316 df-vsca 17317 df-ip 17318 df-tset 17319 df-ple 17320 df-ds 17322 df-unif 17323 df-hom 17324 df-cco 17325 df-rest 17465 df-topn 17466 df-0g 17484 df-gsum 17485 df-topgen 17486 df-prds 17490 df-pws 17492 df-mgm 18688 df-sgrp 18767 df-mnd 18783 df-mhm 18831 df-submnd 18832 df-grp 18993 df-minusg 18994 df-sbg 18995 df-subg 19180 df-ghm 19275 df-cntz 19378 df-cmn 19843 df-abl 19844 df-mgp 20208 df-rng 20222 df-ur 20255 df-ring 20308 df-cring 20309 df-oppr 20410 df-dvdsr 20430 df-unit 20431 df-invr 20461 df-dvr 20474 df-rhm 20545 df-subrng 20622 df-subrg 20646 df-drng 20806 df-field 20807 df-abv 20881 df-staf 20911 df-srng 20912 df-lmod 20952 df-lss 21022 df-lmhm 21112 df-lvec 21193 df-sra 21263 df-rgmod 21264 df-psmet 21474 df-xmet 21475 df-met 21476 df-bl 21477 df-mopn 21478 df-cnfld 21483 df-refld 21715 df-phl 21736 df-dsmm 21842 df-frlm 21857 df-top 23012 df-topon 23029 df-topsp 23051 df-bases 23064 df-xms 24438 df-ms 24439 df-nm 24700 df-ngp 24701 df-tng 24702 df-nrg 24703 df-nlm 24704 df-clm 25183 df-cph 25288 df-tcph 25289 df-rrx 25505

This theorem is referenced by: rrxngp 46857

W3C validator