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	⊢ ( 𝑈 ∈ 𝑆 → 𝑃 = , )