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 20313
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 20311 . 2 class PreHil
2 vf . . . . . . . . 9 setvar 𝑓
32cv 1537 . . . . . . . 8 class 𝑓
4 csr 19606 . . . . . . . 8 class *-Ring
53, 4wcel 2114 . . . . . . 7 wff 𝑓 ∈ *-Ring
6 vy . . . . . . . . . . 11 setvar 𝑦
7 vv . . . . . . . . . . . 12 setvar 𝑣
87cv 1537 . . . . . . . . . . 11 class 𝑣
96cv 1537 . . . . . . . . . . . 12 class 𝑦
10 vx . . . . . . . . . . . . 13 setvar 𝑥
1110cv 1537 . . . . . . . . . . . 12 class 𝑥
12 vh . . . . . . . . . . . . 13 setvar
1312cv 1537 . . . . . . . . . . . 12 class
149, 11, 13co 7140 . . . . . . . . . . 11 class (𝑦𝑥)
156, 8, 14cmpt 5122 . . . . . . . . . 10 class (𝑦𝑣 ↦ (𝑦𝑥))
16 vg . . . . . . . . . . . 12 setvar 𝑔
1716cv 1537 . . . . . . . . . . 11 class 𝑔
18 crglmod 19932 . . . . . . . . . . . 12 class ringLMod
193, 18cfv 6334 . . . . . . . . . . 11 class (ringLMod‘𝑓)
20 clmhm 19782 . . . . . . . . . . 11 class LMHom
2117, 19, 20co 7140 . . . . . . . . . 10 class (𝑔 LMHom (ringLMod‘𝑓))
2215, 21wcel 2114 . . . . . . . . 9 wff (𝑦𝑣 ↦ (𝑦𝑥)) ∈ (𝑔 LMHom (ringLMod‘𝑓))
2311, 11, 13co 7140 . . . . . . . . . . 11 class (𝑥𝑥)
24 c0g 16704 . . . . . . . . . . . 12 class 0g
253, 24cfv 6334 . . . . . . . . . . 11 class (0g𝑓)
2623, 25wceq 1538 . . . . . . . . . 10 wff (𝑥𝑥) = (0g𝑓)
2717, 24cfv 6334 . . . . . . . . . . 11 class (0g𝑔)
2811, 27wceq 1538 . . . . . . . . . 10 wff 𝑥 = (0g𝑔)
2926, 28wi 4 . . . . . . . . 9 wff ((𝑥𝑥) = (0g𝑓) → 𝑥 = (0g𝑔))
3011, 9, 13co 7140 . . . . . . . . . . . 12 class (𝑥𝑦)
31 cstv 16558 . . . . . . . . . . . . 13 class *𝑟
323, 31cfv 6334 . . . . . . . . . . . 12 class (*𝑟𝑓)
3330, 32cfv 6334 . . . . . . . . . . 11 class ((*𝑟𝑓)‘(𝑥𝑦))
3433, 14wceq 1538 . . . . . . . . . 10 wff ((*𝑟𝑓)‘(𝑥𝑦)) = (𝑦𝑥)
3534, 6, 8wral 3130 . . . . . . . . 9 wff 𝑦𝑣 ((*𝑟𝑓)‘(𝑥𝑦)) = (𝑦𝑥)
3622, 29, 35w3a 1084 . . . . . . . 8 wff ((𝑦𝑣 ↦ (𝑦𝑥)) ∈ (𝑔 LMHom (ringLMod‘𝑓)) ∧ ((𝑥𝑥) = (0g𝑓) → 𝑥 = (0g𝑔)) ∧ ∀𝑦𝑣 ((*𝑟𝑓)‘(𝑥𝑦)) = (𝑦𝑥))
3736, 10, 8wral 3130 . . . . . . 7 wff 𝑥𝑣 ((𝑦𝑣 ↦ (𝑦𝑥)) ∈ (𝑔 LMHom (ringLMod‘𝑓)) ∧ ((𝑥𝑥) = (0g𝑓) → 𝑥 = (0g𝑔)) ∧ ∀𝑦𝑣 ((*𝑟𝑓)‘(𝑥𝑦)) = (𝑦𝑥))
385, 37wa 399 . . . . . 6 wff (𝑓 ∈ *-Ring ∧ ∀𝑥𝑣 ((𝑦𝑣 ↦ (𝑦𝑥)) ∈ (𝑔 LMHom (ringLMod‘𝑓)) ∧ ((𝑥𝑥) = (0g𝑓) → 𝑥 = (0g𝑔)) ∧ ∀𝑦𝑣 ((*𝑟𝑓)‘(𝑥𝑦)) = (𝑦𝑥)))
39 csca 16559 . . . . . . 7 class Scalar
4017, 39cfv 6334 . . . . . 6 class (Scalar‘𝑔)
4138, 2, 40wsbc 3747 . . . . 5 wff [(Scalar‘𝑔) / 𝑓](𝑓 ∈ *-Ring ∧ ∀𝑥𝑣 ((𝑦𝑣 ↦ (𝑦𝑥)) ∈ (𝑔 LMHom (ringLMod‘𝑓)) ∧ ((𝑥𝑥) = (0g𝑓) → 𝑥 = (0g𝑔)) ∧ ∀𝑦𝑣 ((*𝑟𝑓)‘(𝑥𝑦)) = (𝑦𝑥)))
42 cip 16561 . . . . . 6 class ·𝑖
4317, 42cfv 6334 . . . . 5 class (·𝑖𝑔)
4441, 12, 43wsbc 3747 . . . 4 wff [(·𝑖𝑔) / ][(Scalar‘𝑔) / 𝑓](𝑓 ∈ *-Ring ∧ ∀𝑥𝑣 ((𝑦𝑣 ↦ (𝑦𝑥)) ∈ (𝑔 LMHom (ringLMod‘𝑓)) ∧ ((𝑥𝑥) = (0g𝑓) → 𝑥 = (0g𝑔)) ∧ ∀𝑦𝑣 ((*𝑟𝑓)‘(𝑥𝑦)) = (𝑦𝑥)))
45 cbs 16474 . . . . 5 class Base
4617, 45cfv 6334 . . . 4 class (Base‘𝑔)
4744, 7, 46wsbc 3747 . . 3 wff [(Base‘𝑔) / 𝑣][(·𝑖𝑔) / ][(Scalar‘𝑔) / 𝑓](𝑓 ∈ *-Ring ∧ ∀𝑥𝑣 ((𝑦𝑣 ↦ (𝑦𝑥)) ∈ (𝑔 LMHom (ringLMod‘𝑓)) ∧ ((𝑥𝑥) = (0g𝑓) → 𝑥 = (0g𝑔)) ∧ ∀𝑦𝑣 ((*𝑟𝑓)‘(𝑥𝑦)) = (𝑦𝑥)))
48 clvec 19865 . . 3 class LVec
4947, 16, 48crab 3134 . 2 class {𝑔 ∈ LVec ∣ [(Base‘𝑔) / 𝑣][(·𝑖𝑔) / ][(Scalar‘𝑔) / 𝑓](𝑓 ∈ *-Ring ∧ ∀𝑥𝑣 ((𝑦𝑣 ↦ (𝑦𝑥)) ∈ (𝑔 LMHom (ringLMod‘𝑓)) ∧ ((𝑥𝑥) = (0g𝑓) → 𝑥 = (0g𝑔)) ∧ ∀𝑦𝑣 ((*𝑟𝑓)‘(𝑥𝑦)) = (𝑦𝑥)))}
501, 49wceq 1538 1 wff PreHil = {𝑔 ∈ LVec ∣ [(Base‘𝑔) / 𝑣][(·𝑖𝑔) / ][(Scalar‘𝑔) / 𝑓](𝑓 ∈ *-Ring ∧ ∀𝑥𝑣 ((𝑦𝑣 ↦ (𝑦𝑥)) ∈ (𝑔 LMHom (ringLMod‘𝑓)) ∧ ((𝑥𝑥) = (0g𝑓) → 𝑥 = (0g𝑔)) ∧ ∀𝑦𝑣 ((*𝑟𝑓)‘(𝑥𝑦)) = (𝑦𝑥)))}
Colors of variables: wff setvar class
This definition is referenced by:  isphl  20315
  Copyright terms: Public domain W3C validator