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

Theorem sspval 29976
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 6892 . . . . . . 7 (๐‘ข = ๐‘ˆ โ†’ ( +๐‘ฃ โ€˜๐‘ข) = ( +๐‘ฃ โ€˜๐‘ˆ))
3 sspval.g . . . . . . 7 ๐บ = ( +๐‘ฃ โ€˜๐‘ˆ)
42, 3eqtr4di 2791 . . . . . 6 (๐‘ข = ๐‘ˆ โ†’ ( +๐‘ฃ โ€˜๐‘ข) = ๐บ)
54sseq2d 4015 . . . . 5 (๐‘ข = ๐‘ˆ โ†’ (( +๐‘ฃ โ€˜๐‘ค) โŠ† ( +๐‘ฃ โ€˜๐‘ข) โ†” ( +๐‘ฃ โ€˜๐‘ค) โŠ† ๐บ))
6 fveq2 6892 . . . . . . 7 (๐‘ข = ๐‘ˆ โ†’ ( ยท๐‘ OLD โ€˜๐‘ข) = ( ยท๐‘ OLD โ€˜๐‘ˆ))
7 sspval.s . . . . . . 7 ๐‘† = ( ยท๐‘ OLD โ€˜๐‘ˆ)
86, 7eqtr4di 2791 . . . . . 6 (๐‘ข = ๐‘ˆ โ†’ ( ยท๐‘ OLD โ€˜๐‘ข) = ๐‘†)
98sseq2d 4015 . . . . 5 (๐‘ข = ๐‘ˆ โ†’ (( ยท๐‘ OLD โ€˜๐‘ค) โŠ† ( ยท๐‘ OLD โ€˜๐‘ข) โ†” ( ยท๐‘ OLD โ€˜๐‘ค) โŠ† ๐‘†))
10 fveq2 6892 . . . . . . 7 (๐‘ข = ๐‘ˆ โ†’ (normCVโ€˜๐‘ข) = (normCVโ€˜๐‘ˆ))
11 sspval.n . . . . . . 7 ๐‘ = (normCVโ€˜๐‘ˆ)
1210, 11eqtr4di 2791 . . . . . 6 (๐‘ข = ๐‘ˆ โ†’ (normCVโ€˜๐‘ข) = ๐‘)
1312sseq2d 4015 . . . . 5 (๐‘ข = ๐‘ˆ โ†’ ((normCVโ€˜๐‘ค) โŠ† (normCVโ€˜๐‘ข) โ†” (normCVโ€˜๐‘ค) โŠ† ๐‘))
145, 9, 133anbi123d 1437 . . . 4 (๐‘ข = ๐‘ˆ โ†’ ((( +๐‘ฃ โ€˜๐‘ค) โŠ† ( +๐‘ฃ โ€˜๐‘ข) โˆง ( ยท๐‘ OLD โ€˜๐‘ค) โŠ† ( ยท๐‘ OLD โ€˜๐‘ข) โˆง (normCVโ€˜๐‘ค) โŠ† (normCVโ€˜๐‘ข)) โ†” (( +๐‘ฃ โ€˜๐‘ค) โŠ† ๐บ โˆง ( ยท๐‘ OLD โ€˜๐‘ค) โŠ† ๐‘† โˆง (normCVโ€˜๐‘ค) โŠ† ๐‘)))
1514rabbidv 3441 . . 3 (๐‘ข = ๐‘ˆ โ†’ {๐‘ค โˆˆ NrmCVec โˆฃ (( +๐‘ฃ โ€˜๐‘ค) โŠ† ( +๐‘ฃ โ€˜๐‘ข) โˆง ( ยท๐‘ OLD โ€˜๐‘ค) โŠ† ( ยท๐‘ OLD โ€˜๐‘ข) โˆง (normCVโ€˜๐‘ค) โŠ† (normCVโ€˜๐‘ข))} = {๐‘ค โˆˆ NrmCVec โˆฃ (( +๐‘ฃ โ€˜๐‘ค) โŠ† ๐บ โˆง ( ยท๐‘ OLD โ€˜๐‘ค) โŠ† ๐‘† โˆง (normCVโ€˜๐‘ค) โŠ† ๐‘)})
16 df-ssp 29975 . . 3 SubSp = (๐‘ข โˆˆ NrmCVec โ†ฆ {๐‘ค โˆˆ NrmCVec โˆฃ (( +๐‘ฃ โ€˜๐‘ค) โŠ† ( +๐‘ฃ โ€˜๐‘ข) โˆง ( ยท๐‘ OLD โ€˜๐‘ค) โŠ† ( ยท๐‘ OLD โ€˜๐‘ข) โˆง (normCVโ€˜๐‘ค) โŠ† (normCVโ€˜๐‘ข))})
173fvexi 6906 . . . . . . 7 ๐บ โˆˆ V
1817pwex 5379 . . . . . 6 ๐’ซ ๐บ โˆˆ V
197fvexi 6906 . . . . . . 7 ๐‘† โˆˆ V
2019pwex 5379 . . . . . 6 ๐’ซ ๐‘† โˆˆ V
2118, 20xpex 7740 . . . . 5 (๐’ซ ๐บ ร— ๐’ซ ๐‘†) โˆˆ V
2211fvexi 6906 . . . . . 6 ๐‘ โˆˆ V
2322pwex 5379 . . . . 5 ๐’ซ ๐‘ โˆˆ V
2421, 23xpex 7740 . . . 4 ((๐’ซ ๐บ ร— ๐’ซ ๐‘†) ร— ๐’ซ ๐‘) โˆˆ V
25 rabss 4070 . . . . 5 ({๐‘ค โˆˆ NrmCVec โˆฃ (( +๐‘ฃ โ€˜๐‘ค) โŠ† ๐บ โˆง ( ยท๐‘ OLD โ€˜๐‘ค) โŠ† ๐‘† โˆง (normCVโ€˜๐‘ค) โŠ† ๐‘)} โŠ† ((๐’ซ ๐บ ร— ๐’ซ ๐‘†) ร— ๐’ซ ๐‘) โ†” โˆ€๐‘ค โˆˆ NrmCVec ((( +๐‘ฃ โ€˜๐‘ค) โŠ† ๐บ โˆง ( ยท๐‘ OLD โ€˜๐‘ค) โŠ† ๐‘† โˆง (normCVโ€˜๐‘ค) โŠ† ๐‘) โ†’ ๐‘ค โˆˆ ((๐’ซ ๐บ ร— ๐’ซ ๐‘†) ร— ๐’ซ ๐‘)))
26 fvex 6905 . . . . . . . . . 10 ( +๐‘ฃ โ€˜๐‘ค) โˆˆ V
2726elpw 4607 . . . . . . . . 9 (( +๐‘ฃ โ€˜๐‘ค) โˆˆ ๐’ซ ๐บ โ†” ( +๐‘ฃ โ€˜๐‘ค) โŠ† ๐บ)
28 fvex 6905 . . . . . . . . . 10 ( ยท๐‘ OLD โ€˜๐‘ค) โˆˆ V
2928elpw 4607 . . . . . . . . 9 (( ยท๐‘ OLD โ€˜๐‘ค) โˆˆ ๐’ซ ๐‘† โ†” ( ยท๐‘ OLD โ€˜๐‘ค) โŠ† ๐‘†)
30 opelxpi 5714 . . . . . . . . 9 ((( +๐‘ฃ โ€˜๐‘ค) โˆˆ ๐’ซ ๐บ โˆง ( ยท๐‘ OLD โ€˜๐‘ค) โˆˆ ๐’ซ ๐‘†) โ†’ โŸจ( +๐‘ฃ โ€˜๐‘ค), ( ยท๐‘ OLD โ€˜๐‘ค)โŸฉ โˆˆ (๐’ซ ๐บ ร— ๐’ซ ๐‘†))
3127, 29, 30syl2anbr 600 . . . . . . . 8 ((( +๐‘ฃ โ€˜๐‘ค) โŠ† ๐บ โˆง ( ยท๐‘ OLD โ€˜๐‘ค) โŠ† ๐‘†) โ†’ โŸจ( +๐‘ฃ โ€˜๐‘ค), ( ยท๐‘ OLD โ€˜๐‘ค)โŸฉ โˆˆ (๐’ซ ๐บ ร— ๐’ซ ๐‘†))
32 fvex 6905 . . . . . . . . . 10 (normCVโ€˜๐‘ค) โˆˆ V
3332elpw 4607 . . . . . . . . 9 ((normCVโ€˜๐‘ค) โˆˆ ๐’ซ ๐‘ โ†” (normCVโ€˜๐‘ค) โŠ† ๐‘)
3433biimpri 227 . . . . . . . 8 ((normCVโ€˜๐‘ค) โŠ† ๐‘ โ†’ (normCVโ€˜๐‘ค) โˆˆ ๐’ซ ๐‘)
35 opelxpi 5714 . . . . . . . 8 ((โŸจ( +๐‘ฃ โ€˜๐‘ค), ( ยท๐‘ OLD โ€˜๐‘ค)โŸฉ โˆˆ (๐’ซ ๐บ ร— ๐’ซ ๐‘†) โˆง (normCVโ€˜๐‘ค) โˆˆ ๐’ซ ๐‘) โ†’ โŸจโŸจ( +๐‘ฃ โ€˜๐‘ค), ( ยท๐‘ OLD โ€˜๐‘ค)โŸฉ, (normCVโ€˜๐‘ค)โŸฉ โˆˆ ((๐’ซ ๐บ ร— ๐’ซ ๐‘†) ร— ๐’ซ ๐‘))
3631, 34, 35syl2an 597 . . . . . . 7 (((( +๐‘ฃ โ€˜๐‘ค) โŠ† ๐บ โˆง ( ยท๐‘ OLD โ€˜๐‘ค) โŠ† ๐‘†) โˆง (normCVโ€˜๐‘ค) โŠ† ๐‘) โ†’ โŸจโŸจ( +๐‘ฃ โ€˜๐‘ค), ( ยท๐‘ OLD โ€˜๐‘ค)โŸฉ, (normCVโ€˜๐‘ค)โŸฉ โˆˆ ((๐’ซ ๐บ ร— ๐’ซ ๐‘†) ร— ๐’ซ ๐‘))
37363impa 1111 . . . . . 6 ((( +๐‘ฃ โ€˜๐‘ค) โŠ† ๐บ โˆง ( ยท๐‘ OLD โ€˜๐‘ค) โŠ† ๐‘† โˆง (normCVโ€˜๐‘ค) โŠ† ๐‘) โ†’ โŸจโŸจ( +๐‘ฃ โ€˜๐‘ค), ( ยท๐‘ OLD โ€˜๐‘ค)โŸฉ, (normCVโ€˜๐‘ค)โŸฉ โˆˆ ((๐’ซ ๐บ ร— ๐’ซ ๐‘†) ร— ๐’ซ ๐‘))
38 eqid 2733 . . . . . . . 8 ( +๐‘ฃ โ€˜๐‘ค) = ( +๐‘ฃ โ€˜๐‘ค)
39 eqid 2733 . . . . . . . 8 ( ยท๐‘ OLD โ€˜๐‘ค) = ( ยท๐‘ OLD โ€˜๐‘ค)
40 eqid 2733 . . . . . . . 8 (normCVโ€˜๐‘ค) = (normCVโ€˜๐‘ค)
4138, 39, 40nvop 29929 . . . . . . 7 (๐‘ค โˆˆ NrmCVec โ†’ ๐‘ค = โŸจโŸจ( +๐‘ฃ โ€˜๐‘ค), ( ยท๐‘ OLD โ€˜๐‘ค)โŸฉ, (normCVโ€˜๐‘ค)โŸฉ)
4241eleq1d 2819 . . . . . 6 (๐‘ค โˆˆ NrmCVec โ†’ (๐‘ค โˆˆ ((๐’ซ ๐บ ร— ๐’ซ ๐‘†) ร— ๐’ซ ๐‘) โ†” โŸจโŸจ( +๐‘ฃ โ€˜๐‘ค), ( ยท๐‘ OLD โ€˜๐‘ค)โŸฉ, (normCVโ€˜๐‘ค)โŸฉ โˆˆ ((๐’ซ ๐บ ร— ๐’ซ ๐‘†) ร— ๐’ซ ๐‘)))
4337, 42imbitrrid 245 . . . . 5 (๐‘ค โˆˆ NrmCVec โ†’ ((( +๐‘ฃ โ€˜๐‘ค) โŠ† ๐บ โˆง ( ยท๐‘ OLD โ€˜๐‘ค) โŠ† ๐‘† โˆง (normCVโ€˜๐‘ค) โŠ† ๐‘) โ†’ ๐‘ค โˆˆ ((๐’ซ ๐บ ร— ๐’ซ ๐‘†) ร— ๐’ซ ๐‘)))
4425, 43mprgbir 3069 . . . 4 {๐‘ค โˆˆ NrmCVec โˆฃ (( +๐‘ฃ โ€˜๐‘ค) โŠ† ๐บ โˆง ( ยท๐‘ OLD โ€˜๐‘ค) โŠ† ๐‘† โˆง (normCVโ€˜๐‘ค) โŠ† ๐‘)} โŠ† ((๐’ซ ๐บ ร— ๐’ซ ๐‘†) ร— ๐’ซ ๐‘)
4524, 44ssexi 5323 . . 3 {๐‘ค โˆˆ NrmCVec โˆฃ (( +๐‘ฃ โ€˜๐‘ค) โŠ† ๐บ โˆง ( ยท๐‘ OLD โ€˜๐‘ค) โŠ† ๐‘† โˆง (normCVโ€˜๐‘ค) โŠ† ๐‘)} โˆˆ V
4615, 16, 45fvmpt 6999 . 2 (๐‘ˆ โˆˆ NrmCVec โ†’ (SubSpโ€˜๐‘ˆ) = {๐‘ค โˆˆ NrmCVec โˆฃ (( +๐‘ฃ โ€˜๐‘ค) โŠ† ๐บ โˆง ( ยท๐‘ OLD โ€˜๐‘ค) โŠ† ๐‘† โˆง (normCVโ€˜๐‘ค) โŠ† ๐‘)})
471, 46eqtrid 2785 1 (๐‘ˆ โˆˆ NrmCVec โ†’ ๐ป = {๐‘ค โˆˆ NrmCVec โˆฃ (( +๐‘ฃ โ€˜๐‘ค) โŠ† ๐บ โˆง ( ยท๐‘ OLD โ€˜๐‘ค) โŠ† ๐‘† โˆง (normCVโ€˜๐‘ค) โŠ† ๐‘)})
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โˆง wa 397   โˆง w3a 1088   = wceq 1542   โˆˆ wcel 2107  {crab 3433   โŠ† wss 3949  ๐’ซ cpw 4603  โŸจcop 4635   ร— cxp 5675  โ€˜cfv 6544  NrmCVeccnv 29837   +๐‘ฃ cpv 29838   ยท๐‘ OLD cns 29840  normCVcnmcv 29843  SubSpcss 29974
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5575  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-fo 6550  df-fv 6552  df-oprab 7413  df-1st 7975  df-2nd 7976  df-vc 29812  df-nv 29845  df-va 29848  df-sm 29850  df-nmcv 29853  df-ssp 29975
This theorem is referenced by:  isssp  29977
  Copyright terms: Public domain W3C validator