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