Step |
Hyp |
Ref |
Expression |
1 |
|
ipffn.1 |
⊢ 𝑉 = ( Base ‘ 𝑊 ) |
2 |
|
ipffn.2 |
⊢ , = ( ·if ‘ 𝑊 ) |
3 |
|
phlipf.s |
⊢ 𝑆 = ( Scalar ‘ 𝑊 ) |
4 |
|
phlipf.k |
⊢ 𝐾 = ( Base ‘ 𝑆 ) |
5 |
|
eqid |
⊢ ( ·𝑖 ‘ 𝑊 ) = ( ·𝑖 ‘ 𝑊 ) |
6 |
3 5 1 4
|
ipcl |
⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) → ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) ∈ 𝐾 ) |
7 |
6
|
3expb |
⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) ∈ 𝐾 ) |
8 |
7
|
ralrimivva |
⊢ ( 𝑊 ∈ PreHil → ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) ∈ 𝐾 ) |
9 |
1 5 2
|
ipffval |
⊢ , = ( 𝑥 ∈ 𝑉 , 𝑦 ∈ 𝑉 ↦ ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) ) |
10 |
9
|
fmpo |
⊢ ( ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) ∈ 𝐾 ↔ , : ( 𝑉 × 𝑉 ) ⟶ 𝐾 ) |
11 |
8 10
|
sylib |
⊢ ( 𝑊 ∈ PreHil → , : ( 𝑉 × 𝑉 ) ⟶ 𝐾 ) |