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