This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database BASIC ALGEBRAIC STRUCTURES Generalized pre-Hilbert and Hilbert spaces Definition and basic properties phssipval
Description: The inner product on a subspace in terms of the inner product on the
parent space. (Contributed by NM , 28-Jan-2008) (Revised by AV , 19-Oct-2021)
Ref
Expression
Hypotheses
ssipeq.x ⊢ 𝑋 = ( 𝑊 ↾s 𝑈 )
ssipeq.i ⊢ , = ( · 𝑖 ‘ 𝑊 )
ssipeq.p ⊢ 𝑃 = ( · 𝑖 ‘ 𝑋 )
ssipeq.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
Assertion
phssipval ⊢ ( ( ( 𝑊 ∈ PreHil ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑈 ) ) → ( 𝐴 𝑃 𝐵 ) = ( 𝐴 , 𝐵 ) )
Proof
Step
Hyp
Ref
Expression
1
ssipeq.x ⊢ 𝑋 = ( 𝑊 ↾s 𝑈 )
2
ssipeq.i ⊢ , = ( · 𝑖 ‘ 𝑊 )
3
ssipeq.p ⊢ 𝑃 = ( · 𝑖 ‘ 𝑋 )
4
ssipeq.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
5
1 2 3
ssipeq ⊢ ( 𝑈 ∈ 𝑆 → 𝑃 = , )
6
5
oveqd ⊢ ( 𝑈 ∈ 𝑆 → ( 𝐴 𝑃 𝐵 ) = ( 𝐴 , 𝐵 ) )
7
6
ad2antlr ⊢ ( ( ( 𝑊 ∈ PreHil ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑈 ) ) → ( 𝐴 𝑃 𝐵 ) = ( 𝐴 , 𝐵 ) )