# Metamath Proof Explorer

## Theorem phssip

Description: The inner product (as a function) on a subspace is a restriction of the inner product (as a function) on the parent space. (Contributed by NM, 28-Jan-2008) (Revised by AV, 19-Oct-2021)

Ref Expression
Hypotheses phssip.x ${⊢}{X}={W}{↾}_{𝑠}{U}$
phssip.s ${⊢}{S}=\mathrm{LSubSp}\left({W}\right)$
phssip.i
phssip.p ${⊢}{P}={\cdot }_{\mathrm{if}}\left({X}\right)$
Assertion phssip

### Proof

Step Hyp Ref Expression
1 phssip.x ${⊢}{X}={W}{↾}_{𝑠}{U}$
2 phssip.s ${⊢}{S}=\mathrm{LSubSp}\left({W}\right)$
3 phssip.i
4 phssip.p ${⊢}{P}={\cdot }_{\mathrm{if}}\left({X}\right)$
5 eqid ${⊢}{\mathrm{Base}}_{{X}}={\mathrm{Base}}_{{X}}$
6 eqid ${⊢}{\cdot }_{𝑖}\left({X}\right)={\cdot }_{𝑖}\left({X}\right)$
7 5 6 4 ipffval ${⊢}{P}=\left({x}\in {\mathrm{Base}}_{{X}},{y}\in {\mathrm{Base}}_{{X}}⟼{x}{\cdot }_{𝑖}\left({X}\right){y}\right)$
8 phllmod ${⊢}{W}\in \mathrm{PreHil}\to {W}\in \mathrm{LMod}$
9 2 lsssubg ${⊢}\left({W}\in \mathrm{LMod}\wedge {U}\in {S}\right)\to {U}\in \mathrm{SubGrp}\left({W}\right)$
10 8 9 sylan ${⊢}\left({W}\in \mathrm{PreHil}\wedge {U}\in {S}\right)\to {U}\in \mathrm{SubGrp}\left({W}\right)$
11 1 subgbas ${⊢}{U}\in \mathrm{SubGrp}\left({W}\right)\to {U}={\mathrm{Base}}_{{X}}$
12 10 11 syl ${⊢}\left({W}\in \mathrm{PreHil}\wedge {U}\in {S}\right)\to {U}={\mathrm{Base}}_{{X}}$
13 eqidd ${⊢}\left({W}\in \mathrm{PreHil}\wedge {U}\in {S}\right)\to {x}{\cdot }_{𝑖}\left({W}\right){y}={x}{\cdot }_{𝑖}\left({W}\right){y}$
14 12 12 13 mpoeq123dv ${⊢}\left({W}\in \mathrm{PreHil}\wedge {U}\in {S}\right)\to \left({x}\in {U},{y}\in {U}⟼{x}{\cdot }_{𝑖}\left({W}\right){y}\right)=\left({x}\in {\mathrm{Base}}_{{X}},{y}\in {\mathrm{Base}}_{{X}}⟼{x}{\cdot }_{𝑖}\left({W}\right){y}\right)$
15 eqid ${⊢}{\mathrm{Base}}_{{W}}={\mathrm{Base}}_{{W}}$
16 15 subgss ${⊢}{U}\in \mathrm{SubGrp}\left({W}\right)\to {U}\subseteq {\mathrm{Base}}_{{W}}$
17 10 16 syl ${⊢}\left({W}\in \mathrm{PreHil}\wedge {U}\in {S}\right)\to {U}\subseteq {\mathrm{Base}}_{{W}}$
18 resmpo ${⊢}\left({U}\subseteq {\mathrm{Base}}_{{W}}\wedge {U}\subseteq {\mathrm{Base}}_{{W}}\right)\to {\left({x}\in {\mathrm{Base}}_{{W}},{y}\in {\mathrm{Base}}_{{W}}⟼{x}{\cdot }_{𝑖}\left({W}\right){y}\right)↾}_{\left({U}×{U}\right)}=\left({x}\in {U},{y}\in {U}⟼{x}{\cdot }_{𝑖}\left({W}\right){y}\right)$
19 17 17 18 syl2anc ${⊢}\left({W}\in \mathrm{PreHil}\wedge {U}\in {S}\right)\to {\left({x}\in {\mathrm{Base}}_{{W}},{y}\in {\mathrm{Base}}_{{W}}⟼{x}{\cdot }_{𝑖}\left({W}\right){y}\right)↾}_{\left({U}×{U}\right)}=\left({x}\in {U},{y}\in {U}⟼{x}{\cdot }_{𝑖}\left({W}\right){y}\right)$
20 eqid ${⊢}{\cdot }_{𝑖}\left({W}\right)={\cdot }_{𝑖}\left({W}\right)$
21 1 20 6 ssipeq ${⊢}{U}\in {S}\to {\cdot }_{𝑖}\left({X}\right)={\cdot }_{𝑖}\left({W}\right)$
22 21 adantl ${⊢}\left({W}\in \mathrm{PreHil}\wedge {U}\in {S}\right)\to {\cdot }_{𝑖}\left({X}\right)={\cdot }_{𝑖}\left({W}\right)$
23 22 oveqd ${⊢}\left({W}\in \mathrm{PreHil}\wedge {U}\in {S}\right)\to {x}{\cdot }_{𝑖}\left({X}\right){y}={x}{\cdot }_{𝑖}\left({W}\right){y}$
24 23 mpoeq3dv ${⊢}\left({W}\in \mathrm{PreHil}\wedge {U}\in {S}\right)\to \left({x}\in {\mathrm{Base}}_{{X}},{y}\in {\mathrm{Base}}_{{X}}⟼{x}{\cdot }_{𝑖}\left({X}\right){y}\right)=\left({x}\in {\mathrm{Base}}_{{X}},{y}\in {\mathrm{Base}}_{{X}}⟼{x}{\cdot }_{𝑖}\left({W}\right){y}\right)$
25 14 19 24 3eqtr4rd ${⊢}\left({W}\in \mathrm{PreHil}\wedge {U}\in {S}\right)\to \left({x}\in {\mathrm{Base}}_{{X}},{y}\in {\mathrm{Base}}_{{X}}⟼{x}{\cdot }_{𝑖}\left({X}\right){y}\right)={\left({x}\in {\mathrm{Base}}_{{W}},{y}\in {\mathrm{Base}}_{{W}}⟼{x}{\cdot }_{𝑖}\left({W}\right){y}\right)↾}_{\left({U}×{U}\right)}$
26 7 25 syl5eq ${⊢}\left({W}\in \mathrm{PreHil}\wedge {U}\in {S}\right)\to {P}={\left({x}\in {\mathrm{Base}}_{{W}},{y}\in {\mathrm{Base}}_{{W}}⟼{x}{\cdot }_{𝑖}\left({W}\right){y}\right)↾}_{\left({U}×{U}\right)}$
27 15 20 3 ipffval
28 27 a1i
29 28 reseq1d
30 26 29 eqtr4d