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 20181
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 20179 . 2 class PreHil
2 vf . . . . . . . . 9 setvar 𝑓
32cv 1636 . . . . . . . 8 class 𝑓
4 csr 19048 . . . . . . . 8 class *-Ring
53, 4wcel 2156 . . . . . . 7 wff 𝑓 ∈ *-Ring
6 vy . . . . . . . . . . 11 setvar 𝑦
7 vv . . . . . . . . . . . 12 setvar 𝑣
87cv 1636 . . . . . . . . . . 11 class 𝑣
96cv 1636 . . . . . . . . . . . 12 class 𝑦
10 vx . . . . . . . . . . . . 13 setvar 𝑥
1110cv 1636 . . . . . . . . . . . 12 class 𝑥
12 vh . . . . . . . . . . . . 13 setvar
1312cv 1636 . . . . . . . . . . . 12 class
149, 11, 13co 6874 . . . . . . . . . . 11 class (𝑦𝑥)
156, 8, 14cmpt 4923 . . . . . . . . . 10 class (𝑦𝑣 ↦ (𝑦𝑥))
16 vg . . . . . . . . . . . 12 setvar 𝑔
1716cv 1636 . . . . . . . . . . 11 class 𝑔
18 crglmod 19378 . . . . . . . . . . . 12 class ringLMod
193, 18cfv 6101 . . . . . . . . . . 11 class (ringLMod‘𝑓)
20 clmhm 19226 . . . . . . . . . . 11 class LMHom
2117, 19, 20co 6874 . . . . . . . . . 10 class (𝑔 LMHom (ringLMod‘𝑓))
2215, 21wcel 2156 . . . . . . . . 9 wff (𝑦𝑣 ↦ (𝑦𝑥)) ∈ (𝑔 LMHom (ringLMod‘𝑓))
2311, 11, 13co 6874 . . . . . . . . . . 11 class (𝑥𝑥)
24 c0g 16305 . . . . . . . . . . . 12 class 0g
253, 24cfv 6101 . . . . . . . . . . 11 class (0g𝑓)
2623, 25wceq 1637 . . . . . . . . . 10 wff (𝑥𝑥) = (0g𝑓)
2717, 24cfv 6101 . . . . . . . . . . 11 class (0g𝑔)
2811, 27wceq 1637 . . . . . . . . . 10 wff 𝑥 = (0g𝑔)
2926, 28wi 4 . . . . . . . . 9 wff ((𝑥𝑥) = (0g𝑓) → 𝑥 = (0g𝑔))
3011, 9, 13co 6874 . . . . . . . . . . . 12 class (𝑥𝑦)
31 cstv 16155 . . . . . . . . . . . . 13 class *𝑟
323, 31cfv 6101 . . . . . . . . . . . 12 class (*𝑟𝑓)
3330, 32cfv 6101 . . . . . . . . . . 11 class ((*𝑟𝑓)‘(𝑥𝑦))
3433, 14wceq 1637 . . . . . . . . . 10 wff ((*𝑟𝑓)‘(𝑥𝑦)) = (𝑦𝑥)
3534, 6, 8wral 3096 . . . . . . . . 9 wff 𝑦𝑣 ((*𝑟𝑓)‘(𝑥𝑦)) = (𝑦𝑥)
3622, 29, 35w3a 1100 . . . . . . . 8 wff ((𝑦𝑣 ↦ (𝑦𝑥)) ∈ (𝑔 LMHom (ringLMod‘𝑓)) ∧ ((𝑥𝑥) = (0g𝑓) → 𝑥 = (0g𝑔)) ∧ ∀𝑦𝑣 ((*𝑟𝑓)‘(𝑥𝑦)) = (𝑦𝑥))
3736, 10, 8wral 3096 . . . . . . 7 wff 𝑥𝑣 ((𝑦𝑣 ↦ (𝑦𝑥)) ∈ (𝑔 LMHom (ringLMod‘𝑓)) ∧ ((𝑥𝑥) = (0g𝑓) → 𝑥 = (0g𝑔)) ∧ ∀𝑦𝑣 ((*𝑟𝑓)‘(𝑥𝑦)) = (𝑦𝑥))
385, 37wa 384 . . . . . 6 wff (𝑓 ∈ *-Ring ∧ ∀𝑥𝑣 ((𝑦𝑣 ↦ (𝑦𝑥)) ∈ (𝑔 LMHom (ringLMod‘𝑓)) ∧ ((𝑥𝑥) = (0g𝑓) → 𝑥 = (0g𝑔)) ∧ ∀𝑦𝑣 ((*𝑟𝑓)‘(𝑥𝑦)) = (𝑦𝑥)))
39 csca 16156 . . . . . . 7 class Scalar
4017, 39cfv 6101 . . . . . 6 class (Scalar‘𝑔)
4138, 2, 40wsbc 3633 . . . . 5 wff [(Scalar‘𝑔) / 𝑓](𝑓 ∈ *-Ring ∧ ∀𝑥𝑣 ((𝑦𝑣 ↦ (𝑦𝑥)) ∈ (𝑔 LMHom (ringLMod‘𝑓)) ∧ ((𝑥𝑥) = (0g𝑓) → 𝑥 = (0g𝑔)) ∧ ∀𝑦𝑣 ((*𝑟𝑓)‘(𝑥𝑦)) = (𝑦𝑥)))
42 cip 16158 . . . . . 6 class ·𝑖
4317, 42cfv 6101 . . . . 5 class (·𝑖𝑔)
4441, 12, 43wsbc 3633 . . . 4 wff [(·𝑖𝑔) / ][(Scalar‘𝑔) / 𝑓](𝑓 ∈ *-Ring ∧ ∀𝑥𝑣 ((𝑦𝑣 ↦ (𝑦𝑥)) ∈ (𝑔 LMHom (ringLMod‘𝑓)) ∧ ((𝑥𝑥) = (0g𝑓) → 𝑥 = (0g𝑔)) ∧ ∀𝑦𝑣 ((*𝑟𝑓)‘(𝑥𝑦)) = (𝑦𝑥)))
45 cbs 16068 . . . . 5 class Base
4617, 45cfv 6101 . . . 4 class (Base‘𝑔)
4744, 7, 46wsbc 3633 . . 3 wff [(Base‘𝑔) / 𝑣][(·𝑖𝑔) / ][(Scalar‘𝑔) / 𝑓](𝑓 ∈ *-Ring ∧ ∀𝑥𝑣 ((𝑦𝑣 ↦ (𝑦𝑥)) ∈ (𝑔 LMHom (ringLMod‘𝑓)) ∧ ((𝑥𝑥) = (0g𝑓) → 𝑥 = (0g𝑔)) ∧ ∀𝑦𝑣 ((*𝑟𝑓)‘(𝑥𝑦)) = (𝑦𝑥)))
48 clvec 19309 . . 3 class LVec
4947, 16, 48crab 3100 . 2 class {𝑔 ∈ LVec ∣ [(Base‘𝑔) / 𝑣][(·𝑖𝑔) / ][(Scalar‘𝑔) / 𝑓](𝑓 ∈ *-Ring ∧ ∀𝑥𝑣 ((𝑦𝑣 ↦ (𝑦𝑥)) ∈ (𝑔 LMHom (ringLMod‘𝑓)) ∧ ((𝑥𝑥) = (0g𝑓) → 𝑥 = (0g𝑔)) ∧ ∀𝑦𝑣 ((*𝑟𝑓)‘(𝑥𝑦)) = (𝑦𝑥)))}
501, 49wceq 1637 1 wff PreHil = {𝑔 ∈ LVec ∣ [(Base‘𝑔) / 𝑣][(·𝑖𝑔) / ][(Scalar‘𝑔) / 𝑓](𝑓 ∈ *-Ring ∧ ∀𝑥𝑣 ((𝑦𝑣 ↦ (𝑦𝑥)) ∈ (𝑔 LMHom (ringLMod‘𝑓)) ∧ ((𝑥𝑥) = (0g𝑓) → 𝑥 = (0g𝑔)) ∧ ∀𝑦𝑣 ((*𝑟𝑓)‘(𝑥𝑦)) = (𝑦𝑥)))}
Colors of variables: wff setvar class
This definition is referenced by:  isphl  20183
  Copyright terms: Public domain W3C validator