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 |`s U )
phssip.s 
|- S = ( LSubSp ` W )
phssip.i 
|- .x. = ( .if ` W )
phssip.p 
|- P = ( .if ` X )
Assertion phssip 
|- ( ( W e. PreHil /\ U e. S ) -> P = ( .x. |` ( U X. U ) ) )

Proof

Step Hyp Ref Expression
1 phssip.x 
 |-  X = ( W |`s U )
2 phssip.s 
 |-  S = ( LSubSp ` W )
3 phssip.i 
 |-  .x. = ( .if ` W )
4 phssip.p 
 |-  P = ( .if ` X )
5 eqid 
 |-  ( Base ` X ) = ( Base ` X )
6 eqid 
 |-  ( .i ` X ) = ( .i ` X )
7 5 6 4 ipffval 
 |-  P = ( x e. ( Base ` X ) , y e. ( Base ` X ) |-> ( x ( .i ` X ) y ) )
8 phllmod 
 |-  ( W e. PreHil -> W e. LMod )
9 2 lsssubg 
 |-  ( ( W e. LMod /\ U e. S ) -> U e. ( SubGrp ` W ) )
10 8 9 sylan 
 |-  ( ( W e. PreHil /\ U e. S ) -> U e. ( SubGrp ` W ) )
11 1 subgbas 
 |-  ( U e. ( SubGrp ` W ) -> U = ( Base ` X ) )
12 10 11 syl 
 |-  ( ( W e. PreHil /\ U e. S ) -> U = ( Base ` X ) )
13 eqidd 
 |-  ( ( W e. PreHil /\ U e. S ) -> ( x ( .i ` W ) y ) = ( x ( .i ` W ) y ) )
14 12 12 13 mpoeq123dv 
 |-  ( ( W e. PreHil /\ U e. S ) -> ( x e. U , y e. U |-> ( x ( .i ` W ) y ) ) = ( x e. ( Base ` X ) , y e. ( Base ` X ) |-> ( x ( .i ` W ) y ) ) )
15 eqid 
 |-  ( Base ` W ) = ( Base ` W )
16 15 subgss 
 |-  ( U e. ( SubGrp ` W ) -> U C_ ( Base ` W ) )
17 10 16 syl 
 |-  ( ( W e. PreHil /\ U e. S ) -> U C_ ( Base ` W ) )
18 resmpo 
 |-  ( ( U C_ ( Base ` W ) /\ U C_ ( Base ` W ) ) -> ( ( x e. ( Base ` W ) , y e. ( Base ` W ) |-> ( x ( .i ` W ) y ) ) |` ( U X. U ) ) = ( x e. U , y e. U |-> ( x ( .i ` W ) y ) ) )
19 17 17 18 syl2anc 
 |-  ( ( W e. PreHil /\ U e. S ) -> ( ( x e. ( Base ` W ) , y e. ( Base ` W ) |-> ( x ( .i ` W ) y ) ) |` ( U X. U ) ) = ( x e. U , y e. U |-> ( x ( .i ` W ) y ) ) )
20 eqid 
 |-  ( .i ` W ) = ( .i ` W )
21 1 20 6 ssipeq 
 |-  ( U e. S -> ( .i ` X ) = ( .i ` W ) )
22 21 adantl 
 |-  ( ( W e. PreHil /\ U e. S ) -> ( .i ` X ) = ( .i ` W ) )
23 22 oveqd 
 |-  ( ( W e. PreHil /\ U e. S ) -> ( x ( .i ` X ) y ) = ( x ( .i ` W ) y ) )
24 23 mpoeq3dv 
 |-  ( ( W e. PreHil /\ U e. S ) -> ( x e. ( Base ` X ) , y e. ( Base ` X ) |-> ( x ( .i ` X ) y ) ) = ( x e. ( Base ` X ) , y e. ( Base ` X ) |-> ( x ( .i ` W ) y ) ) )
25 14 19 24 3eqtr4rd 
 |-  ( ( W e. PreHil /\ U e. S ) -> ( x e. ( Base ` X ) , y e. ( Base ` X ) |-> ( x ( .i ` X ) y ) ) = ( ( x e. ( Base ` W ) , y e. ( Base ` W ) |-> ( x ( .i ` W ) y ) ) |` ( U X. U ) ) )
26 7 25 syl5eq 
 |-  ( ( W e. PreHil /\ U e. S ) -> P = ( ( x e. ( Base ` W ) , y e. ( Base ` W ) |-> ( x ( .i ` W ) y ) ) |` ( U X. U ) ) )
27 15 20 3 ipffval 
 |-  .x. = ( x e. ( Base ` W ) , y e. ( Base ` W ) |-> ( x ( .i ` W ) y ) )
28 27 a1i 
 |-  ( ( W e. PreHil /\ U e. S ) -> .x. = ( x e. ( Base ` W ) , y e. ( Base ` W ) |-> ( x ( .i ` W ) y ) ) )
29 28 reseq1d 
 |-  ( ( W e. PreHil /\ U e. S ) -> ( .x. |` ( U X. U ) ) = ( ( x e. ( Base ` W ) , y e. ( Base ` W ) |-> ( x ( .i ` W ) y ) ) |` ( U X. U ) ) )
30 26 29 eqtr4d 
 |-  ( ( W e. PreHil /\ U e. S ) -> P = ( .x. |` ( U X. U ) ) )