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 25714

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 25709	. 2 ⊢ (𝐼 ∈ 𝑉 → 𝐻 = (toℂPreHil‘(ℝ_fld freeLMod 𝐼)))
3		eqid 2760	. . 3 ⊢ (toℂPreHil‘(ℝ_fld freeLMod 𝐼)) = (toℂPreHil‘(ℝ_fld freeLMod 𝐼))
4		eqid 2760	. . 3 ⊢ (Base‘(ℝ_fld freeLMod 𝐼)) = (Base‘(ℝ_fld freeLMod 𝐼))
5		eqid 2760	. . 3 ⊢ (Scalar‘(ℝ_fld freeLMod 𝐼)) = (Scalar‘(ℝ_fld freeLMod 𝐼))
6		eqid 2760	. . . 4 ⊢ (ℝ_fld freeLMod 𝐼) = (ℝ_fld freeLMod 𝐼)
7		rebase 21913	. . . 4 ⊢ ℝ = (Base‘ℝ_fld)
8		remulr 21918	. . . 4 ⊢ · = (._r‘ℝ_fld)
9		eqid 2760	. . . 4 ⊢ (·_𝑖‘(ℝ_fld freeLMod 𝐼)) = (·_𝑖‘(ℝ_fld freeLMod 𝐼))
10		eqid 2760	. . . 4 ⊢ (0_g‘(ℝ_fld freeLMod 𝐼)) = (0_g‘(ℝ_fld freeLMod 𝐼))
11		re0g 21919	. . . 4 ⊢ 0 = (0_g‘ℝ_fld)
12		refldcj 21927	. . . 4 ⊢ ∗ = (*_𝑟‘ℝ_fld)
13		refld 21926	. . . . 5 ⊢ ℝ_fld ∈ Field
14	13	a1i 11	. . . 4 ⊢ (𝐼 ∈ 𝑉 → ℝ_fld ∈ Field)
15		fconstmpt 5712	. . . . 5 ⊢ (𝐼 × {0}) = (𝑥 ∈ 𝐼 ↦ 0)
16	6, 7, 4	frlmbasf 22067	. . . . . . . 8 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) → 𝑓:𝐼⟶ℝ)
17	16	ffnd 6710	. . . . . . 7 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) → 𝑓 Fn 𝐼)
18	17	3adant3 1150	. . . . . 6 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) → 𝑓 Fn 𝐼)
19		simpl 488	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) → 𝐼 ∈ 𝑉)
20	13	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) → ℝ_fld ∈ Field)
21		simpr 490	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) → 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)))
22	6, 7, 8, 4, 9	frlmipval 22086	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐼 ∈ 𝑉 ∧ ℝ_fld ∈ Field) ∧ (𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)))) → (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = (ℝ_fld Σ_g (𝑓 ∘_f · 𝑓)))
23	19, 20, 21, 21, 22	syl22anc 852	. . . . . . . . . . . . . . . 16 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) → (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = (ℝ_fld Σ_g (𝑓 ∘_f · 𝑓)))
24		inidm 4123	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐼 ∩ 𝐼) = 𝐼
25		eqidd 2761	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) ∧ 𝑥 ∈ 𝐼) → (𝑓‘𝑥) = (𝑓‘𝑥))
26	17, 17, 19, 19, 24, 25, 25	offval 7702	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) → (𝑓 ∘_f · 𝑓) = (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥) · (𝑓‘𝑥))))
27	16	ffvelcdmda 7084	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) ∧ 𝑥 ∈ 𝐼) → (𝑓‘𝑥) ∈ ℝ)
28	27, 27	remulcld 11340	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) ∧ 𝑥 ∈ 𝐼) → ((𝑓‘𝑥) · (𝑓‘𝑥)) ∈ ℝ)
29	26, 28	fmpt3d 7116	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) → (𝑓 ∘_f · 𝑓):𝐼⟶ℝ)
30		ovexd 7455	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) → (𝑓 ∘_f · 𝑓) ∈ V)
31	29	ffund 6714	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) → Fun (𝑓 ∘_f · 𝑓))
32	6, 11, 4	frlmbasfsupp 22065	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) → 𝑓 finSupp 0)
33		0red 11312	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) → 0 ∈ ℝ)
34		simpr 490	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℝ)
35	34	recnd 11338	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℂ)
36	35	mul02d 11509	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) ∧ 𝑥 ∈ ℝ) → (0 · 𝑥) = 0)
37	19, 33, 16, 16, 36	suppofss1d 8222	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) → ((𝑓 ∘_f · 𝑓) supp 0) ⊆ (𝑓 supp 0))
38		fsuppsssupp 9374	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑓 ∘_f · 𝑓) ∈ V ∧ Fun (𝑓 ∘_f · 𝑓)) ∧ (𝑓 finSupp 0 ∧ ((𝑓 ∘_f · 𝑓) supp 0) ⊆ (𝑓 supp 0))) → (𝑓 ∘_f · 𝑓) finSupp 0)
39	30, 31, 32, 37, 38	syl22anc 852	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) → (𝑓 ∘_f · 𝑓) finSupp 0)
40		regsumsupp 21929	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑓 ∘_f · 𝑓):𝐼⟶ℝ ∧ (𝑓 ∘_f · 𝑓) finSupp 0 ∧ 𝐼 ∈ 𝑉) → (ℝ_fld Σ_g (𝑓 ∘_f · 𝑓)) = Σ𝑥 ∈ ((𝑓 ∘_f · 𝑓) supp 0)((𝑓 ∘_f · 𝑓)‘𝑥))
41	29, 39, 19, 40	syl3anc 1398	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) → (ℝ_fld Σ_g (𝑓 ∘_f · 𝑓)) = Σ𝑥 ∈ ((𝑓 ∘_f · 𝑓) supp 0)((𝑓 ∘_f · 𝑓)‘𝑥))
42		suppssdm 8195	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑓 supp 0) ⊆ dom 𝑓
43	42, 16	fssdm 6729	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) → (𝑓 supp 0) ⊆ 𝐼)
44	37, 43	sstrd 3918	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) → ((𝑓 ∘_f · 𝑓) supp 0) ⊆ 𝐼)
45	44	sselda 3908	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) ∧ 𝑥 ∈ ((𝑓 ∘_f · 𝑓) supp 0)) → 𝑥 ∈ 𝐼)
46	17, 17, 19, 19, 24, 25, 25	ofval 7704	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) ∧ 𝑥 ∈ 𝐼) → ((𝑓 ∘_f · 𝑓)‘𝑥) = ((𝑓‘𝑥) · (𝑓‘𝑥)))
47	45, 46	syldan 603	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) ∧ 𝑥 ∈ ((𝑓 ∘_f · 𝑓) supp 0)) → ((𝑓 ∘_f · 𝑓)‘𝑥) = ((𝑓‘𝑥) · (𝑓‘𝑥)))
48	47	sumeq2dv 15870	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) → Σ𝑥 ∈ ((𝑓 ∘_f · 𝑓) supp 0)((𝑓 ∘_f · 𝑓)‘𝑥) = Σ𝑥 ∈ ((𝑓 ∘_f · 𝑓) supp 0)((𝑓‘𝑥) · (𝑓‘𝑥)))
49	41, 48	eqtrd 2795	. . . . . . . . . . . . . . . 16 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) → (ℝ_fld Σ_g (𝑓 ∘_f · 𝑓)) = Σ𝑥 ∈ ((𝑓 ∘_f · 𝑓) supp 0)((𝑓‘𝑥) · (𝑓‘𝑥)))
50	23, 49	eqtrd 2795	. . . . . . . . . . . . . . 15 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) → (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = Σ𝑥 ∈ ((𝑓 ∘_f · 𝑓) supp 0)((𝑓‘𝑥) · (𝑓‘𝑥)))
51	50	3adant3 1150	. . . . . . . . . . . . . 14 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) → (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = Σ𝑥 ∈ ((𝑓 ∘_f · 𝑓) supp 0)((𝑓‘𝑥) · (𝑓‘𝑥)))
52		simp3 1156	. . . . . . . . . . . . . 14 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) → (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0)
53	51, 52	eqtr3d 2797	. . . . . . . . . . . . 13 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) → Σ𝑥 ∈ ((𝑓 ∘_f · 𝑓) supp 0)((𝑓‘𝑥) · (𝑓‘𝑥)) = 0)
54	32	fsuppimpd 9362	. . . . . . . . . . . . . . . 16 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) → (𝑓 supp 0) ∈ Fin)
55	54, 37	ssfid 9261	. . . . . . . . . . . . . . 15 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) → ((𝑓 ∘_f · 𝑓) supp 0) ∈ Fin)
56	45, 28	syldan 603	. . . . . . . . . . . . . . 15 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) ∧ 𝑥 ∈ ((𝑓 ∘_f · 𝑓) supp 0)) → ((𝑓‘𝑥) · (𝑓‘𝑥)) ∈ ℝ)
57	27	msqge0d 11885	. . . . . . . . . . . . . . . 16 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) ∧ 𝑥 ∈ 𝐼) → 0 ≤ ((𝑓‘𝑥) · (𝑓‘𝑥)))
58	45, 57	syldan 603	. . . . . . . . . . . . . . 15 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) ∧ 𝑥 ∈ ((𝑓 ∘_f · 𝑓) supp 0)) → 0 ≤ ((𝑓‘𝑥) · (𝑓‘𝑥)))
59	55, 56, 58	fsum00 15966	. . . . . . . . . . . . . 14 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) → (Σ𝑥 ∈ ((𝑓 ∘_f · 𝑓) supp 0)((𝑓‘𝑥) · (𝑓‘𝑥)) = 0 ↔ ∀𝑥 ∈ ((𝑓 ∘_f · 𝑓) supp 0)((𝑓‘𝑥) · (𝑓‘𝑥)) = 0))
60	59	3adant3 1150	. . . . . . . . . . . . 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 3254	. . . . . . . . . . 11 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ ((𝑓 ∘_f · 𝑓) supp 0)) → ((𝑓‘𝑥) · (𝑓‘𝑥)) = 0)
63	62	adantlr 728	. . . . . . . . . 10 ⊢ ((((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼) ∧ 𝑥 ∈ ((𝑓 ∘_f · 𝑓) supp 0)) → ((𝑓‘𝑥) · (𝑓‘𝑥)) = 0)
64	27	3adantl3 1187	. . . . . . . . . . . . 13 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼) → (𝑓‘𝑥) ∈ ℝ)
65	64	recnd 11338	. . . . . . . . . . . 12 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼) → (𝑓‘𝑥) ∈ ℂ)
66	65, 65	mul0ord 11965	. . . . . . . . . . 11 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼) → (((𝑓‘𝑥) · (𝑓‘𝑥)) = 0 ↔ ((𝑓‘𝑥) = 0 ∨ (𝑓‘𝑥) = 0)))
67	66	adantr 486	. . . . . . . . . 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 918	. . . . . . . . 9 ⊢ (((𝑓‘𝑥) = 0 ∨ (𝑓‘𝑥) = 0) ↔ (𝑓‘𝑥) = 0)
70	68, 69	sylib 221	. . . . . . . 8 ⊢ ((((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼) ∧ 𝑥 ∈ ((𝑓 ∘_f · 𝑓) supp 0)) → (𝑓‘𝑥) = 0)
71	29	3adant3 1150	. . . . . . . . . . 11 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) → (𝑓 ∘_f · 𝑓):𝐼⟶ℝ)
72	71	adantr 486	. . . . . . . . . 10 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼) → (𝑓 ∘_f · 𝑓):𝐼⟶ℝ)
73		ssidd 3931	. . . . . . . . . 10 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼) → ((𝑓 ∘_f · 𝑓) supp 0) ⊆ ((𝑓 ∘_f · 𝑓) supp 0))
74		simpl1 1210	. . . . . . . . . 10 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼) → 𝐼 ∈ 𝑉)
75		0red 11312	. . . . . . . . . 10 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼) → 0 ∈ ℝ)
76	72, 73, 74, 75	suppssr 8213	. . . . . . . . 9 ⊢ ((((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼) ∧ 𝑥 ∈ (𝐼 ∖ ((𝑓 ∘_f · 𝑓) supp 0))) → ((𝑓 ∘_f · 𝑓)‘𝑥) = 0)
77	46	3adantl3 1187	. . . . . . . . . . . . 13 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼) → ((𝑓 ∘_f · 𝑓)‘𝑥) = ((𝑓‘𝑥) · (𝑓‘𝑥)))
78	77	eqeq1d 2762	. . . . . . . . . . . 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 482	. . . . . . . . 9 ⊢ ((((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼) ∧ ((𝑓 ∘_f · 𝑓)‘𝑥) = 0) → (𝑓‘𝑥) = 0)
82	76, 81	syldan 603	. . . . . . . 8 ⊢ ((((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼) ∧ 𝑥 ∈ (𝐼 ∖ ((𝑓 ∘_f · 𝑓) supp 0))) → (𝑓‘𝑥) = 0)
83		undif 4437	. . . . . . . . . . . . 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 2846	. . . . . . . . . . 11 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) → (𝑥 ∈ (((𝑓 ∘_f · 𝑓) supp 0) ∪ (𝐼 ∖ ((𝑓 ∘_f · 𝑓) supp 0))) ↔ 𝑥 ∈ 𝐼))
86	85	3adant3 1150	. . . . . . . . . 10 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) → (𝑥 ∈ (((𝑓 ∘_f · 𝑓) supp 0) ∪ (𝐼 ∖ ((𝑓 ∘_f · 𝑓) supp 0))) ↔ 𝑥 ∈ 𝐼))
87	86	biimpar 483	. . . . . . . . 9 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼) → 𝑥 ∈ (((𝑓 ∘_f · 𝑓) supp 0) ∪ (𝐼 ∖ ((𝑓 ∘_f · 𝑓) supp 0))))
88		elun 4152	. . . . . . . . 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 3154	. . . . . 6 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) → ∀𝑥 ∈ 𝐼 (𝑓‘𝑥) = 0)
92		fconstfv 7218	. . . . . . 7 ⊢ (𝑓:𝐼⟶{0} ↔ (𝑓 Fn 𝐼 ∧ ∀𝑥 ∈ 𝐼 (𝑓‘𝑥) = 0))
93		c0ex 11301	. . . . . . . 8 ⊢ 0 ∈ V
94	93	fconst2 7211	. . . . . . 7 ⊢ (𝑓:𝐼⟶{0} ↔ 𝑓 = (𝐼 × {0}))
95	92, 94	sylbb1 240	. . . . . 6 ⊢ ((𝑓 Fn 𝐼 ∧ ∀𝑥 ∈ 𝐼 (𝑓‘𝑥) = 0) → 𝑓 = (𝐼 × {0}))
96	18, 91, 95	syl2anc 596	. . . . 5 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) → 𝑓 = (𝐼 × {0}))
97		isfld 20994	. . . . . . . . . . 11 ⊢ (ℝ_fld ∈ Field ↔ (ℝ_fld ∈ DivRing ∧ ℝ_fld ∈ CRing))
98	13, 97	mpbi 233	. . . . . . . . . 10 ⊢ (ℝ_fld ∈ DivRing ∧ ℝ_fld ∈ CRing)
99	98	simpli 489	. . . . . . . . 9 ⊢ ℝ_fld ∈ DivRing
100		drngring 20988	. . . . . . . . 9 ⊢ (ℝ_fld ∈ DivRing → ℝ_fld ∈ Ring)
101	99, 100	ax-mp 5	. . . . . . . 8 ⊢ ℝ_fld ∈ Ring
102	6, 11	frlm0 22061	. . . . . . . 8 ⊢ ((ℝ_fld ∈ Ring ∧ 𝐼 ∈ 𝑉) → (𝐼 × {0}) = (0_g‘(ℝ_fld freeLMod 𝐼)))
103	101, 102	mpan 703	. . . . . . 7 ⊢ (𝐼 ∈ 𝑉 → (𝐼 × {0}) = (0_g‘(ℝ_fld freeLMod 𝐼)))
104	103, 15	eqtr3di 2810	. . . . . 6 ⊢ (𝐼 ∈ 𝑉 → (0_g‘(ℝ_fld freeLMod 𝐼)) = (𝑥 ∈ 𝐼 ↦ 0))
105	104	3ad2ant1 1151	. . . . 5 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) → (0_g‘(ℝ_fld freeLMod 𝐼)) = (𝑥 ∈ 𝐼 ↦ 0))
106	15, 96, 105	3eqtr4a 2821	. . . 4 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼)) ∧ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓) = 0) → 𝑓 = (0_g‘(ℝ_fld freeLMod 𝐼)))
107		cjre 15307	. . . . 5 ⊢ (𝑥 ∈ ℝ → (∗‘𝑥) = 𝑥)
108	107	adantl 487	. . . 4 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ ℝ) → (∗‘𝑥) = 𝑥)
109		id 23	. . . 4 ⊢ (𝐼 ∈ 𝑉 → 𝐼 ∈ 𝑉)
110	6, 7, 8, 4, 9, 10, 11, 12, 14, 106, 108, 109	frlmphl 22088	. . 3 ⊢ (𝐼 ∈ 𝑉 → (ℝ_fld freeLMod 𝐼) ∈ PreHil)
111	6	frlmsca 22060	. . . . 5 ⊢ ((ℝ_fld ∈ Field ∧ 𝐼 ∈ 𝑉) → ℝ_fld = (Scalar‘(ℝ_fld freeLMod 𝐼)))
112	13, 111	mpan 703	. . . 4 ⊢ (𝐼 ∈ 𝑉 → ℝ_fld = (Scalar‘(ℝ_fld freeLMod 𝐼)))
113		df-refld 21912	. . . 4 ⊢ ℝ_fld = (ℂ_fld ↾_s ℝ)
114	112, 113	eqtr3di 2810	. . 3 ⊢ (𝐼 ∈ 𝑉 → (Scalar‘(ℝ_fld freeLMod 𝐼)) = (ℂ_fld ↾_s ℝ))
115		simpr1 1213	. . . 4 ⊢ ((𝐼 ∈ 𝑉 ∧ (𝑓 ∈ ℝ ∧ 𝑓 ∈ ℝ ∧ 0 ≤ 𝑓)) → 𝑓 ∈ ℝ)
116		simpr3 1215	. . . 4 ⊢ ((𝐼 ∈ 𝑉 ∧ (𝑓 ∈ ℝ ∧ 𝑓 ∈ ℝ ∧ 0 ≤ 𝑓)) → 0 ≤ 𝑓)
117	115, 116	resqrtcld 15586	. . 3 ⊢ ((𝐼 ∈ 𝑉 ∧ (𝑓 ∈ ℝ ∧ 𝑓 ∈ ℝ ∧ 0 ≤ 𝑓)) → (√‘𝑓) ∈ ℝ)
118	55, 56, 58	fsumge0 15963	. . . . 5 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) → 0 ≤ Σ𝑥 ∈ ((𝑓 ∘_f · 𝑓) supp 0)((𝑓‘𝑥) · (𝑓‘𝑥)))
119	118, 49	breqtrrd 5132	. . . 4 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) → 0 ≤ (ℝ_fld Σ_g (𝑓 ∘_f · 𝑓)))
120	119, 23	breqtrrd 5132	. . 3 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝ_fld freeLMod 𝐼))) → 0 ≤ (𝑓(·_𝑖‘(ℝ_fld freeLMod 𝐼))𝑓))
121	3, 4, 5, 110, 114, 9, 117, 120	tcphcph 25559	. 2 ⊢ (𝐼 ∈ 𝑉 → (toℂPreHil‘(ℝ_fld freeLMod 𝐼)) ∈ ℂPreHil)
122	2, 121	eqeltrd 2860	1 ⊢ (𝐼 ∈ 𝑉 → 𝐻 ∈ ℂPreHil)

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 ∨ wo 861 ∧ w3a 1103 = wceq 1569 ∈ wcel 2144 ∀wral 3076 Vcvv 3450 ⊆ wss 3895 ∖ cdif 4045 ∪ cun 4149 {csn 4583 class class class wbr 5102 ↦ cmpt 5185 × cxp 5648 Fun wfun 6532 Fn wfn 6533 ⟶wf 6534 ‘cfv 6538 (class class class)co 7420 ∘_f cof 7691 supp csupp 8177 finSupp cfsupp 9354 ℝcr 11200 0cc0 11201 · cmul 11206 ≤ cle 11345 ∗ccj 15264 Σcsu 15854 Basecbs 17388 ↾_s cress 17409 Scalarcsca 17432 ·_𝑖cip 17434 0_gc0g 17611 Σ_g cgsu 17612 Ringcrg 20460 CRingccrg 20461 DivRingcdr 20981 Fieldcfield 20982 ℂ_fldccnfld 21679 ℝ_fldcrefld 21911 freeLMod cfrlm 22053 ℂPreHilccph 25488 toℂPreHilctcph 25489 ℝ^crrx 25705

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2212 ax-ext 2732 ax-rep 5231 ax-sep 5248 ax-nul 5259 ax-pow 5326 ax-pr 5390 ax-un 7751 ax-inf2 9643 ax-cnex 11257 ax-resscn 11258 ax-1cn 11259 ax-icn 11260 ax-addcl 11261 ax-addrcl 11262 ax-mulcl 11263 ax-mulrcl 11264 ax-mulcom 11265 ax-addass 11266 ax-mulass 11267 ax-distr 11268 ax-i2m1 11269 ax-1ne0 11270 ax-1rid 11271 ax-rnegex 11272 ax-rrecex 11273 ax-cnre 11274 ax-pre-lttri 11275 ax-pre-lttrn 11276 ax-pre-ltadd 11277 ax-pre-mulgt0 11278 ax-pre-sup 11279 ax-addf 11280 ax-mulf 11281

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2099 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3739 df-csb 3847 df-ss 3896 df-pss 4014 df-dif 4047 df-in 4091 df-un 4151 df-nul 4279 df-if 4482 df-pw 4558 df-sn 4584 df-pr 4586 df-tp 4588 df-op 4590 df-uni 4867 df-int 4907 df-iun 4952 df-br 5103 df-opab 5167 df-mpt 5186 df-tr 5212 df-id 5545 df-eprel 5550 df-po 5558 df-so 5559 df-fr 5603 df-se 5604 df-we 5605 df-xp 5656 df-rel 5657 df-cnv 5658 df-co 5659 df-dm 5660 df-rn 5661 df-res 5662 df-ima 5663 df-pred 6304 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6494 df-fun 6540 df-fn 6541 df-f 6542 df-f1 6543 df-fo 6544 df-f1o 6545 df-fv 6546 df-isom 6547 df-riota 7377 df-ov 7423 df-oprab 7424 df-mpo 7425 df-of 7693 df-om 7878 df-1st 8001 df-2nd 8002 df-supp 8178 df-tpos 8244 df-frecs 8300 df-wrecs 8331 df-recs 8380 df-rdg 8419 df-1o 8477 df-er 8718 df-map 8850 df-ixp 8927 df-en 8975 df-dom 8976 df-sdom 8977 df-fin 8978 df-fsupp 9355 df-sup 9435 df-inf 9436 df-oi 9505 df-card 10021 df-pnf 11346 df-mnf 11347 df-xr 11348 df-ltxr 11349 df-le 11350 df-sub 11544 df-neg 11545 df-div 11975 df-nn 12337 df-2 12406 df-3 12407 df-4 12408 df-5 12409 df-6 12410 df-7 12411 df-8 12412 df-9 12413 df-n0 12608 df-z 12695 df-dec 12816 df-uz 12967 df-q 13077 df-rp 13122 df-xneg 13242 df-xadd 13243 df-xmul 13244 df-ico 13483 df-fz 13641 df-fzo 13790 df-seq 14146 df-exp 14206 df-hash 14476 df-cj 15267 df-re 15268 df-im 15269 df-sqrt 15403 df-abs 15404 df-clim 15656 df-sum 15855 df-struct 17326 df-sets 17343 df-slot 17361 df-ndx 17373 df-base 17389 df-ress 17410 df-plusg 17442 df-mulr 17443 df-starv 17444 df-sca 17445 df-vsca 17446 df-ip 17447 df-tset 17448 df-ple 17449 df-ds 17451 df-unif 17452 df-hom 17453 df-cco 17454 df-rest 17594 df-topn 17595 df-0g 17613 df-gsum 17614 df-topgen 17615 df-prds 17619 df-pws 17621 df-mgm 18817 df-sgrp 18909 df-mnd 18925 df-mhm 18979 df-submnd 18980 df-grp 19148 df-minusg 19149 df-sbg 19150 df-subg 19334 df-ghm 19429 df-cntz 19532 df-cmn 19997 df-abl 19998 df-mgp 20362 df-rng 20376 df-ur 20409 df-ring 20462 df-cring 20463 df-oppr 20568 df-dvdsr 20588 df-unit 20589 df-invr 20619 df-dvr 20632 df-rhm 20703 df-subrng 20799 df-subrg 20823 df-drng 20983 df-field 20984 df-abv 21067 df-staf 21097 df-srng 21098 df-lmod 21138 df-lss 21208 df-lmhm 21298 df-lvec 21379 df-sra 21449 df-rgmod 21450 df-psmet 21671 df-xmet 21672 df-met 21673 df-bl 21674 df-mopn 21675 df-cnfld 21680 df-refld 21912 df-phl 21933 df-dsmm 22039 df-frlm 22054 df-top 23213 df-topon 23230 df-topsp 23252 df-bases 23265 df-xms 24640 df-ms 24641 df-nm 24902 df-ngp 24903 df-tng 24904 df-nrg 24905 df-nlm 24906 df-clm 25385 df-cph 25490 df-tcph 25491 df-rrx 25707

This theorem is used by: rrxngp 47339

W3C validator