Metamath Proof Explorer


Theorem ssipeq

Description: The inner product on a subspace equals the inner product on the parent space. (Contributed by AV, 19-Oct-2021)

Ref Expression
Hypotheses ssipeq.x 𝑋 = ( 𝑊s 𝑈 )
ssipeq.i , = ( ·𝑖𝑊 )
ssipeq.p 𝑃 = ( ·𝑖𝑋 )
Assertion ssipeq ( 𝑈𝑆𝑃 = , )

Proof

Step Hyp Ref Expression
1 ssipeq.x 𝑋 = ( 𝑊s 𝑈 )
2 ssipeq.i , = ( ·𝑖𝑊 )
3 ssipeq.p 𝑃 = ( ·𝑖𝑋 )
4 1 2 ressip ( 𝑈𝑆, = ( ·𝑖𝑋 ) )
5 3 4 eqtr4id ( 𝑈𝑆𝑃 = , )