MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-phl Structured version   Visualization version   GIF version

Definition df-phl 20165
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
StepHypRef Expression
1 cphl 20163 . 2 class PreHil
2 vf . . . . . . . . 9 setvar 𝑓
32cv 1623 . . . . . . . 8 class 𝑓
4 csr 19038 . . . . . . . 8 class *-Ring
53, 4wcel 2131 . . . . . . 7 wff 𝑓 ∈ *-Ring
6 vy . . . . . . . . . . 11 setvar 𝑦
7 vv . . . . . . . . . . . 12 setvar 𝑣
87cv 1623 . . . . . . . . . . 11 class 𝑣
96cv 1623 . . . . . . . . . . . 12 class 𝑦
10 vx . . . . . . . . . . . . 13 setvar 𝑥
1110cv 1623 . . . . . . . . . . . 12 class 𝑥
12 vh . . . . . . . . . . . . 13 setvar
1312cv 1623 . . . . . . . . . . . 12 class
149, 11, 13co 6805 . . . . . . . . . . 11 class (𝑦𝑥)
156, 8, 14cmpt 4873 . . . . . . . . . 10 class (𝑦𝑣 ↦ (𝑦𝑥))
16 vg . . . . . . . . . . . 12 setvar 𝑔
1716cv 1623 . . . . . . . . . . 11 class 𝑔
18 crglmod 19363 . . . . . . . . . . . 12 class ringLMod
193, 18cfv 6041 . . . . . . . . . . 11 class (ringLMod‘𝑓)
20 clmhm 19213 . . . . . . . . . . 11 class LMHom
2117, 19, 20co 6805 . . . . . . . . . 10 class (𝑔 LMHom (ringLMod‘𝑓))
2215, 21wcel 2131 . . . . . . . . 9 wff (𝑦𝑣 ↦ (𝑦𝑥)) ∈ (𝑔 LMHom (ringLMod‘𝑓))
2311, 11, 13co 6805 . . . . . . . . . . 11 class (𝑥𝑥)
24 c0g 16294 . . . . . . . . . . . 12 class 0g
253, 24cfv 6041 . . . . . . . . . . 11 class (0g𝑓)
2623, 25wceq 1624 . . . . . . . . . 10 wff (𝑥𝑥) = (0g𝑓)
2717, 24cfv 6041 . . . . . . . . . . 11 class (0g𝑔)
2811, 27wceq 1624 . . . . . . . . . 10 wff 𝑥 = (0g𝑔)
2926, 28wi 4 . . . . . . . . 9 wff ((𝑥𝑥) = (0g𝑓) → 𝑥 = (0g𝑔))
3011, 9, 13co 6805 . . . . . . . . . . . 12 class (𝑥𝑦)
31 cstv 16137 . . . . . . . . . . . . 13 class *𝑟
323, 31cfv 6041 . . . . . . . . . . . 12 class (*𝑟𝑓)
3330, 32cfv 6041 . . . . . . . . . . 11 class ((*𝑟𝑓)‘(𝑥𝑦))
3433, 14wceq 1624 . . . . . . . . . 10 wff ((*𝑟𝑓)‘(𝑥𝑦)) = (𝑦𝑥)
3534, 6, 8wral 3042 . . . . . . . . 9 wff 𝑦𝑣 ((*𝑟𝑓)‘(𝑥𝑦)) = (𝑦𝑥)
3622, 29, 35w3a 1072 . . . . . . . 8 wff ((𝑦𝑣 ↦ (𝑦𝑥)) ∈ (𝑔 LMHom (ringLMod‘𝑓)) ∧ ((𝑥𝑥) = (0g𝑓) → 𝑥 = (0g𝑔)) ∧ ∀𝑦𝑣 ((*𝑟𝑓)‘(𝑥𝑦)) = (𝑦𝑥))
3736, 10, 8wral 3042 . . . . . . 7 wff 𝑥𝑣 ((𝑦𝑣 ↦ (𝑦𝑥)) ∈ (𝑔 LMHom (ringLMod‘𝑓)) ∧ ((𝑥𝑥) = (0g𝑓) → 𝑥 = (0g𝑔)) ∧ ∀𝑦𝑣 ((*𝑟𝑓)‘(𝑥𝑦)) = (𝑦𝑥))
385, 37wa 383 . . . . . 6 wff (𝑓 ∈ *-Ring ∧ ∀𝑥𝑣 ((𝑦𝑣 ↦ (𝑦𝑥)) ∈ (𝑔 LMHom (ringLMod‘𝑓)) ∧ ((𝑥𝑥) = (0g𝑓) → 𝑥 = (0g𝑔)) ∧ ∀𝑦𝑣 ((*𝑟𝑓)‘(𝑥𝑦)) = (𝑦𝑥)))
39 csca 16138 . . . . . . 7 class Scalar
4017, 39cfv 6041 . . . . . 6 class (Scalar‘𝑔)
4138, 2, 40wsbc 3568 . . . . 5 wff [(Scalar‘𝑔) / 𝑓](𝑓 ∈ *-Ring ∧ ∀𝑥𝑣 ((𝑦𝑣 ↦ (𝑦𝑥)) ∈ (𝑔 LMHom (ringLMod‘𝑓)) ∧ ((𝑥𝑥) = (0g𝑓) → 𝑥 = (0g𝑔)) ∧ ∀𝑦𝑣 ((*𝑟𝑓)‘(𝑥𝑦)) = (𝑦𝑥)))
42 cip 16140 . . . . . 6 class ·𝑖
4317, 42cfv 6041 . . . . 5 class (·𝑖𝑔)
4441, 12, 43wsbc 3568 . . . 4 wff [(·𝑖𝑔) / ][(Scalar‘𝑔) / 𝑓](𝑓 ∈ *-Ring ∧ ∀𝑥𝑣 ((𝑦𝑣 ↦ (𝑦𝑥)) ∈ (𝑔 LMHom (ringLMod‘𝑓)) ∧ ((𝑥𝑥) = (0g𝑓) → 𝑥 = (0g𝑔)) ∧ ∀𝑦𝑣 ((*𝑟𝑓)‘(𝑥𝑦)) = (𝑦𝑥)))
45 cbs 16051 . . . . 5 class Base
4617, 45cfv 6041 . . . 4 class (Base‘𝑔)
4744, 7, 46wsbc 3568 . . 3 wff [(Base‘𝑔) / 𝑣][(·𝑖𝑔) / ][(Scalar‘𝑔) / 𝑓](𝑓 ∈ *-Ring ∧ ∀𝑥𝑣 ((𝑦𝑣 ↦ (𝑦𝑥)) ∈ (𝑔 LMHom (ringLMod‘𝑓)) ∧ ((𝑥𝑥) = (0g𝑓) → 𝑥 = (0g𝑔)) ∧ ∀𝑦𝑣 ((*𝑟𝑓)‘(𝑥𝑦)) = (𝑦𝑥)))
48 clvec 19296 . . 3 class LVec
4947, 16, 48crab 3046 . 2 class {𝑔 ∈ LVec ∣ [(Base‘𝑔) / 𝑣][(·𝑖𝑔) / ][(Scalar‘𝑔) / 𝑓](𝑓 ∈ *-Ring ∧ ∀𝑥𝑣 ((𝑦𝑣 ↦ (𝑦𝑥)) ∈ (𝑔 LMHom (ringLMod‘𝑓)) ∧ ((𝑥𝑥) = (0g𝑓) → 𝑥 = (0g𝑔)) ∧ ∀𝑦𝑣 ((*𝑟𝑓)‘(𝑥𝑦)) = (𝑦𝑥)))}
501, 49wceq 1624 1 wff PreHil = {𝑔 ∈ LVec ∣ [(Base‘𝑔) / 𝑣][(·𝑖𝑔) / ][(Scalar‘𝑔) / 𝑓](𝑓 ∈ *-Ring ∧ ∀𝑥𝑣 ((𝑦𝑣 ↦ (𝑦𝑥)) ∈ (𝑔 LMHom (ringLMod‘𝑓)) ∧ ((𝑥𝑥) = (0g𝑓) → 𝑥 = (0g𝑔)) ∧ ∀𝑦𝑣 ((*𝑟𝑓)‘(𝑥𝑦)) = (𝑦𝑥)))}
Colors of variables: wff setvar class
This definition is referenced by:  isphl  20167
  Copyright terms: Public domain W3C validator