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 20019
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 20017 . 2 class PreHil
2 vf . . . . . . . . 9 setvar 𝑓
32cv 1522 . . . . . . . 8 class 𝑓
4 csr 18892 . . . . . . . 8 class *-Ring
53, 4wcel 2030 . . . . . . 7 wff 𝑓 ∈ *-Ring
6 vy . . . . . . . . . . 11 setvar 𝑦
7 vv . . . . . . . . . . . 12 setvar 𝑣
87cv 1522 . . . . . . . . . . 11 class 𝑣
96cv 1522 . . . . . . . . . . . 12 class 𝑦
10 vx . . . . . . . . . . . . 13 setvar 𝑥
1110cv 1522 . . . . . . . . . . . 12 class 𝑥
12 vh . . . . . . . . . . . . 13 setvar
1312cv 1522 . . . . . . . . . . . 12 class
149, 11, 13co 6690 . . . . . . . . . . 11 class (𝑦𝑥)
156, 8, 14cmpt 4762 . . . . . . . . . 10 class (𝑦𝑣 ↦ (𝑦𝑥))
16 vg . . . . . . . . . . . 12 setvar 𝑔
1716cv 1522 . . . . . . . . . . 11 class 𝑔
18 crglmod 19217 . . . . . . . . . . . 12 class ringLMod
193, 18cfv 5926 . . . . . . . . . . 11 class (ringLMod‘𝑓)
20 clmhm 19067 . . . . . . . . . . 11 class LMHom
2117, 19, 20co 6690 . . . . . . . . . 10 class (𝑔 LMHom (ringLMod‘𝑓))
2215, 21wcel 2030 . . . . . . . . 9 wff (𝑦𝑣 ↦ (𝑦𝑥)) ∈ (𝑔 LMHom (ringLMod‘𝑓))
2311, 11, 13co 6690 . . . . . . . . . . 11 class (𝑥𝑥)
24 c0g 16147 . . . . . . . . . . . 12 class 0g
253, 24cfv 5926 . . . . . . . . . . 11 class (0g𝑓)
2623, 25wceq 1523 . . . . . . . . . 10 wff (𝑥𝑥) = (0g𝑓)
2717, 24cfv 5926 . . . . . . . . . . 11 class (0g𝑔)
2811, 27wceq 1523 . . . . . . . . . 10 wff 𝑥 = (0g𝑔)
2926, 28wi 4 . . . . . . . . 9 wff ((𝑥𝑥) = (0g𝑓) → 𝑥 = (0g𝑔))
3011, 9, 13co 6690 . . . . . . . . . . . 12 class (𝑥𝑦)
31 cstv 15990 . . . . . . . . . . . . 13 class *𝑟
323, 31cfv 5926 . . . . . . . . . . . 12 class (*𝑟𝑓)
3330, 32cfv 5926 . . . . . . . . . . 11 class ((*𝑟𝑓)‘(𝑥𝑦))
3433, 14wceq 1523 . . . . . . . . . 10 wff ((*𝑟𝑓)‘(𝑥𝑦)) = (𝑦𝑥)
3534, 6, 8wral 2941 . . . . . . . . 9 wff 𝑦𝑣 ((*𝑟𝑓)‘(𝑥𝑦)) = (𝑦𝑥)
3622, 29, 35w3a 1054 . . . . . . . 8 wff ((𝑦𝑣 ↦ (𝑦𝑥)) ∈ (𝑔 LMHom (ringLMod‘𝑓)) ∧ ((𝑥𝑥) = (0g𝑓) → 𝑥 = (0g𝑔)) ∧ ∀𝑦𝑣 ((*𝑟𝑓)‘(𝑥𝑦)) = (𝑦𝑥))
3736, 10, 8wral 2941 . . . . . . 7 wff 𝑥𝑣 ((𝑦𝑣 ↦ (𝑦𝑥)) ∈ (𝑔 LMHom (ringLMod‘𝑓)) ∧ ((𝑥𝑥) = (0g𝑓) → 𝑥 = (0g𝑔)) ∧ ∀𝑦𝑣 ((*𝑟𝑓)‘(𝑥𝑦)) = (𝑦𝑥))
385, 37wa 383 . . . . . 6 wff (𝑓 ∈ *-Ring ∧ ∀𝑥𝑣 ((𝑦𝑣 ↦ (𝑦𝑥)) ∈ (𝑔 LMHom (ringLMod‘𝑓)) ∧ ((𝑥𝑥) = (0g𝑓) → 𝑥 = (0g𝑔)) ∧ ∀𝑦𝑣 ((*𝑟𝑓)‘(𝑥𝑦)) = (𝑦𝑥)))
39 csca 15991 . . . . . . 7 class Scalar
4017, 39cfv 5926 . . . . . 6 class (Scalar‘𝑔)
4138, 2, 40wsbc 3468 . . . . 5 wff [(Scalar‘𝑔) / 𝑓](𝑓 ∈ *-Ring ∧ ∀𝑥𝑣 ((𝑦𝑣 ↦ (𝑦𝑥)) ∈ (𝑔 LMHom (ringLMod‘𝑓)) ∧ ((𝑥𝑥) = (0g𝑓) → 𝑥 = (0g𝑔)) ∧ ∀𝑦𝑣 ((*𝑟𝑓)‘(𝑥𝑦)) = (𝑦𝑥)))
42 cip 15993 . . . . . 6 class ·𝑖
4317, 42cfv 5926 . . . . 5 class (·𝑖𝑔)
4441, 12, 43wsbc 3468 . . . 4 wff [(·𝑖𝑔) / ][(Scalar‘𝑔) / 𝑓](𝑓 ∈ *-Ring ∧ ∀𝑥𝑣 ((𝑦𝑣 ↦ (𝑦𝑥)) ∈ (𝑔 LMHom (ringLMod‘𝑓)) ∧ ((𝑥𝑥) = (0g𝑓) → 𝑥 = (0g𝑔)) ∧ ∀𝑦𝑣 ((*𝑟𝑓)‘(𝑥𝑦)) = (𝑦𝑥)))
45 cbs 15904 . . . . 5 class Base
4617, 45cfv 5926 . . . 4 class (Base‘𝑔)
4744, 7, 46wsbc 3468 . . 3 wff [(Base‘𝑔) / 𝑣][(·𝑖𝑔) / ][(Scalar‘𝑔) / 𝑓](𝑓 ∈ *-Ring ∧ ∀𝑥𝑣 ((𝑦𝑣 ↦ (𝑦𝑥)) ∈ (𝑔 LMHom (ringLMod‘𝑓)) ∧ ((𝑥𝑥) = (0g𝑓) → 𝑥 = (0g𝑔)) ∧ ∀𝑦𝑣 ((*𝑟𝑓)‘(𝑥𝑦)) = (𝑦𝑥)))
48 clvec 19150 . . 3 class LVec
4947, 16, 48crab 2945 . 2 class {𝑔 ∈ LVec ∣ [(Base‘𝑔) / 𝑣][(·𝑖𝑔) / ][(Scalar‘𝑔) / 𝑓](𝑓 ∈ *-Ring ∧ ∀𝑥𝑣 ((𝑦𝑣 ↦ (𝑦𝑥)) ∈ (𝑔 LMHom (ringLMod‘𝑓)) ∧ ((𝑥𝑥) = (0g𝑓) → 𝑥 = (0g𝑔)) ∧ ∀𝑦𝑣 ((*𝑟𝑓)‘(𝑥𝑦)) = (𝑦𝑥)))}
501, 49wceq 1523 1 wff PreHil = {𝑔 ∈ LVec ∣ [(Base‘𝑔) / 𝑣][(·𝑖𝑔) / ][(Scalar‘𝑔) / 𝑓](𝑓 ∈ *-Ring ∧ ∀𝑥𝑣 ((𝑦𝑣 ↦ (𝑦𝑥)) ∈ (𝑔 LMHom (ringLMod‘𝑓)) ∧ ((𝑥𝑥) = (0g𝑓) → 𝑥 = (0g𝑔)) ∧ ∀𝑦𝑣 ((*𝑟𝑓)‘(𝑥𝑦)) = (𝑦𝑥)))}
Colors of variables: wff setvar class
This definition is referenced by:  isphl  20021
  Copyright terms: Public domain W3C validator