MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sspval Structured version   Visualization version   GIF version

Theorem sspval 29971
Description: The set of all subspaces of a normed complex vector space. (Contributed by NM, 26-Jan-2008.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.)
Hypotheses
Ref Expression
sspval.g ๐บ = ( +๐‘ฃ โ€˜๐‘ˆ)
sspval.s ๐‘† = ( ยท๐‘ OLD โ€˜๐‘ˆ)
sspval.n ๐‘ = (normCVโ€˜๐‘ˆ)
sspval.h ๐ป = (SubSpโ€˜๐‘ˆ)
Assertion
Ref Expression
sspval (๐‘ˆ โˆˆ NrmCVec โ†’ ๐ป = {๐‘ค โˆˆ NrmCVec โˆฃ (( +๐‘ฃ โ€˜๐‘ค) โŠ† ๐บ โˆง ( ยท๐‘ OLD โ€˜๐‘ค) โŠ† ๐‘† โˆง (normCVโ€˜๐‘ค) โŠ† ๐‘)})
Distinct variable groups:   ๐‘ค,๐บ   ๐‘ค,๐‘   ๐‘ค,๐‘†   ๐‘ค,๐‘ˆ
Allowed substitution hint:   ๐ป(๐‘ค)

Proof of Theorem sspval
Dummy variable ๐‘ข is distinct from all other variables.
StepHypRef Expression
1 sspval.h . 2 ๐ป = (SubSpโ€˜๐‘ˆ)
2 fveq2 6891 . . . . . . 7 (๐‘ข = ๐‘ˆ โ†’ ( +๐‘ฃ โ€˜๐‘ข) = ( +๐‘ฃ โ€˜๐‘ˆ))
3 sspval.g . . . . . . 7 ๐บ = ( +๐‘ฃ โ€˜๐‘ˆ)
42, 3eqtr4di 2790 . . . . . 6 (๐‘ข = ๐‘ˆ โ†’ ( +๐‘ฃ โ€˜๐‘ข) = ๐บ)
54sseq2d 4014 . . . . 5 (๐‘ข = ๐‘ˆ โ†’ (( +๐‘ฃ โ€˜๐‘ค) โŠ† ( +๐‘ฃ โ€˜๐‘ข) โ†” ( +๐‘ฃ โ€˜๐‘ค) โŠ† ๐บ))
6 fveq2 6891 . . . . . . 7 (๐‘ข = ๐‘ˆ โ†’ ( ยท๐‘ OLD โ€˜๐‘ข) = ( ยท๐‘ OLD โ€˜๐‘ˆ))
7 sspval.s . . . . . . 7 ๐‘† = ( ยท๐‘ OLD โ€˜๐‘ˆ)
86, 7eqtr4di 2790 . . . . . 6 (๐‘ข = ๐‘ˆ โ†’ ( ยท๐‘ OLD โ€˜๐‘ข) = ๐‘†)
98sseq2d 4014 . . . . 5 (๐‘ข = ๐‘ˆ โ†’ (( ยท๐‘ OLD โ€˜๐‘ค) โŠ† ( ยท๐‘ OLD โ€˜๐‘ข) โ†” ( ยท๐‘ OLD โ€˜๐‘ค) โŠ† ๐‘†))
10 fveq2 6891 . . . . . . 7 (๐‘ข = ๐‘ˆ โ†’ (normCVโ€˜๐‘ข) = (normCVโ€˜๐‘ˆ))
11 sspval.n . . . . . . 7 ๐‘ = (normCVโ€˜๐‘ˆ)
1210, 11eqtr4di 2790 . . . . . 6 (๐‘ข = ๐‘ˆ โ†’ (normCVโ€˜๐‘ข) = ๐‘)
1312sseq2d 4014 . . . . 5 (๐‘ข = ๐‘ˆ โ†’ ((normCVโ€˜๐‘ค) โŠ† (normCVโ€˜๐‘ข) โ†” (normCVโ€˜๐‘ค) โŠ† ๐‘))
145, 9, 133anbi123d 1436 . . . 4 (๐‘ข = ๐‘ˆ โ†’ ((( +๐‘ฃ โ€˜๐‘ค) โŠ† ( +๐‘ฃ โ€˜๐‘ข) โˆง ( ยท๐‘ OLD โ€˜๐‘ค) โŠ† ( ยท๐‘ OLD โ€˜๐‘ข) โˆง (normCVโ€˜๐‘ค) โŠ† (normCVโ€˜๐‘ข)) โ†” (( +๐‘ฃ โ€˜๐‘ค) โŠ† ๐บ โˆง ( ยท๐‘ OLD โ€˜๐‘ค) โŠ† ๐‘† โˆง (normCVโ€˜๐‘ค) โŠ† ๐‘)))
1514rabbidv 3440 . . 3 (๐‘ข = ๐‘ˆ โ†’ {๐‘ค โˆˆ NrmCVec โˆฃ (( +๐‘ฃ โ€˜๐‘ค) โŠ† ( +๐‘ฃ โ€˜๐‘ข) โˆง ( ยท๐‘ OLD โ€˜๐‘ค) โŠ† ( ยท๐‘ OLD โ€˜๐‘ข) โˆง (normCVโ€˜๐‘ค) โŠ† (normCVโ€˜๐‘ข))} = {๐‘ค โˆˆ NrmCVec โˆฃ (( +๐‘ฃ โ€˜๐‘ค) โŠ† ๐บ โˆง ( ยท๐‘ OLD โ€˜๐‘ค) โŠ† ๐‘† โˆง (normCVโ€˜๐‘ค) โŠ† ๐‘)})
16 df-ssp 29970 . . 3 SubSp = (๐‘ข โˆˆ NrmCVec โ†ฆ {๐‘ค โˆˆ NrmCVec โˆฃ (( +๐‘ฃ โ€˜๐‘ค) โŠ† ( +๐‘ฃ โ€˜๐‘ข) โˆง ( ยท๐‘ OLD โ€˜๐‘ค) โŠ† ( ยท๐‘ OLD โ€˜๐‘ข) โˆง (normCVโ€˜๐‘ค) โŠ† (normCVโ€˜๐‘ข))})
173fvexi 6905 . . . . . . 7 ๐บ โˆˆ V
1817pwex 5378 . . . . . 6 ๐’ซ ๐บ โˆˆ V
197fvexi 6905 . . . . . . 7 ๐‘† โˆˆ V
2019pwex 5378 . . . . . 6 ๐’ซ ๐‘† โˆˆ V
2118, 20xpex 7739 . . . . 5 (๐’ซ ๐บ ร— ๐’ซ ๐‘†) โˆˆ V
2211fvexi 6905 . . . . . 6 ๐‘ โˆˆ V
2322pwex 5378 . . . . 5 ๐’ซ ๐‘ โˆˆ V
2421, 23xpex 7739 . . . 4 ((๐’ซ ๐บ ร— ๐’ซ ๐‘†) ร— ๐’ซ ๐‘) โˆˆ V
25 rabss 4069 . . . . 5 ({๐‘ค โˆˆ NrmCVec โˆฃ (( +๐‘ฃ โ€˜๐‘ค) โŠ† ๐บ โˆง ( ยท๐‘ OLD โ€˜๐‘ค) โŠ† ๐‘† โˆง (normCVโ€˜๐‘ค) โŠ† ๐‘)} โŠ† ((๐’ซ ๐บ ร— ๐’ซ ๐‘†) ร— ๐’ซ ๐‘) โ†” โˆ€๐‘ค โˆˆ NrmCVec ((( +๐‘ฃ โ€˜๐‘ค) โŠ† ๐บ โˆง ( ยท๐‘ OLD โ€˜๐‘ค) โŠ† ๐‘† โˆง (normCVโ€˜๐‘ค) โŠ† ๐‘) โ†’ ๐‘ค โˆˆ ((๐’ซ ๐บ ร— ๐’ซ ๐‘†) ร— ๐’ซ ๐‘)))
26 fvex 6904 . . . . . . . . . 10 ( +๐‘ฃ โ€˜๐‘ค) โˆˆ V
2726elpw 4606 . . . . . . . . 9 (( +๐‘ฃ โ€˜๐‘ค) โˆˆ ๐’ซ ๐บ โ†” ( +๐‘ฃ โ€˜๐‘ค) โŠ† ๐บ)
28 fvex 6904 . . . . . . . . . 10 ( ยท๐‘ OLD โ€˜๐‘ค) โˆˆ V
2928elpw 4606 . . . . . . . . 9 (( ยท๐‘ OLD โ€˜๐‘ค) โˆˆ ๐’ซ ๐‘† โ†” ( ยท๐‘ OLD โ€˜๐‘ค) โŠ† ๐‘†)
30 opelxpi 5713 . . . . . . . . 9 ((( +๐‘ฃ โ€˜๐‘ค) โˆˆ ๐’ซ ๐บ โˆง ( ยท๐‘ OLD โ€˜๐‘ค) โˆˆ ๐’ซ ๐‘†) โ†’ โŸจ( +๐‘ฃ โ€˜๐‘ค), ( ยท๐‘ OLD โ€˜๐‘ค)โŸฉ โˆˆ (๐’ซ ๐บ ร— ๐’ซ ๐‘†))
3127, 29, 30syl2anbr 599 . . . . . . . 8 ((( +๐‘ฃ โ€˜๐‘ค) โŠ† ๐บ โˆง ( ยท๐‘ OLD โ€˜๐‘ค) โŠ† ๐‘†) โ†’ โŸจ( +๐‘ฃ โ€˜๐‘ค), ( ยท๐‘ OLD โ€˜๐‘ค)โŸฉ โˆˆ (๐’ซ ๐บ ร— ๐’ซ ๐‘†))
32 fvex 6904 . . . . . . . . . 10 (normCVโ€˜๐‘ค) โˆˆ V
3332elpw 4606 . . . . . . . . 9 ((normCVโ€˜๐‘ค) โˆˆ ๐’ซ ๐‘ โ†” (normCVโ€˜๐‘ค) โŠ† ๐‘)
3433biimpri 227 . . . . . . . 8 ((normCVโ€˜๐‘ค) โŠ† ๐‘ โ†’ (normCVโ€˜๐‘ค) โˆˆ ๐’ซ ๐‘)
35 opelxpi 5713 . . . . . . . 8 ((โŸจ( +๐‘ฃ โ€˜๐‘ค), ( ยท๐‘ OLD โ€˜๐‘ค)โŸฉ โˆˆ (๐’ซ ๐บ ร— ๐’ซ ๐‘†) โˆง (normCVโ€˜๐‘ค) โˆˆ ๐’ซ ๐‘) โ†’ โŸจโŸจ( +๐‘ฃ โ€˜๐‘ค), ( ยท๐‘ OLD โ€˜๐‘ค)โŸฉ, (normCVโ€˜๐‘ค)โŸฉ โˆˆ ((๐’ซ ๐บ ร— ๐’ซ ๐‘†) ร— ๐’ซ ๐‘))
3631, 34, 35syl2an 596 . . . . . . 7 (((( +๐‘ฃ โ€˜๐‘ค) โŠ† ๐บ โˆง ( ยท๐‘ OLD โ€˜๐‘ค) โŠ† ๐‘†) โˆง (normCVโ€˜๐‘ค) โŠ† ๐‘) โ†’ โŸจโŸจ( +๐‘ฃ โ€˜๐‘ค), ( ยท๐‘ OLD โ€˜๐‘ค)โŸฉ, (normCVโ€˜๐‘ค)โŸฉ โˆˆ ((๐’ซ ๐บ ร— ๐’ซ ๐‘†) ร— ๐’ซ ๐‘))
37363impa 1110 . . . . . 6 ((( +๐‘ฃ โ€˜๐‘ค) โŠ† ๐บ โˆง ( ยท๐‘ OLD โ€˜๐‘ค) โŠ† ๐‘† โˆง (normCVโ€˜๐‘ค) โŠ† ๐‘) โ†’ โŸจโŸจ( +๐‘ฃ โ€˜๐‘ค), ( ยท๐‘ OLD โ€˜๐‘ค)โŸฉ, (normCVโ€˜๐‘ค)โŸฉ โˆˆ ((๐’ซ ๐บ ร— ๐’ซ ๐‘†) ร— ๐’ซ ๐‘))
38 eqid 2732 . . . . . . . 8 ( +๐‘ฃ โ€˜๐‘ค) = ( +๐‘ฃ โ€˜๐‘ค)
39 eqid 2732 . . . . . . . 8 ( ยท๐‘ OLD โ€˜๐‘ค) = ( ยท๐‘ OLD โ€˜๐‘ค)
40 eqid 2732 . . . . . . . 8 (normCVโ€˜๐‘ค) = (normCVโ€˜๐‘ค)
4138, 39, 40nvop 29924 . . . . . . 7 (๐‘ค โˆˆ NrmCVec โ†’ ๐‘ค = โŸจโŸจ( +๐‘ฃ โ€˜๐‘ค), ( ยท๐‘ OLD โ€˜๐‘ค)โŸฉ, (normCVโ€˜๐‘ค)โŸฉ)
4241eleq1d 2818 . . . . . 6 (๐‘ค โˆˆ NrmCVec โ†’ (๐‘ค โˆˆ ((๐’ซ ๐บ ร— ๐’ซ ๐‘†) ร— ๐’ซ ๐‘) โ†” โŸจโŸจ( +๐‘ฃ โ€˜๐‘ค), ( ยท๐‘ OLD โ€˜๐‘ค)โŸฉ, (normCVโ€˜๐‘ค)โŸฉ โˆˆ ((๐’ซ ๐บ ร— ๐’ซ ๐‘†) ร— ๐’ซ ๐‘)))
4337, 42imbitrrid 245 . . . . 5 (๐‘ค โˆˆ NrmCVec โ†’ ((( +๐‘ฃ โ€˜๐‘ค) โŠ† ๐บ โˆง ( ยท๐‘ OLD โ€˜๐‘ค) โŠ† ๐‘† โˆง (normCVโ€˜๐‘ค) โŠ† ๐‘) โ†’ ๐‘ค โˆˆ ((๐’ซ ๐บ ร— ๐’ซ ๐‘†) ร— ๐’ซ ๐‘)))
4425, 43mprgbir 3068 . . . 4 {๐‘ค โˆˆ NrmCVec โˆฃ (( +๐‘ฃ โ€˜๐‘ค) โŠ† ๐บ โˆง ( ยท๐‘ OLD โ€˜๐‘ค) โŠ† ๐‘† โˆง (normCVโ€˜๐‘ค) โŠ† ๐‘)} โŠ† ((๐’ซ ๐บ ร— ๐’ซ ๐‘†) ร— ๐’ซ ๐‘)
4524, 44ssexi 5322 . . 3 {๐‘ค โˆˆ NrmCVec โˆฃ (( +๐‘ฃ โ€˜๐‘ค) โŠ† ๐บ โˆง ( ยท๐‘ OLD โ€˜๐‘ค) โŠ† ๐‘† โˆง (normCVโ€˜๐‘ค) โŠ† ๐‘)} โˆˆ V
4615, 16, 45fvmpt 6998 . 2 (๐‘ˆ โˆˆ NrmCVec โ†’ (SubSpโ€˜๐‘ˆ) = {๐‘ค โˆˆ NrmCVec โˆฃ (( +๐‘ฃ โ€˜๐‘ค) โŠ† ๐บ โˆง ( ยท๐‘ OLD โ€˜๐‘ค) โŠ† ๐‘† โˆง (normCVโ€˜๐‘ค) โŠ† ๐‘)})
471, 46eqtrid 2784 1 (๐‘ˆ โˆˆ NrmCVec โ†’ ๐ป = {๐‘ค โˆˆ NrmCVec โˆฃ (( +๐‘ฃ โ€˜๐‘ค) โŠ† ๐บ โˆง ( ยท๐‘ OLD โ€˜๐‘ค) โŠ† ๐‘† โˆง (normCVโ€˜๐‘ค) โŠ† ๐‘)})
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โˆง wa 396   โˆง w3a 1087   = wceq 1541   โˆˆ wcel 2106  {crab 3432   โŠ† wss 3948  ๐’ซ cpw 4602  โŸจcop 4634   ร— cxp 5674  โ€˜cfv 6543  NrmCVeccnv 29832   +๐‘ฃ cpv 29833   ยท๐‘ OLD cns 29835  normCVcnmcv 29838  SubSpcss 29969
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7724
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-fo 6549  df-fv 6551  df-oprab 7412  df-1st 7974  df-2nd 7975  df-vc 29807  df-nv 29840  df-va 29843  df-sm 29845  df-nmcv 29848  df-ssp 29970
This theorem is referenced by:  isssp  29972
  Copyright terms: Public domain W3C validator