This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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