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 19735
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 19733 . 2 class PreHil
2 vf . . . . . . . . 9 setvar 𝑓
32cv 1473 . . . . . . . 8 class 𝑓
4 csr 18613 . . . . . . . 8 class *-Ring
53, 4wcel 1976 . . . . . . 7 wff 𝑓 ∈ *-Ring
6 vy . . . . . . . . . . 11 setvar 𝑦
7 vv . . . . . . . . . . . 12 setvar 𝑣
87cv 1473 . . . . . . . . . . 11 class 𝑣
96cv 1473 . . . . . . . . . . . 12 class 𝑦
10 vx . . . . . . . . . . . . 13 setvar 𝑥
1110cv 1473 . . . . . . . . . . . 12 class 𝑥
12 vh . . . . . . . . . . . . 13 setvar
1312cv 1473 . . . . . . . . . . . 12 class
149, 11, 13co 6527 . . . . . . . . . . 11 class (𝑦𝑥)
156, 8, 14cmpt 4637 . . . . . . . . . 10 class (𝑦𝑣 ↦ (𝑦𝑥))
16 vg . . . . . . . . . . . 12 setvar 𝑔
1716cv 1473 . . . . . . . . . . 11 class 𝑔
18 crglmod 18936 . . . . . . . . . . . 12 class ringLMod
193, 18cfv 5790 . . . . . . . . . . 11 class (ringLMod‘𝑓)
20 clmhm 18786 . . . . . . . . . . 11 class LMHom
2117, 19, 20co 6527 . . . . . . . . . 10 class (𝑔 LMHom (ringLMod‘𝑓))
2215, 21wcel 1976 . . . . . . . . 9 wff (𝑦𝑣 ↦ (𝑦𝑥)) ∈ (𝑔 LMHom (ringLMod‘𝑓))
2311, 11, 13co 6527 . . . . . . . . . . 11 class (𝑥𝑥)
24 c0g 15869 . . . . . . . . . . . 12 class 0g
253, 24cfv 5790 . . . . . . . . . . 11 class (0g𝑓)
2623, 25wceq 1474 . . . . . . . . . 10 wff (𝑥𝑥) = (0g𝑓)
2717, 24cfv 5790 . . . . . . . . . . 11 class (0g𝑔)
2811, 27wceq 1474 . . . . . . . . . 10 wff 𝑥 = (0g𝑔)
2926, 28wi 4 . . . . . . . . 9 wff ((𝑥𝑥) = (0g𝑓) → 𝑥 = (0g𝑔))
3011, 9, 13co 6527 . . . . . . . . . . . 12 class (𝑥𝑦)
31 cstv 15716 . . . . . . . . . . . . 13 class *𝑟
323, 31cfv 5790 . . . . . . . . . . . 12 class (*𝑟𝑓)
3330, 32cfv 5790 . . . . . . . . . . 11 class ((*𝑟𝑓)‘(𝑥𝑦))
3433, 14wceq 1474 . . . . . . . . . 10 wff ((*𝑟𝑓)‘(𝑥𝑦)) = (𝑦𝑥)
3534, 6, 8wral 2895 . . . . . . . . 9 wff 𝑦𝑣 ((*𝑟𝑓)‘(𝑥𝑦)) = (𝑦𝑥)
3622, 29, 35w3a 1030 . . . . . . . 8 wff ((𝑦𝑣 ↦ (𝑦𝑥)) ∈ (𝑔 LMHom (ringLMod‘𝑓)) ∧ ((𝑥𝑥) = (0g𝑓) → 𝑥 = (0g𝑔)) ∧ ∀𝑦𝑣 ((*𝑟𝑓)‘(𝑥𝑦)) = (𝑦𝑥))
3736, 10, 8wral 2895 . . . . . . 7 wff 𝑥𝑣 ((𝑦𝑣 ↦ (𝑦𝑥)) ∈ (𝑔 LMHom (ringLMod‘𝑓)) ∧ ((𝑥𝑥) = (0g𝑓) → 𝑥 = (0g𝑔)) ∧ ∀𝑦𝑣 ((*𝑟𝑓)‘(𝑥𝑦)) = (𝑦𝑥))
385, 37wa 382 . . . . . 6 wff (𝑓 ∈ *-Ring ∧ ∀𝑥𝑣 ((𝑦𝑣 ↦ (𝑦𝑥)) ∈ (𝑔 LMHom (ringLMod‘𝑓)) ∧ ((𝑥𝑥) = (0g𝑓) → 𝑥 = (0g𝑔)) ∧ ∀𝑦𝑣 ((*𝑟𝑓)‘(𝑥𝑦)) = (𝑦𝑥)))
39 csca 15717 . . . . . . 7 class Scalar
4017, 39cfv 5790 . . . . . 6 class (Scalar‘𝑔)
4138, 2, 40wsbc 3401 . . . . 5 wff [(Scalar‘𝑔) / 𝑓](𝑓 ∈ *-Ring ∧ ∀𝑥𝑣 ((𝑦𝑣 ↦ (𝑦𝑥)) ∈ (𝑔 LMHom (ringLMod‘𝑓)) ∧ ((𝑥𝑥) = (0g𝑓) → 𝑥 = (0g𝑔)) ∧ ∀𝑦𝑣 ((*𝑟𝑓)‘(𝑥𝑦)) = (𝑦𝑥)))
42 cip 15719 . . . . . 6 class ·𝑖
4317, 42cfv 5790 . . . . 5 class (·𝑖𝑔)
4441, 12, 43wsbc 3401 . . . 4 wff [(·𝑖𝑔) / ][(Scalar‘𝑔) / 𝑓](𝑓 ∈ *-Ring ∧ ∀𝑥𝑣 ((𝑦𝑣 ↦ (𝑦𝑥)) ∈ (𝑔 LMHom (ringLMod‘𝑓)) ∧ ((𝑥𝑥) = (0g𝑓) → 𝑥 = (0g𝑔)) ∧ ∀𝑦𝑣 ((*𝑟𝑓)‘(𝑥𝑦)) = (𝑦𝑥)))
45 cbs 15641 . . . . 5 class Base
4617, 45cfv 5790 . . . 4 class (Base‘𝑔)
4744, 7, 46wsbc 3401 . . 3 wff [(Base‘𝑔) / 𝑣][(·𝑖𝑔) / ][(Scalar‘𝑔) / 𝑓](𝑓 ∈ *-Ring ∧ ∀𝑥𝑣 ((𝑦𝑣 ↦ (𝑦𝑥)) ∈ (𝑔 LMHom (ringLMod‘𝑓)) ∧ ((𝑥𝑥) = (0g𝑓) → 𝑥 = (0g𝑔)) ∧ ∀𝑦𝑣 ((*𝑟𝑓)‘(𝑥𝑦)) = (𝑦𝑥)))
48 clvec 18869 . . 3 class LVec
4947, 16, 48crab 2899 . 2 class {𝑔 ∈ LVec ∣ [(Base‘𝑔) / 𝑣][(·𝑖𝑔) / ][(Scalar‘𝑔) / 𝑓](𝑓 ∈ *-Ring ∧ ∀𝑥𝑣 ((𝑦𝑣 ↦ (𝑦𝑥)) ∈ (𝑔 LMHom (ringLMod‘𝑓)) ∧ ((𝑥𝑥) = (0g𝑓) → 𝑥 = (0g𝑔)) ∧ ∀𝑦𝑣 ((*𝑟𝑓)‘(𝑥𝑦)) = (𝑦𝑥)))}
501, 49wceq 1474 1 wff PreHil = {𝑔 ∈ LVec ∣ [(Base‘𝑔) / 𝑣][(·𝑖𝑔) / ][(Scalar‘𝑔) / 𝑓](𝑓 ∈ *-Ring ∧ ∀𝑥𝑣 ((𝑦𝑣 ↦ (𝑦𝑥)) ∈ (𝑔 LMHom (ringLMod‘𝑓)) ∧ ((𝑥𝑥) = (0g𝑓) → 𝑥 = (0g𝑔)) ∧ ∀𝑦𝑣 ((*𝑟𝑓)‘(𝑥𝑦)) = (𝑦𝑥)))}
Colors of variables: wff setvar class
This definition is referenced by:  isphl  19737
  Copyright terms: Public domain W3C validator