Step | Hyp | Ref
| Expression |
1 | | fvex 6113 |
. . . . 5
⊢
(Base‘𝑔)
∈ V |
2 | 1 | a1i 11 |
. . . 4
⊢ (𝑔 = 𝑊 → (Base‘𝑔) ∈ V) |
3 | | fvex 6113 |
. . . . . 6
⊢
(·𝑖‘𝑔) ∈ V |
4 | 3 | a1i 11 |
. . . . 5
⊢ ((𝑔 = 𝑊 ∧ 𝑣 = (Base‘𝑔)) →
(·𝑖‘𝑔) ∈ V) |
5 | | fvex 6113 |
. . . . . . 7
⊢
(Scalar‘𝑔)
∈ V |
6 | 5 | a1i 11 |
. . . . . 6
⊢ (((𝑔 = 𝑊 ∧ 𝑣 = (Base‘𝑔)) ∧ ℎ =
(·𝑖‘𝑔)) → (Scalar‘𝑔) ∈ V) |
7 | | id 22 |
. . . . . . . . 9
⊢ (𝑓 = (Scalar‘𝑔) → 𝑓 = (Scalar‘𝑔)) |
8 | | simpll 786 |
. . . . . . . . . . 11
⊢ (((𝑔 = 𝑊 ∧ 𝑣 = (Base‘𝑔)) ∧ ℎ =
(·𝑖‘𝑔)) → 𝑔 = 𝑊) |
9 | 8 | fveq2d 6107 |
. . . . . . . . . 10
⊢ (((𝑔 = 𝑊 ∧ 𝑣 = (Base‘𝑔)) ∧ ℎ =
(·𝑖‘𝑔)) → (Scalar‘𝑔) = (Scalar‘𝑊)) |
10 | | isphl.f |
. . . . . . . . . 10
⊢ 𝐹 = (Scalar‘𝑊) |
11 | 9, 10 | syl6eqr 2662 |
. . . . . . . . 9
⊢ (((𝑔 = 𝑊 ∧ 𝑣 = (Base‘𝑔)) ∧ ℎ =
(·𝑖‘𝑔)) → (Scalar‘𝑔) = 𝐹) |
12 | 7, 11 | sylan9eqr 2666 |
. . . . . . . 8
⊢ ((((𝑔 = 𝑊 ∧ 𝑣 = (Base‘𝑔)) ∧ ℎ =
(·𝑖‘𝑔)) ∧ 𝑓 = (Scalar‘𝑔)) → 𝑓 = 𝐹) |
13 | 12 | eleq1d 2672 |
. . . . . . 7
⊢ ((((𝑔 = 𝑊 ∧ 𝑣 = (Base‘𝑔)) ∧ ℎ =
(·𝑖‘𝑔)) ∧ 𝑓 = (Scalar‘𝑔)) → (𝑓 ∈ *-Ring ↔ 𝐹 ∈ *-Ring)) |
14 | | simpllr 795 |
. . . . . . . . 9
⊢ ((((𝑔 = 𝑊 ∧ 𝑣 = (Base‘𝑔)) ∧ ℎ =
(·𝑖‘𝑔)) ∧ 𝑓 = (Scalar‘𝑔)) → 𝑣 = (Base‘𝑔)) |
15 | | simplll 794 |
. . . . . . . . . . 11
⊢ ((((𝑔 = 𝑊 ∧ 𝑣 = (Base‘𝑔)) ∧ ℎ =
(·𝑖‘𝑔)) ∧ 𝑓 = (Scalar‘𝑔)) → 𝑔 = 𝑊) |
16 | 15 | fveq2d 6107 |
. . . . . . . . . 10
⊢ ((((𝑔 = 𝑊 ∧ 𝑣 = (Base‘𝑔)) ∧ ℎ =
(·𝑖‘𝑔)) ∧ 𝑓 = (Scalar‘𝑔)) → (Base‘𝑔) = (Base‘𝑊)) |
17 | | isphl.v |
. . . . . . . . . 10
⊢ 𝑉 = (Base‘𝑊) |
18 | 16, 17 | syl6eqr 2662 |
. . . . . . . . 9
⊢ ((((𝑔 = 𝑊 ∧ 𝑣 = (Base‘𝑔)) ∧ ℎ =
(·𝑖‘𝑔)) ∧ 𝑓 = (Scalar‘𝑔)) → (Base‘𝑔) = 𝑉) |
19 | 14, 18 | eqtrd 2644 |
. . . . . . . 8
⊢ ((((𝑔 = 𝑊 ∧ 𝑣 = (Base‘𝑔)) ∧ ℎ =
(·𝑖‘𝑔)) ∧ 𝑓 = (Scalar‘𝑔)) → 𝑣 = 𝑉) |
20 | | simplr 788 |
. . . . . . . . . . . . 13
⊢ ((((𝑔 = 𝑊 ∧ 𝑣 = (Base‘𝑔)) ∧ ℎ =
(·𝑖‘𝑔)) ∧ 𝑓 = (Scalar‘𝑔)) → ℎ =
(·𝑖‘𝑔)) |
21 | 15 | fveq2d 6107 |
. . . . . . . . . . . . . 14
⊢ ((((𝑔 = 𝑊 ∧ 𝑣 = (Base‘𝑔)) ∧ ℎ =
(·𝑖‘𝑔)) ∧ 𝑓 = (Scalar‘𝑔)) →
(·𝑖‘𝑔) =
(·𝑖‘𝑊)) |
22 | | isphl.h |
. . . . . . . . . . . . . 14
⊢ , =
(·𝑖‘𝑊) |
23 | 21, 22 | syl6eqr 2662 |
. . . . . . . . . . . . 13
⊢ ((((𝑔 = 𝑊 ∧ 𝑣 = (Base‘𝑔)) ∧ ℎ =
(·𝑖‘𝑔)) ∧ 𝑓 = (Scalar‘𝑔)) →
(·𝑖‘𝑔) = , ) |
24 | 20, 23 | eqtrd 2644 |
. . . . . . . . . . . 12
⊢ ((((𝑔 = 𝑊 ∧ 𝑣 = (Base‘𝑔)) ∧ ℎ =
(·𝑖‘𝑔)) ∧ 𝑓 = (Scalar‘𝑔)) → ℎ = , ) |
25 | 24 | oveqd 6566 |
. . . . . . . . . . 11
⊢ ((((𝑔 = 𝑊 ∧ 𝑣 = (Base‘𝑔)) ∧ ℎ =
(·𝑖‘𝑔)) ∧ 𝑓 = (Scalar‘𝑔)) → (𝑦ℎ𝑥) = (𝑦 , 𝑥)) |
26 | 19, 25 | mpteq12dv 4663 |
. . . . . . . . . 10
⊢ ((((𝑔 = 𝑊 ∧ 𝑣 = (Base‘𝑔)) ∧ ℎ =
(·𝑖‘𝑔)) ∧ 𝑓 = (Scalar‘𝑔)) → (𝑦 ∈ 𝑣 ↦ (𝑦ℎ𝑥)) = (𝑦 ∈ 𝑉 ↦ (𝑦 , 𝑥))) |
27 | 12 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ ((((𝑔 = 𝑊 ∧ 𝑣 = (Base‘𝑔)) ∧ ℎ =
(·𝑖‘𝑔)) ∧ 𝑓 = (Scalar‘𝑔)) → (ringLMod‘𝑓) = (ringLMod‘𝐹)) |
28 | 15, 27 | oveq12d 6567 |
. . . . . . . . . 10
⊢ ((((𝑔 = 𝑊 ∧ 𝑣 = (Base‘𝑔)) ∧ ℎ =
(·𝑖‘𝑔)) ∧ 𝑓 = (Scalar‘𝑔)) → (𝑔 LMHom (ringLMod‘𝑓)) = (𝑊 LMHom (ringLMod‘𝐹))) |
29 | 26, 28 | eleq12d 2682 |
. . . . . . . . 9
⊢ ((((𝑔 = 𝑊 ∧ 𝑣 = (Base‘𝑔)) ∧ ℎ =
(·𝑖‘𝑔)) ∧ 𝑓 = (Scalar‘𝑔)) → ((𝑦 ∈ 𝑣 ↦ (𝑦ℎ𝑥)) ∈ (𝑔 LMHom (ringLMod‘𝑓)) ↔ (𝑦 ∈ 𝑉 ↦ (𝑦 , 𝑥)) ∈ (𝑊 LMHom (ringLMod‘𝐹)))) |
30 | 24 | oveqd 6566 |
. . . . . . . . . . 11
⊢ ((((𝑔 = 𝑊 ∧ 𝑣 = (Base‘𝑔)) ∧ ℎ =
(·𝑖‘𝑔)) ∧ 𝑓 = (Scalar‘𝑔)) → (𝑥ℎ𝑥) = (𝑥 , 𝑥)) |
31 | 12 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ ((((𝑔 = 𝑊 ∧ 𝑣 = (Base‘𝑔)) ∧ ℎ =
(·𝑖‘𝑔)) ∧ 𝑓 = (Scalar‘𝑔)) → (0g‘𝑓) = (0g‘𝐹)) |
32 | | isphl.z |
. . . . . . . . . . . 12
⊢ 𝑍 = (0g‘𝐹) |
33 | 31, 32 | syl6eqr 2662 |
. . . . . . . . . . 11
⊢ ((((𝑔 = 𝑊 ∧ 𝑣 = (Base‘𝑔)) ∧ ℎ =
(·𝑖‘𝑔)) ∧ 𝑓 = (Scalar‘𝑔)) → (0g‘𝑓) = 𝑍) |
34 | 30, 33 | eqeq12d 2625 |
. . . . . . . . . 10
⊢ ((((𝑔 = 𝑊 ∧ 𝑣 = (Base‘𝑔)) ∧ ℎ =
(·𝑖‘𝑔)) ∧ 𝑓 = (Scalar‘𝑔)) → ((𝑥ℎ𝑥) = (0g‘𝑓) ↔ (𝑥 , 𝑥) = 𝑍)) |
35 | 15 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ ((((𝑔 = 𝑊 ∧ 𝑣 = (Base‘𝑔)) ∧ ℎ =
(·𝑖‘𝑔)) ∧ 𝑓 = (Scalar‘𝑔)) → (0g‘𝑔) = (0g‘𝑊)) |
36 | | isphl.o |
. . . . . . . . . . . 12
⊢ 0 =
(0g‘𝑊) |
37 | 35, 36 | syl6eqr 2662 |
. . . . . . . . . . 11
⊢ ((((𝑔 = 𝑊 ∧ 𝑣 = (Base‘𝑔)) ∧ ℎ =
(·𝑖‘𝑔)) ∧ 𝑓 = (Scalar‘𝑔)) → (0g‘𝑔) = 0 ) |
38 | 37 | eqeq2d 2620 |
. . . . . . . . . 10
⊢ ((((𝑔 = 𝑊 ∧ 𝑣 = (Base‘𝑔)) ∧ ℎ =
(·𝑖‘𝑔)) ∧ 𝑓 = (Scalar‘𝑔)) → (𝑥 = (0g‘𝑔) ↔ 𝑥 = 0 )) |
39 | 34, 38 | imbi12d 333 |
. . . . . . . . 9
⊢ ((((𝑔 = 𝑊 ∧ 𝑣 = (Base‘𝑔)) ∧ ℎ =
(·𝑖‘𝑔)) ∧ 𝑓 = (Scalar‘𝑔)) → (((𝑥ℎ𝑥) = (0g‘𝑓) → 𝑥 = (0g‘𝑔)) ↔ ((𝑥 , 𝑥) = 𝑍 → 𝑥 = 0 ))) |
40 | 12 | fveq2d 6107 |
. . . . . . . . . . . . 13
⊢ ((((𝑔 = 𝑊 ∧ 𝑣 = (Base‘𝑔)) ∧ ℎ =
(·𝑖‘𝑔)) ∧ 𝑓 = (Scalar‘𝑔)) → (*𝑟‘𝑓) =
(*𝑟‘𝐹)) |
41 | | isphl.i |
. . . . . . . . . . . . 13
⊢ ∗ =
(*𝑟‘𝐹) |
42 | 40, 41 | syl6eqr 2662 |
. . . . . . . . . . . 12
⊢ ((((𝑔 = 𝑊 ∧ 𝑣 = (Base‘𝑔)) ∧ ℎ =
(·𝑖‘𝑔)) ∧ 𝑓 = (Scalar‘𝑔)) → (*𝑟‘𝑓) = ∗ ) |
43 | 24 | oveqd 6566 |
. . . . . . . . . . . 12
⊢ ((((𝑔 = 𝑊 ∧ 𝑣 = (Base‘𝑔)) ∧ ℎ =
(·𝑖‘𝑔)) ∧ 𝑓 = (Scalar‘𝑔)) → (𝑥ℎ𝑦) = (𝑥 , 𝑦)) |
44 | 42, 43 | fveq12d 6109 |
. . . . . . . . . . 11
⊢ ((((𝑔 = 𝑊 ∧ 𝑣 = (Base‘𝑔)) ∧ ℎ =
(·𝑖‘𝑔)) ∧ 𝑓 = (Scalar‘𝑔)) → ((*𝑟‘𝑓)‘(𝑥ℎ𝑦)) = ( ∗ ‘(𝑥 , 𝑦))) |
45 | 44, 25 | eqeq12d 2625 |
. . . . . . . . . 10
⊢ ((((𝑔 = 𝑊 ∧ 𝑣 = (Base‘𝑔)) ∧ ℎ =
(·𝑖‘𝑔)) ∧ 𝑓 = (Scalar‘𝑔)) →
(((*𝑟‘𝑓)‘(𝑥ℎ𝑦)) = (𝑦ℎ𝑥) ↔ ( ∗ ‘(𝑥 , 𝑦)) = (𝑦 , 𝑥))) |
46 | 19, 45 | raleqbidv 3129 |
. . . . . . . . 9
⊢ ((((𝑔 = 𝑊 ∧ 𝑣 = (Base‘𝑔)) ∧ ℎ =
(·𝑖‘𝑔)) ∧ 𝑓 = (Scalar‘𝑔)) → (∀𝑦 ∈ 𝑣 ((*𝑟‘𝑓)‘(𝑥ℎ𝑦)) = (𝑦ℎ𝑥) ↔ ∀𝑦 ∈ 𝑉 ( ∗ ‘(𝑥 , 𝑦)) = (𝑦 , 𝑥))) |
47 | 29, 39, 46 | 3anbi123d 1391 |
. . . . . . . 8
⊢ ((((𝑔 = 𝑊 ∧ 𝑣 = (Base‘𝑔)) ∧ ℎ =
(·𝑖‘𝑔)) ∧ 𝑓 = (Scalar‘𝑔)) → (((𝑦 ∈ 𝑣 ↦ (𝑦ℎ𝑥)) ∈ (𝑔 LMHom (ringLMod‘𝑓)) ∧ ((𝑥ℎ𝑥) = (0g‘𝑓) → 𝑥 = (0g‘𝑔)) ∧ ∀𝑦 ∈ 𝑣 ((*𝑟‘𝑓)‘(𝑥ℎ𝑦)) = (𝑦ℎ𝑥)) ↔ ((𝑦 ∈ 𝑉 ↦ (𝑦 , 𝑥)) ∈ (𝑊 LMHom (ringLMod‘𝐹)) ∧ ((𝑥 , 𝑥) = 𝑍 → 𝑥 = 0 ) ∧ ∀𝑦 ∈ 𝑉 ( ∗ ‘(𝑥 , 𝑦)) = (𝑦 , 𝑥)))) |
48 | 19, 47 | raleqbidv 3129 |
. . . . . . 7
⊢ ((((𝑔 = 𝑊 ∧ 𝑣 = (Base‘𝑔)) ∧ ℎ =
(·𝑖‘𝑔)) ∧ 𝑓 = (Scalar‘𝑔)) → (∀𝑥 ∈ 𝑣 ((𝑦 ∈ 𝑣 ↦ (𝑦ℎ𝑥)) ∈ (𝑔 LMHom (ringLMod‘𝑓)) ∧ ((𝑥ℎ𝑥) = (0g‘𝑓) → 𝑥 = (0g‘𝑔)) ∧ ∀𝑦 ∈ 𝑣 ((*𝑟‘𝑓)‘(𝑥ℎ𝑦)) = (𝑦ℎ𝑥)) ↔ ∀𝑥 ∈ 𝑉 ((𝑦 ∈ 𝑉 ↦ (𝑦 , 𝑥)) ∈ (𝑊 LMHom (ringLMod‘𝐹)) ∧ ((𝑥 , 𝑥) = 𝑍 → 𝑥 = 0 ) ∧ ∀𝑦 ∈ 𝑉 ( ∗ ‘(𝑥 , 𝑦)) = (𝑦 , 𝑥)))) |
49 | 13, 48 | anbi12d 743 |
. . . . . 6
⊢ ((((𝑔 = 𝑊 ∧ 𝑣 = (Base‘𝑔)) ∧ ℎ =
(·𝑖‘𝑔)) ∧ 𝑓 = (Scalar‘𝑔)) → ((𝑓 ∈ *-Ring ∧ ∀𝑥 ∈ 𝑣 ((𝑦 ∈ 𝑣 ↦ (𝑦ℎ𝑥)) ∈ (𝑔 LMHom (ringLMod‘𝑓)) ∧ ((𝑥ℎ𝑥) = (0g‘𝑓) → 𝑥 = (0g‘𝑔)) ∧ ∀𝑦 ∈ 𝑣 ((*𝑟‘𝑓)‘(𝑥ℎ𝑦)) = (𝑦ℎ𝑥))) ↔ (𝐹 ∈ *-Ring ∧ ∀𝑥 ∈ 𝑉 ((𝑦 ∈ 𝑉 ↦ (𝑦 , 𝑥)) ∈ (𝑊 LMHom (ringLMod‘𝐹)) ∧ ((𝑥 , 𝑥) = 𝑍 → 𝑥 = 0 ) ∧ ∀𝑦 ∈ 𝑉 ( ∗ ‘(𝑥 , 𝑦)) = (𝑦 , 𝑥))))) |
50 | 6, 49 | sbcied 3439 |
. . . . 5
⊢ (((𝑔 = 𝑊 ∧ 𝑣 = (Base‘𝑔)) ∧ ℎ =
(·𝑖‘𝑔)) → ([(Scalar‘𝑔) / 𝑓](𝑓 ∈ *-Ring ∧ ∀𝑥 ∈ 𝑣 ((𝑦 ∈ 𝑣 ↦ (𝑦ℎ𝑥)) ∈ (𝑔 LMHom (ringLMod‘𝑓)) ∧ ((𝑥ℎ𝑥) = (0g‘𝑓) → 𝑥 = (0g‘𝑔)) ∧ ∀𝑦 ∈ 𝑣 ((*𝑟‘𝑓)‘(𝑥ℎ𝑦)) = (𝑦ℎ𝑥))) ↔ (𝐹 ∈ *-Ring ∧ ∀𝑥 ∈ 𝑉 ((𝑦 ∈ 𝑉 ↦ (𝑦 , 𝑥)) ∈ (𝑊 LMHom (ringLMod‘𝐹)) ∧ ((𝑥 , 𝑥) = 𝑍 → 𝑥 = 0 ) ∧ ∀𝑦 ∈ 𝑉 ( ∗ ‘(𝑥 , 𝑦)) = (𝑦 , 𝑥))))) |
51 | 4, 50 | sbcied 3439 |
. . . 4
⊢ ((𝑔 = 𝑊 ∧ 𝑣 = (Base‘𝑔)) →
([(·𝑖‘𝑔) / ℎ][(Scalar‘𝑔) / 𝑓](𝑓 ∈ *-Ring ∧ ∀𝑥 ∈ 𝑣 ((𝑦 ∈ 𝑣 ↦ (𝑦ℎ𝑥)) ∈ (𝑔 LMHom (ringLMod‘𝑓)) ∧ ((𝑥ℎ𝑥) = (0g‘𝑓) → 𝑥 = (0g‘𝑔)) ∧ ∀𝑦 ∈ 𝑣 ((*𝑟‘𝑓)‘(𝑥ℎ𝑦)) = (𝑦ℎ𝑥))) ↔ (𝐹 ∈ *-Ring ∧ ∀𝑥 ∈ 𝑉 ((𝑦 ∈ 𝑉 ↦ (𝑦 , 𝑥)) ∈ (𝑊 LMHom (ringLMod‘𝐹)) ∧ ((𝑥 , 𝑥) = 𝑍 → 𝑥 = 0 ) ∧ ∀𝑦 ∈ 𝑉 ( ∗ ‘(𝑥 , 𝑦)) = (𝑦 , 𝑥))))) |
52 | 2, 51 | sbcied 3439 |
. . 3
⊢ (𝑔 = 𝑊 → ([(Base‘𝑔) / 𝑣][(·𝑖‘𝑔) / ℎ][(Scalar‘𝑔) / 𝑓](𝑓
∈ *-Ring ∧ ∀𝑥 ∈ 𝑣 ((𝑦 ∈ 𝑣
↦ (𝑦ℎ𝑥)) ∈
(𝑔 LMHom (ringLMod‘𝑓)) ∧ ((𝑥ℎ𝑥) = (0g‘𝑓) → 𝑥 =
(0g‘𝑔)) ∧ ∀𝑦 ∈ 𝑣 ((*𝑟‘𝑓)‘(𝑥ℎ𝑦)) = (𝑦ℎ𝑥))) ↔ (𝐹 ∈ *-Ring ∧ ∀𝑥 ∈ 𝑉
((𝑦 ∈ 𝑉 ↦ (𝑦
, 𝑥)) ∈ (𝑊
LMHom (ringLMod‘𝐹)) ∧ ((𝑥 , 𝑥) = 𝑍 →
𝑥 = 0 ) ∧ ∀𝑦 ∈ 𝑉 (
∗ ‘(𝑥 , 𝑦)) = (𝑦
, 𝑥))))) |
53 | | df-phl 19790 |
. . 3
⊢ PreHil =
{𝑔 ∈ LVec ∣
[(Base‘𝑔) /
𝑣][(·𝑖‘𝑔) / ℎ][(Scalar‘𝑔) / 𝑓](𝑓
∈ *-Ring ∧ ∀𝑥 ∈ 𝑣 ((𝑦 ∈ 𝑣
↦ (𝑦ℎ𝑥)) ∈
(𝑔 LMHom (ringLMod‘𝑓)) ∧ ((𝑥ℎ𝑥) = (0g‘𝑓) → 𝑥 =
(0g‘𝑔)) ∧ ∀𝑦 ∈ 𝑣 ((*𝑟‘𝑓)‘(𝑥ℎ𝑦)) = (𝑦ℎ𝑥)))} |
54 | 52, 53 | elrab2 3333 |
. 2
⊢ (𝑊 ∈ PreHil ↔ (𝑊 ∈ LVec ∧ (𝐹 ∈ *-Ring ∧
∀𝑥 ∈ 𝑉 ((𝑦 ∈ 𝑉 ↦ (𝑦 , 𝑥)) ∈ (𝑊 LMHom (ringLMod‘𝐹)) ∧ ((𝑥 , 𝑥) = 𝑍 → 𝑥 = 0 ) ∧ ∀𝑦 ∈ 𝑉 ( ∗ ‘(𝑥 , 𝑦)) = (𝑦 , 𝑥))))) |
55 | | 3anass 1035 |
. 2
⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ *-Ring ∧
∀𝑥 ∈ 𝑉 ((𝑦 ∈ 𝑉 ↦ (𝑦 , 𝑥)) ∈ (𝑊 LMHom (ringLMod‘𝐹)) ∧ ((𝑥 , 𝑥) = 𝑍 → 𝑥 = 0 ) ∧ ∀𝑦 ∈ 𝑉 ( ∗ ‘(𝑥 , 𝑦)) = (𝑦 , 𝑥))) ↔ (𝑊 ∈ LVec ∧ (𝐹 ∈ *-Ring ∧ ∀𝑥 ∈ 𝑉 ((𝑦 ∈ 𝑉 ↦ (𝑦 , 𝑥)) ∈ (𝑊 LMHom (ringLMod‘𝐹)) ∧ ((𝑥 , 𝑥) = 𝑍 → 𝑥 = 0 ) ∧ ∀𝑦 ∈ 𝑉 ( ∗ ‘(𝑥 , 𝑦)) = (𝑦 , 𝑥))))) |
56 | 54, 55 | bitr4i 266 |
1
⊢ (𝑊 ∈ PreHil ↔ (𝑊 ∈ LVec ∧ 𝐹 ∈ *-Ring ∧
∀𝑥 ∈ 𝑉 ((𝑦 ∈ 𝑉 ↦ (𝑦 , 𝑥)) ∈ (𝑊 LMHom (ringLMod‘𝐹)) ∧ ((𝑥 , 𝑥) = 𝑍 → 𝑥 = 0 ) ∧ ∀𝑦 ∈ 𝑉 ( ∗ ‘(𝑥 , 𝑦)) = (𝑦 , 𝑥)))) |