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	⊢ 𝑋 = ( 𝑊 ↾s 𝑈 )
	ssipeq.i	⊢ , = ( ·𝑖 ‘ 𝑊 )
	ssipeq.p	⊢ 𝑃 = ( ·𝑖 ‘ 𝑋 )
	ssipeq.s	⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
Assertion	phssipval	⊢ ( ( ( 𝑊 ∈ PreHil ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑈 ) ) → ( 𝐴 𝑃 𝐵 ) = ( 𝐴 , 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		ssipeq.x	⊢ 𝑋 = ( 𝑊 ↾s 𝑈 )
2		ssipeq.i	⊢ , = ( ·𝑖 ‘ 𝑊 )
3		ssipeq.p	⊢ 𝑃 = ( ·𝑖 ‘ 𝑋 )
4		ssipeq.s	⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
5	1 2 3	ssipeq	⊢ ( 𝑈 ∈ 𝑆 → 𝑃 = , )
6	5	oveqd	⊢ ( 𝑈 ∈ 𝑆 → ( 𝐴 𝑃 𝐵 ) = ( 𝐴 , 𝐵 ) )
7	6	ad2antlr	⊢ ( ( ( 𝑊 ∈ PreHil ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑈 ) ) → ( 𝐴 𝑃 𝐵 ) = ( 𝐴 , 𝐵 ) )