Step | Hyp | Ref
| Expression |
1 | | phlpropd.1 |
. . . 4
⊢ (𝜑 → 𝐵 = (Base‘𝐾)) |
2 | | phlpropd.2 |
. . . 4
⊢ (𝜑 → 𝐵 = (Base‘𝐿)) |
3 | | phlpropd.3 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦)) |
4 | | phlpropd.4 |
. . . 4
⊢ (𝜑 → 𝐹 = (Scalar‘𝐾)) |
5 | | phlpropd.5 |
. . . 4
⊢ (𝜑 → 𝐹 = (Scalar‘𝐿)) |
6 | | phlpropd.6 |
. . . 4
⊢ 𝑃 = (Base‘𝐹) |
7 | | phlpropd.7 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵)) → (𝑥( ·𝑠
‘𝐾)𝑦) = (𝑥( ·𝑠
‘𝐿)𝑦)) |
8 | 1, 2, 3, 4, 5, 6, 7 | lvecpropd 20418 |
. . 3
⊢ (𝜑 → (𝐾 ∈ LVec ↔ 𝐿 ∈ LVec)) |
9 | 4, 5 | eqtr3d 2780 |
. . . 4
⊢ (𝜑 → (Scalar‘𝐾) = (Scalar‘𝐿)) |
10 | 9 | eleq1d 2823 |
. . 3
⊢ (𝜑 → ((Scalar‘𝐾) ∈ *-Ring ↔
(Scalar‘𝐿) ∈
*-Ring)) |
11 | | phlpropd.8 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(·𝑖‘𝐾)𝑦) = (𝑥(·𝑖‘𝐿)𝑦)) |
12 | 11 | oveqrspc2v 7296 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵)) → (𝑏(·𝑖‘𝐾)𝑎) = (𝑏(·𝑖‘𝐿)𝑎)) |
13 | 12 | anass1rs 652 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) → (𝑏(·𝑖‘𝐾)𝑎) = (𝑏(·𝑖‘𝐿)𝑎)) |
14 | 13 | mpteq2dva 5175 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → (𝑏 ∈ 𝐵 ↦ (𝑏(·𝑖‘𝐾)𝑎)) = (𝑏 ∈ 𝐵 ↦ (𝑏(·𝑖‘𝐿)𝑎))) |
15 | 1 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → 𝐵 = (Base‘𝐾)) |
16 | 15 | mpteq1d 5170 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → (𝑏 ∈ 𝐵 ↦ (𝑏(·𝑖‘𝐾)𝑎)) = (𝑏 ∈ (Base‘𝐾) ↦ (𝑏(·𝑖‘𝐾)𝑎))) |
17 | 2 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → 𝐵 = (Base‘𝐿)) |
18 | 17 | mpteq1d 5170 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → (𝑏 ∈ 𝐵 ↦ (𝑏(·𝑖‘𝐿)𝑎)) = (𝑏 ∈ (Base‘𝐿) ↦ (𝑏(·𝑖‘𝐿)𝑎))) |
19 | 14, 16, 18 | 3eqtr3d 2786 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → (𝑏 ∈ (Base‘𝐾) ↦ (𝑏(·𝑖‘𝐾)𝑎)) = (𝑏 ∈ (Base‘𝐿) ↦ (𝑏(·𝑖‘𝐿)𝑎))) |
20 | | rlmbas 20454 |
. . . . . . . . . . . 12
⊢
(Base‘𝐹) =
(Base‘(ringLMod‘𝐹)) |
21 | 6, 20 | eqtri 2766 |
. . . . . . . . . . 11
⊢ 𝑃 =
(Base‘(ringLMod‘𝐹)) |
22 | 21 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑃 = (Base‘(ringLMod‘𝐹))) |
23 | | fvex 6781 |
. . . . . . . . . . . 12
⊢
(Scalar‘𝐾)
∈ V |
24 | 4, 23 | eqeltrdi 2847 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹 ∈ V) |
25 | | rlmsca 20459 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ V → 𝐹 =
(Scalar‘(ringLMod‘𝐹))) |
26 | 24, 25 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹 = (Scalar‘(ringLMod‘𝐹))) |
27 | | eqidd 2739 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃)) → (𝑥(+g‘(ringLMod‘𝐹))𝑦) = (𝑥(+g‘(ringLMod‘𝐹))𝑦)) |
28 | | eqidd 2739 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃)) → (𝑥( ·𝑠
‘(ringLMod‘𝐹))𝑦) = (𝑥( ·𝑠
‘(ringLMod‘𝐹))𝑦)) |
29 | 1, 22, 2, 22, 4, 26, 5, 26, 6, 6, 3, 27,
7, 28 | lmhmpropd 20324 |
. . . . . . . . 9
⊢ (𝜑 → (𝐾 LMHom (ringLMod‘𝐹)) = (𝐿 LMHom (ringLMod‘𝐹))) |
30 | 4 | fveq2d 6772 |
. . . . . . . . . 10
⊢ (𝜑 → (ringLMod‘𝐹) =
(ringLMod‘(Scalar‘𝐾))) |
31 | 30 | oveq2d 7285 |
. . . . . . . . 9
⊢ (𝜑 → (𝐾 LMHom (ringLMod‘𝐹)) = (𝐾 LMHom (ringLMod‘(Scalar‘𝐾)))) |
32 | 5 | fveq2d 6772 |
. . . . . . . . . 10
⊢ (𝜑 → (ringLMod‘𝐹) =
(ringLMod‘(Scalar‘𝐿))) |
33 | 32 | oveq2d 7285 |
. . . . . . . . 9
⊢ (𝜑 → (𝐿 LMHom (ringLMod‘𝐹)) = (𝐿 LMHom (ringLMod‘(Scalar‘𝐿)))) |
34 | 29, 31, 33 | 3eqtr3d 2786 |
. . . . . . . 8
⊢ (𝜑 → (𝐾 LMHom (ringLMod‘(Scalar‘𝐾))) = (𝐿 LMHom (ringLMod‘(Scalar‘𝐿)))) |
35 | 34 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → (𝐾 LMHom (ringLMod‘(Scalar‘𝐾))) = (𝐿 LMHom (ringLMod‘(Scalar‘𝐿)))) |
36 | 19, 35 | eleq12d 2833 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → ((𝑏 ∈ (Base‘𝐾) ↦ (𝑏(·𝑖‘𝐾)𝑎)) ∈ (𝐾 LMHom (ringLMod‘(Scalar‘𝐾))) ↔ (𝑏 ∈ (Base‘𝐿) ↦ (𝑏(·𝑖‘𝐿)𝑎)) ∈ (𝐿 LMHom (ringLMod‘(Scalar‘𝐿))))) |
37 | 11 | oveqrspc2v 7296 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵)) → (𝑎(·𝑖‘𝐾)𝑎) = (𝑎(·𝑖‘𝐿)𝑎)) |
38 | 37 | anabsan2 671 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → (𝑎(·𝑖‘𝐾)𝑎) = (𝑎(·𝑖‘𝐿)𝑎)) |
39 | 9 | fveq2d 6772 |
. . . . . . . . 9
⊢ (𝜑 →
(0g‘(Scalar‘𝐾)) =
(0g‘(Scalar‘𝐿))) |
40 | 39 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) →
(0g‘(Scalar‘𝐾)) =
(0g‘(Scalar‘𝐿))) |
41 | 38, 40 | eqeq12d 2754 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → ((𝑎(·𝑖‘𝐾)𝑎) = (0g‘(Scalar‘𝐾)) ↔ (𝑎(·𝑖‘𝐿)𝑎) = (0g‘(Scalar‘𝐿)))) |
42 | 1, 2, 3 | grpidpropd 18335 |
. . . . . . . . 9
⊢ (𝜑 → (0g‘𝐾) = (0g‘𝐿)) |
43 | 42 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → (0g‘𝐾) = (0g‘𝐿)) |
44 | 43 | eqeq2d 2749 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → (𝑎 = (0g‘𝐾) ↔ 𝑎 = (0g‘𝐿))) |
45 | 41, 44 | imbi12d 345 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → (((𝑎(·𝑖‘𝐾)𝑎) = (0g‘(Scalar‘𝐾)) → 𝑎 = (0g‘𝐾)) ↔ ((𝑎(·𝑖‘𝐿)𝑎) = (0g‘(Scalar‘𝐿)) → 𝑎 = (0g‘𝐿)))) |
46 | 9 | fveq2d 6772 |
. . . . . . . . . . . 12
⊢ (𝜑 →
(*𝑟‘(Scalar‘𝐾)) =
(*𝑟‘(Scalar‘𝐿))) |
47 | 46 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) →
(*𝑟‘(Scalar‘𝐾)) =
(*𝑟‘(Scalar‘𝐿))) |
48 | 11 | oveqrspc2v 7296 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝑎(·𝑖‘𝐾)𝑏) = (𝑎(·𝑖‘𝐿)𝑏)) |
49 | 47, 48 | fveq12d 6775 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) →
((*𝑟‘(Scalar‘𝐾))‘(𝑎(·𝑖‘𝐾)𝑏)) =
((*𝑟‘(Scalar‘𝐿))‘(𝑎(·𝑖‘𝐿)𝑏))) |
50 | 49 | anassrs 468 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) →
((*𝑟‘(Scalar‘𝐾))‘(𝑎(·𝑖‘𝐾)𝑏)) =
((*𝑟‘(Scalar‘𝐿))‘(𝑎(·𝑖‘𝐿)𝑏))) |
51 | 50, 13 | eqeq12d 2754 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) →
(((*𝑟‘(Scalar‘𝐾))‘(𝑎(·𝑖‘𝐾)𝑏)) = (𝑏(·𝑖‘𝐾)𝑎) ↔
((*𝑟‘(Scalar‘𝐿))‘(𝑎(·𝑖‘𝐿)𝑏)) = (𝑏(·𝑖‘𝐿)𝑎))) |
52 | 51 | ralbidva 3117 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → (∀𝑏 ∈ 𝐵
((*𝑟‘(Scalar‘𝐾))‘(𝑎(·𝑖‘𝐾)𝑏)) = (𝑏(·𝑖‘𝐾)𝑎) ↔ ∀𝑏 ∈ 𝐵
((*𝑟‘(Scalar‘𝐿))‘(𝑎(·𝑖‘𝐿)𝑏)) = (𝑏(·𝑖‘𝐿)𝑎))) |
53 | 15 | raleqdv 3347 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → (∀𝑏 ∈ 𝐵
((*𝑟‘(Scalar‘𝐾))‘(𝑎(·𝑖‘𝐾)𝑏)) = (𝑏(·𝑖‘𝐾)𝑎) ↔ ∀𝑏 ∈ (Base‘𝐾)((*𝑟‘(Scalar‘𝐾))‘(𝑎(·𝑖‘𝐾)𝑏)) = (𝑏(·𝑖‘𝐾)𝑎))) |
54 | 17 | raleqdv 3347 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → (∀𝑏 ∈ 𝐵
((*𝑟‘(Scalar‘𝐿))‘(𝑎(·𝑖‘𝐿)𝑏)) = (𝑏(·𝑖‘𝐿)𝑎) ↔ ∀𝑏 ∈ (Base‘𝐿)((*𝑟‘(Scalar‘𝐿))‘(𝑎(·𝑖‘𝐿)𝑏)) = (𝑏(·𝑖‘𝐿)𝑎))) |
55 | 52, 53, 54 | 3bitr3d 309 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → (∀𝑏 ∈ (Base‘𝐾)((*𝑟‘(Scalar‘𝐾))‘(𝑎(·𝑖‘𝐾)𝑏)) = (𝑏(·𝑖‘𝐾)𝑎) ↔ ∀𝑏 ∈ (Base‘𝐿)((*𝑟‘(Scalar‘𝐿))‘(𝑎(·𝑖‘𝐿)𝑏)) = (𝑏(·𝑖‘𝐿)𝑎))) |
56 | 36, 45, 55 | 3anbi123d 1435 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → (((𝑏 ∈ (Base‘𝐾) ↦ (𝑏(·𝑖‘𝐾)𝑎)) ∈ (𝐾 LMHom (ringLMod‘(Scalar‘𝐾))) ∧ ((𝑎(·𝑖‘𝐾)𝑎) = (0g‘(Scalar‘𝐾)) → 𝑎 = (0g‘𝐾)) ∧ ∀𝑏 ∈ (Base‘𝐾)((*𝑟‘(Scalar‘𝐾))‘(𝑎(·𝑖‘𝐾)𝑏)) = (𝑏(·𝑖‘𝐾)𝑎)) ↔ ((𝑏 ∈ (Base‘𝐿) ↦ (𝑏(·𝑖‘𝐿)𝑎)) ∈ (𝐿 LMHom (ringLMod‘(Scalar‘𝐿))) ∧ ((𝑎(·𝑖‘𝐿)𝑎) = (0g‘(Scalar‘𝐿)) → 𝑎 = (0g‘𝐿)) ∧ ∀𝑏 ∈ (Base‘𝐿)((*𝑟‘(Scalar‘𝐿))‘(𝑎(·𝑖‘𝐿)𝑏)) = (𝑏(·𝑖‘𝐿)𝑎)))) |
57 | 56 | ralbidva 3117 |
. . . 4
⊢ (𝜑 → (∀𝑎 ∈ 𝐵 ((𝑏 ∈ (Base‘𝐾) ↦ (𝑏(·𝑖‘𝐾)𝑎)) ∈ (𝐾 LMHom (ringLMod‘(Scalar‘𝐾))) ∧ ((𝑎(·𝑖‘𝐾)𝑎) = (0g‘(Scalar‘𝐾)) → 𝑎 = (0g‘𝐾)) ∧ ∀𝑏 ∈ (Base‘𝐾)((*𝑟‘(Scalar‘𝐾))‘(𝑎(·𝑖‘𝐾)𝑏)) = (𝑏(·𝑖‘𝐾)𝑎)) ↔ ∀𝑎 ∈ 𝐵 ((𝑏 ∈ (Base‘𝐿) ↦ (𝑏(·𝑖‘𝐿)𝑎)) ∈ (𝐿 LMHom (ringLMod‘(Scalar‘𝐿))) ∧ ((𝑎(·𝑖‘𝐿)𝑎) = (0g‘(Scalar‘𝐿)) → 𝑎 = (0g‘𝐿)) ∧ ∀𝑏 ∈ (Base‘𝐿)((*𝑟‘(Scalar‘𝐿))‘(𝑎(·𝑖‘𝐿)𝑏)) = (𝑏(·𝑖‘𝐿)𝑎)))) |
58 | 1 | raleqdv 3347 |
. . . 4
⊢ (𝜑 → (∀𝑎 ∈ 𝐵 ((𝑏 ∈ (Base‘𝐾) ↦ (𝑏(·𝑖‘𝐾)𝑎)) ∈ (𝐾 LMHom (ringLMod‘(Scalar‘𝐾))) ∧ ((𝑎(·𝑖‘𝐾)𝑎) = (0g‘(Scalar‘𝐾)) → 𝑎 = (0g‘𝐾)) ∧ ∀𝑏 ∈ (Base‘𝐾)((*𝑟‘(Scalar‘𝐾))‘(𝑎(·𝑖‘𝐾)𝑏)) = (𝑏(·𝑖‘𝐾)𝑎)) ↔ ∀𝑎 ∈ (Base‘𝐾)((𝑏 ∈ (Base‘𝐾) ↦ (𝑏(·𝑖‘𝐾)𝑎)) ∈ (𝐾 LMHom (ringLMod‘(Scalar‘𝐾))) ∧ ((𝑎(·𝑖‘𝐾)𝑎) = (0g‘(Scalar‘𝐾)) → 𝑎 = (0g‘𝐾)) ∧ ∀𝑏 ∈ (Base‘𝐾)((*𝑟‘(Scalar‘𝐾))‘(𝑎(·𝑖‘𝐾)𝑏)) = (𝑏(·𝑖‘𝐾)𝑎)))) |
59 | 2 | raleqdv 3347 |
. . . 4
⊢ (𝜑 → (∀𝑎 ∈ 𝐵 ((𝑏 ∈ (Base‘𝐿) ↦ (𝑏(·𝑖‘𝐿)𝑎)) ∈ (𝐿 LMHom (ringLMod‘(Scalar‘𝐿))) ∧ ((𝑎(·𝑖‘𝐿)𝑎) = (0g‘(Scalar‘𝐿)) → 𝑎 = (0g‘𝐿)) ∧ ∀𝑏 ∈ (Base‘𝐿)((*𝑟‘(Scalar‘𝐿))‘(𝑎(·𝑖‘𝐿)𝑏)) = (𝑏(·𝑖‘𝐿)𝑎)) ↔ ∀𝑎 ∈ (Base‘𝐿)((𝑏 ∈ (Base‘𝐿) ↦ (𝑏(·𝑖‘𝐿)𝑎)) ∈ (𝐿 LMHom (ringLMod‘(Scalar‘𝐿))) ∧ ((𝑎(·𝑖‘𝐿)𝑎) = (0g‘(Scalar‘𝐿)) → 𝑎 = (0g‘𝐿)) ∧ ∀𝑏 ∈ (Base‘𝐿)((*𝑟‘(Scalar‘𝐿))‘(𝑎(·𝑖‘𝐿)𝑏)) = (𝑏(·𝑖‘𝐿)𝑎)))) |
60 | 57, 58, 59 | 3bitr3d 309 |
. . 3
⊢ (𝜑 → (∀𝑎 ∈ (Base‘𝐾)((𝑏 ∈ (Base‘𝐾) ↦ (𝑏(·𝑖‘𝐾)𝑎)) ∈ (𝐾 LMHom (ringLMod‘(Scalar‘𝐾))) ∧ ((𝑎(·𝑖‘𝐾)𝑎) = (0g‘(Scalar‘𝐾)) → 𝑎 = (0g‘𝐾)) ∧ ∀𝑏 ∈ (Base‘𝐾)((*𝑟‘(Scalar‘𝐾))‘(𝑎(·𝑖‘𝐾)𝑏)) = (𝑏(·𝑖‘𝐾)𝑎)) ↔ ∀𝑎 ∈ (Base‘𝐿)((𝑏 ∈ (Base‘𝐿) ↦ (𝑏(·𝑖‘𝐿)𝑎)) ∈ (𝐿 LMHom (ringLMod‘(Scalar‘𝐿))) ∧ ((𝑎(·𝑖‘𝐿)𝑎) = (0g‘(Scalar‘𝐿)) → 𝑎 = (0g‘𝐿)) ∧ ∀𝑏 ∈ (Base‘𝐿)((*𝑟‘(Scalar‘𝐿))‘(𝑎(·𝑖‘𝐿)𝑏)) = (𝑏(·𝑖‘𝐿)𝑎)))) |
61 | 8, 10, 60 | 3anbi123d 1435 |
. 2
⊢ (𝜑 → ((𝐾 ∈ LVec ∧ (Scalar‘𝐾) ∈ *-Ring ∧
∀𝑎 ∈
(Base‘𝐾)((𝑏 ∈ (Base‘𝐾) ↦ (𝑏(·𝑖‘𝐾)𝑎)) ∈ (𝐾 LMHom (ringLMod‘(Scalar‘𝐾))) ∧ ((𝑎(·𝑖‘𝐾)𝑎) = (0g‘(Scalar‘𝐾)) → 𝑎 = (0g‘𝐾)) ∧ ∀𝑏 ∈ (Base‘𝐾)((*𝑟‘(Scalar‘𝐾))‘(𝑎(·𝑖‘𝐾)𝑏)) = (𝑏(·𝑖‘𝐾)𝑎))) ↔ (𝐿 ∈ LVec ∧ (Scalar‘𝐿) ∈ *-Ring ∧ ∀𝑎 ∈ (Base‘𝐿)((𝑏 ∈ (Base‘𝐿) ↦ (𝑏(·𝑖‘𝐿)𝑎)) ∈ (𝐿 LMHom (ringLMod‘(Scalar‘𝐿))) ∧ ((𝑎(·𝑖‘𝐿)𝑎) = (0g‘(Scalar‘𝐿)) → 𝑎 = (0g‘𝐿)) ∧ ∀𝑏 ∈ (Base‘𝐿)((*𝑟‘(Scalar‘𝐿))‘(𝑎(·𝑖‘𝐿)𝑏)) = (𝑏(·𝑖‘𝐿)𝑎))))) |
62 | | eqid 2738 |
. . 3
⊢
(Base‘𝐾) =
(Base‘𝐾) |
63 | | eqid 2738 |
. . 3
⊢
(Scalar‘𝐾) =
(Scalar‘𝐾) |
64 | | eqid 2738 |
. . 3
⊢
(·𝑖‘𝐾) =
(·𝑖‘𝐾) |
65 | | eqid 2738 |
. . 3
⊢
(0g‘𝐾) = (0g‘𝐾) |
66 | | eqid 2738 |
. . 3
⊢
(*𝑟‘(Scalar‘𝐾)) =
(*𝑟‘(Scalar‘𝐾)) |
67 | | eqid 2738 |
. . 3
⊢
(0g‘(Scalar‘𝐾)) =
(0g‘(Scalar‘𝐾)) |
68 | 62, 63, 64, 65, 66, 67 | isphl 20822 |
. 2
⊢ (𝐾 ∈ PreHil ↔ (𝐾 ∈ LVec ∧
(Scalar‘𝐾) ∈
*-Ring ∧ ∀𝑎
∈ (Base‘𝐾)((𝑏 ∈ (Base‘𝐾) ↦ (𝑏(·𝑖‘𝐾)𝑎)) ∈ (𝐾 LMHom (ringLMod‘(Scalar‘𝐾))) ∧ ((𝑎(·𝑖‘𝐾)𝑎) = (0g‘(Scalar‘𝐾)) → 𝑎 = (0g‘𝐾)) ∧ ∀𝑏 ∈ (Base‘𝐾)((*𝑟‘(Scalar‘𝐾))‘(𝑎(·𝑖‘𝐾)𝑏)) = (𝑏(·𝑖‘𝐾)𝑎)))) |
69 | | eqid 2738 |
. . 3
⊢
(Base‘𝐿) =
(Base‘𝐿) |
70 | | eqid 2738 |
. . 3
⊢
(Scalar‘𝐿) =
(Scalar‘𝐿) |
71 | | eqid 2738 |
. . 3
⊢
(·𝑖‘𝐿) =
(·𝑖‘𝐿) |
72 | | eqid 2738 |
. . 3
⊢
(0g‘𝐿) = (0g‘𝐿) |
73 | | eqid 2738 |
. . 3
⊢
(*𝑟‘(Scalar‘𝐿)) =
(*𝑟‘(Scalar‘𝐿)) |
74 | | eqid 2738 |
. . 3
⊢
(0g‘(Scalar‘𝐿)) =
(0g‘(Scalar‘𝐿)) |
75 | 69, 70, 71, 72, 73, 74 | isphl 20822 |
. 2
⊢ (𝐿 ∈ PreHil ↔ (𝐿 ∈ LVec ∧
(Scalar‘𝐿) ∈
*-Ring ∧ ∀𝑎
∈ (Base‘𝐿)((𝑏 ∈ (Base‘𝐿) ↦ (𝑏(·𝑖‘𝐿)𝑎)) ∈ (𝐿 LMHom (ringLMod‘(Scalar‘𝐿))) ∧ ((𝑎(·𝑖‘𝐿)𝑎) = (0g‘(Scalar‘𝐿)) → 𝑎 = (0g‘𝐿)) ∧ ∀𝑏 ∈ (Base‘𝐿)((*𝑟‘(Scalar‘𝐿))‘(𝑎(·𝑖‘𝐿)𝑏)) = (𝑏(·𝑖‘𝐿)𝑎)))) |
76 | 61, 68, 75 | 3bitr4g 314 |
1
⊢ (𝜑 → (𝐾 ∈ PreHil ↔ 𝐿 ∈ PreHil)) |