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 𝑋 = ( 𝑊s 𝑈 )
phssip.s 𝑆 = ( LSubSp ‘ 𝑊 )
phssip.i · = ( ·if𝑊 )
phssip.p 𝑃 = ( ·if𝑋 )
Assertion phssip ( ( 𝑊 ∈ PreHil ∧ 𝑈𝑆 ) → 𝑃 = ( · ↾ ( 𝑈 × 𝑈 ) ) )

Proof

Step Hyp Ref Expression
1 phssip.x 𝑋 = ( 𝑊s 𝑈 )
2 phssip.s 𝑆 = ( LSubSp ‘ 𝑊 )
3 phssip.i · = ( ·if𝑊 )
4 phssip.p 𝑃 = ( ·if𝑋 )
5 eqid ( Base ‘ 𝑋 ) = ( Base ‘ 𝑋 )
6 eqid ( ·𝑖𝑋 ) = ( ·𝑖𝑋 )
7 5 6 4 ipffval 𝑃 = ( 𝑥 ∈ ( Base ‘ 𝑋 ) , 𝑦 ∈ ( Base ‘ 𝑋 ) ↦ ( 𝑥 ( ·𝑖𝑋 ) 𝑦 ) )
8 phllmod ( 𝑊 ∈ PreHil → 𝑊 ∈ LMod )
9 2 lsssubg ( ( 𝑊 ∈ LMod ∧ 𝑈𝑆 ) → 𝑈 ∈ ( SubGrp ‘ 𝑊 ) )
10 8 9 sylan ( ( 𝑊 ∈ PreHil ∧ 𝑈𝑆 ) → 𝑈 ∈ ( SubGrp ‘ 𝑊 ) )
11 1 subgbas ( 𝑈 ∈ ( SubGrp ‘ 𝑊 ) → 𝑈 = ( Base ‘ 𝑋 ) )
12 10 11 syl ( ( 𝑊 ∈ PreHil ∧ 𝑈𝑆 ) → 𝑈 = ( Base ‘ 𝑋 ) )
13 eqidd ( ( 𝑊 ∈ PreHil ∧ 𝑈𝑆 ) → ( 𝑥 ( ·𝑖𝑊 ) 𝑦 ) = ( 𝑥 ( ·𝑖𝑊 ) 𝑦 ) )
14 12 12 13 mpoeq123dv ( ( 𝑊 ∈ PreHil ∧ 𝑈𝑆 ) → ( 𝑥𝑈 , 𝑦𝑈 ↦ ( 𝑥 ( ·𝑖𝑊 ) 𝑦 ) ) = ( 𝑥 ∈ ( Base ‘ 𝑋 ) , 𝑦 ∈ ( Base ‘ 𝑋 ) ↦ ( 𝑥 ( ·𝑖𝑊 ) 𝑦 ) ) )
15 eqid ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
16 15 subgss ( 𝑈 ∈ ( SubGrp ‘ 𝑊 ) → 𝑈 ⊆ ( Base ‘ 𝑊 ) )
17 10 16 syl ( ( 𝑊 ∈ PreHil ∧ 𝑈𝑆 ) → 𝑈 ⊆ ( Base ‘ 𝑊 ) )
18 resmpo ( ( 𝑈 ⊆ ( Base ‘ 𝑊 ) ∧ 𝑈 ⊆ ( Base ‘ 𝑊 ) ) → ( ( 𝑥 ∈ ( Base ‘ 𝑊 ) , 𝑦 ∈ ( Base ‘ 𝑊 ) ↦ ( 𝑥 ( ·𝑖𝑊 ) 𝑦 ) ) ↾ ( 𝑈 × 𝑈 ) ) = ( 𝑥𝑈 , 𝑦𝑈 ↦ ( 𝑥 ( ·𝑖𝑊 ) 𝑦 ) ) )
19 17 17 18 syl2anc ( ( 𝑊 ∈ PreHil ∧ 𝑈𝑆 ) → ( ( 𝑥 ∈ ( Base ‘ 𝑊 ) , 𝑦 ∈ ( Base ‘ 𝑊 ) ↦ ( 𝑥 ( ·𝑖𝑊 ) 𝑦 ) ) ↾ ( 𝑈 × 𝑈 ) ) = ( 𝑥𝑈 , 𝑦𝑈 ↦ ( 𝑥 ( ·𝑖𝑊 ) 𝑦 ) ) )
20 eqid ( ·𝑖𝑊 ) = ( ·𝑖𝑊 )
21 1 20 6 ssipeq ( 𝑈𝑆 → ( ·𝑖𝑋 ) = ( ·𝑖𝑊 ) )
22 21 adantl ( ( 𝑊 ∈ PreHil ∧ 𝑈𝑆 ) → ( ·𝑖𝑋 ) = ( ·𝑖𝑊 ) )
23 22 oveqd ( ( 𝑊 ∈ PreHil ∧ 𝑈𝑆 ) → ( 𝑥 ( ·𝑖𝑋 ) 𝑦 ) = ( 𝑥 ( ·𝑖𝑊 ) 𝑦 ) )
24 23 mpoeq3dv ( ( 𝑊 ∈ PreHil ∧ 𝑈𝑆 ) → ( 𝑥 ∈ ( Base ‘ 𝑋 ) , 𝑦 ∈ ( Base ‘ 𝑋 ) ↦ ( 𝑥 ( ·𝑖𝑋 ) 𝑦 ) ) = ( 𝑥 ∈ ( Base ‘ 𝑋 ) , 𝑦 ∈ ( Base ‘ 𝑋 ) ↦ ( 𝑥 ( ·𝑖𝑊 ) 𝑦 ) ) )
25 14 19 24 3eqtr4rd ( ( 𝑊 ∈ PreHil ∧ 𝑈𝑆 ) → ( 𝑥 ∈ ( Base ‘ 𝑋 ) , 𝑦 ∈ ( Base ‘ 𝑋 ) ↦ ( 𝑥 ( ·𝑖𝑋 ) 𝑦 ) ) = ( ( 𝑥 ∈ ( Base ‘ 𝑊 ) , 𝑦 ∈ ( Base ‘ 𝑊 ) ↦ ( 𝑥 ( ·𝑖𝑊 ) 𝑦 ) ) ↾ ( 𝑈 × 𝑈 ) ) )
26 7 25 syl5eq ( ( 𝑊 ∈ PreHil ∧ 𝑈𝑆 ) → 𝑃 = ( ( 𝑥 ∈ ( Base ‘ 𝑊 ) , 𝑦 ∈ ( Base ‘ 𝑊 ) ↦ ( 𝑥 ( ·𝑖𝑊 ) 𝑦 ) ) ↾ ( 𝑈 × 𝑈 ) ) )
27 15 20 3 ipffval · = ( 𝑥 ∈ ( Base ‘ 𝑊 ) , 𝑦 ∈ ( Base ‘ 𝑊 ) ↦ ( 𝑥 ( ·𝑖𝑊 ) 𝑦 ) )
28 27 a1i ( ( 𝑊 ∈ PreHil ∧ 𝑈𝑆 ) → · = ( 𝑥 ∈ ( Base ‘ 𝑊 ) , 𝑦 ∈ ( Base ‘ 𝑊 ) ↦ ( 𝑥 ( ·𝑖𝑊 ) 𝑦 ) ) )
29 28 reseq1d ( ( 𝑊 ∈ PreHil ∧ 𝑈𝑆 ) → ( · ↾ ( 𝑈 × 𝑈 ) ) = ( ( 𝑥 ∈ ( Base ‘ 𝑊 ) , 𝑦 ∈ ( Base ‘ 𝑊 ) ↦ ( 𝑥 ( ·𝑖𝑊 ) 𝑦 ) ) ↾ ( 𝑈 × 𝑈 ) ) )
30 26 29 eqtr4d ( ( 𝑊 ∈ PreHil ∧ 𝑈𝑆 ) → 𝑃 = ( · ↾ ( 𝑈 × 𝑈 ) ) )