Database
BASIC ALGEBRAIC STRUCTURES
Generalized pre-Hilbert and Hilbert spaces
Definition and basic properties
phssipval
Metamath Proof Explorer
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 ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑈 ) ) → ( 𝐴 𝑃 𝐵 ) = ( 𝐴 , 𝐵 ) )