Theorem isphl

Description: The predicate "is a generalized pre-Hilbert (inner product) space". (Contributed by NM, 22-Sep-2011) (Revised by Mario Carneiro, 7-Oct-2015)

	Ref	Expression
Hypotheses	isphl.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
	isphl.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
	isphl.h	⊢ , = ( ·𝑖 ‘ 𝑊 )
	isphl.o	⊢ 0 = ( 0g ‘ 𝑊 )
	isphl.i	⊢ ∗ = ( *𝑟 ‘ 𝐹 )
	isphl.z	⊢ 𝑍 = ( 0g ‘ 𝐹 )
Assertion	isphl	⊢ ( 𝑊 ∈ PreHil ↔ ( 𝑊 ∈ LVec ∧ 𝐹 ∈ *-Ring ∧ ∀ 𝑥 ∈ 𝑉 ( ( 𝑦 ∈ 𝑉 ↦ ( 𝑦 , 𝑥 ) ) ∈ ( 𝑊 LMHom ( ringLMod ‘ 𝐹 ) ) ∧ ( ( 𝑥 , 𝑥 ) = 𝑍 → 𝑥 = 0 ) ∧ ∀ 𝑦 ∈ 𝑉 ( ∗ ‘ ( 𝑥 , 𝑦 ) ) = ( 𝑦 , 𝑥 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		isphl.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
2		isphl.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
3		isphl.h	⊢ , = ( ·𝑖 ‘ 𝑊 )
4		isphl.o	⊢ 0 = ( 0g ‘ 𝑊 )
5		isphl.i	⊢ ∗ = ( *𝑟 ‘ 𝐹 )
6		isphl.z	⊢ 𝑍 = ( 0g ‘ 𝐹 )
7		fvexd	⊢ ( 𝑔 = 𝑊 → ( Base ‘ 𝑔 ) ∈ V )
8		fvexd	⊢ ( ( 𝑔 = 𝑊 ∧ 𝑣 = ( Base ‘ 𝑔 ) ) → ( ·𝑖 ‘ 𝑔 ) ∈ V )
9		fvexd	⊢ ( ( ( 𝑔 = 𝑊 ∧ 𝑣 = ( Base ‘ 𝑔 ) ) ∧ ℎ = ( ·𝑖 ‘ 𝑔 ) ) → ( Scalar ‘ 𝑔 ) ∈ V )
10		id	⊢ ( 𝑓 = ( Scalar ‘ 𝑔 ) → 𝑓 = ( Scalar ‘ 𝑔 ) )
11		simpll	⊢ ( ( ( 𝑔 = 𝑊 ∧ 𝑣 = ( Base ‘ 𝑔 ) ) ∧ ℎ = ( ·𝑖 ‘ 𝑔 ) ) → 𝑔 = 𝑊 )
12	11	fveq2d	⊢ ( ( ( 𝑔 = 𝑊 ∧ 𝑣 = ( Base ‘ 𝑔 ) ) ∧ ℎ = ( ·𝑖 ‘ 𝑔 ) ) → ( Scalar ‘ 𝑔 ) = ( Scalar ‘ 𝑊 ) )
13	12 2	eqtr4di	⊢ ( ( ( 𝑔 = 𝑊 ∧ 𝑣 = ( Base ‘ 𝑔 ) ) ∧ ℎ = ( ·𝑖 ‘ 𝑔 ) ) → ( Scalar ‘ 𝑔 ) = 𝐹 )
14	10 13	sylan9eqr	⊢ ( ( ( ( 𝑔 = 𝑊 ∧ 𝑣 = ( Base ‘ 𝑔 ) ) ∧ ℎ = ( ·𝑖 ‘ 𝑔 ) ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → 𝑓 = 𝐹 )
15	14	eleq1d	⊢ ( ( ( ( 𝑔 = 𝑊 ∧ 𝑣 = ( Base ‘ 𝑔 ) ) ∧ ℎ = ( ·𝑖 ‘ 𝑔 ) ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( 𝑓 ∈ *-Ring ↔ 𝐹 ∈ *-Ring ) )
16		simpllr	⊢ ( ( ( ( 𝑔 = 𝑊 ∧ 𝑣 = ( Base ‘ 𝑔 ) ) ∧ ℎ = ( ·𝑖 ‘ 𝑔 ) ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → 𝑣 = ( Base ‘ 𝑔 ) )
17		simplll	⊢ ( ( ( ( 𝑔 = 𝑊 ∧ 𝑣 = ( Base ‘ 𝑔 ) ) ∧ ℎ = ( ·𝑖 ‘ 𝑔 ) ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → 𝑔 = 𝑊 )
18	17	fveq2d	⊢ ( ( ( ( 𝑔 = 𝑊 ∧ 𝑣 = ( Base ‘ 𝑔 ) ) ∧ ℎ = ( ·𝑖 ‘ 𝑔 ) ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( Base ‘ 𝑔 ) = ( Base ‘ 𝑊 ) )
19	18 1	eqtr4di	⊢ ( ( ( ( 𝑔 = 𝑊 ∧ 𝑣 = ( Base ‘ 𝑔 ) ) ∧ ℎ = ( ·𝑖 ‘ 𝑔 ) ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( Base ‘ 𝑔 ) = 𝑉 )
20	16 19	eqtrd	⊢ ( ( ( ( 𝑔 = 𝑊 ∧ 𝑣 = ( Base ‘ 𝑔 ) ) ∧ ℎ = ( ·𝑖 ‘ 𝑔 ) ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → 𝑣 = 𝑉 )
21		simplr	⊢ ( ( ( ( 𝑔 = 𝑊 ∧ 𝑣 = ( Base ‘ 𝑔 ) ) ∧ ℎ = ( ·𝑖 ‘ 𝑔 ) ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ℎ = ( ·𝑖 ‘ 𝑔 ) )
22	17	fveq2d	⊢ ( ( ( ( 𝑔 = 𝑊 ∧ 𝑣 = ( Base ‘ 𝑔 ) ) ∧ ℎ = ( ·𝑖 ‘ 𝑔 ) ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( ·𝑖 ‘ 𝑔 ) = ( ·𝑖 ‘ 𝑊 ) )
23	22 3	eqtr4di	⊢ ( ( ( ( 𝑔 = 𝑊 ∧ 𝑣 = ( Base ‘ 𝑔 ) ) ∧ ℎ = ( ·𝑖 ‘ 𝑔 ) ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( ·𝑖 ‘ 𝑔 ) = , )
24	21 23	eqtrd	⊢ ( ( ( ( 𝑔 = 𝑊 ∧ 𝑣 = ( Base ‘ 𝑔 ) ) ∧ ℎ = ( ·𝑖 ‘ 𝑔 ) ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ℎ = , )
25	24	oveqd	⊢ ( ( ( ( 𝑔 = 𝑊 ∧ 𝑣 = ( Base ‘ 𝑔 ) ) ∧ ℎ = ( ·𝑖 ‘ 𝑔 ) ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( 𝑦 ℎ 𝑥 ) = ( 𝑦 , 𝑥 ) )
26	20 25	mpteq12dv	⊢ ( ( ( ( 𝑔 = 𝑊 ∧ 𝑣 = ( Base ‘ 𝑔 ) ) ∧ ℎ = ( ·𝑖 ‘ 𝑔 ) ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( 𝑦 ∈ 𝑣 ↦ ( 𝑦 ℎ 𝑥 ) ) = ( 𝑦 ∈ 𝑉 ↦ ( 𝑦 , 𝑥 ) ) )
27	14	fveq2d	⊢ ( ( ( ( 𝑔 = 𝑊 ∧ 𝑣 = ( Base ‘ 𝑔 ) ) ∧ ℎ = ( ·𝑖 ‘ 𝑔 ) ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( ringLMod ‘ 𝑓 ) = ( ringLMod ‘ 𝐹 ) )
28	17 27	oveq12d	⊢ ( ( ( ( 𝑔 = 𝑊 ∧ 𝑣 = ( Base ‘ 𝑔 ) ) ∧ ℎ = ( ·𝑖 ‘ 𝑔 ) ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( 𝑔 LMHom ( ringLMod ‘ 𝑓 ) ) = ( 𝑊 LMHom ( ringLMod ‘ 𝐹 ) ) )
29	26 28	eleq12d	⊢ ( ( ( ( 𝑔 = 𝑊 ∧ 𝑣 = ( Base ‘ 𝑔 ) ) ∧ ℎ = ( ·𝑖 ‘ 𝑔 ) ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( ( 𝑦 ∈ 𝑣 ↦ ( 𝑦 ℎ 𝑥 ) ) ∈ ( 𝑔 LMHom ( ringLMod ‘ 𝑓 ) ) ↔ ( 𝑦 ∈ 𝑉 ↦ ( 𝑦 , 𝑥 ) ) ∈ ( 𝑊 LMHom ( ringLMod ‘ 𝐹 ) ) ) )
30	24	oveqd	⊢ ( ( ( ( 𝑔 = 𝑊 ∧ 𝑣 = ( Base ‘ 𝑔 ) ) ∧ ℎ = ( ·𝑖 ‘ 𝑔 ) ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( 𝑥 ℎ 𝑥 ) = ( 𝑥 , 𝑥 ) )
31	14	fveq2d	⊢ ( ( ( ( 𝑔 = 𝑊 ∧ 𝑣 = ( Base ‘ 𝑔 ) ) ∧ ℎ = ( ·𝑖 ‘ 𝑔 ) ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( 0g ‘ 𝑓 ) = ( 0g ‘ 𝐹 ) )
32	31 6	eqtr4di	⊢ ( ( ( ( 𝑔 = 𝑊 ∧ 𝑣 = ( Base ‘ 𝑔 ) ) ∧ ℎ = ( ·𝑖 ‘ 𝑔 ) ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( 0g ‘ 𝑓 ) = 𝑍 )
33	30 32	eqeq12d	⊢ ( ( ( ( 𝑔 = 𝑊 ∧ 𝑣 = ( Base ‘ 𝑔 ) ) ∧ ℎ = ( ·𝑖 ‘ 𝑔 ) ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( ( 𝑥 ℎ 𝑥 ) = ( 0g ‘ 𝑓 ) ↔ ( 𝑥 , 𝑥 ) = 𝑍 ) )
34	17	fveq2d	⊢ ( ( ( ( 𝑔 = 𝑊 ∧ 𝑣 = ( Base ‘ 𝑔 ) ) ∧ ℎ = ( ·𝑖 ‘ 𝑔 ) ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( 0g ‘ 𝑔 ) = ( 0g ‘ 𝑊 ) )
35	34 4	eqtr4di	⊢ ( ( ( ( 𝑔 = 𝑊 ∧ 𝑣 = ( Base ‘ 𝑔 ) ) ∧ ℎ = ( ·𝑖 ‘ 𝑔 ) ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( 0g ‘ 𝑔 ) = 0 )
36	35	eqeq2d	⊢ ( ( ( ( 𝑔 = 𝑊 ∧ 𝑣 = ( Base ‘ 𝑔 ) ) ∧ ℎ = ( ·𝑖 ‘ 𝑔 ) ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( 𝑥 = ( 0g ‘ 𝑔 ) ↔ 𝑥 = 0 ) )
37	33 36	imbi12d	⊢ ( ( ( ( 𝑔 = 𝑊 ∧ 𝑣 = ( Base ‘ 𝑔 ) ) ∧ ℎ = ( ·𝑖 ‘ 𝑔 ) ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( ( ( 𝑥 ℎ 𝑥 ) = ( 0g ‘ 𝑓 ) → 𝑥 = ( 0g ‘ 𝑔 ) ) ↔ ( ( 𝑥 , 𝑥 ) = 𝑍 → 𝑥 = 0 ) ) )
38	14	fveq2d	⊢ ( ( ( ( 𝑔 = 𝑊 ∧ 𝑣 = ( Base ‘ 𝑔 ) ) ∧ ℎ = ( ·𝑖 ‘ 𝑔 ) ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( *𝑟 ‘ 𝑓 ) = ( *𝑟 ‘ 𝐹 ) )
39	38 5	eqtr4di	⊢ ( ( ( ( 𝑔 = 𝑊 ∧ 𝑣 = ( Base ‘ 𝑔 ) ) ∧ ℎ = ( ·𝑖 ‘ 𝑔 ) ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( *𝑟 ‘ 𝑓 ) = ∗ )
40	24	oveqd	⊢ ( ( ( ( 𝑔 = 𝑊 ∧ 𝑣 = ( Base ‘ 𝑔 ) ) ∧ ℎ = ( ·𝑖 ‘ 𝑔 ) ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( 𝑥 ℎ 𝑦 ) = ( 𝑥 , 𝑦 ) )
41	39 40	fveq12d	⊢ ( ( ( ( 𝑔 = 𝑊 ∧ 𝑣 = ( Base ‘ 𝑔 ) ) ∧ ℎ = ( ·𝑖 ‘ 𝑔 ) ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( ( *𝑟 ‘ 𝑓 ) ‘ ( 𝑥 ℎ 𝑦 ) ) = ( ∗ ‘ ( 𝑥 , 𝑦 ) ) )
42	41 25	eqeq12d	⊢ ( ( ( ( 𝑔 = 𝑊 ∧ 𝑣 = ( Base ‘ 𝑔 ) ) ∧ ℎ = ( ·𝑖 ‘ 𝑔 ) ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( ( ( *𝑟 ‘ 𝑓 ) ‘ ( 𝑥 ℎ 𝑦 ) ) = ( 𝑦 ℎ 𝑥 ) ↔ ( ∗ ‘ ( 𝑥 , 𝑦 ) ) = ( 𝑦 , 𝑥 ) ) )
43	20 42	raleqbidv	⊢ ( ( ( ( 𝑔 = 𝑊 ∧ 𝑣 = ( Base ‘ 𝑔 ) ) ∧ ℎ = ( ·𝑖 ‘ 𝑔 ) ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( ∀ 𝑦 ∈ 𝑣 ( ( *𝑟 ‘ 𝑓 ) ‘ ( 𝑥 ℎ 𝑦 ) ) = ( 𝑦 ℎ 𝑥 ) ↔ ∀ 𝑦 ∈ 𝑉 ( ∗ ‘ ( 𝑥 , 𝑦 ) ) = ( 𝑦 , 𝑥 ) ) )
44	29 37 43	3anbi123d	⊢ ( ( ( ( 𝑔 = 𝑊 ∧ 𝑣 = ( Base ‘ 𝑔 ) ) ∧ ℎ = ( ·𝑖 ‘ 𝑔 ) ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( ( ( 𝑦 ∈ 𝑣 ↦ ( 𝑦 ℎ 𝑥 ) ) ∈ ( 𝑔 LMHom ( ringLMod ‘ 𝑓 ) ) ∧ ( ( 𝑥 ℎ 𝑥 ) = ( 0g ‘ 𝑓 ) → 𝑥 = ( 0g ‘ 𝑔 ) ) ∧ ∀ 𝑦 ∈ 𝑣 ( ( *𝑟 ‘ 𝑓 ) ‘ ( 𝑥 ℎ 𝑦 ) ) = ( 𝑦 ℎ 𝑥 ) ) ↔ ( ( 𝑦 ∈ 𝑉 ↦ ( 𝑦 , 𝑥 ) ) ∈ ( 𝑊 LMHom ( ringLMod ‘ 𝐹 ) ) ∧ ( ( 𝑥 , 𝑥 ) = 𝑍 → 𝑥 = 0 ) ∧ ∀ 𝑦 ∈ 𝑉 ( ∗ ‘ ( 𝑥 , 𝑦 ) ) = ( 𝑦 , 𝑥 ) ) ) )
45	20 44	raleqbidv	⊢ ( ( ( ( 𝑔 = 𝑊 ∧ 𝑣 = ( Base ‘ 𝑔 ) ) ∧ ℎ = ( ·𝑖 ‘ 𝑔 ) ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( ∀ 𝑥 ∈ 𝑣 ( ( 𝑦 ∈ 𝑣 ↦ ( 𝑦 ℎ 𝑥 ) ) ∈ ( 𝑔 LMHom ( ringLMod ‘ 𝑓 ) ) ∧ ( ( 𝑥 ℎ 𝑥 ) = ( 0g ‘ 𝑓 ) → 𝑥 = ( 0g ‘ 𝑔 ) ) ∧ ∀ 𝑦 ∈ 𝑣 ( ( *𝑟 ‘ 𝑓 ) ‘ ( 𝑥 ℎ 𝑦 ) ) = ( 𝑦 ℎ 𝑥 ) ) ↔ ∀ 𝑥 ∈ 𝑉 ( ( 𝑦 ∈ 𝑉 ↦ ( 𝑦 , 𝑥 ) ) ∈ ( 𝑊 LMHom ( ringLMod ‘ 𝐹 ) ) ∧ ( ( 𝑥 , 𝑥 ) = 𝑍 → 𝑥 = 0 ) ∧ ∀ 𝑦 ∈ 𝑉 ( ∗ ‘ ( 𝑥 , 𝑦 ) ) = ( 𝑦 , 𝑥 ) ) ) )
46	15 45	anbi12d	⊢ ( ( ( ( 𝑔 = 𝑊 ∧ 𝑣 = ( Base ‘ 𝑔 ) ) ∧ ℎ = ( ·𝑖 ‘ 𝑔 ) ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( ( 𝑓 ∈ *-Ring ∧ ∀ 𝑥 ∈ 𝑣 ( ( 𝑦 ∈ 𝑣 ↦ ( 𝑦 ℎ 𝑥 ) ) ∈ ( 𝑔 LMHom ( ringLMod ‘ 𝑓 ) ) ∧ ( ( 𝑥 ℎ 𝑥 ) = ( 0g ‘ 𝑓 ) → 𝑥 = ( 0g ‘ 𝑔 ) ) ∧ ∀ 𝑦 ∈ 𝑣 ( ( *𝑟 ‘ 𝑓 ) ‘ ( 𝑥 ℎ 𝑦 ) ) = ( 𝑦 ℎ 𝑥 ) ) ) ↔ ( 𝐹 ∈ *-Ring ∧ ∀ 𝑥 ∈ 𝑉 ( ( 𝑦 ∈ 𝑉 ↦ ( 𝑦 , 𝑥 ) ) ∈ ( 𝑊 LMHom ( ringLMod ‘ 𝐹 ) ) ∧ ( ( 𝑥 , 𝑥 ) = 𝑍 → 𝑥 = 0 ) ∧ ∀ 𝑦 ∈ 𝑉 ( ∗ ‘ ( 𝑥 , 𝑦 ) ) = ( 𝑦 , 𝑥 ) ) ) ) )
47	9 46	sbcied	⊢ ( ( ( 𝑔 = 𝑊 ∧ 𝑣 = ( Base ‘ 𝑔 ) ) ∧ ℎ = ( ·𝑖 ‘ 𝑔 ) ) → ( [ ( Scalar ‘ 𝑔 ) / 𝑓 ] ( 𝑓 ∈ *-Ring ∧ ∀ 𝑥 ∈ 𝑣 ( ( 𝑦 ∈ 𝑣 ↦ ( 𝑦 ℎ 𝑥 ) ) ∈ ( 𝑔 LMHom ( ringLMod ‘ 𝑓 ) ) ∧ ( ( 𝑥 ℎ 𝑥 ) = ( 0g ‘ 𝑓 ) → 𝑥 = ( 0g ‘ 𝑔 ) ) ∧ ∀ 𝑦 ∈ 𝑣 ( ( *𝑟 ‘ 𝑓 ) ‘ ( 𝑥 ℎ 𝑦 ) ) = ( 𝑦 ℎ 𝑥 ) ) ) ↔ ( 𝐹 ∈ *-Ring ∧ ∀ 𝑥 ∈ 𝑉 ( ( 𝑦 ∈ 𝑉 ↦ ( 𝑦 , 𝑥 ) ) ∈ ( 𝑊 LMHom ( ringLMod ‘ 𝐹 ) ) ∧ ( ( 𝑥 , 𝑥 ) = 𝑍 → 𝑥 = 0 ) ∧ ∀ 𝑦 ∈ 𝑉 ( ∗ ‘ ( 𝑥 , 𝑦 ) ) = ( 𝑦 , 𝑥 ) ) ) ) )
48	8 47	sbcied	⊢ ( ( 𝑔 = 𝑊 ∧ 𝑣 = ( Base ‘ 𝑔 ) ) → ( [ ( ·𝑖 ‘ 𝑔 ) / ℎ ] [ ( Scalar ‘ 𝑔 ) / 𝑓 ] ( 𝑓 ∈ *-Ring ∧ ∀ 𝑥 ∈ 𝑣 ( ( 𝑦 ∈ 𝑣 ↦ ( 𝑦 ℎ 𝑥 ) ) ∈ ( 𝑔 LMHom ( ringLMod ‘ 𝑓 ) ) ∧ ( ( 𝑥 ℎ 𝑥 ) = ( 0g ‘ 𝑓 ) → 𝑥 = ( 0g ‘ 𝑔 ) ) ∧ ∀ 𝑦 ∈ 𝑣 ( ( *𝑟 ‘ 𝑓 ) ‘ ( 𝑥 ℎ 𝑦 ) ) = ( 𝑦 ℎ 𝑥 ) ) ) ↔ ( 𝐹 ∈ *-Ring ∧ ∀ 𝑥 ∈ 𝑉 ( ( 𝑦 ∈ 𝑉 ↦ ( 𝑦 , 𝑥 ) ) ∈ ( 𝑊 LMHom ( ringLMod ‘ 𝐹 ) ) ∧ ( ( 𝑥 , 𝑥 ) = 𝑍 → 𝑥 = 0 ) ∧ ∀ 𝑦 ∈ 𝑉 ( ∗ ‘ ( 𝑥 , 𝑦 ) ) = ( 𝑦 , 𝑥 ) ) ) ) )
49	7 48	sbcied	⊢ ( 𝑔 = 𝑊 → ( [ ( Base ‘ 𝑔 ) / 𝑣 ] [ ( ·𝑖 ‘ 𝑔 ) / ℎ ] [ ( Scalar ‘ 𝑔 ) / 𝑓 ] ( 𝑓 ∈ *-Ring ∧ ∀ 𝑥 ∈ 𝑣 ( ( 𝑦 ∈ 𝑣 ↦ ( 𝑦 ℎ 𝑥 ) ) ∈ ( 𝑔 LMHom ( ringLMod ‘ 𝑓 ) ) ∧ ( ( 𝑥 ℎ 𝑥 ) = ( 0g ‘ 𝑓 ) → 𝑥 = ( 0g ‘ 𝑔 ) ) ∧ ∀ 𝑦 ∈ 𝑣 ( ( *𝑟 ‘ 𝑓 ) ‘ ( 𝑥 ℎ 𝑦 ) ) = ( 𝑦 ℎ 𝑥 ) ) ) ↔ ( 𝐹 ∈ *-Ring ∧ ∀ 𝑥 ∈ 𝑉 ( ( 𝑦 ∈ 𝑉 ↦ ( 𝑦 , 𝑥 ) ) ∈ ( 𝑊 LMHom ( ringLMod ‘ 𝐹 ) ) ∧ ( ( 𝑥 , 𝑥 ) = 𝑍 → 𝑥 = 0 ) ∧ ∀ 𝑦 ∈ 𝑉 ( ∗ ‘ ( 𝑥 , 𝑦 ) ) = ( 𝑦 , 𝑥 ) ) ) ) )
50		df-phl	⊢ PreHil = { 𝑔 ∈ LVec ∣ [ ( Base ‘ 𝑔 ) / 𝑣 ] [ ( ·𝑖 ‘ 𝑔 ) / ℎ ] [ ( Scalar ‘ 𝑔 ) / 𝑓 ] ( 𝑓 ∈ *-Ring ∧ ∀ 𝑥 ∈ 𝑣 ( ( 𝑦 ∈ 𝑣 ↦ ( 𝑦 ℎ 𝑥 ) ) ∈ ( 𝑔 LMHom ( ringLMod ‘ 𝑓 ) ) ∧ ( ( 𝑥 ℎ 𝑥 ) = ( 0g ‘ 𝑓 ) → 𝑥 = ( 0g ‘ 𝑔 ) ) ∧ ∀ 𝑦 ∈ 𝑣 ( ( *𝑟 ‘ 𝑓 ) ‘ ( 𝑥 ℎ 𝑦 ) ) = ( 𝑦 ℎ 𝑥 ) ) ) }
51	49 50	elrab2	⊢ ( 𝑊 ∈ PreHil ↔ ( 𝑊 ∈ LVec ∧ ( 𝐹 ∈ *-Ring ∧ ∀ 𝑥 ∈ 𝑉 ( ( 𝑦 ∈ 𝑉 ↦ ( 𝑦 , 𝑥 ) ) ∈ ( 𝑊 LMHom ( ringLMod ‘ 𝐹 ) ) ∧ ( ( 𝑥 , 𝑥 ) = 𝑍 → 𝑥 = 0 ) ∧ ∀ 𝑦 ∈ 𝑉 ( ∗ ‘ ( 𝑥 , 𝑦 ) ) = ( 𝑦 , 𝑥 ) ) ) ) )
52		3anass	⊢ ( ( 𝑊 ∈ LVec ∧ 𝐹 ∈ *-Ring ∧ ∀ 𝑥 ∈ 𝑉 ( ( 𝑦 ∈ 𝑉 ↦ ( 𝑦 , 𝑥 ) ) ∈ ( 𝑊 LMHom ( ringLMod ‘ 𝐹 ) ) ∧ ( ( 𝑥 , 𝑥 ) = 𝑍 → 𝑥 = 0 ) ∧ ∀ 𝑦 ∈ 𝑉 ( ∗ ‘ ( 𝑥 , 𝑦 ) ) = ( 𝑦 , 𝑥 ) ) ) ↔ ( 𝑊 ∈ LVec ∧ ( 𝐹 ∈ *-Ring ∧ ∀ 𝑥 ∈ 𝑉 ( ( 𝑦 ∈ 𝑉 ↦ ( 𝑦 , 𝑥 ) ) ∈ ( 𝑊 LMHom ( ringLMod ‘ 𝐹 ) ) ∧ ( ( 𝑥 , 𝑥 ) = 𝑍 → 𝑥 = 0 ) ∧ ∀ 𝑦 ∈ 𝑉 ( ∗ ‘ ( 𝑥 , 𝑦 ) ) = ( 𝑦 , 𝑥 ) ) ) ) )
53	51 52	bitr4i	⊢ ( 𝑊 ∈ PreHil ↔ ( 𝑊 ∈ LVec ∧ 𝐹 ∈ *-Ring ∧ ∀ 𝑥 ∈ 𝑉 ( ( 𝑦 ∈ 𝑉 ↦ ( 𝑦 , 𝑥 ) ) ∈ ( 𝑊 LMHom ( ringLMod ‘ 𝐹 ) ) ∧ ( ( 𝑥 , 𝑥 ) = 𝑍 → 𝑥 = 0 ) ∧ ∀ 𝑦 ∈ 𝑉 ( ∗ ‘ ( 𝑥 , 𝑦 ) ) = ( 𝑦 , 𝑥 ) ) ) )