Step | Hyp | Ref
| Expression |
1 | | isphld.l |
. 2
⊢ (𝜑 → 𝑊 ∈ LVec) |
2 | | isphld.f |
. . 3
⊢ (𝜑 → 𝐹 = (Scalar‘𝑊)) |
3 | | isphld.r |
. . 3
⊢ (𝜑 → 𝐹 ∈ *-Ring) |
4 | 2, 3 | eqeltrrd 2839 |
. 2
⊢ (𝜑 → (Scalar‘𝑊) ∈
*-Ring) |
5 | | oveq1 7220 |
. . . . . 6
⊢ (𝑦 = 𝑤 → (𝑦(·𝑖‘𝑊)𝑥) = (𝑤(·𝑖‘𝑊)𝑥)) |
6 | 5 | cbvmptv 5158 |
. . . . 5
⊢ (𝑦 ∈ (Base‘𝑊) ↦ (𝑦(·𝑖‘𝑊)𝑥)) = (𝑤 ∈ (Base‘𝑊) ↦ (𝑤(·𝑖‘𝑊)𝑥)) |
7 | | isphld.cl |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → (𝑥𝐼𝑦) ∈ 𝐾) |
8 | 7 | 3expib 1124 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → (𝑥𝐼𝑦) ∈ 𝐾)) |
9 | | isphld.v |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑉 = (Base‘𝑊)) |
10 | 9 | eleq2d 2823 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑥 ∈ 𝑉 ↔ 𝑥 ∈ (Base‘𝑊))) |
11 | 9 | eleq2d 2823 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑦 ∈ 𝑉 ↔ 𝑦 ∈ (Base‘𝑊))) |
12 | 10, 11 | anbi12d 634 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ↔ (𝑥 ∈ (Base‘𝑊) ∧ 𝑦 ∈ (Base‘𝑊)))) |
13 | | isphld.i |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐼 =
(·𝑖‘𝑊)) |
14 | 13 | oveqd 7230 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑥𝐼𝑦) = (𝑥(·𝑖‘𝑊)𝑦)) |
15 | | isphld.k |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐾 = (Base‘𝐹)) |
16 | 2 | fveq2d 6721 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (Base‘𝐹) =
(Base‘(Scalar‘𝑊))) |
17 | 15, 16 | eqtrd 2777 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐾 = (Base‘(Scalar‘𝑊))) |
18 | 14, 17 | eleq12d 2832 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑥𝐼𝑦) ∈ 𝐾 ↔ (𝑥(·𝑖‘𝑊)𝑦) ∈ (Base‘(Scalar‘𝑊)))) |
19 | 8, 12, 18 | 3imtr3d 296 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑥 ∈ (Base‘𝑊) ∧ 𝑦 ∈ (Base‘𝑊)) → (𝑥(·𝑖‘𝑊)𝑦) ∈ (Base‘(Scalar‘𝑊)))) |
20 | 19 | impl 459 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑊)) ∧ 𝑦 ∈ (Base‘𝑊)) → (𝑥(·𝑖‘𝑊)𝑦) ∈ (Base‘(Scalar‘𝑊))) |
21 | 20 | an32s 652 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ (Base‘𝑊)) ∧ 𝑥 ∈ (Base‘𝑊)) → (𝑥(·𝑖‘𝑊)𝑦) ∈ (Base‘(Scalar‘𝑊))) |
22 | | oveq1 7220 |
. . . . . . . . . . . 12
⊢ (𝑤 = 𝑥 → (𝑤(·𝑖‘𝑊)𝑦) = (𝑥(·𝑖‘𝑊)𝑦)) |
23 | 22 | cbvmptv 5158 |
. . . . . . . . . . 11
⊢ (𝑤 ∈ (Base‘𝑊) ↦ (𝑤(·𝑖‘𝑊)𝑦)) = (𝑥 ∈ (Base‘𝑊) ↦ (𝑥(·𝑖‘𝑊)𝑦)) |
24 | 21, 23 | fmptd 6931 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝑊)) → (𝑤 ∈ (Base‘𝑊) ↦ (𝑤(·𝑖‘𝑊)𝑦)):(Base‘𝑊)⟶(Base‘(Scalar‘𝑊))) |
25 | 24 | ralrimiva 3105 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑦 ∈ (Base‘𝑊)(𝑤 ∈ (Base‘𝑊) ↦ (𝑤(·𝑖‘𝑊)𝑦)):(Base‘𝑊)⟶(Base‘(Scalar‘𝑊))) |
26 | | oveq2 7221 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑧 → (𝑤(·𝑖‘𝑊)𝑦) = (𝑤(·𝑖‘𝑊)𝑧)) |
27 | 26 | mpteq2dv 5151 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑧 → (𝑤 ∈ (Base‘𝑊) ↦ (𝑤(·𝑖‘𝑊)𝑦)) = (𝑤 ∈ (Base‘𝑊) ↦ (𝑤(·𝑖‘𝑊)𝑧))) |
28 | 27 | feq1d 6530 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑧 → ((𝑤 ∈ (Base‘𝑊) ↦ (𝑤(·𝑖‘𝑊)𝑦)):(Base‘𝑊)⟶(Base‘(Scalar‘𝑊)) ↔ (𝑤 ∈ (Base‘𝑊) ↦ (𝑤(·𝑖‘𝑊)𝑧)):(Base‘𝑊)⟶(Base‘(Scalar‘𝑊)))) |
29 | 28 | rspccva 3536 |
. . . . . . . . 9
⊢
((∀𝑦 ∈
(Base‘𝑊)(𝑤 ∈ (Base‘𝑊) ↦ (𝑤(·𝑖‘𝑊)𝑦)):(Base‘𝑊)⟶(Base‘(Scalar‘𝑊)) ∧ 𝑧 ∈ (Base‘𝑊)) → (𝑤 ∈ (Base‘𝑊) ↦ (𝑤(·𝑖‘𝑊)𝑧)):(Base‘𝑊)⟶(Base‘(Scalar‘𝑊))) |
30 | 25, 29 | sylan 583 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ (Base‘𝑊)) → (𝑤 ∈ (Base‘𝑊) ↦ (𝑤(·𝑖‘𝑊)𝑧)):(Base‘𝑊)⟶(Base‘(Scalar‘𝑊))) |
31 | | eqidd 2738 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ (Base‘𝑊)) → (Scalar‘𝑊) = (Scalar‘𝑊)) |
32 | | isphld.d |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐾 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (((𝑞 · 𝑥) + 𝑦)𝐼𝑧) = ((𝑞 × (𝑥𝐼𝑧)) ⨣ (𝑦𝐼𝑧))) |
33 | 32 | 3exp 1121 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑞 ∈ 𝐾 → ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉) → (((𝑞 · 𝑥) + 𝑦)𝐼𝑧) = ((𝑞 × (𝑥𝐼𝑧)) ⨣ (𝑦𝐼𝑧))))) |
34 | 17 | eleq2d 2823 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑞 ∈ 𝐾 ↔ 𝑞 ∈ (Base‘(Scalar‘𝑊)))) |
35 | | 3anrot 1102 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑧 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ↔ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) |
36 | 9 | eleq2d 2823 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑧 ∈ 𝑉 ↔ 𝑧 ∈ (Base‘𝑊))) |
37 | 36, 10, 11 | 3anbi123d 1438 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝑧 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ↔ (𝑧 ∈ (Base‘𝑊) ∧ 𝑥 ∈ (Base‘𝑊) ∧ 𝑦 ∈ (Base‘𝑊)))) |
38 | 35, 37 | bitr3id 288 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉) ↔ (𝑧 ∈ (Base‘𝑊) ∧ 𝑥 ∈ (Base‘𝑊) ∧ 𝑦 ∈ (Base‘𝑊)))) |
39 | | isphld.a |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → + =
(+g‘𝑊)) |
40 | | isphld.s |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → · = (
·𝑠 ‘𝑊)) |
41 | 40 | oveqd 7230 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑞 · 𝑥) = (𝑞( ·𝑠
‘𝑊)𝑥)) |
42 | | eqidd 2738 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑦 = 𝑦) |
43 | 39, 41, 42 | oveq123d 7234 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((𝑞 · 𝑥) + 𝑦) = ((𝑞( ·𝑠
‘𝑊)𝑥)(+g‘𝑊)𝑦)) |
44 | | eqidd 2738 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑧 = 𝑧) |
45 | 13, 43, 44 | oveq123d 7234 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (((𝑞 · 𝑥) + 𝑦)𝐼𝑧) = (((𝑞( ·𝑠
‘𝑊)𝑥)(+g‘𝑊)𝑦)(·𝑖‘𝑊)𝑧)) |
46 | | isphld.p |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ⨣ =
(+g‘𝐹)) |
47 | 2 | fveq2d 6721 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (+g‘𝐹) =
(+g‘(Scalar‘𝑊))) |
48 | 46, 47 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ⨣ =
(+g‘(Scalar‘𝑊))) |
49 | | isphld.t |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → × =
(.r‘𝐹)) |
50 | 2 | fveq2d 6721 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (.r‘𝐹) =
(.r‘(Scalar‘𝑊))) |
51 | 49, 50 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → × =
(.r‘(Scalar‘𝑊))) |
52 | | eqidd 2738 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑞 = 𝑞) |
53 | 13 | oveqd 7230 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑥𝐼𝑧) = (𝑥(·𝑖‘𝑊)𝑧)) |
54 | 51, 52, 53 | oveq123d 7234 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑞 × (𝑥𝐼𝑧)) = (𝑞(.r‘(Scalar‘𝑊))(𝑥(·𝑖‘𝑊)𝑧))) |
55 | 13 | oveqd 7230 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑦𝐼𝑧) = (𝑦(·𝑖‘𝑊)𝑧)) |
56 | 48, 54, 55 | oveq123d 7234 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝑞 × (𝑥𝐼𝑧)) ⨣ (𝑦𝐼𝑧)) = ((𝑞(.r‘(Scalar‘𝑊))(𝑥(·𝑖‘𝑊)𝑧))(+g‘(Scalar‘𝑊))(𝑦(·𝑖‘𝑊)𝑧))) |
57 | 45, 56 | eqeq12d 2753 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((((𝑞 · 𝑥) + 𝑦)𝐼𝑧) = ((𝑞 × (𝑥𝐼𝑧)) ⨣ (𝑦𝐼𝑧)) ↔ (((𝑞( ·𝑠
‘𝑊)𝑥)(+g‘𝑊)𝑦)(·𝑖‘𝑊)𝑧) = ((𝑞(.r‘(Scalar‘𝑊))(𝑥(·𝑖‘𝑊)𝑧))(+g‘(Scalar‘𝑊))(𝑦(·𝑖‘𝑊)𝑧)))) |
58 | 38, 57 | imbi12d 348 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉) → (((𝑞 · 𝑥) + 𝑦)𝐼𝑧) = ((𝑞 × (𝑥𝐼𝑧)) ⨣ (𝑦𝐼𝑧))) ↔ ((𝑧 ∈ (Base‘𝑊) ∧ 𝑥 ∈ (Base‘𝑊) ∧ 𝑦 ∈ (Base‘𝑊)) → (((𝑞( ·𝑠
‘𝑊)𝑥)(+g‘𝑊)𝑦)(·𝑖‘𝑊)𝑧) = ((𝑞(.r‘(Scalar‘𝑊))(𝑥(·𝑖‘𝑊)𝑧))(+g‘(Scalar‘𝑊))(𝑦(·𝑖‘𝑊)𝑧))))) |
59 | 33, 34, 58 | 3imtr3d 296 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑞 ∈ (Base‘(Scalar‘𝑊)) → ((𝑧 ∈ (Base‘𝑊) ∧ 𝑥 ∈ (Base‘𝑊) ∧ 𝑦 ∈ (Base‘𝑊)) → (((𝑞( ·𝑠
‘𝑊)𝑥)(+g‘𝑊)𝑦)(·𝑖‘𝑊)𝑧) = ((𝑞(.r‘(Scalar‘𝑊))(𝑥(·𝑖‘𝑊)𝑧))(+g‘(Scalar‘𝑊))(𝑦(·𝑖‘𝑊)𝑧))))) |
60 | 59 | imp31 421 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑞 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑧 ∈ (Base‘𝑊) ∧ 𝑥 ∈ (Base‘𝑊) ∧ 𝑦 ∈ (Base‘𝑊))) → (((𝑞( ·𝑠
‘𝑊)𝑥)(+g‘𝑊)𝑦)(·𝑖‘𝑊)𝑧) = ((𝑞(.r‘(Scalar‘𝑊))(𝑥(·𝑖‘𝑊)𝑧))(+g‘(Scalar‘𝑊))(𝑦(·𝑖‘𝑊)𝑧))) |
61 | 60 | 3exp2 1356 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑞 ∈ (Base‘(Scalar‘𝑊))) → (𝑧 ∈ (Base‘𝑊) → (𝑥 ∈ (Base‘𝑊) → (𝑦 ∈ (Base‘𝑊) → (((𝑞( ·𝑠
‘𝑊)𝑥)(+g‘𝑊)𝑦)(·𝑖‘𝑊)𝑧) = ((𝑞(.r‘(Scalar‘𝑊))(𝑥(·𝑖‘𝑊)𝑧))(+g‘(Scalar‘𝑊))(𝑦(·𝑖‘𝑊)𝑧)))))) |
62 | 61 | impancom 455 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ (Base‘𝑊)) → (𝑞 ∈ (Base‘(Scalar‘𝑊)) → (𝑥 ∈ (Base‘𝑊) → (𝑦 ∈ (Base‘𝑊) → (((𝑞( ·𝑠
‘𝑊)𝑥)(+g‘𝑊)𝑦)(·𝑖‘𝑊)𝑧) = ((𝑞(.r‘(Scalar‘𝑊))(𝑥(·𝑖‘𝑊)𝑧))(+g‘(Scalar‘𝑊))(𝑦(·𝑖‘𝑊)𝑧)))))) |
63 | 62 | 3imp2 1351 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ (Base‘𝑊)) ∧ (𝑞 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑥 ∈ (Base‘𝑊) ∧ 𝑦 ∈ (Base‘𝑊))) → (((𝑞( ·𝑠
‘𝑊)𝑥)(+g‘𝑊)𝑦)(·𝑖‘𝑊)𝑧) = ((𝑞(.r‘(Scalar‘𝑊))(𝑥(·𝑖‘𝑊)𝑧))(+g‘(Scalar‘𝑊))(𝑦(·𝑖‘𝑊)𝑧))) |
64 | | lveclmod 20143 |
. . . . . . . . . . . . . . . 16
⊢ (𝑊 ∈ LVec → 𝑊 ∈ LMod) |
65 | 1, 64 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑊 ∈ LMod) |
66 | 65 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑧 ∈ (Base‘𝑊)) → 𝑊 ∈ LMod) |
67 | 66 | adantr 484 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑧 ∈ (Base‘𝑊)) ∧ (𝑞 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑥 ∈ (Base‘𝑊) ∧ 𝑦 ∈ (Base‘𝑊))) → 𝑊 ∈ LMod) |
68 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢
(Base‘𝑊) =
(Base‘𝑊) |
69 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢
(LSubSp‘𝑊) =
(LSubSp‘𝑊) |
70 | 68, 69 | lss1 19975 |
. . . . . . . . . . . . 13
⊢ (𝑊 ∈ LMod →
(Base‘𝑊) ∈
(LSubSp‘𝑊)) |
71 | 67, 70 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ∈ (Base‘𝑊)) ∧ (𝑞 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑥 ∈ (Base‘𝑊) ∧ 𝑦 ∈ (Base‘𝑊))) → (Base‘𝑊) ∈ (LSubSp‘𝑊)) |
72 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢
(Scalar‘𝑊) =
(Scalar‘𝑊) |
73 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢
(Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊)) |
74 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢
(+g‘𝑊) = (+g‘𝑊) |
75 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢ (
·𝑠 ‘𝑊) = ( ·𝑠
‘𝑊) |
76 | 72, 73, 74, 75, 69 | lsscl 19979 |
. . . . . . . . . . . 12
⊢
(((Base‘𝑊)
∈ (LSubSp‘𝑊)
∧ (𝑞 ∈
(Base‘(Scalar‘𝑊)) ∧ 𝑥 ∈ (Base‘𝑊) ∧ 𝑦 ∈ (Base‘𝑊))) → ((𝑞( ·𝑠
‘𝑊)𝑥)(+g‘𝑊)𝑦) ∈ (Base‘𝑊)) |
77 | 71, 76 | sylancom 591 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ (Base‘𝑊)) ∧ (𝑞 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑥 ∈ (Base‘𝑊) ∧ 𝑦 ∈ (Base‘𝑊))) → ((𝑞( ·𝑠
‘𝑊)𝑥)(+g‘𝑊)𝑦) ∈ (Base‘𝑊)) |
78 | | oveq1 7220 |
. . . . . . . . . . . 12
⊢ (𝑤 = ((𝑞( ·𝑠
‘𝑊)𝑥)(+g‘𝑊)𝑦) → (𝑤(·𝑖‘𝑊)𝑧) = (((𝑞( ·𝑠
‘𝑊)𝑥)(+g‘𝑊)𝑦)(·𝑖‘𝑊)𝑧)) |
79 | | eqid 2737 |
. . . . . . . . . . . 12
⊢ (𝑤 ∈ (Base‘𝑊) ↦ (𝑤(·𝑖‘𝑊)𝑧)) = (𝑤 ∈ (Base‘𝑊) ↦ (𝑤(·𝑖‘𝑊)𝑧)) |
80 | | ovex 7246 |
. . . . . . . . . . . 12
⊢ (𝑤(·𝑖‘𝑊)𝑧) ∈ V |
81 | 78, 79, 80 | fvmpt3i 6823 |
. . . . . . . . . . 11
⊢ (((𝑞(
·𝑠 ‘𝑊)𝑥)(+g‘𝑊)𝑦) ∈ (Base‘𝑊) → ((𝑤 ∈ (Base‘𝑊) ↦ (𝑤(·𝑖‘𝑊)𝑧))‘((𝑞( ·𝑠
‘𝑊)𝑥)(+g‘𝑊)𝑦)) = (((𝑞( ·𝑠
‘𝑊)𝑥)(+g‘𝑊)𝑦)(·𝑖‘𝑊)𝑧)) |
82 | 77, 81 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ (Base‘𝑊)) ∧ (𝑞 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑥 ∈ (Base‘𝑊) ∧ 𝑦 ∈ (Base‘𝑊))) → ((𝑤 ∈ (Base‘𝑊) ↦ (𝑤(·𝑖‘𝑊)𝑧))‘((𝑞( ·𝑠
‘𝑊)𝑥)(+g‘𝑊)𝑦)) = (((𝑞( ·𝑠
‘𝑊)𝑥)(+g‘𝑊)𝑦)(·𝑖‘𝑊)𝑧)) |
83 | | simpr2 1197 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑧 ∈ (Base‘𝑊)) ∧ (𝑞 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑥 ∈ (Base‘𝑊) ∧ 𝑦 ∈ (Base‘𝑊))) → 𝑥 ∈ (Base‘𝑊)) |
84 | | oveq1 7220 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = 𝑥 → (𝑤(·𝑖‘𝑊)𝑧) = (𝑥(·𝑖‘𝑊)𝑧)) |
85 | 84, 79, 80 | fvmpt3i 6823 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (Base‘𝑊) → ((𝑤 ∈ (Base‘𝑊) ↦ (𝑤(·𝑖‘𝑊)𝑧))‘𝑥) = (𝑥(·𝑖‘𝑊)𝑧)) |
86 | 83, 85 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ∈ (Base‘𝑊)) ∧ (𝑞 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑥 ∈ (Base‘𝑊) ∧ 𝑦 ∈ (Base‘𝑊))) → ((𝑤 ∈ (Base‘𝑊) ↦ (𝑤(·𝑖‘𝑊)𝑧))‘𝑥) = (𝑥(·𝑖‘𝑊)𝑧)) |
87 | 86 | oveq2d 7229 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ (Base‘𝑊)) ∧ (𝑞 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑥 ∈ (Base‘𝑊) ∧ 𝑦 ∈ (Base‘𝑊))) → (𝑞(.r‘(Scalar‘𝑊))((𝑤 ∈ (Base‘𝑊) ↦ (𝑤(·𝑖‘𝑊)𝑧))‘𝑥)) = (𝑞(.r‘(Scalar‘𝑊))(𝑥(·𝑖‘𝑊)𝑧))) |
88 | | simpr3 1198 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ∈ (Base‘𝑊)) ∧ (𝑞 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑥 ∈ (Base‘𝑊) ∧ 𝑦 ∈ (Base‘𝑊))) → 𝑦 ∈ (Base‘𝑊)) |
89 | | oveq1 7220 |
. . . . . . . . . . . . 13
⊢ (𝑤 = 𝑦 → (𝑤(·𝑖‘𝑊)𝑧) = (𝑦(·𝑖‘𝑊)𝑧)) |
90 | 89, 79, 80 | fvmpt3i 6823 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ (Base‘𝑊) → ((𝑤 ∈ (Base‘𝑊) ↦ (𝑤(·𝑖‘𝑊)𝑧))‘𝑦) = (𝑦(·𝑖‘𝑊)𝑧)) |
91 | 88, 90 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ (Base‘𝑊)) ∧ (𝑞 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑥 ∈ (Base‘𝑊) ∧ 𝑦 ∈ (Base‘𝑊))) → ((𝑤 ∈ (Base‘𝑊) ↦ (𝑤(·𝑖‘𝑊)𝑧))‘𝑦) = (𝑦(·𝑖‘𝑊)𝑧)) |
92 | 87, 91 | oveq12d 7231 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ (Base‘𝑊)) ∧ (𝑞 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑥 ∈ (Base‘𝑊) ∧ 𝑦 ∈ (Base‘𝑊))) → ((𝑞(.r‘(Scalar‘𝑊))((𝑤 ∈ (Base‘𝑊) ↦ (𝑤(·𝑖‘𝑊)𝑧))‘𝑥))(+g‘(Scalar‘𝑊))((𝑤 ∈ (Base‘𝑊) ↦ (𝑤(·𝑖‘𝑊)𝑧))‘𝑦)) = ((𝑞(.r‘(Scalar‘𝑊))(𝑥(·𝑖‘𝑊)𝑧))(+g‘(Scalar‘𝑊))(𝑦(·𝑖‘𝑊)𝑧))) |
93 | 63, 82, 92 | 3eqtr4d 2787 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ (Base‘𝑊)) ∧ (𝑞 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑥 ∈ (Base‘𝑊) ∧ 𝑦 ∈ (Base‘𝑊))) → ((𝑤 ∈ (Base‘𝑊) ↦ (𝑤(·𝑖‘𝑊)𝑧))‘((𝑞( ·𝑠
‘𝑊)𝑥)(+g‘𝑊)𝑦)) = ((𝑞(.r‘(Scalar‘𝑊))((𝑤 ∈ (Base‘𝑊) ↦ (𝑤(·𝑖‘𝑊)𝑧))‘𝑥))(+g‘(Scalar‘𝑊))((𝑤 ∈ (Base‘𝑊) ↦ (𝑤(·𝑖‘𝑊)𝑧))‘𝑦))) |
94 | 93 | ralrimivvva 3113 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ (Base‘𝑊)) → ∀𝑞 ∈ (Base‘(Scalar‘𝑊))∀𝑥 ∈ (Base‘𝑊)∀𝑦 ∈ (Base‘𝑊)((𝑤 ∈ (Base‘𝑊) ↦ (𝑤(·𝑖‘𝑊)𝑧))‘((𝑞( ·𝑠
‘𝑊)𝑥)(+g‘𝑊)𝑦)) = ((𝑞(.r‘(Scalar‘𝑊))((𝑤 ∈ (Base‘𝑊) ↦ (𝑤(·𝑖‘𝑊)𝑧))‘𝑥))(+g‘(Scalar‘𝑊))((𝑤 ∈ (Base‘𝑊) ↦ (𝑤(·𝑖‘𝑊)𝑧))‘𝑦))) |
95 | 72 | lmodring 19907 |
. . . . . . . . . . 11
⊢ (𝑊 ∈ LMod →
(Scalar‘𝑊) ∈
Ring) |
96 | | rlmlmod 20242 |
. . . . . . . . . . 11
⊢
((Scalar‘𝑊)
∈ Ring → (ringLMod‘(Scalar‘𝑊)) ∈ LMod) |
97 | 65, 95, 96 | 3syl 18 |
. . . . . . . . . 10
⊢ (𝜑 →
(ringLMod‘(Scalar‘𝑊)) ∈ LMod) |
98 | 97 | adantr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ (Base‘𝑊)) →
(ringLMod‘(Scalar‘𝑊)) ∈ LMod) |
99 | | rlmbas 20232 |
. . . . . . . . . 10
⊢
(Base‘(Scalar‘𝑊)) =
(Base‘(ringLMod‘(Scalar‘𝑊))) |
100 | | fvex 6730 |
. . . . . . . . . . 11
⊢
(Scalar‘𝑊)
∈ V |
101 | | rlmsca 20237 |
. . . . . . . . . . 11
⊢
((Scalar‘𝑊)
∈ V → (Scalar‘𝑊) =
(Scalar‘(ringLMod‘(Scalar‘𝑊)))) |
102 | 100, 101 | ax-mp 5 |
. . . . . . . . . 10
⊢
(Scalar‘𝑊) =
(Scalar‘(ringLMod‘(Scalar‘𝑊))) |
103 | | rlmplusg 20233 |
. . . . . . . . . 10
⊢
(+g‘(Scalar‘𝑊)) =
(+g‘(ringLMod‘(Scalar‘𝑊))) |
104 | | rlmvsca 20239 |
. . . . . . . . . 10
⊢
(.r‘(Scalar‘𝑊)) = ( ·𝑠
‘(ringLMod‘(Scalar‘𝑊))) |
105 | 68, 99, 72, 102, 73, 74, 103, 75, 104 | islmhm2 20075 |
. . . . . . . . 9
⊢ ((𝑊 ∈ LMod ∧
(ringLMod‘(Scalar‘𝑊)) ∈ LMod) → ((𝑤 ∈ (Base‘𝑊) ↦ (𝑤(·𝑖‘𝑊)𝑧)) ∈ (𝑊 LMHom (ringLMod‘(Scalar‘𝑊))) ↔ ((𝑤 ∈ (Base‘𝑊) ↦ (𝑤(·𝑖‘𝑊)𝑧)):(Base‘𝑊)⟶(Base‘(Scalar‘𝑊)) ∧ (Scalar‘𝑊) = (Scalar‘𝑊) ∧ ∀𝑞 ∈ (Base‘(Scalar‘𝑊))∀𝑥 ∈ (Base‘𝑊)∀𝑦 ∈ (Base‘𝑊)((𝑤 ∈ (Base‘𝑊) ↦ (𝑤(·𝑖‘𝑊)𝑧))‘((𝑞( ·𝑠
‘𝑊)𝑥)(+g‘𝑊)𝑦)) = ((𝑞(.r‘(Scalar‘𝑊))((𝑤 ∈ (Base‘𝑊) ↦ (𝑤(·𝑖‘𝑊)𝑧))‘𝑥))(+g‘(Scalar‘𝑊))((𝑤 ∈ (Base‘𝑊) ↦ (𝑤(·𝑖‘𝑊)𝑧))‘𝑦))))) |
106 | 66, 98, 105 | syl2anc 587 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ (Base‘𝑊)) → ((𝑤 ∈ (Base‘𝑊) ↦ (𝑤(·𝑖‘𝑊)𝑧)) ∈ (𝑊 LMHom (ringLMod‘(Scalar‘𝑊))) ↔ ((𝑤 ∈ (Base‘𝑊) ↦ (𝑤(·𝑖‘𝑊)𝑧)):(Base‘𝑊)⟶(Base‘(Scalar‘𝑊)) ∧ (Scalar‘𝑊) = (Scalar‘𝑊) ∧ ∀𝑞 ∈ (Base‘(Scalar‘𝑊))∀𝑥 ∈ (Base‘𝑊)∀𝑦 ∈ (Base‘𝑊)((𝑤 ∈ (Base‘𝑊) ↦ (𝑤(·𝑖‘𝑊)𝑧))‘((𝑞( ·𝑠
‘𝑊)𝑥)(+g‘𝑊)𝑦)) = ((𝑞(.r‘(Scalar‘𝑊))((𝑤 ∈ (Base‘𝑊) ↦ (𝑤(·𝑖‘𝑊)𝑧))‘𝑥))(+g‘(Scalar‘𝑊))((𝑤 ∈ (Base‘𝑊) ↦ (𝑤(·𝑖‘𝑊)𝑧))‘𝑦))))) |
107 | 30, 31, 94, 106 | mpbir3and 1344 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ (Base‘𝑊)) → (𝑤 ∈ (Base‘𝑊) ↦ (𝑤(·𝑖‘𝑊)𝑧)) ∈ (𝑊 LMHom (ringLMod‘(Scalar‘𝑊)))) |
108 | 107 | ralrimiva 3105 |
. . . . . 6
⊢ (𝜑 → ∀𝑧 ∈ (Base‘𝑊)(𝑤 ∈ (Base‘𝑊) ↦ (𝑤(·𝑖‘𝑊)𝑧)) ∈ (𝑊 LMHom (ringLMod‘(Scalar‘𝑊)))) |
109 | | oveq2 7221 |
. . . . . . . . 9
⊢ (𝑧 = 𝑥 → (𝑤(·𝑖‘𝑊)𝑧) = (𝑤(·𝑖‘𝑊)𝑥)) |
110 | 109 | mpteq2dv 5151 |
. . . . . . . 8
⊢ (𝑧 = 𝑥 → (𝑤 ∈ (Base‘𝑊) ↦ (𝑤(·𝑖‘𝑊)𝑧)) = (𝑤 ∈ (Base‘𝑊) ↦ (𝑤(·𝑖‘𝑊)𝑥))) |
111 | 110 | eleq1d 2822 |
. . . . . . 7
⊢ (𝑧 = 𝑥 → ((𝑤 ∈ (Base‘𝑊) ↦ (𝑤(·𝑖‘𝑊)𝑧)) ∈ (𝑊 LMHom (ringLMod‘(Scalar‘𝑊))) ↔ (𝑤 ∈ (Base‘𝑊) ↦ (𝑤(·𝑖‘𝑊)𝑥)) ∈ (𝑊 LMHom (ringLMod‘(Scalar‘𝑊))))) |
112 | 111 | rspccva 3536 |
. . . . . 6
⊢
((∀𝑧 ∈
(Base‘𝑊)(𝑤 ∈ (Base‘𝑊) ↦ (𝑤(·𝑖‘𝑊)𝑧)) ∈ (𝑊 LMHom (ringLMod‘(Scalar‘𝑊))) ∧ 𝑥 ∈ (Base‘𝑊)) → (𝑤 ∈ (Base‘𝑊) ↦ (𝑤(·𝑖‘𝑊)𝑥)) ∈ (𝑊 LMHom (ringLMod‘(Scalar‘𝑊)))) |
113 | 108, 112 | sylan 583 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑊)) → (𝑤 ∈ (Base‘𝑊) ↦ (𝑤(·𝑖‘𝑊)𝑥)) ∈ (𝑊 LMHom (ringLMod‘(Scalar‘𝑊)))) |
114 | 6, 113 | eqeltrid 2842 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑊)) → (𝑦 ∈ (Base‘𝑊) ↦ (𝑦(·𝑖‘𝑊)𝑥)) ∈ (𝑊 LMHom (ringLMod‘(Scalar‘𝑊)))) |
115 | | isphld.ns |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉 ∧ (𝑥𝐼𝑥) = 𝑂) → 𝑥 = 0 ) |
116 | 115 | 3exp 1121 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ 𝑉 → ((𝑥𝐼𝑥) = 𝑂 → 𝑥 = 0 ))) |
117 | 13 | oveqd 7230 |
. . . . . . . 8
⊢ (𝜑 → (𝑥𝐼𝑥) = (𝑥(·𝑖‘𝑊)𝑥)) |
118 | | isphld.o |
. . . . . . . . 9
⊢ (𝜑 → 𝑂 = (0g‘𝐹)) |
119 | 2 | fveq2d 6721 |
. . . . . . . . 9
⊢ (𝜑 → (0g‘𝐹) =
(0g‘(Scalar‘𝑊))) |
120 | 118, 119 | eqtrd 2777 |
. . . . . . . 8
⊢ (𝜑 → 𝑂 = (0g‘(Scalar‘𝑊))) |
121 | 117, 120 | eqeq12d 2753 |
. . . . . . 7
⊢ (𝜑 → ((𝑥𝐼𝑥) = 𝑂 ↔ (𝑥(·𝑖‘𝑊)𝑥) = (0g‘(Scalar‘𝑊)))) |
122 | | isphld.z |
. . . . . . . 8
⊢ (𝜑 → 0 =
(0g‘𝑊)) |
123 | 122 | eqeq2d 2748 |
. . . . . . 7
⊢ (𝜑 → (𝑥 = 0 ↔ 𝑥 = (0g‘𝑊))) |
124 | 121, 123 | imbi12d 348 |
. . . . . 6
⊢ (𝜑 → (((𝑥𝐼𝑥) = 𝑂 → 𝑥 = 0 ) ↔ ((𝑥(·𝑖‘𝑊)𝑥) = (0g‘(Scalar‘𝑊)) → 𝑥 = (0g‘𝑊)))) |
125 | 116, 10, 124 | 3imtr3d 296 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (Base‘𝑊) → ((𝑥(·𝑖‘𝑊)𝑥) = (0g‘(Scalar‘𝑊)) → 𝑥 = (0g‘𝑊)))) |
126 | 125 | imp 410 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑊)) → ((𝑥(·𝑖‘𝑊)𝑥) = (0g‘(Scalar‘𝑊)) → 𝑥 = (0g‘𝑊))) |
127 | | isphld.cj |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → ( ∗ ‘(𝑥𝐼𝑦)) = (𝑦𝐼𝑥)) |
128 | 127 | 3expib 1124 |
. . . . . . 7
⊢ (𝜑 → ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → ( ∗ ‘(𝑥𝐼𝑦)) = (𝑦𝐼𝑥))) |
129 | | isphld.c |
. . . . . . . . . 10
⊢ (𝜑 → ∗ =
(*𝑟‘𝐹)) |
130 | 2 | fveq2d 6721 |
. . . . . . . . . 10
⊢ (𝜑 →
(*𝑟‘𝐹) =
(*𝑟‘(Scalar‘𝑊))) |
131 | 129, 130 | eqtrd 2777 |
. . . . . . . . 9
⊢ (𝜑 → ∗ =
(*𝑟‘(Scalar‘𝑊))) |
132 | 131, 14 | fveq12d 6724 |
. . . . . . . 8
⊢ (𝜑 → ( ∗ ‘(𝑥𝐼𝑦)) =
((*𝑟‘(Scalar‘𝑊))‘(𝑥(·𝑖‘𝑊)𝑦))) |
133 | 13 | oveqd 7230 |
. . . . . . . 8
⊢ (𝜑 → (𝑦𝐼𝑥) = (𝑦(·𝑖‘𝑊)𝑥)) |
134 | 132, 133 | eqeq12d 2753 |
. . . . . . 7
⊢ (𝜑 → (( ∗ ‘(𝑥𝐼𝑦)) = (𝑦𝐼𝑥) ↔
((*𝑟‘(Scalar‘𝑊))‘(𝑥(·𝑖‘𝑊)𝑦)) = (𝑦(·𝑖‘𝑊)𝑥))) |
135 | 128, 12, 134 | 3imtr3d 296 |
. . . . . 6
⊢ (𝜑 → ((𝑥 ∈ (Base‘𝑊) ∧ 𝑦 ∈ (Base‘𝑊)) →
((*𝑟‘(Scalar‘𝑊))‘(𝑥(·𝑖‘𝑊)𝑦)) = (𝑦(·𝑖‘𝑊)𝑥))) |
136 | 135 | expdimp 456 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑊)) → (𝑦 ∈ (Base‘𝑊) →
((*𝑟‘(Scalar‘𝑊))‘(𝑥(·𝑖‘𝑊)𝑦)) = (𝑦(·𝑖‘𝑊)𝑥))) |
137 | 136 | ralrimiv 3104 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑊)) → ∀𝑦 ∈ (Base‘𝑊)((*𝑟‘(Scalar‘𝑊))‘(𝑥(·𝑖‘𝑊)𝑦)) = (𝑦(·𝑖‘𝑊)𝑥)) |
138 | 114, 126,
137 | 3jca 1130 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑊)) → ((𝑦 ∈ (Base‘𝑊) ↦ (𝑦(·𝑖‘𝑊)𝑥)) ∈ (𝑊 LMHom (ringLMod‘(Scalar‘𝑊))) ∧ ((𝑥(·𝑖‘𝑊)𝑥) = (0g‘(Scalar‘𝑊)) → 𝑥 = (0g‘𝑊)) ∧ ∀𝑦 ∈ (Base‘𝑊)((*𝑟‘(Scalar‘𝑊))‘(𝑥(·𝑖‘𝑊)𝑦)) = (𝑦(·𝑖‘𝑊)𝑥))) |
139 | 138 | ralrimiva 3105 |
. 2
⊢ (𝜑 → ∀𝑥 ∈ (Base‘𝑊)((𝑦 ∈ (Base‘𝑊) ↦ (𝑦(·𝑖‘𝑊)𝑥)) ∈ (𝑊 LMHom (ringLMod‘(Scalar‘𝑊))) ∧ ((𝑥(·𝑖‘𝑊)𝑥) = (0g‘(Scalar‘𝑊)) → 𝑥 = (0g‘𝑊)) ∧ ∀𝑦 ∈ (Base‘𝑊)((*𝑟‘(Scalar‘𝑊))‘(𝑥(·𝑖‘𝑊)𝑦)) = (𝑦(·𝑖‘𝑊)𝑥))) |
140 | | eqid 2737 |
. . 3
⊢
(·𝑖‘𝑊) =
(·𝑖‘𝑊) |
141 | | eqid 2737 |
. . 3
⊢
(0g‘𝑊) = (0g‘𝑊) |
142 | | eqid 2737 |
. . 3
⊢
(*𝑟‘(Scalar‘𝑊)) =
(*𝑟‘(Scalar‘𝑊)) |
143 | | eqid 2737 |
. . 3
⊢
(0g‘(Scalar‘𝑊)) =
(0g‘(Scalar‘𝑊)) |
144 | 68, 72, 140, 141, 142, 143 | isphl 20590 |
. 2
⊢ (𝑊 ∈ PreHil ↔ (𝑊 ∈ LVec ∧
(Scalar‘𝑊) ∈
*-Ring ∧ ∀𝑥
∈ (Base‘𝑊)((𝑦 ∈ (Base‘𝑊) ↦ (𝑦(·𝑖‘𝑊)𝑥)) ∈ (𝑊 LMHom (ringLMod‘(Scalar‘𝑊))) ∧ ((𝑥(·𝑖‘𝑊)𝑥) = (0g‘(Scalar‘𝑊)) → 𝑥 = (0g‘𝑊)) ∧ ∀𝑦 ∈ (Base‘𝑊)((*𝑟‘(Scalar‘𝑊))‘(𝑥(·𝑖‘𝑊)𝑦)) = (𝑦(·𝑖‘𝑊)𝑥)))) |
145 | 1, 4, 139, 144 | syl3anbrc 1345 |
1
⊢ (𝜑 → 𝑊 ∈ PreHil) |