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 25292

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 25287	. 2 ⊢ (𝐼 ∈ 𝑉 → 𝐻 = (toℂPreHil‘(ℝ_fld freeLMod 𝐼)))
3		eqid 2729	. . 3 ⊢ (toℂPreHil‘(ℝ_fld freeLMod 𝐼)) = (toℂPreHil‘(ℝ_fld freeLMod 𝐼))
4		eqid 2729	. . 3 ⊢ (Base‘(ℝ_fld freeLMod 𝐼)) = (Base‘(ℝ_fld freeLMod 𝐼))
5		eqid 2729	. . 3 ⊢ (Scalar‘(ℝ_fld freeLMod 𝐼)) = (Scalar‘(ℝ_fld freeLMod 𝐼))
6		eqid 2729	. . . 4 ⊢ (ℝ_fld freeLMod 𝐼) = (ℝ_fld freeLMod 𝐼)
7		rebase 21515	. . . 4 ⊢ ℝ = (Base‘ℝ_fld)
8		remulr 21520	. . . 4 ⊢ · = (._r‘ℝ_fld)
9		eqid 2729	. . . 4 ⊢ (·_𝑖‘(ℝ_fld freeLMod 𝐼)) = (·_𝑖‘(ℝ_fld freeLMod 𝐼))
10		eqid 2729	. . . 4 ⊢ (0_g‘(ℝ_fld freeLMod 𝐼)) = (0_g‘(ℝ_fld freeLMod 𝐼))
11		re0g 21521	. . . 4 ⊢ 0 = (0_g‘ℝ_fld)
12		refldcj 21529	. . . 4 ⊢ ∗ = (*_𝑟‘ℝ_fld)
13		refld 21528	. . . . 5 ⊢ ℝ_fld ∈ Field
14	13	a1i 11	. . . 4 ⊢ (𝐼 ∈ 𝑉 → ℝ_fld ∈ Field)
15		fconstmpt 5700	. . . . 5 ⊢ (𝐼 × {0}) = (𝑥 ∈ 𝐼 ↦ 0)
16	6, 7, 4	frlmbasf 21669	. . . . . . . 8 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) → 𝑓:𝐼⟶ℝ)
17	16	ffnd 6689	. . . . . . 7 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) → 𝑓 Fn 𝐼)
18	17	3adant3 1132	. . . . . 6 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) → 𝑓 Fn 𝐼)
19		simpl 482	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) → 𝐼 ∈ 𝑉)
20	13	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) → ℝ_fld ∈ Field)
21		simpr 484	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) → 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)))
22	6, 7, 8, 4, 9	frlmipval 21688	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐼 ∈ 𝑉 ∧ ℝ_fld ∈ Field) ∧ (𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)))) → (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = (ℝ_fld Σ_g (𝑓 ∘_f · 𝑓)))
23	19, 20, 21, 21, 22	syl22anc 838	. . . . . . . . . . . . . . . 16 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) → (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = (ℝ_fld Σ_g (𝑓 ∘_f · 𝑓)))
24		inidm 4190	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐼 ∩ 𝐼) = 𝐼
25		eqidd 2730	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) ∧ 𝑥 ∈ 𝐼) → (𝑓‘𝑥) = (𝑓‘𝑥))
26	17, 17, 19, 19, 24, 25, 25	offval 7662	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) → (𝑓 ∘_f · 𝑓) = (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥) · (𝑓‘𝑥))))
27	16	ffvelcdmda 7056	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) ∧ 𝑥 ∈ 𝐼) → (𝑓‘𝑥) ∈ ℝ)
28	27, 27	remulcld 11204	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) ∧ 𝑥 ∈ 𝐼) → ((𝑓‘𝑥) · (𝑓‘𝑥)) ∈ ℝ)
29	26, 28	fmpt3d 7088	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) → (𝑓 ∘_f · 𝑓):𝐼⟶ℝ)
30		ovexd 7422	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) → (𝑓 ∘_f · 𝑓) ∈ V)
31	29	ffund 6692	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) → Fun (𝑓 ∘_f · 𝑓))
32	6, 11, 4	frlmbasfsupp 21667	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) → 𝑓 finSupp 0)
33		0red 11177	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) → 0 ∈ ℝ)
34		simpr 484	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℝ)
35	34	recnd 11202	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℂ)
36	35	mul02d 11372	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) ∧ 𝑥 ∈ ℝ) → (0 · 𝑥) = 0)
37	19, 33, 16, 16, 36	suppofss1d 8183	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) → ((𝑓 ∘_f · 𝑓) supp 0) ⊆ (𝑓 supp 0))
38		fsuppsssupp 9332	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑓 ∘_f · 𝑓) ∈ V ∧ Fun (𝑓 ∘_f · 𝑓)) ∧ (𝑓 finSupp 0 ∧ ((𝑓 ∘_f · 𝑓) supp 0) ⊆ (𝑓 supp 0))) → (𝑓 ∘_f · 𝑓) finSupp 0)
39	30, 31, 32, 37, 38	syl22anc 838	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) → (𝑓 ∘_f · 𝑓) finSupp 0)
40		regsumsupp 21531	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑓 ∘_f · 𝑓):𝐼⟶ℝ ∧ (𝑓 ∘_f · 𝑓) finSupp 0 ∧ 𝐼 ∈ 𝑉) → (ℝ_fld Σ_g (𝑓 ∘_f · 𝑓)) = Σ𝑥 ∈ ((𝑓 ∘_f · 𝑓) supp 0)((𝑓 ∘_f · 𝑓)‘𝑥))
41	29, 39, 19, 40	syl3anc 1373	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) → (ℝ_fld Σ_g (𝑓 ∘_f · 𝑓)) = Σ𝑥 ∈ ((𝑓 ∘_f · 𝑓) supp 0)((𝑓 ∘_f · 𝑓)‘𝑥))
42		suppssdm 8156	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑓 supp 0) ⊆ dom 𝑓
43	42, 16	fssdm 6707	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) → (𝑓 supp 0) ⊆ 𝐼)
44	37, 43	sstrd 3957	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) → ((𝑓 ∘_f · 𝑓) supp 0) ⊆ 𝐼)
45	44	sselda 3946	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) ∧ 𝑥 ∈ ((𝑓 ∘_f · 𝑓) supp 0)) → 𝑥 ∈ 𝐼)
46	17, 17, 19, 19, 24, 25, 25	ofval 7664	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) ∧ 𝑥 ∈ 𝐼) → ((𝑓 ∘_f · 𝑓)‘𝑥) = ((𝑓‘𝑥) · (𝑓‘𝑥)))
47	45, 46	syldan 591	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) ∧ 𝑥 ∈ ((𝑓 ∘_f · 𝑓) supp 0)) → ((𝑓 ∘_f · 𝑓)‘𝑥) = ((𝑓‘𝑥) · (𝑓‘𝑥)))
48	47	sumeq2dv 15668	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) → Σ𝑥 ∈ ((𝑓 ∘_f · 𝑓) supp 0)((𝑓 ∘_f · 𝑓)‘𝑥) = Σ𝑥 ∈ ((𝑓 ∘_f · 𝑓) supp 0)((𝑓‘𝑥) · (𝑓‘𝑥)))
49	41, 48	eqtrd 2764	. . . . . . . . . . . . . . . 16 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) → (ℝ_fld Σ_g (𝑓 ∘_f · 𝑓)) = Σ𝑥 ∈ ((𝑓 ∘_f · 𝑓) supp 0)((𝑓‘𝑥) · (𝑓‘𝑥)))
50	23, 49	eqtrd 2764	. . . . . . . . . . . . . . 15 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) → (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = Σ𝑥 ∈ ((𝑓 ∘_f · 𝑓) supp 0)((𝑓‘𝑥) · (𝑓‘𝑥)))
51	50	3adant3 1132	. . . . . . . . . . . . . 14 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) → (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = Σ𝑥 ∈ ((𝑓 ∘_f · 𝑓) supp 0)((𝑓‘𝑥) · (𝑓‘𝑥)))
52		simp3 1138	. . . . . . . . . . . . . 14 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) → (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0)
53	51, 52	eqtr3d 2766	. . . . . . . . . . . . 13 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) → Σ𝑥 ∈ ((𝑓 ∘_f · 𝑓) supp 0)((𝑓‘𝑥) · (𝑓‘𝑥)) = 0)
54	32	fsuppimpd 9320	. . . . . . . . . . . . . . . 16 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) → (𝑓 supp 0) ∈ Fin)
55	54, 37	ssfid 9212	. . . . . . . . . . . . . . 15 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) → ((𝑓 ∘_f · 𝑓) supp 0) ∈ Fin)
56	45, 28	syldan 591	. . . . . . . . . . . . . . 15 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) ∧ 𝑥 ∈ ((𝑓 ∘_f · 𝑓) supp 0)) → ((𝑓‘𝑥) · (𝑓‘𝑥)) ∈ ℝ)
57	27	msqge0d 11746	. . . . . . . . . . . . . . . 16 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) ∧ 𝑥 ∈ 𝐼) → 0 ≤ ((𝑓‘𝑥) · (𝑓‘𝑥)))
58	45, 57	syldan 591	. . . . . . . . . . . . . . 15 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) ∧ 𝑥 ∈ ((𝑓 ∘_f · 𝑓) supp 0)) → 0 ≤ ((𝑓‘𝑥) · (𝑓‘𝑥)))
59	55, 56, 58	fsum00 15764	. . . . . . . . . . . . . 14 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) → (Σ𝑥 ∈ ((𝑓 ∘_f · 𝑓) supp 0)((𝑓‘𝑥) · (𝑓‘𝑥)) = 0 ↔ ∀𝑥 ∈ ((𝑓 ∘_f · 𝑓) supp 0)((𝑓‘𝑥) · (𝑓‘𝑥)) = 0))
60	59	3adant3 1132	. . . . . . . . . . . . 13 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) → (Σ𝑥 ∈ ((𝑓 ∘_f · 𝑓) supp 0)((𝑓‘𝑥) · (𝑓‘𝑥)) = 0 ↔ ∀𝑥 ∈ ((𝑓 ∘_f · 𝑓) supp 0)((𝑓‘𝑥) · (𝑓‘𝑥)) = 0))
61	53, 60	mpbid 232	. . . . . . . . . . . 12 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) → ∀𝑥 ∈ ((𝑓 ∘_f · 𝑓) supp 0)((𝑓‘𝑥) · (𝑓‘𝑥)) = 0)
62	61	r19.21bi 3229	. . . . . . . . . . 11 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ ((𝑓 ∘_f · 𝑓) supp 0)) → ((𝑓‘𝑥) · (𝑓‘𝑥)) = 0)
63	62	adantlr 715	. . . . . . . . . 10 ⊢ ((((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼) ∧ 𝑥 ∈ ((𝑓 ∘_f · 𝑓) supp 0)) → ((𝑓‘𝑥) · (𝑓‘𝑥)) = 0)
64	27	3adantl3 1169	. . . . . . . . . . . . 13 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼) → (𝑓‘𝑥) ∈ ℝ)
65	64	recnd 11202	. . . . . . . . . . . 12 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼) → (𝑓‘𝑥) ∈ ℂ)
66	65, 65	mul0ord 11826	. . . . . . . . . . 11 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼) → (((𝑓‘𝑥) · (𝑓‘𝑥)) = 0 ↔ ((𝑓‘𝑥) = 0 ∨ (𝑓‘𝑥) = 0)))
67	66	adantr 480	. . . . . . . . . 10 ⊢ ((((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼) ∧ 𝑥 ∈ ((𝑓 ∘_f · 𝑓) supp 0)) → (((𝑓‘𝑥) · (𝑓‘𝑥)) = 0 ↔ ((𝑓‘𝑥) = 0 ∨ (𝑓‘𝑥) = 0)))
68	63, 67	mpbid 232	. . . . . . . . 9 ⊢ ((((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼) ∧ 𝑥 ∈ ((𝑓 ∘_f · 𝑓) supp 0)) → ((𝑓‘𝑥) = 0 ∨ (𝑓‘𝑥) = 0))
69		oridm 904	. . . . . . . . 9 ⊢ (((𝑓‘𝑥) = 0 ∨ (𝑓‘𝑥) = 0) ↔ (𝑓‘𝑥) = 0)
70	68, 69	sylib 218	. . . . . . . 8 ⊢ ((((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼) ∧ 𝑥 ∈ ((𝑓 ∘_f · 𝑓) supp 0)) → (𝑓‘𝑥) = 0)
71	29	3adant3 1132	. . . . . . . . . . 11 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) → (𝑓 ∘_f · 𝑓):𝐼⟶ℝ)
72	71	adantr 480	. . . . . . . . . 10 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼) → (𝑓 ∘_f · 𝑓):𝐼⟶ℝ)
73		ssidd 3970	. . . . . . . . . 10 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼) → ((𝑓 ∘_f · 𝑓) supp 0) ⊆ ((𝑓 ∘_f · 𝑓) supp 0))
74		simpl1 1192	. . . . . . . . . 10 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼) → 𝐼 ∈ 𝑉)
75		0red 11177	. . . . . . . . . 10 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼) → 0 ∈ ℝ)
76	72, 73, 74, 75	suppssr 8174	. . . . . . . . 9 ⊢ ((((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼) ∧ 𝑥 ∈ (𝐼 ∖ ((𝑓 ∘_f · 𝑓) supp 0))) → ((𝑓 ∘_f · 𝑓)‘𝑥) = 0)
77	46	3adantl3 1169	. . . . . . . . . . . . 13 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼) → ((𝑓 ∘_f · 𝑓)‘𝑥) = ((𝑓‘𝑥) · (𝑓‘𝑥)))
78	77	eqeq1d 2731	. . . . . . . . . . . 12 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼) → (((𝑓 ∘_f · 𝑓)‘𝑥) = 0 ↔ ((𝑓‘𝑥) · (𝑓‘𝑥)) = 0))
79	78, 66	bitrd 279	. . . . . . . . . . 11 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼) → (((𝑓 ∘_f · 𝑓)‘𝑥) = 0 ↔ ((𝑓‘𝑥) = 0 ∨ (𝑓‘𝑥) = 0)))
80	79, 69	bitrdi 287	. . . . . . . . . 10 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼) → (((𝑓 ∘_f · 𝑓)‘𝑥) = 0 ↔ (𝑓‘𝑥) = 0))
81	80	biimpa 476	. . . . . . . . 9 ⊢ ((((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼) ∧ ((𝑓 ∘_f · 𝑓)‘𝑥) = 0) → (𝑓‘𝑥) = 0)
82	76, 81	syldan 591	. . . . . . . 8 ⊢ ((((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼) ∧ 𝑥 ∈ (𝐼 ∖ ((𝑓 ∘_f · 𝑓) supp 0))) → (𝑓‘𝑥) = 0)
83		undif 4445	. . . . . . . . . . . . 13 ⊢ (((𝑓 ∘_f · 𝑓) supp 0) ⊆ 𝐼 ↔ (((𝑓 ∘_f · 𝑓) supp 0) ∪ (𝐼 ∖ ((𝑓 ∘_f · 𝑓) supp 0))) = 𝐼)
84	44, 83	sylib 218	. . . . . . . . . . . 12 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) → (((𝑓 ∘_f · 𝑓) supp 0) ∪ (𝐼 ∖ ((𝑓 ∘_f · 𝑓) supp 0))) = 𝐼)
85	84	eleq2d 2814	. . . . . . . . . . 11 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) → (𝑥 ∈ (((𝑓 ∘_f · 𝑓) supp 0) ∪ (𝐼 ∖ ((𝑓 ∘_f · 𝑓) supp 0))) ↔ 𝑥 ∈ 𝐼))
86	85	3adant3 1132	. . . . . . . . . 10 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) → (𝑥 ∈ (((𝑓 ∘_f · 𝑓) supp 0) ∪ (𝐼 ∖ ((𝑓 ∘_f · 𝑓) supp 0))) ↔ 𝑥 ∈ 𝐼))
87	86	biimpar 477	. . . . . . . . 9 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼) → 𝑥 ∈ (((𝑓 ∘_f · 𝑓) supp 0) ∪ (𝐼 ∖ ((𝑓 ∘_f · 𝑓) supp 0))))
88		elun 4116	. . . . . . . . 9 ⊢ (𝑥 ∈ (((𝑓 ∘_f · 𝑓) supp 0) ∪ (𝐼 ∖ ((𝑓 ∘_f · 𝑓) supp 0))) ↔ (𝑥 ∈ ((𝑓 ∘_f · 𝑓) supp 0) ∨ 𝑥 ∈ (𝐼 ∖ ((𝑓 ∘_f · 𝑓) supp 0))))
89	87, 88	sylib 218	. . . . . . . 8 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼) → (𝑥 ∈ ((𝑓 ∘_f · 𝑓) supp 0) ∨ 𝑥 ∈ (𝐼 ∖ ((𝑓 ∘_f · 𝑓) supp 0))))
90	70, 82, 89	mpjaodan 960	. . . . . . 7 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼) → (𝑓‘𝑥) = 0)
91	90	ralrimiva 3125	. . . . . 6 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) → ∀𝑥 ∈ 𝐼 (𝑓‘𝑥) = 0)
92		fconstfv 7186	. . . . . . 7 ⊢ (𝑓:𝐼⟶{0} ↔ (𝑓 Fn 𝐼 ∧ ∀𝑥 ∈ 𝐼 (𝑓‘𝑥) = 0))
93		c0ex 11168	. . . . . . . 8 ⊢ 0 ∈ V
94	93	fconst2 7179	. . . . . . 7 ⊢ (𝑓:𝐼⟶{0} ↔ 𝑓 = (𝐼 × {0}))
95	92, 94	sylbb1 237	. . . . . 6 ⊢ ((𝑓 Fn 𝐼 ∧ ∀𝑥 ∈ 𝐼 (𝑓‘𝑥) = 0) → 𝑓 = (𝐼 × {0}))
96	18, 91, 95	syl2anc 584	. . . . 5 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) → 𝑓 = (𝐼 × {0}))
97		isfld 20649	. . . . . . . . . . 11 ⊢ (ℝ_fld ∈ Field ↔ (ℝ_fld ∈ DivRing ∧ ℝ_fld ∈ CRing))
98	13, 97	mpbi 230	. . . . . . . . . 10 ⊢ (ℝ_fld ∈ DivRing ∧ ℝ_fld ∈ CRing)
99	98	simpli 483	. . . . . . . . 9 ⊢ ℝ_fld ∈ DivRing
100		drngring 20645	. . . . . . . . 9 ⊢ (ℝ_fld ∈ DivRing → ℝ_fld ∈ Ring)
101	99, 100	ax-mp 5	. . . . . . . 8 ⊢ ℝ_fld ∈ Ring
102	6, 11	frlm0 21663	. . . . . . . 8 ⊢ ((ℝ_fld ∈ Ring ∧ 𝐼 ∈ 𝑉) → (𝐼 × {0}) = (0_g‘(ℝ_fld freeLMod 𝐼)))
103	101, 102	mpan 690	. . . . . . 7 ⊢ (𝐼 ∈ 𝑉 → (𝐼 × {0}) = (0_g‘(ℝ_fld freeLMod 𝐼)))
104	103, 15	eqtr3di 2779	. . . . . 6 ⊢ (𝐼 ∈ 𝑉 → (0_g‘(ℝ_fld freeLMod 𝐼)) = (𝑥 ∈ 𝐼 ↦ 0))
105	104	3ad2ant1 1133	. . . . 5 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) → (0_g‘(ℝ_fld freeLMod 𝐼)) = (𝑥 ∈ 𝐼 ↦ 0))
106	15, 96, 105	3eqtr4a 2790	. . . 4 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) → 𝑓 = (0_g‘(ℝ_fld freeLMod 𝐼)))
107		cjre 15105	. . . . 5 ⊢ (𝑥 ∈ ℝ → (∗‘𝑥) = 𝑥)
108	107	adantl 481	. . . 4 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ ℝ) → (∗‘𝑥) = 𝑥)
109		id 22	. . . 4 ⊢ (𝐼 ∈ 𝑉 → 𝐼 ∈ 𝑉)
110	6, 7, 8, 4, 9, 10, 11, 12, 14, 106, 108, 109	frlmphl 21690	. . 3 ⊢ (𝐼 ∈ 𝑉 → (ℝ_fld freeLMod 𝐼) ∈ PreHil)
111	6	frlmsca 21662	. . . . 5 ⊢ ((ℝ_fld ∈ Field ∧ 𝐼 ∈ 𝑉) → ℝ_fld = (Scalar‘(ℝ_fld freeLMod 𝐼)))
112	13, 111	mpan 690	. . . 4 ⊢ (𝐼 ∈ 𝑉 → ℝ_fld = (Scalar‘(ℝ_fld freeLMod 𝐼)))
113		df-refld 21514	. . . 4 ⊢ ℝ_fld = (ℂ_fld ↾_s ℝ)
114	112, 113	eqtr3di 2779	. . 3 ⊢ (𝐼 ∈ 𝑉 → (Scalar‘(ℝ_fld freeLMod 𝐼)) = (ℂ_fld ↾_s ℝ))
115		simpr1 1195	. . . 4 ⊢ ((𝐼 ∈ 𝑉 ∧ (𝑓 ∈ ℝ ∧ 𝑓 ∈ ℝ ∧ 0 ≤ 𝑓)) → 𝑓 ∈ ℝ)
116		simpr3 1197	. . . 4 ⊢ ((𝐼 ∈ 𝑉 ∧ (𝑓 ∈ ℝ ∧ 𝑓 ∈ ℝ ∧ 0 ≤ 𝑓)) → 0 ≤ 𝑓)
117	115, 116	resqrtcld 15384	. . 3 ⊢ ((𝐼 ∈ 𝑉 ∧ (𝑓 ∈ ℝ ∧ 𝑓 ∈ ℝ ∧ 0 ≤ 𝑓)) → (√‘𝑓) ∈ ℝ)
118	55, 56, 58	fsumge0 15761	. . . . 5 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) → 0 ≤ Σ𝑥 ∈ ((𝑓 ∘_f · 𝑓) supp 0)((𝑓‘𝑥) · (𝑓‘𝑥)))
119	118, 49	breqtrrd 5135	. . . 4 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) → 0 ≤ (ℝ_fld Σ_g (𝑓 ∘_f · 𝑓)))
120	119, 23	breqtrrd 5135	. . 3 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) → 0 ≤ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓))
121	3, 4, 5, 110, 114, 9, 117, 120	tcphcph 25137	. 2 ⊢ (𝐼 ∈ 𝑉 → (toℂPreHil‘(ℝ_fld freeLMod 𝐼)) ∈ ℂPreHil)
122	2, 121	eqeltrd 2828	1 ⊢ (𝐼 ∈ 𝑉 → 𝐻 ∈ ℂPreHil)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∨ wo 847 ∧ w3a 1086 = wceq 1540 ∈ wcel 2109 ∀wral 3044 Vcvv 3447 ∖ cdif 3911 ∪ cun 3912 ⊆ wss 3914 {csn 4589 class class class wbr 5107 ↦ cmpt 5188 × cxp 5636 Fun wfun 6505 Fn wfn 6506 ⟶wf 6507 ‘cfv 6511 (class class class)co 7387 ∘_f cof 7651 supp csupp 8139 finSupp cfsupp 9312 ℝcr 11067 0cc0 11068 · cmul 11073 ≤ cle 11209 ∗ccj 15062 Σcsu 15652 Basecbs 17179 ↾_s cress 17200 Scalarcsca 17223 ·_𝑖cip 17225 0_gc0g 17402 Σ_g cgsu 17403 Ringcrg 20142 CRingccrg 20143 DivRingcdr 20638 Fieldcfield 20639 ℂ_fldccnfld 21264 ℝ_fldcrefld 21513 freeLMod cfrlm 21655 ℂPreHilccph 25066 toℂPreHilctcph 25067 ℝ^crrx 25283

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-rep 5234 ax-sep 5251 ax-nul 5261 ax-pow 5320 ax-pr 5387 ax-un 7711 ax-inf2 9594 ax-cnex 11124 ax-resscn 11125 ax-1cn 11126 ax-icn 11127 ax-addcl 11128 ax-addrcl 11129 ax-mulcl 11130 ax-mulrcl 11131 ax-mulcom 11132 ax-addass 11133 ax-mulass 11134 ax-distr 11135 ax-i2m1 11136 ax-1ne0 11137 ax-1rid 11138 ax-rnegex 11139 ax-rrecex 11140 ax-cnre 11141 ax-pre-lttri 11142 ax-pre-lttrn 11143 ax-pre-ltadd 11144 ax-pre-mulgt0 11145 ax-pre-sup 11146 ax-addf 11147 ax-mulf 11148

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-rmo 3354 df-reu 3355 df-rab 3406 df-v 3449 df-sbc 3754 df-csb 3863 df-dif 3917 df-un 3919 df-in 3921 df-ss 3931 df-pss 3934 df-nul 4297 df-if 4489 df-pw 4565 df-sn 4590 df-pr 4592 df-tp 4594 df-op 4596 df-uni 4872 df-int 4911 df-iun 4957 df-br 5108 df-opab 5170 df-mpt 5189 df-tr 5215 df-id 5533 df-eprel 5538 df-po 5546 df-so 5547 df-fr 5591 df-se 5592 df-we 5593 df-xp 5644 df-rel 5645 df-cnv 5646 df-co 5647 df-dm 5648 df-rn 5649 df-res 5650 df-ima 5651 df-pred 6274 df-ord 6335 df-on 6336 df-lim 6337 df-suc 6338 df-iota 6464 df-fun 6513 df-fn 6514 df-f 6515 df-f1 6516 df-fo 6517 df-f1o 6518 df-fv 6519 df-isom 6520 df-riota 7344 df-ov 7390 df-oprab 7391 df-mpo 7392 df-of 7653 df-om 7843 df-1st 7968 df-2nd 7969 df-supp 8140 df-tpos 8205 df-frecs 8260 df-wrecs 8291 df-recs 8340 df-rdg 8378 df-1o 8434 df-er 8671 df-map 8801 df-ixp 8871 df-en 8919 df-dom 8920 df-sdom 8921 df-fin 8922 df-fsupp 9313 df-sup 9393 df-inf 9394 df-oi 9463 df-card 9892 df-pnf 11210 df-mnf 11211 df-xr 11212 df-ltxr 11213 df-le 11214 df-sub 11407 df-neg 11408 df-div 11836 df-nn 12187 df-2 12249 df-3 12250 df-4 12251 df-5 12252 df-6 12253 df-7 12254 df-8 12255 df-9 12256 df-n0 12443 df-z 12530 df-dec 12650 df-uz 12794 df-q 12908 df-rp 12952 df-xneg 13072 df-xadd 13073 df-xmul 13074 df-ico 13312 df-fz 13469 df-fzo 13616 df-seq 13967 df-exp 14027 df-hash 14296 df-cj 15065 df-re 15066 df-im 15067 df-sqrt 15201 df-abs 15202 df-clim 15454 df-sum 15653 df-struct 17117 df-sets 17134 df-slot 17152 df-ndx 17164 df-base 17180 df-ress 17201 df-plusg 17233 df-mulr 17234 df-starv 17235 df-sca 17236 df-vsca 17237 df-ip 17238 df-tset 17239 df-ple 17240 df-ds 17242 df-unif 17243 df-hom 17244 df-cco 17245 df-rest 17385 df-topn 17386 df-0g 17404 df-gsum 17405 df-topgen 17406 df-prds 17410 df-pws 17412 df-mgm 18567 df-sgrp 18646 df-mnd 18662 df-mhm 18710 df-submnd 18711 df-grp 18868 df-minusg 18869 df-sbg 18870 df-subg 19055 df-ghm 19145 df-cntz 19249 df-cmn 19712 df-abl 19713 df-mgp 20050 df-rng 20062 df-ur 20091 df-ring 20144 df-cring 20145 df-oppr 20246 df-dvdsr 20266 df-unit 20267 df-invr 20297 df-dvr 20310 df-rhm 20381 df-subrng 20455 df-subrg 20479 df-drng 20640 df-field 20641 df-abv 20718 df-staf 20748 df-srng 20749 df-lmod 20768 df-lss 20838 df-lmhm 20929 df-lvec 21010 df-sra 21080 df-rgmod 21081 df-psmet 21256 df-xmet 21257 df-met 21258 df-bl 21259 df-mopn 21260 df-cnfld 21265 df-refld 21514 df-phl 21535 df-dsmm 21641 df-frlm 21656 df-top 22781 df-topon 22798 df-topsp 22820 df-bases 22833 df-xms 24208 df-ms 24209 df-nm 24470 df-ngp 24471 df-tng 24472 df-nrg 24473 df-nlm 24474 df-clm 24963 df-cph 25068 df-tcph 25069 df-rrx 25285

This theorem is referenced by: rrxngp 46283

W3C validator