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{\upharpoonright }_{𝑠}U$$
	ssipeq.i	$$⊢\underset{\dot{}}{,}={\cdot }_{𝑖}\left(W\right)$$
	ssipeq.p	$$⊢P={\cdot }_{𝑖}\left(X\right)$$
	ssipeq.s	$$⊢S=\mathrm{LSubSp}\left(W\right)$$
Assertion	phssipval	$$⊢\left(\left(W\in \mathrm{PreHil}\wedge U\in S\right)\wedge \left(A\in U\wedge B\in U\right)\right)\to APB=A\underset{\dot{}}{,}B$$

Proof

Step	Hyp	Ref	Expression
1		ssipeq.x	$$⊢X=W{\upharpoonright }_{𝑠}U$$
2		ssipeq.i	$$⊢\underset{\dot{}}{,}={\cdot }_{𝑖}\left(W\right)$$
3		ssipeq.p	$$⊢P={\cdot }_{𝑖}\left(X\right)$$
4		ssipeq.s	$$⊢S=\mathrm{LSubSp}\left(W\right)$$
5	1 2 3	ssipeq	$$⊢U\in S\to P=\underset{\dot{}}{,}$$
6	5	oveqd	$$⊢U\in S\to APB=A\underset{\dot{}}{,}B$$
7	6	ad2antlr	$$⊢\left(\left(W\in \mathrm{PreHil}\wedge U\in S\right)\wedge \left(A\in U\wedge B\in U\right)\right)\to APB=A\underset{\dot{}}{,}B$$