| 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 21169 |
. . 3
⊢ (𝜑 → (𝐾 ∈ LVec ↔ 𝐿 ∈ LVec)) |
| 9 | 4, 5 | eqtr3d 2779 |
. . . 4
⊢ (𝜑 → (Scalar‘𝐾) = (Scalar‘𝐿)) |
| 10 | 9 | eleq1d 2826 |
. . 3
⊢ (𝜑 → ((Scalar‘𝐾) ∈ *-Ring ↔
(Scalar‘𝐿) ∈
*-Ring)) |
| 11 | | phlpropd.8 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(·𝑖‘𝐾)𝑦) = (𝑥(·𝑖‘𝐿)𝑦)) |
| 12 | 11 | oveqrspc2v 7458 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵)) → (𝑏(·𝑖‘𝐾)𝑎) = (𝑏(·𝑖‘𝐿)𝑎)) |
| 13 | 12 | anass1rs 655 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) → (𝑏(·𝑖‘𝐾)𝑎) = (𝑏(·𝑖‘𝐿)𝑎)) |
| 14 | 13 | mpteq2dva 5242 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → (𝑏 ∈ 𝐵 ↦ (𝑏(·𝑖‘𝐾)𝑎)) = (𝑏 ∈ 𝐵 ↦ (𝑏(·𝑖‘𝐿)𝑎))) |
| 15 | 1 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → 𝐵 = (Base‘𝐾)) |
| 16 | 15 | mpteq1d 5237 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → (𝑏 ∈ 𝐵 ↦ (𝑏(·𝑖‘𝐾)𝑎)) = (𝑏 ∈ (Base‘𝐾) ↦ (𝑏(·𝑖‘𝐾)𝑎))) |
| 17 | 2 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → 𝐵 = (Base‘𝐿)) |
| 18 | 17 | mpteq1d 5237 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → (𝑏 ∈ 𝐵 ↦ (𝑏(·𝑖‘𝐿)𝑎)) = (𝑏 ∈ (Base‘𝐿) ↦ (𝑏(·𝑖‘𝐿)𝑎))) |
| 19 | 14, 16, 18 | 3eqtr3d 2785 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → (𝑏 ∈ (Base‘𝐾) ↦ (𝑏(·𝑖‘𝐾)𝑎)) = (𝑏 ∈ (Base‘𝐿) ↦ (𝑏(·𝑖‘𝐿)𝑎))) |
| 20 | | rlmbas 21200 |
. . . . . . . . . . . 12
⊢
(Base‘𝐹) =
(Base‘(ringLMod‘𝐹)) |
| 21 | 6, 20 | eqtri 2765 |
. . . . . . . . . . 11
⊢ 𝑃 =
(Base‘(ringLMod‘𝐹)) |
| 22 | 21 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑃 = (Base‘(ringLMod‘𝐹))) |
| 23 | | fvex 6919 |
. . . . . . . . . . . 12
⊢
(Scalar‘𝐾)
∈ V |
| 24 | 4, 23 | eqeltrdi 2849 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹 ∈ V) |
| 25 | | rlmsca 21205 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ V → 𝐹 =
(Scalar‘(ringLMod‘𝐹))) |
| 26 | 24, 25 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹 = (Scalar‘(ringLMod‘𝐹))) |
| 27 | | eqidd 2738 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃)) → (𝑥(+g‘(ringLMod‘𝐹))𝑦) = (𝑥(+g‘(ringLMod‘𝐹))𝑦)) |
| 28 | | eqidd 2738 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃)) → (𝑥( ·𝑠
‘(ringLMod‘𝐹))𝑦) = (𝑥( ·𝑠
‘(ringLMod‘𝐹))𝑦)) |
| 29 | 1, 22, 2, 22, 4, 26, 5, 26, 6, 6, 3, 27,
7, 28 | lmhmpropd 21072 |
. . . . . . . . 9
⊢ (𝜑 → (𝐾 LMHom (ringLMod‘𝐹)) = (𝐿 LMHom (ringLMod‘𝐹))) |
| 30 | 4 | fveq2d 6910 |
. . . . . . . . . 10
⊢ (𝜑 → (ringLMod‘𝐹) =
(ringLMod‘(Scalar‘𝐾))) |
| 31 | 30 | oveq2d 7447 |
. . . . . . . . 9
⊢ (𝜑 → (𝐾 LMHom (ringLMod‘𝐹)) = (𝐾 LMHom (ringLMod‘(Scalar‘𝐾)))) |
| 32 | 5 | fveq2d 6910 |
. . . . . . . . . 10
⊢ (𝜑 → (ringLMod‘𝐹) =
(ringLMod‘(Scalar‘𝐿))) |
| 33 | 32 | oveq2d 7447 |
. . . . . . . . 9
⊢ (𝜑 → (𝐿 LMHom (ringLMod‘𝐹)) = (𝐿 LMHom (ringLMod‘(Scalar‘𝐿)))) |
| 34 | 29, 31, 33 | 3eqtr3d 2785 |
. . . . . . . 8
⊢ (𝜑 → (𝐾 LMHom (ringLMod‘(Scalar‘𝐾))) = (𝐿 LMHom (ringLMod‘(Scalar‘𝐿)))) |
| 35 | 34 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → (𝐾 LMHom (ringLMod‘(Scalar‘𝐾))) = (𝐿 LMHom (ringLMod‘(Scalar‘𝐿)))) |
| 36 | 19, 35 | eleq12d 2835 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → ((𝑏 ∈ (Base‘𝐾) ↦ (𝑏(·𝑖‘𝐾)𝑎)) ∈ (𝐾 LMHom (ringLMod‘(Scalar‘𝐾))) ↔ (𝑏 ∈ (Base‘𝐿) ↦ (𝑏(·𝑖‘𝐿)𝑎)) ∈ (𝐿 LMHom (ringLMod‘(Scalar‘𝐿))))) |
| 37 | 11 | oveqrspc2v 7458 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵)) → (𝑎(·𝑖‘𝐾)𝑎) = (𝑎(·𝑖‘𝐿)𝑎)) |
| 38 | 37 | anabsan2 674 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → (𝑎(·𝑖‘𝐾)𝑎) = (𝑎(·𝑖‘𝐿)𝑎)) |
| 39 | 9 | fveq2d 6910 |
. . . . . . . . 9
⊢ (𝜑 →
(0g‘(Scalar‘𝐾)) =
(0g‘(Scalar‘𝐿))) |
| 40 | 39 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) →
(0g‘(Scalar‘𝐾)) =
(0g‘(Scalar‘𝐿))) |
| 41 | 38, 40 | eqeq12d 2753 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → ((𝑎(·𝑖‘𝐾)𝑎) = (0g‘(Scalar‘𝐾)) ↔ (𝑎(·𝑖‘𝐿)𝑎) = (0g‘(Scalar‘𝐿)))) |
| 42 | 1, 2, 3 | grpidpropd 18675 |
. . . . . . . . 9
⊢ (𝜑 → (0g‘𝐾) = (0g‘𝐿)) |
| 43 | 42 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → (0g‘𝐾) = (0g‘𝐿)) |
| 44 | 43 | eqeq2d 2748 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → (𝑎 = (0g‘𝐾) ↔ 𝑎 = (0g‘𝐿))) |
| 45 | 41, 44 | imbi12d 344 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → (((𝑎(·𝑖‘𝐾)𝑎) = (0g‘(Scalar‘𝐾)) → 𝑎 = (0g‘𝐾)) ↔ ((𝑎(·𝑖‘𝐿)𝑎) = (0g‘(Scalar‘𝐿)) → 𝑎 = (0g‘𝐿)))) |
| 46 | 9 | fveq2d 6910 |
. . . . . . . . . . . 12
⊢ (𝜑 →
(*𝑟‘(Scalar‘𝐾)) =
(*𝑟‘(Scalar‘𝐿))) |
| 47 | 46 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) →
(*𝑟‘(Scalar‘𝐾)) =
(*𝑟‘(Scalar‘𝐿))) |
| 48 | 11 | oveqrspc2v 7458 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝑎(·𝑖‘𝐾)𝑏) = (𝑎(·𝑖‘𝐿)𝑏)) |
| 49 | 47, 48 | fveq12d 6913 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) →
((*𝑟‘(Scalar‘𝐾))‘(𝑎(·𝑖‘𝐾)𝑏)) =
((*𝑟‘(Scalar‘𝐿))‘(𝑎(·𝑖‘𝐿)𝑏))) |
| 50 | 49 | anassrs 467 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) →
((*𝑟‘(Scalar‘𝐾))‘(𝑎(·𝑖‘𝐾)𝑏)) =
((*𝑟‘(Scalar‘𝐿))‘(𝑎(·𝑖‘𝐿)𝑏))) |
| 51 | 50, 13 | eqeq12d 2753 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) →
(((*𝑟‘(Scalar‘𝐾))‘(𝑎(·𝑖‘𝐾)𝑏)) = (𝑏(·𝑖‘𝐾)𝑎) ↔
((*𝑟‘(Scalar‘𝐿))‘(𝑎(·𝑖‘𝐿)𝑏)) = (𝑏(·𝑖‘𝐿)𝑎))) |
| 52 | 51 | ralbidva 3176 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → (∀𝑏 ∈ 𝐵
((*𝑟‘(Scalar‘𝐾))‘(𝑎(·𝑖‘𝐾)𝑏)) = (𝑏(·𝑖‘𝐾)𝑎) ↔ ∀𝑏 ∈ 𝐵
((*𝑟‘(Scalar‘𝐿))‘(𝑎(·𝑖‘𝐿)𝑏)) = (𝑏(·𝑖‘𝐿)𝑎))) |
| 53 | 15 | raleqdv 3326 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → (∀𝑏 ∈ 𝐵
((*𝑟‘(Scalar‘𝐾))‘(𝑎(·𝑖‘𝐾)𝑏)) = (𝑏(·𝑖‘𝐾)𝑎) ↔ ∀𝑏 ∈ (Base‘𝐾)((*𝑟‘(Scalar‘𝐾))‘(𝑎(·𝑖‘𝐾)𝑏)) = (𝑏(·𝑖‘𝐾)𝑎))) |
| 54 | 17 | raleqdv 3326 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → (∀𝑏 ∈ 𝐵
((*𝑟‘(Scalar‘𝐿))‘(𝑎(·𝑖‘𝐿)𝑏)) = (𝑏(·𝑖‘𝐿)𝑎) ↔ ∀𝑏 ∈ (Base‘𝐿)((*𝑟‘(Scalar‘𝐿))‘(𝑎(·𝑖‘𝐿)𝑏)) = (𝑏(·𝑖‘𝐿)𝑎))) |
| 55 | 52, 53, 54 | 3bitr3d 309 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → (∀𝑏 ∈ (Base‘𝐾)((*𝑟‘(Scalar‘𝐾))‘(𝑎(·𝑖‘𝐾)𝑏)) = (𝑏(·𝑖‘𝐾)𝑎) ↔ ∀𝑏 ∈ (Base‘𝐿)((*𝑟‘(Scalar‘𝐿))‘(𝑎(·𝑖‘𝐿)𝑏)) = (𝑏(·𝑖‘𝐿)𝑎))) |
| 56 | 36, 45, 55 | 3anbi123d 1438 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → (((𝑏 ∈ (Base‘𝐾) ↦ (𝑏(·𝑖‘𝐾)𝑎)) ∈ (𝐾 LMHom (ringLMod‘(Scalar‘𝐾))) ∧ ((𝑎(·𝑖‘𝐾)𝑎) = (0g‘(Scalar‘𝐾)) → 𝑎 = (0g‘𝐾)) ∧ ∀𝑏 ∈ (Base‘𝐾)((*𝑟‘(Scalar‘𝐾))‘(𝑎(·𝑖‘𝐾)𝑏)) = (𝑏(·𝑖‘𝐾)𝑎)) ↔ ((𝑏 ∈ (Base‘𝐿) ↦ (𝑏(·𝑖‘𝐿)𝑎)) ∈ (𝐿 LMHom (ringLMod‘(Scalar‘𝐿))) ∧ ((𝑎(·𝑖‘𝐿)𝑎) = (0g‘(Scalar‘𝐿)) → 𝑎 = (0g‘𝐿)) ∧ ∀𝑏 ∈ (Base‘𝐿)((*𝑟‘(Scalar‘𝐿))‘(𝑎(·𝑖‘𝐿)𝑏)) = (𝑏(·𝑖‘𝐿)𝑎)))) |
| 57 | 56 | ralbidva 3176 |
. . . 4
⊢ (𝜑 → (∀𝑎 ∈ 𝐵 ((𝑏 ∈ (Base‘𝐾) ↦ (𝑏(·𝑖‘𝐾)𝑎)) ∈ (𝐾 LMHom (ringLMod‘(Scalar‘𝐾))) ∧ ((𝑎(·𝑖‘𝐾)𝑎) = (0g‘(Scalar‘𝐾)) → 𝑎 = (0g‘𝐾)) ∧ ∀𝑏 ∈ (Base‘𝐾)((*𝑟‘(Scalar‘𝐾))‘(𝑎(·𝑖‘𝐾)𝑏)) = (𝑏(·𝑖‘𝐾)𝑎)) ↔ ∀𝑎 ∈ 𝐵 ((𝑏 ∈ (Base‘𝐿) ↦ (𝑏(·𝑖‘𝐿)𝑎)) ∈ (𝐿 LMHom (ringLMod‘(Scalar‘𝐿))) ∧ ((𝑎(·𝑖‘𝐿)𝑎) = (0g‘(Scalar‘𝐿)) → 𝑎 = (0g‘𝐿)) ∧ ∀𝑏 ∈ (Base‘𝐿)((*𝑟‘(Scalar‘𝐿))‘(𝑎(·𝑖‘𝐿)𝑏)) = (𝑏(·𝑖‘𝐿)𝑎)))) |
| 58 | 1 | raleqdv 3326 |
. . . 4
⊢ (𝜑 → (∀𝑎 ∈ 𝐵 ((𝑏 ∈ (Base‘𝐾) ↦ (𝑏(·𝑖‘𝐾)𝑎)) ∈ (𝐾 LMHom (ringLMod‘(Scalar‘𝐾))) ∧ ((𝑎(·𝑖‘𝐾)𝑎) = (0g‘(Scalar‘𝐾)) → 𝑎 = (0g‘𝐾)) ∧ ∀𝑏 ∈ (Base‘𝐾)((*𝑟‘(Scalar‘𝐾))‘(𝑎(·𝑖‘𝐾)𝑏)) = (𝑏(·𝑖‘𝐾)𝑎)) ↔ ∀𝑎 ∈ (Base‘𝐾)((𝑏 ∈ (Base‘𝐾) ↦ (𝑏(·𝑖‘𝐾)𝑎)) ∈ (𝐾 LMHom (ringLMod‘(Scalar‘𝐾))) ∧ ((𝑎(·𝑖‘𝐾)𝑎) = (0g‘(Scalar‘𝐾)) → 𝑎 = (0g‘𝐾)) ∧ ∀𝑏 ∈ (Base‘𝐾)((*𝑟‘(Scalar‘𝐾))‘(𝑎(·𝑖‘𝐾)𝑏)) = (𝑏(·𝑖‘𝐾)𝑎)))) |
| 59 | 2 | raleqdv 3326 |
. . . 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 1438 |
. 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 2737 |
. . 3
⊢
(Base‘𝐾) =
(Base‘𝐾) |
| 63 | | eqid 2737 |
. . 3
⊢
(Scalar‘𝐾) =
(Scalar‘𝐾) |
| 64 | | eqid 2737 |
. . 3
⊢
(·𝑖‘𝐾) =
(·𝑖‘𝐾) |
| 65 | | eqid 2737 |
. . 3
⊢
(0g‘𝐾) = (0g‘𝐾) |
| 66 | | eqid 2737 |
. . 3
⊢
(*𝑟‘(Scalar‘𝐾)) =
(*𝑟‘(Scalar‘𝐾)) |
| 67 | | eqid 2737 |
. . 3
⊢
(0g‘(Scalar‘𝐾)) =
(0g‘(Scalar‘𝐾)) |
| 68 | 62, 63, 64, 65, 66, 67 | isphl 21646 |
. 2
⊢ (𝐾 ∈ PreHil ↔ (𝐾 ∈ LVec ∧
(Scalar‘𝐾) ∈
*-Ring ∧ ∀𝑎
∈ (Base‘𝐾)((𝑏 ∈ (Base‘𝐾) ↦ (𝑏(·𝑖‘𝐾)𝑎)) ∈ (𝐾 LMHom (ringLMod‘(Scalar‘𝐾))) ∧ ((𝑎(·𝑖‘𝐾)𝑎) = (0g‘(Scalar‘𝐾)) → 𝑎 = (0g‘𝐾)) ∧ ∀𝑏 ∈ (Base‘𝐾)((*𝑟‘(Scalar‘𝐾))‘(𝑎(·𝑖‘𝐾)𝑏)) = (𝑏(·𝑖‘𝐾)𝑎)))) |
| 69 | | eqid 2737 |
. . 3
⊢
(Base‘𝐿) =
(Base‘𝐿) |
| 70 | | eqid 2737 |
. . 3
⊢
(Scalar‘𝐿) =
(Scalar‘𝐿) |
| 71 | | eqid 2737 |
. . 3
⊢
(·𝑖‘𝐿) =
(·𝑖‘𝐿) |
| 72 | | eqid 2737 |
. . 3
⊢
(0g‘𝐿) = (0g‘𝐿) |
| 73 | | eqid 2737 |
. . 3
⊢
(*𝑟‘(Scalar‘𝐿)) =
(*𝑟‘(Scalar‘𝐿)) |
| 74 | | eqid 2737 |
. . 3
⊢
(0g‘(Scalar‘𝐿)) =
(0g‘(Scalar‘𝐿)) |
| 75 | 69, 70, 71, 72, 73, 74 | isphl 21646 |
. 2
⊢ (𝐿 ∈ PreHil ↔ (𝐿 ∈ LVec ∧
(Scalar‘𝐿) ∈
*-Ring ∧ ∀𝑎
∈ (Base‘𝐿)((𝑏 ∈ (Base‘𝐿) ↦ (𝑏(·𝑖‘𝐿)𝑎)) ∈ (𝐿 LMHom (ringLMod‘(Scalar‘𝐿))) ∧ ((𝑎(·𝑖‘𝐿)𝑎) = (0g‘(Scalar‘𝐿)) → 𝑎 = (0g‘𝐿)) ∧ ∀𝑏 ∈ (Base‘𝐿)((*𝑟‘(Scalar‘𝐿))‘(𝑎(·𝑖‘𝐿)𝑏)) = (𝑏(·𝑖‘𝐿)𝑎)))) |
| 76 | 61, 68, 75 | 3bitr4g 314 |
1
⊢ (𝜑 → (𝐾 ∈ PreHil ↔ 𝐿 ∈ PreHil)) |