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 ‘ 𝑔 ) ) ∧ ∀ 𝑦 ∈ 𝑣 ( ( *𝑟 ‘ 𝑓 ) ‘ ( 𝑥 ℎ 𝑦 ) ) = ( 𝑦 ℎ 𝑥 ) ) ) }