Metamath Proof Explorer

Definition df-phl

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)

Ref Expression
Assertion df-phl ⊢ PreHil = g ∈ LVec | [˙Base g / v]˙ [˙ ⋅ 𝑖 ⁡ g / h]˙ [˙ Scalar ⁡ g / f]˙ f ∈ *-Ring ∧ ∀ x ∈ v y ∈ v ⟼ y h x ∈ g LMHom ringLMod ⁡ f ∧ x h x = 0 f → x = 0 g ∧ ∀ y ∈ v x h y * f = y h x

Detailed syntax breakdown

Step Hyp Ref Expression
0 cphl class PreHil
1 vg setvar g
2 clvec class LVec
3 cbs class Base
4 1 cv setvar g
5 4 3 cfv class Base g
6 vv setvar v
7 cip class ⋅ 𝑖
8 4 7 cfv class ⋅ 𝑖 ⁡ g
9 vh setvar h
10 csca class Scalar
11 4 10 cfv class Scalar ⁡ g
12 vf setvar f
13 12 cv setvar f
14 csr class *-Ring
15 13 14 wcel wff f ∈ *-Ring
16 vx setvar x
17 6 cv setvar v
18 vy setvar y
19 18 cv setvar y
20 9 cv setvar h
21 16 cv setvar x
22 19 21 20 co class y h x
23 18 17 22 cmpt class y ∈ v ⟼ y h x
24 clmhm class LMHom
25 crglmod class ringLMod
26 13 25 cfv class ringLMod ⁡ f
27 4 26 24 co class g LMHom ringLMod ⁡ f
28 23 27 wcel wff y ∈ v ⟼ y h x ∈ g LMHom ringLMod ⁡ f
29 21 21 20 co class x h x
30 c0g class 0 𝑔
31 13 30 cfv class 0 f
32 29 31 wceq wff x h x = 0 f
33 4 30 cfv class 0 g
34 21 33 wceq wff x = 0 g
35 32 34 wi wff x h x = 0 f → x = 0 g
36 cstv class ∗ 𝑟
37 13 36 cfv class * f
38 21 19 20 co class x h y
39 38 37 cfv class x h y * f
40 39 22 wceq wff x h y * f = y h x
41 40 18 17 wral wff ∀ y ∈ v x h y * f = y h x
42 28 35 41 w3a wff y ∈ v ⟼ y h x ∈ g LMHom ringLMod ⁡ f ∧ x h x = 0 f → x = 0 g ∧ ∀ y ∈ v x h y * f = y h x
43 42 16 17 wral wff ∀ x ∈ v y ∈ v ⟼ y h x ∈ g LMHom ringLMod ⁡ f ∧ x h x = 0 f → x = 0 g ∧ ∀ y ∈ v x h y * f = y h x
44 15 43 wa wff f ∈ *-Ring ∧ ∀ x ∈ v y ∈ v ⟼ y h x ∈ g LMHom ringLMod ⁡ f ∧ x h x = 0 f → x = 0 g ∧ ∀ y ∈ v x h y * f = y h x
45 44 12 11 wsbc wff [˙ Scalar ⁡ g / f]˙ f ∈ *-Ring ∧ ∀ x ∈ v y ∈ v ⟼ y h x ∈ g LMHom ringLMod ⁡ f ∧ x h x = 0 f → x = 0 g ∧ ∀ y ∈ v x h y * f = y h x
46 45 9 8 wsbc wff [˙ ⋅ 𝑖 ⁡ g / h]˙ [˙ Scalar ⁡ g / f]˙ f ∈ *-Ring ∧ ∀ x ∈ v y ∈ v ⟼ y h x ∈ g LMHom ringLMod ⁡ f ∧ x h x = 0 f → x = 0 g ∧ ∀ y ∈ v x h y * f = y h x
47 46 6 5 wsbc wff [˙Base g / v]˙ [˙ ⋅ 𝑖 ⁡ g / h]˙ [˙ Scalar ⁡ g / f]˙ f ∈ *-Ring ∧ ∀ x ∈ v y ∈ v ⟼ y h x ∈ g LMHom ringLMod ⁡ f ∧ x h x = 0 f → x = 0 g ∧ ∀ y ∈ v x h y * f = y h x
48 47 1 2 crab class g ∈ LVec | [˙Base g / v]˙ [˙ ⋅ 𝑖 ⁡ g / h]˙ [˙ Scalar ⁡ g / f]˙ f ∈ *-Ring ∧ ∀ x ∈ v y ∈ v ⟼ y h x ∈ g LMHom ringLMod ⁡ f ∧ x h x = 0 f → x = 0 g ∧ ∀ y ∈ v x h y * f = y h x
49 0 48 wceq wff PreHil = g ∈ LVec | [˙Base g / v]˙ [˙ ⋅ 𝑖 ⁡ g / h]˙ [˙ Scalar ⁡ g / f]˙ f ∈ *-Ring ∧ ∀ x ∈ v y ∈ v ⟼ y h x ∈ g LMHom ringLMod ⁡ f ∧ x h x = 0 f → x = 0 g ∧ ∀ y ∈ v x h y * f = y h x