# Metamath Proof Explorer

## Definition df-phl

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)

Ref Expression
Assertion df-phl

### Detailed syntax breakdown

Step Hyp Ref Expression
0 cphl ${class}\mathrm{PreHil}$
1 vg ${setvar}{g}$
2 clvec ${class}\mathrm{LVec}$
3 cbs ${class}\mathrm{Base}$
4 1 cv ${setvar}{g}$
5 4 3 cfv ${class}{\mathrm{Base}}_{{g}}$
6 vv ${setvar}{v}$
7 cip ${class}{\cdot }_{𝑖}$
8 4 7 cfv ${class}{\cdot }_{𝑖}\left({g}\right)$
9 vh ${setvar}{h}$
10 csca ${class}\mathrm{Scalar}$
11 4 10 cfv ${class}\mathrm{Scalar}\left({g}\right)$
12 vf ${setvar}{f}$
13 12 cv ${setvar}{f}$
14 csr ${class}\mathrm{*-Ring}$
15 13 14 wcel ${wff}{f}\in \mathrm{*-Ring}$
16 vx ${setvar}{x}$
17 6 cv ${setvar}{v}$
18 vy ${setvar}{y}$
19 18 cv ${setvar}{y}$
20 9 cv ${setvar}{h}$
21 16 cv ${setvar}{x}$
22 19 21 20 co ${class}\left({y}{h}{x}\right)$
23 18 17 22 cmpt ${class}\left({y}\in {v}⟼{y}{h}{x}\right)$
24 clmhm ${class}\mathrm{LMHom}$
25 crglmod ${class}\mathrm{ringLMod}$
26 13 25 cfv ${class}\mathrm{ringLMod}\left({f}\right)$
27 4 26 24 co ${class}\left({g}\mathrm{LMHom}\mathrm{ringLMod}\left({f}\right)\right)$
28 23 27 wcel ${wff}\left({y}\in {v}⟼{y}{h}{x}\right)\in \left({g}\mathrm{LMHom}\mathrm{ringLMod}\left({f}\right)\right)$
29 21 21 20 co ${class}\left({x}{h}{x}\right)$
30 c0g ${class}{0}_{𝑔}$
31 13 30 cfv ${class}{0}_{{f}}$
32 29 31 wceq ${wff}{x}{h}{x}={0}_{{f}}$
33 4 30 cfv ${class}{0}_{{g}}$
34 21 33 wceq ${wff}{x}={0}_{{g}}$
35 32 34 wi ${wff}\left({x}{h}{x}={0}_{{f}}\to {x}={0}_{{g}}\right)$
36 cstv ${class}{\ast }_{𝑟}$
37 13 36 cfv ${class}{*}_{{f}}$
38 21 19 20 co ${class}\left({x}{h}{y}\right)$
39 38 37 cfv ${class}{\left({x}{h}{y}\right)}^{{*}_{{f}}}$
40 39 22 wceq ${wff}{\left({x}{h}{y}\right)}^{{*}_{{f}}}={y}{h}{x}$
41 40 18 17 wral ${wff}\forall {y}\in {v}\phantom{\rule{.4em}{0ex}}{\left({x}{h}{y}\right)}^{{*}_{{f}}}={y}{h}{x}$
42 28 35 41 w3a ${wff}\left(\left({y}\in {v}⟼{y}{h}{x}\right)\in \left({g}\mathrm{LMHom}\mathrm{ringLMod}\left({f}\right)\right)\wedge \left({x}{h}{x}={0}_{{f}}\to {x}={0}_{{g}}\right)\wedge \forall {y}\in {v}\phantom{\rule{.4em}{0ex}}{\left({x}{h}{y}\right)}^{{*}_{{f}}}={y}{h}{x}\right)$
43 42 16 17 wral ${wff}\forall {x}\in {v}\phantom{\rule{.4em}{0ex}}\left(\left({y}\in {v}⟼{y}{h}{x}\right)\in \left({g}\mathrm{LMHom}\mathrm{ringLMod}\left({f}\right)\right)\wedge \left({x}{h}{x}={0}_{{f}}\to {x}={0}_{{g}}\right)\wedge \forall {y}\in {v}\phantom{\rule{.4em}{0ex}}{\left({x}{h}{y}\right)}^{{*}_{{f}}}={y}{h}{x}\right)$
44 15 43 wa ${wff}\left({f}\in \mathrm{*-Ring}\wedge \forall {x}\in {v}\phantom{\rule{.4em}{0ex}}\left(\left({y}\in {v}⟼{y}{h}{x}\right)\in \left({g}\mathrm{LMHom}\mathrm{ringLMod}\left({f}\right)\right)\wedge \left({x}{h}{x}={0}_{{f}}\to {x}={0}_{{g}}\right)\wedge \forall {y}\in {v}\phantom{\rule{.4em}{0ex}}{\left({x}{h}{y}\right)}^{{*}_{{f}}}={y}{h}{x}\right)\right)$
45 44 12 11 wsbc
46 45 9 8 wsbc
47 46 6 5 wsbc
48 47 1 2 crab
49 0 48 wceq