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

Metamath Proof Explorer

Theorem ressip

Description: The inner product is unaffected by restriction. (Contributed by Thierry Arnoux, 16-Jun-2019)

Ref Expression
Hypotheses resssca.1 ⊢ 𝐻 = ( 𝐺 ↾s 𝐴 )
ressip.2 ⊢ , = ( ·𝑖 ‘ 𝐺 )
Assertion ressip ( 𝐴 ∈ 𝑉 → , = ( ·𝑖 ‘ 𝐻 ) )

Proof

Step Hyp Ref Expression
1 resssca.1 ⊢ 𝐻 = ( 𝐺 ↾s 𝐴 )
2 ressip.2 ⊢ , = ( ·𝑖 ‘ 𝐺 )
3 ipid ⊢ ·𝑖 = Slot ( ·𝑖 ‘ ndx )
4 ipndxnbasendx ⊢ ( ·𝑖 ‘ ndx ) ≠ ( Base ‘ ndx )
5 1 2 3 4 resseqnbas ⊢ ( 𝐴 ∈ 𝑉 → , = ( ·𝑖 ‘ 𝐻 ) )