Metamath Proof Explorer

Theorem sspg

Description: Vector addition on a subspace is a restriction of vector addition on the parent space. (Contributed by NM, 28-Jan-2008) (New usage is discouraged.)

Ref Expression
Hypotheses sspg.y 
|- Y = ( BaseSet ` W )
sspg.g 
|- G = ( +v ` U )
sspg.f 
|- F = ( +v ` W )
sspg.h 
|- H = ( SubSp ` U )
Assertion sspg 
|- ( ( U e. NrmCVec /\ W e. H ) -> F = ( G |` ( Y X. Y ) ) )

Proof

Step Hyp Ref Expression
1 sspg.y 
 |-  Y = ( BaseSet ` W )
2 sspg.g 
 |-  G = ( +v ` U )
3 sspg.f 
 |-  F = ( +v ` W )
4 sspg.h 
 |-  H = ( SubSp ` U )
5 eqid 
 |-  ( BaseSet ` U ) = ( BaseSet ` U )
6 5 2 nvgf 
 |-  ( U e. NrmCVec -> G : ( ( BaseSet ` U ) X. ( BaseSet ` U ) ) --> ( BaseSet ` U ) )
7 6 ffund 
 |-  ( U e. NrmCVec -> Fun G )
8 funres 
 |-  ( Fun G -> Fun ( G |` ( Y X. Y ) ) )
9 7 8 syl 
 |-  ( U e. NrmCVec -> Fun ( G |` ( Y X. Y ) ) )
10 9 adantr 
 |-  ( ( U e. NrmCVec /\ W e. H ) -> Fun ( G |` ( Y X. Y ) ) )
11 4 sspnv 
 |-  ( ( U e. NrmCVec /\ W e. H ) -> W e. NrmCVec )
12 1 3 nvgf 
 |-  ( W e. NrmCVec -> F : ( Y X. Y ) --> Y )
13 11 12 syl 
 |-  ( ( U e. NrmCVec /\ W e. H ) -> F : ( Y X. Y ) --> Y )
14 13 ffnd 
 |-  ( ( U e. NrmCVec /\ W e. H ) -> F Fn ( Y X. Y ) )
15 fnresdm 
 |-  ( F Fn ( Y X. Y ) -> ( F |` ( Y X. Y ) ) = F )
16 14 15 syl 
 |-  ( ( U e. NrmCVec /\ W e. H ) -> ( F |` ( Y X. Y ) ) = F )
17 eqid 
 |-  ( .sOLD ` U ) = ( .sOLD ` U )
18 eqid 
 |-  ( .sOLD ` W ) = ( .sOLD ` W )
19 eqid 
 |-  ( normCV ` U ) = ( normCV ` U )
20 eqid 
 |-  ( normCV ` W ) = ( normCV ` W )
21 2 3 17 18 19 20 4 isssp 
 |-  ( U e. NrmCVec -> ( W e. H <-> ( W e. NrmCVec /\ ( F C_ G /\ ( .sOLD ` W ) C_ ( .sOLD ` U ) /\ ( normCV ` W ) C_ ( normCV ` U ) ) ) ) )
22 21 simplbda 
 |-  ( ( U e. NrmCVec /\ W e. H ) -> ( F C_ G /\ ( .sOLD ` W ) C_ ( .sOLD ` U ) /\ ( normCV ` W ) C_ ( normCV ` U ) ) )
23 22 simp1d 
 |-  ( ( U e. NrmCVec /\ W e. H ) -> F C_ G )
24 ssres 
 |-  ( F C_ G -> ( F |` ( Y X. Y ) ) C_ ( G |` ( Y X. Y ) ) )
25 23 24 syl 
 |-  ( ( U e. NrmCVec /\ W e. H ) -> ( F |` ( Y X. Y ) ) C_ ( G |` ( Y X. Y ) ) )
26 16 25 eqsstrrd 
 |-  ( ( U e. NrmCVec /\ W e. H ) -> F C_ ( G |` ( Y X. Y ) ) )
27 10 14 26 3jca 
 |-  ( ( U e. NrmCVec /\ W e. H ) -> ( Fun ( G |` ( Y X. Y ) ) /\ F Fn ( Y X. Y ) /\ F C_ ( G |` ( Y X. Y ) ) ) )
28 oprssov 
 |-  ( ( ( Fun ( G |` ( Y X. Y ) ) /\ F Fn ( Y X. Y ) /\ F C_ ( G |` ( Y X. Y ) ) ) /\ ( x e. Y /\ y e. Y ) ) -> ( x ( G |` ( Y X. Y ) ) y ) = ( x F y ) )
29 27 28 sylan 
 |-  ( ( ( U e. NrmCVec /\ W e. H ) /\ ( x e. Y /\ y e. Y ) ) -> ( x ( G |` ( Y X. Y ) ) y ) = ( x F y ) )
30 29 eqcomd 
 |-  ( ( ( U e. NrmCVec /\ W e. H ) /\ ( x e. Y /\ y e. Y ) ) -> ( x F y ) = ( x ( G |` ( Y X. Y ) ) y ) )
31 30 ralrimivva 
 |-  ( ( U e. NrmCVec /\ W e. H ) -> A. x e. Y A. y e. Y ( x F y ) = ( x ( G |` ( Y X. Y ) ) y ) )
32 eqid 
 |-  ( Y X. Y ) = ( Y X. Y )
33 31 32 jctil 
 |-  ( ( U e. NrmCVec /\ W e. H ) -> ( ( Y X. Y ) = ( Y X. Y ) /\ A. x e. Y A. y e. Y ( x F y ) = ( x ( G |` ( Y X. Y ) ) y ) ) )
34 6 ffnd 
 |-  ( U e. NrmCVec -> G Fn ( ( BaseSet ` U ) X. ( BaseSet ` U ) ) )
35 34 adantr 
 |-  ( ( U e. NrmCVec /\ W e. H ) -> G Fn ( ( BaseSet ` U ) X. ( BaseSet ` U ) ) )
36 5 1 4 sspba 
 |-  ( ( U e. NrmCVec /\ W e. H ) -> Y C_ ( BaseSet ` U ) )
37 xpss12 
 |-  ( ( Y C_ ( BaseSet ` U ) /\ Y C_ ( BaseSet ` U ) ) -> ( Y X. Y ) C_ ( ( BaseSet ` U ) X. ( BaseSet ` U ) ) )
38 36 36 37 syl2anc 
 |-  ( ( U e. NrmCVec /\ W e. H ) -> ( Y X. Y ) C_ ( ( BaseSet ` U ) X. ( BaseSet ` U ) ) )
39 fnssres 
 |-  ( ( G Fn ( ( BaseSet ` U ) X. ( BaseSet ` U ) ) /\ ( Y X. Y ) C_ ( ( BaseSet ` U ) X. ( BaseSet ` U ) ) ) -> ( G |` ( Y X. Y ) ) Fn ( Y X. Y ) )
40 35 38 39 syl2anc 
 |-  ( ( U e. NrmCVec /\ W e. H ) -> ( G |` ( Y X. Y ) ) Fn ( Y X. Y ) )
41 eqfnov 
 |-  ( ( F Fn ( Y X. Y ) /\ ( G |` ( Y X. Y ) ) Fn ( Y X. Y ) ) -> ( F = ( G |` ( Y X. Y ) ) <-> ( ( Y X. Y ) = ( Y X. Y ) /\ A. x e. Y A. y e. Y ( x F y ) = ( x ( G |` ( Y X. Y ) ) y ) ) ) )
42 14 40 41 syl2anc 
 |-  ( ( U e. NrmCVec /\ W e. H ) -> ( F = ( G |` ( Y X. Y ) ) <-> ( ( Y X. Y ) = ( Y X. Y ) /\ A. x e. Y A. y e. Y ( x F y ) = ( x ( G |` ( Y X. Y ) ) y ) ) ) )
43 33 42 mpbird 
 |-  ( ( U e. NrmCVec /\ W e. H ) -> F = ( G |` ( Y X. Y ) ) )