Definition df-phl 19971

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 = { g e. LVec | [. ( Base ` g ) / v ]. [. ( .i ` g ) / h ]. [. (Scalar ` g ) / f ]. ( f e. *Ring /\ A. x e. v ( ( y e. v |-> ( y h x ) ) e. ( g LMHom (ringLMod ` f ) ) /\ ( ( x h x ) = ( 0g ` f ) -> x = ( 0g ` g ) ) /\ A. y e. v ( ( *r ` f ) ` ( x h y ) ) = ( y h x ) ) ) }

Distinct variable group:   f, g, h, v, x, y

Detailed syntax breakdown of Definition df-phl

Step	Hyp	Ref	Expression
1		cphl 19969	. 2 class PreHil
2		vf	. . . . . . . . 9 setvar f
3	2	cv 1482	. . . . . . . 8 class f
4		csr 18844	. . . . . . . 8 class *Ring
5	3, 4	wcel 1990	. . . . . . 7 wff f e. *Ring
6		vy	. . . . . . . . . . 11 setvar y
7		vv	. . . . . . . . . . . 12 setvar v
8	7	cv 1482	. . . . . . . . . . 11 class v
9	6	cv 1482	. . . . . . . . . . . 12 class y
10		vx	. . . . . . . . . . . . 13 setvar x
11	10	cv 1482	. . . . . . . . . . . 12 class x
12		vh	. . . . . . . . . . . . 13 setvar h
13	12	cv 1482	. . . . . . . . . . . 12 class h
14	9, 11, 13	co 6650	. . . . . . . . . . 11 class ( y h x )
15	6, 8, 14	cmpt 4729	. . . . . . . . . 10 class ( y e. v |-> ( y h x ) )
16		vg	. . . . . . . . . . . 12 setvar g
17	16	cv 1482	. . . . . . . . . . 11 class g
18		crglmod 19169	. . . . . . . . . . . 12 class ringLMod
19	3, 18	cfv 5888	. . . . . . . . . . 11 class (ringLMod ` f )
20		clmhm 19019	. . . . . . . . . . 11 class LMHom
21	17, 19, 20	co 6650	. . . . . . . . . 10 class ( g LMHom (ringLMod ` f ) )
22	15, 21	wcel 1990	. . . . . . . . 9 wff ( y e. v |-> ( y h x ) ) e. ( g LMHom (ringLMod ` f ) )
23	11, 11, 13	co 6650	. . . . . . . . . . 11 class ( x h x )
24		c0g 16100	. . . . . . . . . . . 12 class 0g
25	3, 24	cfv 5888	. . . . . . . . . . 11 class ( 0g ` f )
26	23, 25	wceq 1483	. . . . . . . . . 10 wff ( x h x ) = ( 0g ` f )
27	17, 24	cfv 5888	. . . . . . . . . . 11 class ( 0g ` g )
28	11, 27	wceq 1483	. . . . . . . . . 10 wff x = ( 0g ` g )
29	26, 28	wi 4	. . . . . . . . 9 wff ( ( x h x ) = ( 0g ` f ) -> x = ( 0g ` g ) )
30	11, 9, 13	co 6650	. . . . . . . . . . . 12 class ( x h y )
31		cstv 15943	. . . . . . . . . . . . 13 class *r
32	3, 31	cfv 5888	. . . . . . . . . . . 12 class ( *r ` f )
33	30, 32	cfv 5888	. . . . . . . . . . 11 class ( ( *r ` f ) ` ( x h y ) )
34	33, 14	wceq 1483	. . . . . . . . . 10 wff ( ( *r ` f ) ` ( x h y ) ) = ( y h x )
35	34, 6, 8	wral 2912	. . . . . . . . 9 wff A. y e. v ( ( *r ` f ) ` ( x h y ) ) = ( y h x )
36	22, 29, 35	w3a 1037	. . . . . . . 8 wff ( ( y e. v |-> ( y h x ) ) e. ( g LMHom (ringLMod ` f ) ) /\ ( ( x h x ) = ( 0g ` f ) -> x = ( 0g ` g ) ) /\ A. y e. v ( ( *r ` f ) ` ( x h y ) ) = ( y h x ) )
37	36, 10, 8	wral 2912	. . . . . . 7 wff A. x e. v ( ( y e. v |-> ( y h x ) ) e. ( g LMHom (ringLMod ` f ) ) /\ ( ( x h x ) = ( 0g ` f ) -> x = ( 0g ` g ) ) /\ A. y e. v ( ( *r ` f ) ` ( x h y ) ) = ( y h x ) )
38	5, 37	wa 384	. . . . . 6 wff ( f e. *Ring /\ A. x e. v ( ( y e. v |-> ( y h x ) ) e. ( g LMHom (ringLMod ` f ) ) /\ ( ( x h x ) = ( 0g ` f ) -> x = ( 0g ` g ) ) /\ A. y e. v ( ( *r ` f ) ` ( x h y ) ) = ( y h x ) ) )
39		csca 15944	. . . . . . 7 class Scalar
40	17, 39	cfv 5888	. . . . . 6 class (Scalar ` g )
41	38, 2, 40	wsbc 3435	. . . . 5 wff [. (Scalar ` g ) / f ]. ( f e. *Ring /\ A. x e. v ( ( y e. v |-> ( y h x ) ) e. ( g LMHom (ringLMod ` f ) ) /\ ( ( x h x ) = ( 0g ` f ) -> x = ( 0g ` g ) ) /\ A. y e. v ( ( *r ` f ) ` ( x h y ) ) = ( y h x ) ) )
42		cip 15946	. . . . . 6 class .i
43	17, 42	cfv 5888	. . . . 5 class ( .i ` g )
44	41, 12, 43	wsbc 3435	. . . 4 wff [. ( .i ` g ) / h ]. [. (Scalar ` g ) / f ]. ( f e. *Ring /\ A. x e. v ( ( y e. v |-> ( y h x ) ) e. ( g LMHom (ringLMod ` f ) ) /\ ( ( x h x ) = ( 0g ` f ) -> x = ( 0g ` g ) ) /\ A. y e. v ( ( *r ` f ) ` ( x h y ) ) = ( y h x ) ) )
45		cbs 15857	. . . . 5 class Base
46	17, 45	cfv 5888	. . . 4 class ( Base ` g )
47	44, 7, 46	wsbc 3435	. . 3 wff [. ( Base ` g ) / v ]. [. ( .i ` g ) / h ]. [. (Scalar ` g ) / f ]. ( f e. *Ring /\ A. x e. v ( ( y e. v |-> ( y h x ) ) e. ( g LMHom (ringLMod ` f ) ) /\ ( ( x h x ) = ( 0g ` f ) -> x = ( 0g ` g ) ) /\ A. y e. v ( ( *r ` f ) ` ( x h y ) ) = ( y h x ) ) )
48		clvec 19102	. . 3 class LVec
49	47, 16, 48	crab 2916	. 2 class { g e. LVec | [. ( Base ` g ) / v ]. [. ( .i ` g ) / h ]. [. (Scalar ` g ) / f ]. ( f e. *Ring /\ A. x e. v ( ( y e. v |-> ( y h x ) ) e. ( g LMHom (ringLMod ` f ) ) /\ ( ( x h x ) = ( 0g ` f ) -> x = ( 0g ` g ) ) /\ A. y e. v ( ( *r ` f ) ` ( x h y ) ) = ( y h x ) ) ) }
50	1, 49	wceq 1483	1 wff PreHil = { g e. LVec | [. ( Base ` g ) / v ]. [. ( .i ` g ) / h ]. [. (Scalar ` g ) / f ]. ( f e. *Ring /\ A. x e. v ( ( y e. v |-> ( y h x ) ) e. ( g LMHom (ringLMod ` f ) ) /\ ( ( x h x ) = ( 0g ` f ) -> x = ( 0g ` g ) ) /\ A. y e. v ( ( *r ` f ) ` ( x h y ) ) = ( y h x ) ) ) }

This definition is referenced by:  isphl  19973