Metamath Proof Explorer


Theorem 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 ∧ 𝑈𝑆 ) ∧ ( 𝐴𝑈𝐵𝑈 ) ) → ( 𝐴 𝑃 𝐵 ) = ( 𝐴 , 𝐵 ) )