This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ∧ ∀ 𝑦 ∈ 𝑉 ( ∗ ‘ ( 𝑥 , 𝑦 ) ) = ( 𝑦 , 𝑥 ) ) ) )