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

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	1 2	ressip	$$⊢U\in S\to \underset{\dot{}}{,}={\cdot }_{𝑖}\left(X\right)$$
5	3 4	eqtr4id	$$⊢U\in S\to P=\underset{\dot{}}{,}$$