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 PreHil = { 𝑔 ∈ LVec ∣ [ ( Base ‘ 𝑔 ) / 𝑣 ] [ ( ·𝑖𝑔 ) / ] [ ( Scalar ‘ 𝑔 ) / 𝑓 ] ( 𝑓 ∈ *-Ring ∧ ∀ 𝑥𝑣 ( ( 𝑦𝑣 ↦ ( 𝑦 𝑥 ) ) ∈ ( 𝑔 LMHom ( ringLMod ‘ 𝑓 ) ) ∧ ( ( 𝑥 𝑥 ) = ( 0g𝑓 ) → 𝑥 = ( 0g𝑔 ) ) ∧ ∀ 𝑦𝑣 ( ( *𝑟𝑓 ) ‘ ( 𝑥 𝑦 ) ) = ( 𝑦 𝑥 ) ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 cphl PreHil
1 vg 𝑔
2 clvec LVec
3 cbs Base
4 1 cv 𝑔
5 4 3 cfv ( Base ‘ 𝑔 )
6 vv 𝑣
7 cip ·𝑖
8 4 7 cfv ( ·𝑖𝑔 )
9 vh
10 csca Scalar
11 4 10 cfv ( Scalar ‘ 𝑔 )
12 vf 𝑓
13 12 cv 𝑓
14 csr *-Ring
15 13 14 wcel 𝑓 ∈ *-Ring
16 vx 𝑥
17 6 cv 𝑣
18 vy 𝑦
19 18 cv 𝑦
20 9 cv
21 16 cv 𝑥
22 19 21 20 co ( 𝑦 𝑥 )
23 18 17 22 cmpt ( 𝑦𝑣 ↦ ( 𝑦 𝑥 ) )
24 clmhm LMHom
25 crglmod ringLMod
26 13 25 cfv ( ringLMod ‘ 𝑓 )
27 4 26 24 co ( 𝑔 LMHom ( ringLMod ‘ 𝑓 ) )
28 23 27 wcel ( 𝑦𝑣 ↦ ( 𝑦 𝑥 ) ) ∈ ( 𝑔 LMHom ( ringLMod ‘ 𝑓 ) )
29 21 21 20 co ( 𝑥 𝑥 )
30 c0g 0g
31 13 30 cfv ( 0g𝑓 )
32 29 31 wceq ( 𝑥 𝑥 ) = ( 0g𝑓 )
33 4 30 cfv ( 0g𝑔 )
34 21 33 wceq 𝑥 = ( 0g𝑔 )
35 32 34 wi ( ( 𝑥 𝑥 ) = ( 0g𝑓 ) → 𝑥 = ( 0g𝑔 ) )
36 cstv *𝑟
37 13 36 cfv ( *𝑟𝑓 )
38 21 19 20 co ( 𝑥 𝑦 )
39 38 37 cfv ( ( *𝑟𝑓 ) ‘ ( 𝑥 𝑦 ) )
40 39 22 wceq ( ( *𝑟𝑓 ) ‘ ( 𝑥 𝑦 ) ) = ( 𝑦 𝑥 )
41 40 18 17 wral 𝑦𝑣 ( ( *𝑟𝑓 ) ‘ ( 𝑥 𝑦 ) ) = ( 𝑦 𝑥 )
42 28 35 41 w3a ( ( 𝑦𝑣 ↦ ( 𝑦 𝑥 ) ) ∈ ( 𝑔 LMHom ( ringLMod ‘ 𝑓 ) ) ∧ ( ( 𝑥 𝑥 ) = ( 0g𝑓 ) → 𝑥 = ( 0g𝑔 ) ) ∧ ∀ 𝑦𝑣 ( ( *𝑟𝑓 ) ‘ ( 𝑥 𝑦 ) ) = ( 𝑦 𝑥 ) )
43 42 16 17 wral 𝑥𝑣 ( ( 𝑦𝑣 ↦ ( 𝑦 𝑥 ) ) ∈ ( 𝑔 LMHom ( ringLMod ‘ 𝑓 ) ) ∧ ( ( 𝑥 𝑥 ) = ( 0g𝑓 ) → 𝑥 = ( 0g𝑔 ) ) ∧ ∀ 𝑦𝑣 ( ( *𝑟𝑓 ) ‘ ( 𝑥 𝑦 ) ) = ( 𝑦 𝑥 ) )
44 15 43 wa ( 𝑓 ∈ *-Ring ∧ ∀ 𝑥𝑣 ( ( 𝑦𝑣 ↦ ( 𝑦 𝑥 ) ) ∈ ( 𝑔 LMHom ( ringLMod ‘ 𝑓 ) ) ∧ ( ( 𝑥 𝑥 ) = ( 0g𝑓 ) → 𝑥 = ( 0g𝑔 ) ) ∧ ∀ 𝑦𝑣 ( ( *𝑟𝑓 ) ‘ ( 𝑥 𝑦 ) ) = ( 𝑦 𝑥 ) ) )
45 44 12 11 wsbc [ ( Scalar ‘ 𝑔 ) / 𝑓 ] ( 𝑓 ∈ *-Ring ∧ ∀ 𝑥𝑣 ( ( 𝑦𝑣 ↦ ( 𝑦 𝑥 ) ) ∈ ( 𝑔 LMHom ( ringLMod ‘ 𝑓 ) ) ∧ ( ( 𝑥 𝑥 ) = ( 0g𝑓 ) → 𝑥 = ( 0g𝑔 ) ) ∧ ∀ 𝑦𝑣 ( ( *𝑟𝑓 ) ‘ ( 𝑥 𝑦 ) ) = ( 𝑦 𝑥 ) ) )
46 45 9 8 wsbc [ ( ·𝑖𝑔 ) / ] [ ( Scalar ‘ 𝑔 ) / 𝑓 ] ( 𝑓 ∈ *-Ring ∧ ∀ 𝑥𝑣 ( ( 𝑦𝑣 ↦ ( 𝑦 𝑥 ) ) ∈ ( 𝑔 LMHom ( ringLMod ‘ 𝑓 ) ) ∧ ( ( 𝑥 𝑥 ) = ( 0g𝑓 ) → 𝑥 = ( 0g𝑔 ) ) ∧ ∀ 𝑦𝑣 ( ( *𝑟𝑓 ) ‘ ( 𝑥 𝑦 ) ) = ( 𝑦 𝑥 ) ) )
47 46 6 5 wsbc [ ( Base ‘ 𝑔 ) / 𝑣 ] [ ( ·𝑖𝑔 ) / ] [ ( Scalar ‘ 𝑔 ) / 𝑓 ] ( 𝑓 ∈ *-Ring ∧ ∀ 𝑥𝑣 ( ( 𝑦𝑣 ↦ ( 𝑦 𝑥 ) ) ∈ ( 𝑔 LMHom ( ringLMod ‘ 𝑓 ) ) ∧ ( ( 𝑥 𝑥 ) = ( 0g𝑓 ) → 𝑥 = ( 0g𝑔 ) ) ∧ ∀ 𝑦𝑣 ( ( *𝑟𝑓 ) ‘ ( 𝑥 𝑦 ) ) = ( 𝑦 𝑥 ) ) )
48 47 1 2 crab { 𝑔 ∈ LVec ∣ [ ( Base ‘ 𝑔 ) / 𝑣 ] [ ( ·𝑖𝑔 ) / ] [ ( Scalar ‘ 𝑔 ) / 𝑓 ] ( 𝑓 ∈ *-Ring ∧ ∀ 𝑥𝑣 ( ( 𝑦𝑣 ↦ ( 𝑦 𝑥 ) ) ∈ ( 𝑔 LMHom ( ringLMod ‘ 𝑓 ) ) ∧ ( ( 𝑥 𝑥 ) = ( 0g𝑓 ) → 𝑥 = ( 0g𝑔 ) ) ∧ ∀ 𝑦𝑣 ( ( *𝑟𝑓 ) ‘ ( 𝑥 𝑦 ) ) = ( 𝑦 𝑥 ) ) ) }
49 0 48 wceq PreHil = { 𝑔 ∈ LVec ∣ [ ( Base ‘ 𝑔 ) / 𝑣 ] [ ( ·𝑖𝑔 ) / ] [ ( Scalar ‘ 𝑔 ) / 𝑓 ] ( 𝑓 ∈ *-Ring ∧ ∀ 𝑥𝑣 ( ( 𝑦𝑣 ↦ ( 𝑦 𝑥 ) ) ∈ ( 𝑔 LMHom ( ringLMod ‘ 𝑓 ) ) ∧ ( ( 𝑥 𝑥 ) = ( 0g𝑓 ) → 𝑥 = ( 0g𝑔 ) ) ∧ ∀ 𝑦𝑣 ( ( *𝑟𝑓 ) ‘ ( 𝑥 𝑦 ) ) = ( 𝑦 𝑥 ) ) ) }