Metamath Proof Explorer


Theorem ssps

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

Ref Expression
Hypotheses ssps.y
|- Y = ( BaseSet ` W )
ssps.s
|- S = ( .sOLD ` U )
ssps.r
|- R = ( .sOLD ` W )
ssps.h
|- H = ( SubSp ` U )
Assertion ssps
|- ( ( U e. NrmCVec /\ W e. H ) -> R = ( S |` ( CC X. Y ) ) )

Proof

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