| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | phllmhm.v | . . . . 5
⊢ 𝑉 = (Base‘𝑊) | 
| 2 |  | phlsrng.f | . . . . 5
⊢ 𝐹 = (Scalar‘𝑊) | 
| 3 |  | phllmhm.h | . . . . 5
⊢  , =
(·𝑖‘𝑊) | 
| 4 |  | eqid 2736 | . . . . 5
⊢
(0g‘𝑊) = (0g‘𝑊) | 
| 5 |  | eqid 2736 | . . . . 5
⊢
(*𝑟‘𝐹) = (*𝑟‘𝐹) | 
| 6 |  | eqid 2736 | . . . . 5
⊢
(0g‘𝐹) = (0g‘𝐹) | 
| 7 | 1, 2, 3, 4, 5, 6 | isphl 21647 | . . . 4
⊢ (𝑊 ∈ PreHil ↔ (𝑊 ∈ LVec ∧ 𝐹 ∈ *-Ring ∧
∀𝑦 ∈ 𝑉 ((𝑥 ∈ 𝑉 ↦ (𝑥 , 𝑦)) ∈ (𝑊 LMHom (ringLMod‘𝐹)) ∧ ((𝑦 , 𝑦) = (0g‘𝐹) → 𝑦 = (0g‘𝑊)) ∧ ∀𝑥 ∈ 𝑉 ((*𝑟‘𝐹)‘(𝑦 , 𝑥)) = (𝑥 , 𝑦)))) | 
| 8 | 7 | simp3bi 1147 | . . 3
⊢ (𝑊 ∈ PreHil →
∀𝑦 ∈ 𝑉 ((𝑥 ∈ 𝑉 ↦ (𝑥 , 𝑦)) ∈ (𝑊 LMHom (ringLMod‘𝐹)) ∧ ((𝑦 , 𝑦) = (0g‘𝐹) → 𝑦 = (0g‘𝑊)) ∧ ∀𝑥 ∈ 𝑉 ((*𝑟‘𝐹)‘(𝑦 , 𝑥)) = (𝑥 , 𝑦))) | 
| 9 |  | simp1 1136 | . . . 4
⊢ (((𝑥 ∈ 𝑉 ↦ (𝑥 , 𝑦)) ∈ (𝑊 LMHom (ringLMod‘𝐹)) ∧ ((𝑦 , 𝑦) = (0g‘𝐹) → 𝑦 = (0g‘𝑊)) ∧ ∀𝑥 ∈ 𝑉 ((*𝑟‘𝐹)‘(𝑦 , 𝑥)) = (𝑥 , 𝑦)) → (𝑥 ∈ 𝑉 ↦ (𝑥 , 𝑦)) ∈ (𝑊 LMHom (ringLMod‘𝐹))) | 
| 10 | 9 | ralimi 3082 | . . 3
⊢
(∀𝑦 ∈
𝑉 ((𝑥 ∈ 𝑉 ↦ (𝑥 , 𝑦)) ∈ (𝑊 LMHom (ringLMod‘𝐹)) ∧ ((𝑦 , 𝑦) = (0g‘𝐹) → 𝑦 = (0g‘𝑊)) ∧ ∀𝑥 ∈ 𝑉 ((*𝑟‘𝐹)‘(𝑦 , 𝑥)) = (𝑥 , 𝑦)) → ∀𝑦 ∈ 𝑉 (𝑥 ∈ 𝑉 ↦ (𝑥 , 𝑦)) ∈ (𝑊 LMHom (ringLMod‘𝐹))) | 
| 11 | 8, 10 | syl 17 | . 2
⊢ (𝑊 ∈ PreHil →
∀𝑦 ∈ 𝑉 (𝑥 ∈ 𝑉 ↦ (𝑥 , 𝑦)) ∈ (𝑊 LMHom (ringLMod‘𝐹))) | 
| 12 |  | oveq2 7440 | . . . . . 6
⊢ (𝑦 = 𝐴 → (𝑥 , 𝑦) = (𝑥 , 𝐴)) | 
| 13 | 12 | mpteq2dv 5243 | . . . . 5
⊢ (𝑦 = 𝐴 → (𝑥 ∈ 𝑉 ↦ (𝑥 , 𝑦)) = (𝑥 ∈ 𝑉 ↦ (𝑥 , 𝐴))) | 
| 14 |  | phllmhm.g | . . . . 5
⊢ 𝐺 = (𝑥 ∈ 𝑉 ↦ (𝑥 , 𝐴)) | 
| 15 | 13, 14 | eqtr4di 2794 | . . . 4
⊢ (𝑦 = 𝐴 → (𝑥 ∈ 𝑉 ↦ (𝑥 , 𝑦)) = 𝐺) | 
| 16 | 15 | eleq1d 2825 | . . 3
⊢ (𝑦 = 𝐴 → ((𝑥 ∈ 𝑉 ↦ (𝑥 , 𝑦)) ∈ (𝑊 LMHom (ringLMod‘𝐹)) ↔ 𝐺 ∈ (𝑊 LMHom (ringLMod‘𝐹)))) | 
| 17 | 16 | rspccva 3620 | . 2
⊢
((∀𝑦 ∈
𝑉 (𝑥 ∈ 𝑉 ↦ (𝑥 , 𝑦)) ∈ (𝑊 LMHom (ringLMod‘𝐹)) ∧ 𝐴 ∈ 𝑉) → 𝐺 ∈ (𝑊 LMHom (ringLMod‘𝐹))) | 
| 18 | 11, 17 | sylan 580 | 1
⊢ ((𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉) → 𝐺 ∈ (𝑊 LMHom (ringLMod‘𝐹))) |