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
|- X = ( W |`s U )
ssipeq.i
|- ., = ( .i ` W )
ssipeq.p
|- P = ( .i ` X )
ssipeq.s
|- S = ( LSubSp ` W )
Assertion phssipval
|- ( ( ( W e. PreHil /\ U e. S ) /\ ( A e. U /\ B e. U ) ) -> ( A P B ) = ( A ., B ) )

Proof

Step Hyp Ref Expression
1 ssipeq.x
 |-  X = ( W |`s U )
2 ssipeq.i
 |-  ., = ( .i ` W )
3 ssipeq.p
 |-  P = ( .i ` X )
4 ssipeq.s
 |-  S = ( LSubSp ` W )
5 1 2 3 ssipeq
 |-  ( U e. S -> P = ., )
6 5 oveqd
 |-  ( U e. S -> ( A P B ) = ( A ., B ) )
7 6 ad2antlr
 |-  ( ( ( W e. PreHil /\ U e. S ) /\ ( A e. U /\ B e. U ) ) -> ( A P B ) = ( A ., B ) )