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 21179
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 21177 . 2 class PreHil
2 vf . . . . . . . . 9 setvar 𝑓
32cv 1541 . . . . . . . 8 class 𝑓
4 csr 20452 . . . . . . . 8 class *-Ring
53, 4wcel 2107 . . . . . . 7 wff 𝑓 ∈ *-Ring
6 vy . . . . . . . . . . 11 setvar 𝑦
7 vv . . . . . . . . . . . 12 setvar 𝑣
87cv 1541 . . . . . . . . . . 11 class 𝑣
96cv 1541 . . . . . . . . . . . 12 class 𝑦
10 vx . . . . . . . . . . . . 13 setvar π‘₯
1110cv 1541 . . . . . . . . . . . 12 class π‘₯
12 vh . . . . . . . . . . . . 13 setvar β„Ž
1312cv 1541 . . . . . . . . . . . 12 class β„Ž
149, 11, 13co 7409 . . . . . . . . . . 11 class (π‘¦β„Žπ‘₯)
156, 8, 14cmpt 5232 . . . . . . . . . 10 class (𝑦 ∈ 𝑣 ↦ (π‘¦β„Žπ‘₯))
16 vg . . . . . . . . . . . 12 setvar 𝑔
1716cv 1541 . . . . . . . . . . 11 class 𝑔
18 crglmod 20782 . . . . . . . . . . . 12 class ringLMod
193, 18cfv 6544 . . . . . . . . . . 11 class (ringLModβ€˜π‘“)
20 clmhm 20630 . . . . . . . . . . 11 class LMHom
2117, 19, 20co 7409 . . . . . . . . . 10 class (𝑔 LMHom (ringLModβ€˜π‘“))
2215, 21wcel 2107 . . . . . . . . 9 wff (𝑦 ∈ 𝑣 ↦ (π‘¦β„Žπ‘₯)) ∈ (𝑔 LMHom (ringLModβ€˜π‘“))
2311, 11, 13co 7409 . . . . . . . . . . 11 class (π‘₯β„Žπ‘₯)
24 c0g 17385 . . . . . . . . . . . 12 class 0g
253, 24cfv 6544 . . . . . . . . . . 11 class (0gβ€˜π‘“)
2623, 25wceq 1542 . . . . . . . . . 10 wff (π‘₯β„Žπ‘₯) = (0gβ€˜π‘“)
2717, 24cfv 6544 . . . . . . . . . . 11 class (0gβ€˜π‘”)
2811, 27wceq 1542 . . . . . . . . . 10 wff π‘₯ = (0gβ€˜π‘”)
2926, 28wi 4 . . . . . . . . 9 wff ((π‘₯β„Žπ‘₯) = (0gβ€˜π‘“) β†’ π‘₯ = (0gβ€˜π‘”))
3011, 9, 13co 7409 . . . . . . . . . . . 12 class (π‘₯β„Žπ‘¦)
31 cstv 17199 . . . . . . . . . . . . 13 class *π‘Ÿ
323, 31cfv 6544 . . . . . . . . . . . 12 class (*π‘Ÿβ€˜π‘“)
3330, 32cfv 6544 . . . . . . . . . . 11 class ((*π‘Ÿβ€˜π‘“)β€˜(π‘₯β„Žπ‘¦))
3433, 14wceq 1542 . . . . . . . . . 10 wff ((*π‘Ÿβ€˜π‘“)β€˜(π‘₯β„Žπ‘¦)) = (π‘¦β„Žπ‘₯)
3534, 6, 8wral 3062 . . . . . . . . 9 wff βˆ€π‘¦ ∈ 𝑣 ((*π‘Ÿβ€˜π‘“)β€˜(π‘₯β„Žπ‘¦)) = (π‘¦β„Žπ‘₯)
3622, 29, 35w3a 1088 . . . . . . . 8 wff ((𝑦 ∈ 𝑣 ↦ (π‘¦β„Žπ‘₯)) ∈ (𝑔 LMHom (ringLModβ€˜π‘“)) ∧ ((π‘₯β„Žπ‘₯) = (0gβ€˜π‘“) β†’ π‘₯ = (0gβ€˜π‘”)) ∧ βˆ€π‘¦ ∈ 𝑣 ((*π‘Ÿβ€˜π‘“)β€˜(π‘₯β„Žπ‘¦)) = (π‘¦β„Žπ‘₯))
3736, 10, 8wral 3062 . . . . . . 7 wff βˆ€π‘₯ ∈ 𝑣 ((𝑦 ∈ 𝑣 ↦ (π‘¦β„Žπ‘₯)) ∈ (𝑔 LMHom (ringLModβ€˜π‘“)) ∧ ((π‘₯β„Žπ‘₯) = (0gβ€˜π‘“) β†’ π‘₯ = (0gβ€˜π‘”)) ∧ βˆ€π‘¦ ∈ 𝑣 ((*π‘Ÿβ€˜π‘“)β€˜(π‘₯β„Žπ‘¦)) = (π‘¦β„Žπ‘₯))
385, 37wa 397 . . . . . 6 wff (𝑓 ∈ *-Ring ∧ βˆ€π‘₯ ∈ 𝑣 ((𝑦 ∈ 𝑣 ↦ (π‘¦β„Žπ‘₯)) ∈ (𝑔 LMHom (ringLModβ€˜π‘“)) ∧ ((π‘₯β„Žπ‘₯) = (0gβ€˜π‘“) β†’ π‘₯ = (0gβ€˜π‘”)) ∧ βˆ€π‘¦ ∈ 𝑣 ((*π‘Ÿβ€˜π‘“)β€˜(π‘₯β„Žπ‘¦)) = (π‘¦β„Žπ‘₯)))
39 csca 17200 . . . . . . 7 class Scalar
4017, 39cfv 6544 . . . . . 6 class (Scalarβ€˜π‘”)
4138, 2, 40wsbc 3778 . . . . 5 wff [(Scalarβ€˜π‘”) / 𝑓](𝑓 ∈ *-Ring ∧ βˆ€π‘₯ ∈ 𝑣 ((𝑦 ∈ 𝑣 ↦ (π‘¦β„Žπ‘₯)) ∈ (𝑔 LMHom (ringLModβ€˜π‘“)) ∧ ((π‘₯β„Žπ‘₯) = (0gβ€˜π‘“) β†’ π‘₯ = (0gβ€˜π‘”)) ∧ βˆ€π‘¦ ∈ 𝑣 ((*π‘Ÿβ€˜π‘“)β€˜(π‘₯β„Žπ‘¦)) = (π‘¦β„Žπ‘₯)))
42 cip 17202 . . . . . 6 class ·𝑖
4317, 42cfv 6544 . . . . 5 class (Β·π‘–β€˜π‘”)
4441, 12, 43wsbc 3778 . . . 4 wff [(Β·π‘–β€˜π‘”) / β„Ž][(Scalarβ€˜π‘”) / 𝑓](𝑓 ∈ *-Ring ∧ βˆ€π‘₯ ∈ 𝑣 ((𝑦 ∈ 𝑣 ↦ (π‘¦β„Žπ‘₯)) ∈ (𝑔 LMHom (ringLModβ€˜π‘“)) ∧ ((π‘₯β„Žπ‘₯) = (0gβ€˜π‘“) β†’ π‘₯ = (0gβ€˜π‘”)) ∧ βˆ€π‘¦ ∈ 𝑣 ((*π‘Ÿβ€˜π‘“)β€˜(π‘₯β„Žπ‘¦)) = (π‘¦β„Žπ‘₯)))
45 cbs 17144 . . . . 5 class Base
4617, 45cfv 6544 . . . 4 class (Baseβ€˜π‘”)
4744, 7, 46wsbc 3778 . . 3 wff [(Baseβ€˜π‘”) / 𝑣][(Β·π‘–β€˜π‘”) / β„Ž][(Scalarβ€˜π‘”) / 𝑓](𝑓 ∈ *-Ring ∧ βˆ€π‘₯ ∈ 𝑣 ((𝑦 ∈ 𝑣 ↦ (π‘¦β„Žπ‘₯)) ∈ (𝑔 LMHom (ringLModβ€˜π‘“)) ∧ ((π‘₯β„Žπ‘₯) = (0gβ€˜π‘“) β†’ π‘₯ = (0gβ€˜π‘”)) ∧ βˆ€π‘¦ ∈ 𝑣 ((*π‘Ÿβ€˜π‘“)β€˜(π‘₯β„Žπ‘¦)) = (π‘¦β„Žπ‘₯)))
48 clvec 20713 . . 3 class LVec
4947, 16, 48crab 3433 . 2 class {𝑔 ∈ LVec ∣ [(Baseβ€˜π‘”) / 𝑣][(Β·π‘–β€˜π‘”) / β„Ž][(Scalarβ€˜π‘”) / 𝑓](𝑓 ∈ *-Ring ∧ βˆ€π‘₯ ∈ 𝑣 ((𝑦 ∈ 𝑣 ↦ (π‘¦β„Žπ‘₯)) ∈ (𝑔 LMHom (ringLModβ€˜π‘“)) ∧ ((π‘₯β„Žπ‘₯) = (0gβ€˜π‘“) β†’ π‘₯ = (0gβ€˜π‘”)) ∧ βˆ€π‘¦ ∈ 𝑣 ((*π‘Ÿβ€˜π‘“)β€˜(π‘₯β„Žπ‘¦)) = (π‘¦β„Žπ‘₯)))}
501, 49wceq 1542 1 wff PreHil = {𝑔 ∈ LVec ∣ [(Baseβ€˜π‘”) / 𝑣][(Β·π‘–β€˜π‘”) / β„Ž][(Scalarβ€˜π‘”) / 𝑓](𝑓 ∈ *-Ring ∧ βˆ€π‘₯ ∈ 𝑣 ((𝑦 ∈ 𝑣 ↦ (π‘¦β„Žπ‘₯)) ∈ (𝑔 LMHom (ringLModβ€˜π‘“)) ∧ ((π‘₯β„Žπ‘₯) = (0gβ€˜π‘“) β†’ π‘₯ = (0gβ€˜π‘”)) ∧ βˆ€π‘¦ ∈ 𝑣 ((*π‘Ÿβ€˜π‘“)β€˜(π‘₯β„Žπ‘¦)) = (π‘¦β„Žπ‘₯)))}
Colors of variables: wff setvar class
This definition is referenced by:  isphl  21181
  Copyright terms: Public domain W3C validator