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 25434

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 25429	. 2 ⊢ (𝐼 ∈ 𝑉 → 𝐻 = (toℂPreHil‘(ℝ_fld freeLMod 𝐼)))
3		eqid 2761	. . 3 ⊢ (toℂPreHil‘(ℝ_fld freeLMod 𝐼)) = (toℂPreHil‘(ℝ_fld freeLMod 𝐼))
4		eqid 2761	. . 3 ⊢ (Base‘(ℝ_fld freeLMod 𝐼)) = (Base‘(ℝ_fld freeLMod 𝐼))
5		eqid 2761	. . 3 ⊢ (Scalar‘(ℝ_fld freeLMod 𝐼)) = (Scalar‘(ℝ_fld freeLMod 𝐼))
6		eqid 2761	. . . 4 ⊢ (ℝ_fld freeLMod 𝐼) = (ℝ_fld freeLMod 𝐼)
7		rebase 21638	. . . 4 ⊢ ℝ = (Base‘ℝ_fld)
8		remulr 21643	. . . 4 ⊢ · = (._r‘ℝ_fld)
9		eqid 2761	. . . 4 ⊢ (·_𝑖‘(ℝ_fld freeLMod 𝐼)) = (·_𝑖‘(ℝ_fld freeLMod 𝐼))
10		eqid 2761	. . . 4 ⊢ (0_g‘(ℝ_fld freeLMod 𝐼)) = (0_g‘(ℝ_fld freeLMod 𝐼))
11		re0g 21644	. . . 4 ⊢ 0 = (0_g‘ℝ_fld)
12		refldcj 21652	. . . 4 ⊢ ∗ = (*_𝑟‘ℝ_fld)
13		refld 21651	. . . . 5 ⊢ ℝ_fld ∈ Field
14	13	a1i 11	. . . 4 ⊢ (𝐼 ∈ 𝑉 → ℝ_fld ∈ Field)
15		fconstmpt 5707	. . . . 5 ⊢ (𝐼 × {0}) = (𝑥 ∈ 𝐼 ↦ 0)
16	6, 7, 4	frlmbasf 21792	. . . . . . . 8 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) → 𝑓:𝐼⟶ℝ)
17	16	ffnd 6688	. . . . . . 7 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) → 𝑓 Fn 𝐼)
18	17	3adant3 1144	. . . . . 6 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) → 𝑓 Fn 𝐼)
19		simpl 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) → 𝐼 ∈ 𝑉)
20	13	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) → ℝ_fld ∈ Field)
21		simpr 488	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) → 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)))
22	6, 7, 8, 4, 9	frlmipval 21811	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐼 ∈ 𝑉 ∧ ℝ_fld ∈ Field) ∧ (𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)))) → (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = (ℝ_fld Σ_g (𝑓 ∘_f · 𝑓)))
23	19, 20, 21, 21, 22	syl22anc 849	. . . . . . . . . . . . . . . 16 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) → (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = (ℝ_fld Σ_g (𝑓 ∘_f · 𝑓)))
24		inidm 4178	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐼 ∩ 𝐼) = 𝐼
25		eqidd 2762	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) ∧ 𝑥 ∈ 𝐼) → (𝑓‘𝑥) = (𝑓‘𝑥))
26	17, 17, 19, 19, 24, 25, 25	offval 7665	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) → (𝑓 ∘_f · 𝑓) = (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥) · (𝑓‘𝑥))))
27	16	ffvelcdmda 7061	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) ∧ 𝑥 ∈ 𝐼) → (𝑓‘𝑥) ∈ ℝ)
28	27, 27	remulcld 11209	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) ∧ 𝑥 ∈ 𝐼) → ((𝑓‘𝑥) · (𝑓‘𝑥)) ∈ ℝ)
29	26, 28	fmpt3d 7093	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) → (𝑓 ∘_f · 𝑓):𝐼⟶ℝ)
30		ovexd 7427	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) → (𝑓 ∘_f · 𝑓) ∈ V)
31	29	ffund 6692	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) → Fun (𝑓 ∘_f · 𝑓))
32	6, 11, 4	frlmbasfsupp 21790	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) → 𝑓 finSupp 0)
33		0red 11181	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) → 0 ∈ ℝ)
34		simpr 488	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℝ)
35	34	recnd 11207	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℂ)
36	35	mul02d 11378	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) ∧ 𝑥 ∈ ℝ) → (0 · 𝑥) = 0)
37	19, 33, 16, 16, 36	suppofss1d 8179	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) → ((𝑓 ∘_f · 𝑓) supp 0) ⊆ (𝑓 supp 0))
38		fsuppsssupp 9324	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑓 ∘_f · 𝑓) ∈ V ∧ Fun (𝑓 ∘_f · 𝑓)) ∧ (𝑓 finSupp 0 ∧ ((𝑓 ∘_f · 𝑓) supp 0) ⊆ (𝑓 supp 0))) → (𝑓 ∘_f · 𝑓) finSupp 0)
39	30, 31, 32, 37, 38	syl22anc 849	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) → (𝑓 ∘_f · 𝑓) finSupp 0)
40		regsumsupp 21654	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑓 ∘_f · 𝑓):𝐼⟶ℝ ∧ (𝑓 ∘_f · 𝑓) finSupp 0 ∧ 𝐼 ∈ 𝑉) → (ℝ_fld Σ_g (𝑓 ∘_f · 𝑓)) = Σ𝑥 ∈ ((𝑓 ∘_f · 𝑓) supp 0)((𝑓 ∘_f · 𝑓)‘𝑥))
41	29, 39, 19, 40	syl3anc 1389	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) → (ℝ_fld Σ_g (𝑓 ∘_f · 𝑓)) = Σ𝑥 ∈ ((𝑓 ∘_f · 𝑓) supp 0)((𝑓 ∘_f · 𝑓)‘𝑥))
42		suppssdm 8152	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑓 supp 0) ⊆ dom 𝑓
43	42, 16	fssdm 6707	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) → (𝑓 supp 0) ⊆ 𝐼)
44	37, 43	sstrd 3946	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) → ((𝑓 ∘_f · 𝑓) supp 0) ⊆ 𝐼)
45	44	sselda 3936	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) ∧ 𝑥 ∈ ((𝑓 ∘_f · 𝑓) supp 0)) → 𝑥 ∈ 𝐼)
46	17, 17, 19, 19, 24, 25, 25	ofval 7667	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) ∧ 𝑥 ∈ 𝐼) → ((𝑓 ∘_f · 𝑓)‘𝑥) = ((𝑓‘𝑥) · (𝑓‘𝑥)))
47	45, 46	syldan 600	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) ∧ 𝑥 ∈ ((𝑓 ∘_f · 𝑓) supp 0)) → ((𝑓 ∘_f · 𝑓)‘𝑥) = ((𝑓‘𝑥) · (𝑓‘𝑥)))
48	47	sumeq2dv 15712	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) → Σ𝑥 ∈ ((𝑓 ∘_f · 𝑓) supp 0)((𝑓 ∘_f · 𝑓)‘𝑥) = Σ𝑥 ∈ ((𝑓 ∘_f · 𝑓) supp 0)((𝑓‘𝑥) · (𝑓‘𝑥)))
49	41, 48	eqtrd 2796	. . . . . . . . . . . . . . . 16 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) → (ℝ_fld Σ_g (𝑓 ∘_f · 𝑓)) = Σ𝑥 ∈ ((𝑓 ∘_f · 𝑓) supp 0)((𝑓‘𝑥) · (𝑓‘𝑥)))
50	23, 49	eqtrd 2796	. . . . . . . . . . . . . . 15 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) → (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = Σ𝑥 ∈ ((𝑓 ∘_f · 𝑓) supp 0)((𝑓‘𝑥) · (𝑓‘𝑥)))
51	50	3adant3 1144	. . . . . . . . . . . . . 14 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) → (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = Σ𝑥 ∈ ((𝑓 ∘_f · 𝑓) supp 0)((𝑓‘𝑥) · (𝑓‘𝑥)))
52		simp3 1150	. . . . . . . . . . . . . 14 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) → (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0)
53	51, 52	eqtr3d 2798	. . . . . . . . . . . . 13 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) → Σ𝑥 ∈ ((𝑓 ∘_f · 𝑓) supp 0)((𝑓‘𝑥) · (𝑓‘𝑥)) = 0)
54	32	fsuppimpd 9312	. . . . . . . . . . . . . . . 16 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) → (𝑓 supp 0) ∈ Fin)
55	54, 37	ssfid 9209	. . . . . . . . . . . . . . 15 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) → ((𝑓 ∘_f · 𝑓) supp 0) ∈ Fin)
56	45, 28	syldan 600	. . . . . . . . . . . . . . 15 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) ∧ 𝑥 ∈ ((𝑓 ∘_f · 𝑓) supp 0)) → ((𝑓‘𝑥) · (𝑓‘𝑥)) ∈ ℝ)
57	27	msqge0d 11752	. . . . . . . . . . . . . . . 16 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) ∧ 𝑥 ∈ 𝐼) → 0 ≤ ((𝑓‘𝑥) · (𝑓‘𝑥)))
58	45, 57	syldan 600	. . . . . . . . . . . . . . 15 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) ∧ 𝑥 ∈ ((𝑓 ∘_f · 𝑓) supp 0)) → 0 ≤ ((𝑓‘𝑥) · (𝑓‘𝑥)))
59	55, 56, 58	fsum00 15809	. . . . . . . . . . . . . 14 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) → (Σ𝑥 ∈ ((𝑓 ∘_f · 𝑓) supp 0)((𝑓‘𝑥) · (𝑓‘𝑥)) = 0 ↔ ∀𝑥 ∈ ((𝑓 ∘_f · 𝑓) supp 0)((𝑓‘𝑥) · (𝑓‘𝑥)) = 0))
60	59	3adant3 1144	. . . . . . . . . . . . 13 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) → (Σ𝑥 ∈ ((𝑓 ∘_f · 𝑓) supp 0)((𝑓‘𝑥) · (𝑓‘𝑥)) = 0 ↔ ∀𝑥 ∈ ((𝑓 ∘_f · 𝑓) supp 0)((𝑓‘𝑥) · (𝑓‘𝑥)) = 0))
61	53, 60	mpbid 234	. . . . . . . . . . . 12 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) → ∀𝑥 ∈ ((𝑓 ∘_f · 𝑓) supp 0)((𝑓‘𝑥) · (𝑓‘𝑥)) = 0)
62	61	r19.21bi 3253	. . . . . . . . . . 11 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ ((𝑓 ∘_f · 𝑓) supp 0)) → ((𝑓‘𝑥) · (𝑓‘𝑥)) = 0)
63	62	adantlr 725	. . . . . . . . . 10 ⊢ ((((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼) ∧ 𝑥 ∈ ((𝑓 ∘_f · 𝑓) supp 0)) → ((𝑓‘𝑥) · (𝑓‘𝑥)) = 0)
64	27	3adantl3 1181	. . . . . . . . . . . . 13 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼) → (𝑓‘𝑥) ∈ ℝ)
65	64	recnd 11207	. . . . . . . . . . . 12 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼) → (𝑓‘𝑥) ∈ ℂ)
66	65, 65	mul0ord 11832	. . . . . . . . . . 11 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼) → (((𝑓‘𝑥) · (𝑓‘𝑥)) = 0 ↔ ((𝑓‘𝑥) = 0 ∨ (𝑓‘𝑥) = 0)))
67	66	adantr 484	. . . . . . . . . 10 ⊢ ((((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼) ∧ 𝑥 ∈ ((𝑓 ∘_f · 𝑓) supp 0)) → (((𝑓‘𝑥) · (𝑓‘𝑥)) = 0 ↔ ((𝑓‘𝑥) = 0 ∨ (𝑓‘𝑥) = 0)))
68	63, 67	mpbid 234	. . . . . . . . 9 ⊢ ((((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼) ∧ 𝑥 ∈ ((𝑓 ∘_f · 𝑓) supp 0)) → ((𝑓‘𝑥) = 0 ∨ (𝑓‘𝑥) = 0))
69		oridm 915	. . . . . . . . 9 ⊢ (((𝑓‘𝑥) = 0 ∨ (𝑓‘𝑥) = 0) ↔ (𝑓‘𝑥) = 0)
70	68, 69	sylib 220	. . . . . . . 8 ⊢ ((((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼) ∧ 𝑥 ∈ ((𝑓 ∘_f · 𝑓) supp 0)) → (𝑓‘𝑥) = 0)
71	29	3adant3 1144	. . . . . . . . . . 11 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) → (𝑓 ∘_f · 𝑓):𝐼⟶ℝ)
72	71	adantr 484	. . . . . . . . . 10 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼) → (𝑓 ∘_f · 𝑓):𝐼⟶ℝ)
73		ssidd 3959	. . . . . . . . . 10 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼) → ((𝑓 ∘_f · 𝑓) supp 0) ⊆ ((𝑓 ∘_f · 𝑓) supp 0))
74		simpl1 1204	. . . . . . . . . 10 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼) → 𝐼 ∈ 𝑉)
75		0red 11181	. . . . . . . . . 10 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼) → 0 ∈ ℝ)
76	72, 73, 74, 75	suppssr 8170	. . . . . . . . 9 ⊢ ((((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼) ∧ 𝑥 ∈ (𝐼 ∖ ((𝑓 ∘_f · 𝑓) supp 0))) → ((𝑓 ∘_f · 𝑓)‘𝑥) = 0)
77	46	3adantl3 1181	. . . . . . . . . . . . 13 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼) → ((𝑓 ∘_f · 𝑓)‘𝑥) = ((𝑓‘𝑥) · (𝑓‘𝑥)))
78	77	eqeq1d 2763	. . . . . . . . . . . 12 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼) → (((𝑓 ∘_f · 𝑓)‘𝑥) = 0 ↔ ((𝑓‘𝑥) · (𝑓‘𝑥)) = 0))
79	78, 66	bitrd 281	. . . . . . . . . . 11 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼) → (((𝑓 ∘_f · 𝑓)‘𝑥) = 0 ↔ ((𝑓‘𝑥) = 0 ∨ (𝑓‘𝑥) = 0)))
80	79, 69	bitrdi 289	. . . . . . . . . 10 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼) → (((𝑓 ∘_f · 𝑓)‘𝑥) = 0 ↔ (𝑓‘𝑥) = 0))
81	80	biimpa 480	. . . . . . . . 9 ⊢ ((((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼) ∧ ((𝑓 ∘_f · 𝑓)‘𝑥) = 0) → (𝑓‘𝑥) = 0)
82	76, 81	syldan 600	. . . . . . . 8 ⊢ ((((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼) ∧ 𝑥 ∈ (𝐼 ∖ ((𝑓 ∘_f · 𝑓) supp 0))) → (𝑓‘𝑥) = 0)
83		undif 4435	. . . . . . . . . . . . 13 ⊢ (((𝑓 ∘_f · 𝑓) supp 0) ⊆ 𝐼 ↔ (((𝑓 ∘_f · 𝑓) supp 0) ∪ (𝐼 ∖ ((𝑓 ∘_f · 𝑓) supp 0))) = 𝐼)
84	44, 83	sylib 220	. . . . . . . . . . . 12 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) → (((𝑓 ∘_f · 𝑓) supp 0) ∪ (𝐼 ∖ ((𝑓 ∘_f · 𝑓) supp 0))) = 𝐼)
85	84	eleq2d 2847	. . . . . . . . . . 11 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) → (𝑥 ∈ (((𝑓 ∘_f · 𝑓) supp 0) ∪ (𝐼 ∖ ((𝑓 ∘_f · 𝑓) supp 0))) ↔ 𝑥 ∈ 𝐼))
86	85	3adant3 1144	. . . . . . . . . 10 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) → (𝑥 ∈ (((𝑓 ∘_f · 𝑓) supp 0) ∪ (𝐼 ∖ ((𝑓 ∘_f · 𝑓) supp 0))) ↔ 𝑥 ∈ 𝐼))
87	86	biimpar 481	. . . . . . . . 9 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼) → 𝑥 ∈ (((𝑓 ∘_f · 𝑓) supp 0) ∪ (𝐼 ∖ ((𝑓 ∘_f · 𝑓) supp 0))))
88		elun 4106	. . . . . . . . 9 ⊢ (𝑥 ∈ (((𝑓 ∘_f · 𝑓) supp 0) ∪ (𝐼 ∖ ((𝑓 ∘_f · 𝑓) supp 0))) ↔ (𝑥 ∈ ((𝑓 ∘_f · 𝑓) supp 0) ∨ 𝑥 ∈ (𝐼 ∖ ((𝑓 ∘_f · 𝑓) supp 0))))
89	87, 88	sylib 220	. . . . . . . 8 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼) → (𝑥 ∈ ((𝑓 ∘_f · 𝑓) supp 0) ∨ 𝑥 ∈ (𝐼 ∖ ((𝑓 ∘_f · 𝑓) supp 0))))
90	70, 82, 89	mpjaodan 971	. . . . . . 7 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼) → (𝑓‘𝑥) = 0)
91	90	ralrimiva 3153	. . . . . 6 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) → ∀𝑥 ∈ 𝐼 (𝑓‘𝑥) = 0)
92		fconstfv 7192	. . . . . . 7 ⊢ (𝑓:𝐼⟶{0} ↔ (𝑓 Fn 𝐼 ∧ ∀𝑥 ∈ 𝐼 (𝑓‘𝑥) = 0))
93		c0ex 11170	. . . . . . . 8 ⊢ 0 ∈ V
94	93	fconst2 7185	. . . . . . 7 ⊢ (𝑓:𝐼⟶{0} ↔ 𝑓 = (𝐼 × {0}))
95	92, 94	sylbb1 239	. . . . . 6 ⊢ ((𝑓 Fn 𝐼 ∧ ∀𝑥 ∈ 𝐼 (𝑓‘𝑥) = 0) → 𝑓 = (𝐼 × {0}))
96	18, 91, 95	syl2anc 593	. . . . 5 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) → 𝑓 = (𝐼 × {0}))
97		isfld 20769	. . . . . . . . . . 11 ⊢ (ℝ_fld ∈ Field ↔ (ℝ_fld ∈ DivRing ∧ ℝ_fld ∈ CRing))
98	13, 97	mpbi 232	. . . . . . . . . 10 ⊢ (ℝ_fld ∈ DivRing ∧ ℝ_fld ∈ CRing)
99	98	simpli 487	. . . . . . . . 9 ⊢ ℝ_fld ∈ DivRing
100		drngring 20765	. . . . . . . . 9 ⊢ (ℝ_fld ∈ DivRing → ℝ_fld ∈ Ring)
101	99, 100	ax-mp 5	. . . . . . . 8 ⊢ ℝ_fld ∈ Ring
102	6, 11	frlm0 21786	. . . . . . . 8 ⊢ ((ℝ_fld ∈ Ring ∧ 𝐼 ∈ 𝑉) → (𝐼 × {0}) = (0_g‘(ℝ_fld freeLMod 𝐼)))
103	101, 102	mpan 700	. . . . . . 7 ⊢ (𝐼 ∈ 𝑉 → (𝐼 × {0}) = (0_g‘(ℝ_fld freeLMod 𝐼)))
104	103, 15	eqtr3di 2811	. . . . . 6 ⊢ (𝐼 ∈ 𝑉 → (0_g‘(ℝ_fld freeLMod 𝐼)) = (𝑥 ∈ 𝐼 ↦ 0))
105	104	3ad2ant1 1145	. . . . 5 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) → (0_g‘(ℝ_fld freeLMod 𝐼)) = (𝑥 ∈ 𝐼 ↦ 0))
106	15, 96, 105	3eqtr4a 2822	. . . 4 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) → 𝑓 = (0_g‘(ℝ_fld freeLMod 𝐼)))
107		cjre 15149	. . . . 5 ⊢ (𝑥 ∈ ℝ → (∗‘𝑥) = 𝑥)
108	107	adantl 485	. . . 4 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ ℝ) → (∗‘𝑥) = 𝑥)
109		id 22	. . . 4 ⊢ (𝐼 ∈ 𝑉 → 𝐼 ∈ 𝑉)
110	6, 7, 8, 4, 9, 10, 11, 12, 14, 106, 108, 109	frlmphl 21813	. . 3 ⊢ (𝐼 ∈ 𝑉 → (ℝ_fld freeLMod 𝐼) ∈ PreHil)
111	6	frlmsca 21785	. . . . 5 ⊢ ((ℝ_fld ∈ Field ∧ 𝐼 ∈ 𝑉) → ℝ_fld = (Scalar‘(ℝ_fld freeLMod 𝐼)))
112	13, 111	mpan 700	. . . 4 ⊢ (𝐼 ∈ 𝑉 → ℝ_fld = (Scalar‘(ℝ_fld freeLMod 𝐼)))
113		df-refld 21637	. . . 4 ⊢ ℝ_fld = (ℂ_fld ↾_s ℝ)
114	112, 113	eqtr3di 2811	. . 3 ⊢ (𝐼 ∈ 𝑉 → (Scalar‘(ℝ_fld freeLMod 𝐼)) = (ℂ_fld ↾_s ℝ))
115		simpr1 1207	. . . 4 ⊢ ((𝐼 ∈ 𝑉 ∧ (𝑓 ∈ ℝ ∧ 𝑓 ∈ ℝ ∧ 0 ≤ 𝑓)) → 𝑓 ∈ ℝ)
116		simpr3 1209	. . . 4 ⊢ ((𝐼 ∈ 𝑉 ∧ (𝑓 ∈ ℝ ∧ 𝑓 ∈ ℝ ∧ 0 ≤ 𝑓)) → 0 ≤ 𝑓)
117	115, 116	resqrtcld 15428	. . 3 ⊢ ((𝐼 ∈ 𝑉 ∧ (𝑓 ∈ ℝ ∧ 𝑓 ∈ ℝ ∧ 0 ≤ 𝑓)) → (√‘𝑓) ∈ ℝ)
118	55, 56, 58	fsumge0 15806	. . . . 5 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) → 0 ≤ Σ𝑥 ∈ ((𝑓 ∘_f · 𝑓) supp 0)((𝑓‘𝑥) · (𝑓‘𝑥)))
119	118, 49	breqtrrd 5127	. . . 4 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) → 0 ≤ (ℝ_fld Σ_g (𝑓 ∘_f · 𝑓)))
120	119, 23	breqtrrd 5127	. . 3 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) → 0 ≤ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓))
121	3, 4, 5, 110, 114, 9, 117, 120	tcphcph 25279	. 2 ⊢ (𝐼 ∈ 𝑉 → (toℂPreHil‘(ℝ_fld freeLMod 𝐼)) ∈ ℂPreHil)
122	2, 121	eqeltrd 2861	1 ⊢ (𝐼 ∈ 𝑉 → 𝐻 ∈ ℂPreHil)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 208 ∧ wa 399 ∨ wo 858 ∧ w3a 1097 = wceq 1559 ∈ wcel 2141 ∀wral 3075 Vcvv 3453 ∖ cdif 3901 ∪ cun 3902 ⊆ wss 3904 {csn 4581 class class class wbr 5099 ↦ cmpt 5180 × cxp 5643 Fun wfun 6511 Fn wfn 6512 ⟶wf 6513 ‘cfv 6517 (class class class)co 7392 ∘_f cof 7654 supp csupp 8135 finSupp cfsupp 9304 ℝcr 11069 0cc0 11070 · cmul 11075 ≤ cle 11214 ∗ccj 15106 Σcsu 15696 Basecbs 17228 ↾_s cress 17249 Scalarcsca 17272 ·_𝑖cip 17274 0_gc0g 17451 Σ_g cgsu 17452 Ringcrg 20262 CRingccrg 20263 DivRingcdr 20758 Fieldcfield 20759 ℂ_fldccnfld 21404 ℝ_fldcrefld 21636 freeLMod cfrlm 21778 ℂPreHilccph 25208 toℂPreHilctcph 25209 ℝ^crrx 25425

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1814 ax-4 1828 ax-5 1929 ax-6 1986 ax-7 2027 ax-8 2143 ax-9 2151 ax-10 2174 ax-11 2190 ax-12 2211 ax-ext 2733 ax-rep 5226 ax-sep 5245 ax-nul 5255 ax-pow 5321 ax-pr 5389 ax-un 7714 ax-inf2 9593 ax-cnex 11126 ax-resscn 11127 ax-1cn 11128 ax-icn 11129 ax-addcl 11130 ax-addrcl 11131 ax-mulcl 11132 ax-mulrcl 11133 ax-mulcom 11134 ax-addass 11135 ax-mulass 11136 ax-distr 11137 ax-i2m1 11138 ax-1ne0 11139 ax-1rid 11140 ax-rnegex 11141 ax-rrecex 11142 ax-cnre 11143 ax-pre-lttri 11144 ax-pre-lttrn 11145 ax-pre-ltadd 11146 ax-pre-mulgt0 11147 ax-pre-sup 11148 ax-addf 11149 ax-mulf 11150

This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3or 1098 df-3an 1099 df-tru 1562 df-fal 1572 df-ex 1799 df-nf 1803 df-sb 2090 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3061 df-ral 3076 df-rex 3086 df-rmo 3366 df-reu 3367 df-rab 3414 df-v 3455 df-sbc 3745 df-csb 3853 df-dif 3907 df-un 3909 df-in 3911 df-ss 3921 df-pss 3924 df-nul 4286 df-if 4480 df-pw 4556 df-sn 4582 df-pr 4584 df-tp 4586 df-op 4588 df-uni 4865 df-int 4905 df-iun 4950 df-br 5100 df-opab 5162 df-mpt 5181 df-tr 5207 df-id 5540 df-eprel 5545 df-po 5553 df-so 5554 df-fr 5598 df-se 5599 df-we 5600 df-xp 5651 df-rel 5652 df-cnv 5653 df-co 5654 df-dm 5655 df-rn 5656 df-res 5657 df-ima 5658 df-pred 6284 df-ord 6345 df-on 6346 df-lim 6347 df-suc 6348 df-iota 6473 df-fun 6519 df-fn 6520 df-f 6521 df-f1 6522 df-fo 6523 df-f1o 6524 df-fv 6525 df-isom 6526 df-riota 7349 df-ov 7395 df-oprab 7396 df-mpo 7397 df-of 7656 df-om 7843 df-1st 7966 df-2nd 7967 df-supp 8136 df-tpos 8201 df-frecs 8257 df-wrecs 8288 df-recs 8337 df-rdg 8376 df-1o 8432 df-er 8673 df-map 8805 df-ixp 8876 df-en 8924 df-dom 8925 df-sdom 8926 df-fin 8927 df-fsupp 9305 df-sup 9385 df-inf 9386 df-oi 9455 df-card 9894 df-pnf 11215 df-mnf 11216 df-xr 11217 df-ltxr 11218 df-le 11219 df-sub 11413 df-neg 11414 df-div 11842 df-nn 12208 df-2 12277 df-3 12278 df-4 12279 df-5 12280 df-6 12281 df-7 12282 df-8 12283 df-9 12284 df-n0 12479 df-z 12566 df-dec 12686 df-uz 12837 df-q 12947 df-rp 12991 df-xneg 13111 df-xadd 13112 df-xmul 13113 df-ico 13352 df-fz 13510 df-fzo 13657 df-seq 14012 df-exp 14072 df-hash 14341 df-cj 15109 df-re 15110 df-im 15111 df-sqrt 15245 df-abs 15246 df-clim 15498 df-sum 15697 df-struct 17166 df-sets 17183 df-slot 17201 df-ndx 17213 df-base 17229 df-ress 17250 df-plusg 17282 df-mulr 17283 df-starv 17284 df-sca 17285 df-vsca 17286 df-ip 17287 df-tset 17288 df-ple 17289 df-ds 17291 df-unif 17292 df-hom 17293 df-cco 17294 df-rest 17434 df-topn 17435 df-0g 17453 df-gsum 17454 df-topgen 17455 df-prds 17459 df-pws 17461 df-mgm 18657 df-sgrp 18736 df-mnd 18752 df-mhm 18800 df-submnd 18801 df-grp 18961 df-minusg 18962 df-sbg 18963 df-subg 19148 df-ghm 19237 df-cntz 19340 df-cmn 19805 df-abl 19806 df-mgp 20170 df-rng 20182 df-ur 20211 df-ring 20264 df-cring 20265 df-oppr 20365 df-dvdsr 20385 df-unit 20386 df-invr 20416 df-dvr 20429 df-rhm 20500 df-subrng 20575 df-subrg 20599 df-drng 20760 df-field 20761 df-abv 20838 df-staf 20868 df-srng 20869 df-lmod 20909 df-lss 20979 df-lmhm 21069 df-lvec 21150 df-sra 21220 df-rgmod 21221 df-psmet 21396 df-xmet 21397 df-met 21398 df-bl 21399 df-mopn 21400 df-cnfld 21405 df-refld 21637 df-phl 21658 df-dsmm 21764 df-frlm 21779 df-top 22934 df-topon 22951 df-topsp 22973 df-bases 22986 df-xms 24360 df-ms 24361 df-nm 24622 df-ngp 24623 df-tng 24624 df-nrg 24625 df-nlm 24626 df-clm 25105 df-cph 25210 df-tcph 25211 df-rrx 25427

This theorem is referenced by: rrxngp 46823

W3C validator