Definition df-phl 21678

Description: Define the class of all pre-Hilbert spaces (inner product spaces) over arbitrary fields with involution. (Some textbook definitions are more restrictive and require the field of scalars to be the field of real or complex numbers). (Contributed by NM, 22-Sep-2011.)

Assertion

Ref	Expression
df-phl	⊢ PreHil = {𝑔 ∈ LVec ∣ [(Base‘𝑔) / 𝑣][(·𝑖‘𝑔) / ℎ][(Scalar‘𝑔) / 𝑓](𝑓 ∈ *-Ring ∧ ∀𝑥 ∈ 𝑣 ((𝑦 ∈ 𝑣 ↦ (𝑦ℎ𝑥)) ∈ (𝑔 LMHom (ringLMod‘𝑓)) ∧ ((𝑥ℎ𝑥) = (0g‘𝑓) → 𝑥 = (0g‘𝑔)) ∧ ∀𝑦 ∈ 𝑣 ((*𝑟‘𝑓)‘(𝑥ℎ𝑦)) = (𝑦ℎ𝑥)))}

Distinct variable group:   𝑓,𝑔,ℎ,𝑣,𝑥,𝑦

Detailed syntax breakdown of Definition df-phl

Step	Hyp	Ref	Expression
1		cphl 21676	. 2 class PreHil
2		vf	. . . . . . . . 9 setvar 𝑓
3	2	cv 1559	. . . . . . . 8 class 𝑓
4		csr 20887	. . . . . . . 8 class *-Ring
5	3, 4	wcel 2142	. . . . . . 7 wff 𝑓 ∈ *-Ring
6		vy	. . . . . . . . . . 11 setvar 𝑦
7		vv	. . . . . . . . . . . 12 setvar 𝑣
8	7	cv 1559	. . . . . . . . . . 11 class 𝑣
9	6	cv 1559	. . . . . . . . . . . 12 class 𝑦
10		vx	. . . . . . . . . . . . 13 setvar 𝑥
11	10	cv 1559	. . . . . . . . . . . 12 class 𝑥
12		vh	. . . . . . . . . . . . 13 setvar ℎ
13	12	cv 1559	. . . . . . . . . . . 12 class ℎ
14	9, 11, 13	co 7396	. . . . . . . . . . 11 class (𝑦ℎ𝑥)
15	6, 8, 14	cmpt 5181	. . . . . . . . . 10 class (𝑦 ∈ 𝑣 ↦ (𝑦ℎ𝑥))
16		vg	. . . . . . . . . . . 12 setvar 𝑔
17	16	cv 1559	. . . . . . . . . . 11 class 𝑔
18		crglmod 21239	. . . . . . . . . . . 12 class ringLMod
19	3, 18	cfv 6521	. . . . . . . . . . 11 class (ringLMod‘𝑓)
20		clmhm 21086	. . . . . . . . . . 11 class LMHom
21	17, 19, 20	co 7396	. . . . . . . . . 10 class (𝑔 LMHom (ringLMod‘𝑓))
22	15, 21	wcel 2142	. . . . . . . . 9 wff (𝑦 ∈ 𝑣 ↦ (𝑦ℎ𝑥)) ∈ (𝑔 LMHom (ringLMod‘𝑓))
23	11, 11, 13	co 7396	. . . . . . . . . . 11 class (𝑥ℎ𝑥)
24		c0g 17468	. . . . . . . . . . . 12 class 0g
25	3, 24	cfv 6521	. . . . . . . . . . 11 class (0g‘𝑓)
26	23, 25	wceq 1560	. . . . . . . . . 10 wff (𝑥ℎ𝑥) = (0g‘𝑓)
27	17, 24	cfv 6521	. . . . . . . . . . 11 class (0g‘𝑔)
28	11, 27	wceq 1560	. . . . . . . . . 10 wff 𝑥 = (0g‘𝑔)
29	26, 28	wi 4	. . . . . . . . 9 wff ((𝑥ℎ𝑥) = (0g‘𝑓) → 𝑥 = (0g‘𝑔))
30	11, 9, 13	co 7396	. . . . . . . . . . . 12 class (𝑥ℎ𝑦)
31		cstv 17288	. . . . . . . . . . . . 13 class *𝑟
32	3, 31	cfv 6521	. . . . . . . . . . . 12 class (*𝑟‘𝑓)
33	30, 32	cfv 6521	. . . . . . . . . . 11 class ((*𝑟‘𝑓)‘(𝑥ℎ𝑦))
34	33, 14	wceq 1560	. . . . . . . . . 10 wff ((*𝑟‘𝑓)‘(𝑥ℎ𝑦)) = (𝑦ℎ𝑥)
35	34, 6, 8	wral 3076	. . . . . . . . 9 wff ∀𝑦 ∈ 𝑣 ((*𝑟‘𝑓)‘(𝑥ℎ𝑦)) = (𝑦ℎ𝑥)
36	22, 29, 35	w3a 1098	. . . . . . . 8 wff ((𝑦 ∈ 𝑣 ↦ (𝑦ℎ𝑥)) ∈ (𝑔 LMHom (ringLMod‘𝑓)) ∧ ((𝑥ℎ𝑥) = (0g‘𝑓) → 𝑥 = (0g‘𝑔)) ∧ ∀𝑦 ∈ 𝑣 ((*𝑟‘𝑓)‘(𝑥ℎ𝑦)) = (𝑦ℎ𝑥))
37	36, 10, 8	wral 3076	. . . . . . 7 wff ∀𝑥 ∈ 𝑣 ((𝑦 ∈ 𝑣 ↦ (𝑦ℎ𝑥)) ∈ (𝑔 LMHom (ringLMod‘𝑓)) ∧ ((𝑥ℎ𝑥) = (0g‘𝑓) → 𝑥 = (0g‘𝑔)) ∧ ∀𝑦 ∈ 𝑣 ((*𝑟‘𝑓)‘(𝑥ℎ𝑦)) = (𝑦ℎ𝑥))
38	5, 37	wa 399	. . . . . 6 wff (𝑓 ∈ *-Ring ∧ ∀𝑥 ∈ 𝑣 ((𝑦 ∈ 𝑣 ↦ (𝑦ℎ𝑥)) ∈ (𝑔 LMHom (ringLMod‘𝑓)) ∧ ((𝑥ℎ𝑥) = (0g‘𝑓) → 𝑥 = (0g‘𝑔)) ∧ ∀𝑦 ∈ 𝑣 ((*𝑟‘𝑓)‘(𝑥ℎ𝑦)) = (𝑦ℎ𝑥)))
39		csca 17289	. . . . . . 7 class Scalar
40	17, 39	cfv 6521	. . . . . 6 class (Scalar‘𝑔)
41	38, 2, 40	wsbc 3744	. . . . 5 wff [(Scalar‘𝑔) / 𝑓](𝑓 ∈ *-Ring ∧ ∀𝑥 ∈ 𝑣 ((𝑦 ∈ 𝑣 ↦ (𝑦ℎ𝑥)) ∈ (𝑔 LMHom (ringLMod‘𝑓)) ∧ ((𝑥ℎ𝑥) = (0g‘𝑓) → 𝑥 = (0g‘𝑔)) ∧ ∀𝑦 ∈ 𝑣 ((*𝑟‘𝑓)‘(𝑥ℎ𝑦)) = (𝑦ℎ𝑥)))
42		cip 17291	. . . . . 6 class ·𝑖
43	17, 42	cfv 6521	. . . . 5 class (·𝑖‘𝑔)
44	41, 12, 43	wsbc 3744	. . . 4 wff [(·𝑖‘𝑔) / ℎ][(Scalar‘𝑔) / 𝑓](𝑓 ∈ *-Ring ∧ ∀𝑥 ∈ 𝑣 ((𝑦 ∈ 𝑣 ↦ (𝑦ℎ𝑥)) ∈ (𝑔 LMHom (ringLMod‘𝑓)) ∧ ((𝑥ℎ𝑥) = (0g‘𝑓) → 𝑥 = (0g‘𝑔)) ∧ ∀𝑦 ∈ 𝑣 ((*𝑟‘𝑓)‘(𝑥ℎ𝑦)) = (𝑦ℎ𝑥)))
45		cbs 17245	. . . . 5 class Base
46	17, 45	cfv 6521	. . . 4 class (Base‘𝑔)
47	44, 7, 46	wsbc 3744	. . 3 wff [(Base‘𝑔) / 𝑣][(·𝑖‘𝑔) / ℎ][(Scalar‘𝑔) / 𝑓](𝑓 ∈ *-Ring ∧ ∀𝑥 ∈ 𝑣 ((𝑦 ∈ 𝑣 ↦ (𝑦ℎ𝑥)) ∈ (𝑔 LMHom (ringLMod‘𝑓)) ∧ ((𝑥ℎ𝑥) = (0g‘𝑓) → 𝑥 = (0g‘𝑔)) ∧ ∀𝑦 ∈ 𝑣 ((*𝑟‘𝑓)‘(𝑥ℎ𝑦)) = (𝑦ℎ𝑥)))
48		clvec 21169	. . 3 class LVec
49	47, 16, 48	crab 3414	. 2 class {𝑔 ∈ LVec ∣ [(Base‘𝑔) / 𝑣][(·𝑖‘𝑔) / ℎ][(Scalar‘𝑔) / 𝑓](𝑓 ∈ *-Ring ∧ ∀𝑥 ∈ 𝑣 ((𝑦 ∈ 𝑣 ↦ (𝑦ℎ𝑥)) ∈ (𝑔 LMHom (ringLMod‘𝑓)) ∧ ((𝑥ℎ𝑥) = (0g‘𝑓) → 𝑥 = (0g‘𝑔)) ∧ ∀𝑦 ∈ 𝑣 ((*𝑟‘𝑓)‘(𝑥ℎ𝑦)) = (𝑦ℎ𝑥)))}
50	1, 49	wceq 1560	1 wff PreHil = {𝑔 ∈ LVec ∣ [(Base‘𝑔) / 𝑣][(·𝑖‘𝑔) / ℎ][(Scalar‘𝑔) / 𝑓](𝑓 ∈ *-Ring ∧ ∀𝑥 ∈ 𝑣 ((𝑦 ∈ 𝑣 ↦ (𝑦ℎ𝑥)) ∈ (𝑔 LMHom (ringLMod‘𝑓)) ∧ ((𝑥ℎ𝑥) = (0g‘𝑓) → 𝑥 = (0g‘𝑔)) ∧ ∀𝑦 ∈ 𝑣 ((*𝑟‘𝑓)‘(𝑥ℎ𝑦)) = (𝑦ℎ𝑥)))}

This definition is referenced by:  isphl  21680