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