Metamath Proof Explorer


Theorem isssp

Description: The predicate "is a subspace." (Contributed by NM, 26-Jan-2008) (New usage is discouraged.)

Ref Expression
Hypotheses isssp.g โŠข ๐บ = ( +๐‘ฃ โ€˜ ๐‘ˆ )
isssp.f โŠข ๐น = ( +๐‘ฃ โ€˜ ๐‘Š )
isssp.s โŠข ๐‘† = ( ยท๐‘ OLD โ€˜ ๐‘ˆ )
isssp.r โŠข ๐‘… = ( ยท๐‘ OLD โ€˜ ๐‘Š )
isssp.n โŠข ๐‘ = ( normCV โ€˜ ๐‘ˆ )
isssp.m โŠข ๐‘€ = ( normCV โ€˜ ๐‘Š )
isssp.h โŠข ๐ป = ( SubSp โ€˜ ๐‘ˆ )
Assertion isssp ( ๐‘ˆ โˆˆ NrmCVec โ†’ ( ๐‘Š โˆˆ ๐ป โ†” ( ๐‘Š โˆˆ NrmCVec โˆง ( ๐น โІ ๐บ โˆง ๐‘… โІ ๐‘† โˆง ๐‘€ โІ ๐‘ ) ) ) )

Proof

Step Hyp Ref Expression
1 isssp.g โŠข ๐บ = ( +๐‘ฃ โ€˜ ๐‘ˆ )
2 isssp.f โŠข ๐น = ( +๐‘ฃ โ€˜ ๐‘Š )
3 isssp.s โŠข ๐‘† = ( ยท๐‘ OLD โ€˜ ๐‘ˆ )
4 isssp.r โŠข ๐‘… = ( ยท๐‘ OLD โ€˜ ๐‘Š )
5 isssp.n โŠข ๐‘ = ( normCV โ€˜ ๐‘ˆ )
6 isssp.m โŠข ๐‘€ = ( normCV โ€˜ ๐‘Š )
7 isssp.h โŠข ๐ป = ( SubSp โ€˜ ๐‘ˆ )
8 1 3 5 7 sspval โŠข ( ๐‘ˆ โˆˆ NrmCVec โ†’ ๐ป = { ๐‘ค โˆˆ NrmCVec โˆฃ ( ( +๐‘ฃ โ€˜ ๐‘ค ) โІ ๐บ โˆง ( ยท๐‘ OLD โ€˜ ๐‘ค ) โІ ๐‘† โˆง ( normCV โ€˜ ๐‘ค ) โІ ๐‘ ) } )
9 8 eleq2d โŠข ( ๐‘ˆ โˆˆ NrmCVec โ†’ ( ๐‘Š โˆˆ ๐ป โ†” ๐‘Š โˆˆ { ๐‘ค โˆˆ NrmCVec โˆฃ ( ( +๐‘ฃ โ€˜ ๐‘ค ) โІ ๐บ โˆง ( ยท๐‘ OLD โ€˜ ๐‘ค ) โІ ๐‘† โˆง ( normCV โ€˜ ๐‘ค ) โІ ๐‘ ) } ) )
10 fveq2 โŠข ( ๐‘ค = ๐‘Š โ†’ ( +๐‘ฃ โ€˜ ๐‘ค ) = ( +๐‘ฃ โ€˜ ๐‘Š ) )
11 10 2 eqtr4di โŠข ( ๐‘ค = ๐‘Š โ†’ ( +๐‘ฃ โ€˜ ๐‘ค ) = ๐น )
12 11 sseq1d โŠข ( ๐‘ค = ๐‘Š โ†’ ( ( +๐‘ฃ โ€˜ ๐‘ค ) โІ ๐บ โ†” ๐น โІ ๐บ ) )
13 fveq2 โŠข ( ๐‘ค = ๐‘Š โ†’ ( ยท๐‘ OLD โ€˜ ๐‘ค ) = ( ยท๐‘ OLD โ€˜ ๐‘Š ) )
14 13 4 eqtr4di โŠข ( ๐‘ค = ๐‘Š โ†’ ( ยท๐‘ OLD โ€˜ ๐‘ค ) = ๐‘… )
15 14 sseq1d โŠข ( ๐‘ค = ๐‘Š โ†’ ( ( ยท๐‘ OLD โ€˜ ๐‘ค ) โІ ๐‘† โ†” ๐‘… โІ ๐‘† ) )
16 fveq2 โŠข ( ๐‘ค = ๐‘Š โ†’ ( normCV โ€˜ ๐‘ค ) = ( normCV โ€˜ ๐‘Š ) )
17 16 6 eqtr4di โŠข ( ๐‘ค = ๐‘Š โ†’ ( normCV โ€˜ ๐‘ค ) = ๐‘€ )
18 17 sseq1d โŠข ( ๐‘ค = ๐‘Š โ†’ ( ( normCV โ€˜ ๐‘ค ) โІ ๐‘ โ†” ๐‘€ โІ ๐‘ ) )
19 12 15 18 3anbi123d โŠข ( ๐‘ค = ๐‘Š โ†’ ( ( ( +๐‘ฃ โ€˜ ๐‘ค ) โІ ๐บ โˆง ( ยท๐‘ OLD โ€˜ ๐‘ค ) โІ ๐‘† โˆง ( normCV โ€˜ ๐‘ค ) โІ ๐‘ ) โ†” ( ๐น โІ ๐บ โˆง ๐‘… โІ ๐‘† โˆง ๐‘€ โІ ๐‘ ) ) )
20 19 elrab โŠข ( ๐‘Š โˆˆ { ๐‘ค โˆˆ NrmCVec โˆฃ ( ( +๐‘ฃ โ€˜ ๐‘ค ) โІ ๐บ โˆง ( ยท๐‘ OLD โ€˜ ๐‘ค ) โІ ๐‘† โˆง ( normCV โ€˜ ๐‘ค ) โІ ๐‘ ) } โ†” ( ๐‘Š โˆˆ NrmCVec โˆง ( ๐น โІ ๐บ โˆง ๐‘… โІ ๐‘† โˆง ๐‘€ โІ ๐‘ ) ) )
21 9 20 bitrdi โŠข ( ๐‘ˆ โˆˆ NrmCVec โ†’ ( ๐‘Š โˆˆ ๐ป โ†” ( ๐‘Š โˆˆ NrmCVec โˆง ( ๐น โІ ๐บ โˆง ๐‘… โІ ๐‘† โˆง ๐‘€ โІ ๐‘ ) ) ) )