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 โŠข ๐‘Œ = ( BaseSet โ€˜ ๐‘Š )
ssps.s โŠข ๐‘† = ( ยท๐‘ OLD โ€˜ ๐‘ˆ )
ssps.r โŠข ๐‘… = ( ยท๐‘ OLD โ€˜ ๐‘Š )
ssps.h โŠข ๐ป = ( SubSp โ€˜ ๐‘ˆ )
Assertion ssps ( ( ๐‘ˆ โˆˆ NrmCVec โˆง ๐‘Š โˆˆ ๐ป ) โ†’ ๐‘… = ( ๐‘† โ†พ ( โ„‚ ร— ๐‘Œ ) ) )

Proof

Step Hyp Ref Expression
1 ssps.y โŠข ๐‘Œ = ( BaseSet โ€˜ ๐‘Š )
2 ssps.s โŠข ๐‘† = ( ยท๐‘ OLD โ€˜ ๐‘ˆ )
3 ssps.r โŠข ๐‘… = ( ยท๐‘ OLD โ€˜ ๐‘Š )
4 ssps.h โŠข ๐ป = ( SubSp โ€˜ ๐‘ˆ )
5 eqid โŠข ( BaseSet โ€˜ ๐‘ˆ ) = ( BaseSet โ€˜ ๐‘ˆ )
6 5 2 nvsf โŠข ( ๐‘ˆ โˆˆ NrmCVec โ†’ ๐‘† : ( โ„‚ ร— ( BaseSet โ€˜ ๐‘ˆ ) ) โŸถ ( BaseSet โ€˜ ๐‘ˆ ) )
7 6 ffund โŠข ( ๐‘ˆ โˆˆ NrmCVec โ†’ Fun ๐‘† )
8 7 funresd โŠข ( ๐‘ˆ โˆˆ NrmCVec โ†’ Fun ( ๐‘† โ†พ ( โ„‚ ร— ๐‘Œ ) ) )
9 8 adantr โŠข ( ( ๐‘ˆ โˆˆ NrmCVec โˆง ๐‘Š โˆˆ ๐ป ) โ†’ Fun ( ๐‘† โ†พ ( โ„‚ ร— ๐‘Œ ) ) )
10 4 sspnv โŠข ( ( ๐‘ˆ โˆˆ NrmCVec โˆง ๐‘Š โˆˆ ๐ป ) โ†’ ๐‘Š โˆˆ NrmCVec )
11 1 3 nvsf โŠข ( ๐‘Š โˆˆ NrmCVec โ†’ ๐‘… : ( โ„‚ ร— ๐‘Œ ) โŸถ ๐‘Œ )
12 10 11 syl โŠข ( ( ๐‘ˆ โˆˆ NrmCVec โˆง ๐‘Š โˆˆ ๐ป ) โ†’ ๐‘… : ( โ„‚ ร— ๐‘Œ ) โŸถ ๐‘Œ )
13 12 ffnd โŠข ( ( ๐‘ˆ โˆˆ NrmCVec โˆง ๐‘Š โˆˆ ๐ป ) โ†’ ๐‘… Fn ( โ„‚ ร— ๐‘Œ ) )
14 fnresdm โŠข ( ๐‘… Fn ( โ„‚ ร— ๐‘Œ ) โ†’ ( ๐‘… โ†พ ( โ„‚ ร— ๐‘Œ ) ) = ๐‘… )
15 13 14 syl โŠข ( ( ๐‘ˆ โˆˆ NrmCVec โˆง ๐‘Š โˆˆ ๐ป ) โ†’ ( ๐‘… โ†พ ( โ„‚ ร— ๐‘Œ ) ) = ๐‘… )
16 eqid โŠข ( +๐‘ฃ โ€˜ ๐‘ˆ ) = ( +๐‘ฃ โ€˜ ๐‘ˆ )
17 eqid โŠข ( +๐‘ฃ โ€˜ ๐‘Š ) = ( +๐‘ฃ โ€˜ ๐‘Š )
18 eqid โŠข ( normCV โ€˜ ๐‘ˆ ) = ( normCV โ€˜ ๐‘ˆ )
19 eqid โŠข ( normCV โ€˜ ๐‘Š ) = ( normCV โ€˜ ๐‘Š )
20 16 17 2 3 18 19 4 isssp โŠข ( ๐‘ˆ โˆˆ NrmCVec โ†’ ( ๐‘Š โˆˆ ๐ป โ†” ( ๐‘Š โˆˆ NrmCVec โˆง ( ( +๐‘ฃ โ€˜ ๐‘Š ) โŠ† ( +๐‘ฃ โ€˜ ๐‘ˆ ) โˆง ๐‘… โŠ† ๐‘† โˆง ( normCV โ€˜ ๐‘Š ) โŠ† ( normCV โ€˜ ๐‘ˆ ) ) ) ) )
21 20 simplbda โŠข ( ( ๐‘ˆ โˆˆ NrmCVec โˆง ๐‘Š โˆˆ ๐ป ) โ†’ ( ( +๐‘ฃ โ€˜ ๐‘Š ) โŠ† ( +๐‘ฃ โ€˜ ๐‘ˆ ) โˆง ๐‘… โŠ† ๐‘† โˆง ( normCV โ€˜ ๐‘Š ) โŠ† ( normCV โ€˜ ๐‘ˆ ) ) )
22 21 simp2d โŠข ( ( ๐‘ˆ โˆˆ NrmCVec โˆง ๐‘Š โˆˆ ๐ป ) โ†’ ๐‘… โŠ† ๐‘† )
23 ssres โŠข ( ๐‘… โŠ† ๐‘† โ†’ ( ๐‘… โ†พ ( โ„‚ ร— ๐‘Œ ) ) โŠ† ( ๐‘† โ†พ ( โ„‚ ร— ๐‘Œ ) ) )
24 22 23 syl โŠข ( ( ๐‘ˆ โˆˆ NrmCVec โˆง ๐‘Š โˆˆ ๐ป ) โ†’ ( ๐‘… โ†พ ( โ„‚ ร— ๐‘Œ ) ) โŠ† ( ๐‘† โ†พ ( โ„‚ ร— ๐‘Œ ) ) )
25 15 24 eqsstrrd โŠข ( ( ๐‘ˆ โˆˆ NrmCVec โˆง ๐‘Š โˆˆ ๐ป ) โ†’ ๐‘… โŠ† ( ๐‘† โ†พ ( โ„‚ ร— ๐‘Œ ) ) )
26 9 13 25 3jca โŠข ( ( ๐‘ˆ โˆˆ NrmCVec โˆง ๐‘Š โˆˆ ๐ป ) โ†’ ( Fun ( ๐‘† โ†พ ( โ„‚ ร— ๐‘Œ ) ) โˆง ๐‘… Fn ( โ„‚ ร— ๐‘Œ ) โˆง ๐‘… โŠ† ( ๐‘† โ†พ ( โ„‚ ร— ๐‘Œ ) ) ) )
27 oprssov โŠข ( ( ( Fun ( ๐‘† โ†พ ( โ„‚ ร— ๐‘Œ ) ) โˆง ๐‘… Fn ( โ„‚ ร— ๐‘Œ ) โˆง ๐‘… โŠ† ( ๐‘† โ†พ ( โ„‚ ร— ๐‘Œ ) ) ) โˆง ( ๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ ๐‘Œ ) ) โ†’ ( ๐‘ฅ ( ๐‘† โ†พ ( โ„‚ ร— ๐‘Œ ) ) ๐‘ฆ ) = ( ๐‘ฅ ๐‘… ๐‘ฆ ) )
28 26 27 sylan โŠข ( ( ( ๐‘ˆ โˆˆ NrmCVec โˆง ๐‘Š โˆˆ ๐ป ) โˆง ( ๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ ๐‘Œ ) ) โ†’ ( ๐‘ฅ ( ๐‘† โ†พ ( โ„‚ ร— ๐‘Œ ) ) ๐‘ฆ ) = ( ๐‘ฅ ๐‘… ๐‘ฆ ) )
29 28 eqcomd โŠข ( ( ( ๐‘ˆ โˆˆ NrmCVec โˆง ๐‘Š โˆˆ ๐ป ) โˆง ( ๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ ๐‘Œ ) ) โ†’ ( ๐‘ฅ ๐‘… ๐‘ฆ ) = ( ๐‘ฅ ( ๐‘† โ†พ ( โ„‚ ร— ๐‘Œ ) ) ๐‘ฆ ) )
30 29 ralrimivva โŠข ( ( ๐‘ˆ โˆˆ NrmCVec โˆง ๐‘Š โˆˆ ๐ป ) โ†’ โˆ€ ๐‘ฅ โˆˆ โ„‚ โˆ€ ๐‘ฆ โˆˆ ๐‘Œ ( ๐‘ฅ ๐‘… ๐‘ฆ ) = ( ๐‘ฅ ( ๐‘† โ†พ ( โ„‚ ร— ๐‘Œ ) ) ๐‘ฆ ) )
31 eqid โŠข ( โ„‚ ร— ๐‘Œ ) = ( โ„‚ ร— ๐‘Œ )
32 30 31 jctil โŠข ( ( ๐‘ˆ โˆˆ NrmCVec โˆง ๐‘Š โˆˆ ๐ป ) โ†’ ( ( โ„‚ ร— ๐‘Œ ) = ( โ„‚ ร— ๐‘Œ ) โˆง โˆ€ ๐‘ฅ โˆˆ โ„‚ โˆ€ ๐‘ฆ โˆˆ ๐‘Œ ( ๐‘ฅ ๐‘… ๐‘ฆ ) = ( ๐‘ฅ ( ๐‘† โ†พ ( โ„‚ ร— ๐‘Œ ) ) ๐‘ฆ ) ) )
33 6 ffnd โŠข ( ๐‘ˆ โˆˆ NrmCVec โ†’ ๐‘† Fn ( โ„‚ ร— ( BaseSet โ€˜ ๐‘ˆ ) ) )
34 33 adantr โŠข ( ( ๐‘ˆ โˆˆ NrmCVec โˆง ๐‘Š โˆˆ ๐ป ) โ†’ ๐‘† Fn ( โ„‚ ร— ( BaseSet โ€˜ ๐‘ˆ ) ) )
35 ssid โŠข โ„‚ โŠ† โ„‚
36 5 1 4 sspba โŠข ( ( ๐‘ˆ โˆˆ NrmCVec โˆง ๐‘Š โˆˆ ๐ป ) โ†’ ๐‘Œ โŠ† ( BaseSet โ€˜ ๐‘ˆ ) )
37 xpss12 โŠข ( ( โ„‚ โŠ† โ„‚ โˆง ๐‘Œ โŠ† ( BaseSet โ€˜ ๐‘ˆ ) ) โ†’ ( โ„‚ ร— ๐‘Œ ) โŠ† ( โ„‚ ร— ( BaseSet โ€˜ ๐‘ˆ ) ) )
38 35 36 37 sylancr โŠข ( ( ๐‘ˆ โˆˆ NrmCVec โˆง ๐‘Š โˆˆ ๐ป ) โ†’ ( โ„‚ ร— ๐‘Œ ) โŠ† ( โ„‚ ร— ( BaseSet โ€˜ ๐‘ˆ ) ) )
39 fnssres โŠข ( ( ๐‘† Fn ( โ„‚ ร— ( BaseSet โ€˜ ๐‘ˆ ) ) โˆง ( โ„‚ ร— ๐‘Œ ) โŠ† ( โ„‚ ร— ( BaseSet โ€˜ ๐‘ˆ ) ) ) โ†’ ( ๐‘† โ†พ ( โ„‚ ร— ๐‘Œ ) ) Fn ( โ„‚ ร— ๐‘Œ ) )
40 34 38 39 syl2anc โŠข ( ( ๐‘ˆ โˆˆ NrmCVec โˆง ๐‘Š โˆˆ ๐ป ) โ†’ ( ๐‘† โ†พ ( โ„‚ ร— ๐‘Œ ) ) Fn ( โ„‚ ร— ๐‘Œ ) )
41 eqfnov โŠข ( ( ๐‘… Fn ( โ„‚ ร— ๐‘Œ ) โˆง ( ๐‘† โ†พ ( โ„‚ ร— ๐‘Œ ) ) Fn ( โ„‚ ร— ๐‘Œ ) ) โ†’ ( ๐‘… = ( ๐‘† โ†พ ( โ„‚ ร— ๐‘Œ ) ) โ†” ( ( โ„‚ ร— ๐‘Œ ) = ( โ„‚ ร— ๐‘Œ ) โˆง โˆ€ ๐‘ฅ โˆˆ โ„‚ โˆ€ ๐‘ฆ โˆˆ ๐‘Œ ( ๐‘ฅ ๐‘… ๐‘ฆ ) = ( ๐‘ฅ ( ๐‘† โ†พ ( โ„‚ ร— ๐‘Œ ) ) ๐‘ฆ ) ) ) )
42 13 40 41 syl2anc โŠข ( ( ๐‘ˆ โˆˆ NrmCVec โˆง ๐‘Š โˆˆ ๐ป ) โ†’ ( ๐‘… = ( ๐‘† โ†พ ( โ„‚ ร— ๐‘Œ ) ) โ†” ( ( โ„‚ ร— ๐‘Œ ) = ( โ„‚ ร— ๐‘Œ ) โˆง โˆ€ ๐‘ฅ โˆˆ โ„‚ โˆ€ ๐‘ฆ โˆˆ ๐‘Œ ( ๐‘ฅ ๐‘… ๐‘ฆ ) = ( ๐‘ฅ ( ๐‘† โ†พ ( โ„‚ ร— ๐‘Œ ) ) ๐‘ฆ ) ) ) )
43 32 42 mpbird โŠข ( ( ๐‘ˆ โˆˆ NrmCVec โˆง ๐‘Š โˆˆ ๐ป ) โ†’ ๐‘… = ( ๐‘† โ†พ ( โ„‚ ร— ๐‘Œ ) ) )