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 ∧ 𝑈 ∈ 𝑆 ) → 𝑃 = ( · ↾ ( 𝑈 × 𝑈 ) ) )