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

Theorem sspval 29707
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 6847 . . . . . . 7 (๐‘ข = ๐‘ˆ โ†’ ( +๐‘ฃ โ€˜๐‘ข) = ( +๐‘ฃ โ€˜๐‘ˆ))
3 sspval.g . . . . . . 7 ๐บ = ( +๐‘ฃ โ€˜๐‘ˆ)
42, 3eqtr4di 2795 . . . . . 6 (๐‘ข = ๐‘ˆ โ†’ ( +๐‘ฃ โ€˜๐‘ข) = ๐บ)
54sseq2d 3981 . . . . 5 (๐‘ข = ๐‘ˆ โ†’ (( +๐‘ฃ โ€˜๐‘ค) โŠ† ( +๐‘ฃ โ€˜๐‘ข) โ†” ( +๐‘ฃ โ€˜๐‘ค) โŠ† ๐บ))
6 fveq2 6847 . . . . . . 7 (๐‘ข = ๐‘ˆ โ†’ ( ยท๐‘ OLD โ€˜๐‘ข) = ( ยท๐‘ OLD โ€˜๐‘ˆ))
7 sspval.s . . . . . . 7 ๐‘† = ( ยท๐‘ OLD โ€˜๐‘ˆ)
86, 7eqtr4di 2795 . . . . . 6 (๐‘ข = ๐‘ˆ โ†’ ( ยท๐‘ OLD โ€˜๐‘ข) = ๐‘†)
98sseq2d 3981 . . . . 5 (๐‘ข = ๐‘ˆ โ†’ (( ยท๐‘ OLD โ€˜๐‘ค) โŠ† ( ยท๐‘ OLD โ€˜๐‘ข) โ†” ( ยท๐‘ OLD โ€˜๐‘ค) โŠ† ๐‘†))
10 fveq2 6847 . . . . . . 7 (๐‘ข = ๐‘ˆ โ†’ (normCVโ€˜๐‘ข) = (normCVโ€˜๐‘ˆ))
11 sspval.n . . . . . . 7 ๐‘ = (normCVโ€˜๐‘ˆ)
1210, 11eqtr4di 2795 . . . . . 6 (๐‘ข = ๐‘ˆ โ†’ (normCVโ€˜๐‘ข) = ๐‘)
1312sseq2d 3981 . . . . 5 (๐‘ข = ๐‘ˆ โ†’ ((normCVโ€˜๐‘ค) โŠ† (normCVโ€˜๐‘ข) โ†” (normCVโ€˜๐‘ค) โŠ† ๐‘))
145, 9, 133anbi123d 1437 . . . 4 (๐‘ข = ๐‘ˆ โ†’ ((( +๐‘ฃ โ€˜๐‘ค) โŠ† ( +๐‘ฃ โ€˜๐‘ข) โˆง ( ยท๐‘ OLD โ€˜๐‘ค) โŠ† ( ยท๐‘ OLD โ€˜๐‘ข) โˆง (normCVโ€˜๐‘ค) โŠ† (normCVโ€˜๐‘ข)) โ†” (( +๐‘ฃ โ€˜๐‘ค) โŠ† ๐บ โˆง ( ยท๐‘ OLD โ€˜๐‘ค) โŠ† ๐‘† โˆง (normCVโ€˜๐‘ค) โŠ† ๐‘)))
1514rabbidv 3418 . . 3 (๐‘ข = ๐‘ˆ โ†’ {๐‘ค โˆˆ NrmCVec โˆฃ (( +๐‘ฃ โ€˜๐‘ค) โŠ† ( +๐‘ฃ โ€˜๐‘ข) โˆง ( ยท๐‘ OLD โ€˜๐‘ค) โŠ† ( ยท๐‘ OLD โ€˜๐‘ข) โˆง (normCVโ€˜๐‘ค) โŠ† (normCVโ€˜๐‘ข))} = {๐‘ค โˆˆ NrmCVec โˆฃ (( +๐‘ฃ โ€˜๐‘ค) โŠ† ๐บ โˆง ( ยท๐‘ OLD โ€˜๐‘ค) โŠ† ๐‘† โˆง (normCVโ€˜๐‘ค) โŠ† ๐‘)})
16 df-ssp 29706 . . 3 SubSp = (๐‘ข โˆˆ NrmCVec โ†ฆ {๐‘ค โˆˆ NrmCVec โˆฃ (( +๐‘ฃ โ€˜๐‘ค) โŠ† ( +๐‘ฃ โ€˜๐‘ข) โˆง ( ยท๐‘ OLD โ€˜๐‘ค) โŠ† ( ยท๐‘ OLD โ€˜๐‘ข) โˆง (normCVโ€˜๐‘ค) โŠ† (normCVโ€˜๐‘ข))})
173fvexi 6861 . . . . . . 7 ๐บ โˆˆ V
1817pwex 5340 . . . . . 6 ๐’ซ ๐บ โˆˆ V
197fvexi 6861 . . . . . . 7 ๐‘† โˆˆ V
2019pwex 5340 . . . . . 6 ๐’ซ ๐‘† โˆˆ V
2118, 20xpex 7692 . . . . 5 (๐’ซ ๐บ ร— ๐’ซ ๐‘†) โˆˆ V
2211fvexi 6861 . . . . . 6 ๐‘ โˆˆ V
2322pwex 5340 . . . . 5 ๐’ซ ๐‘ โˆˆ V
2421, 23xpex 7692 . . . 4 ((๐’ซ ๐บ ร— ๐’ซ ๐‘†) ร— ๐’ซ ๐‘) โˆˆ V
25 rabss 4034 . . . . 5 ({๐‘ค โˆˆ NrmCVec โˆฃ (( +๐‘ฃ โ€˜๐‘ค) โŠ† ๐บ โˆง ( ยท๐‘ OLD โ€˜๐‘ค) โŠ† ๐‘† โˆง (normCVโ€˜๐‘ค) โŠ† ๐‘)} โŠ† ((๐’ซ ๐บ ร— ๐’ซ ๐‘†) ร— ๐’ซ ๐‘) โ†” โˆ€๐‘ค โˆˆ NrmCVec ((( +๐‘ฃ โ€˜๐‘ค) โŠ† ๐บ โˆง ( ยท๐‘ OLD โ€˜๐‘ค) โŠ† ๐‘† โˆง (normCVโ€˜๐‘ค) โŠ† ๐‘) โ†’ ๐‘ค โˆˆ ((๐’ซ ๐บ ร— ๐’ซ ๐‘†) ร— ๐’ซ ๐‘)))
26 fvex 6860 . . . . . . . . . 10 ( +๐‘ฃ โ€˜๐‘ค) โˆˆ V
2726elpw 4569 . . . . . . . . 9 (( +๐‘ฃ โ€˜๐‘ค) โˆˆ ๐’ซ ๐บ โ†” ( +๐‘ฃ โ€˜๐‘ค) โŠ† ๐บ)
28 fvex 6860 . . . . . . . . . 10 ( ยท๐‘ OLD โ€˜๐‘ค) โˆˆ V
2928elpw 4569 . . . . . . . . 9 (( ยท๐‘ OLD โ€˜๐‘ค) โˆˆ ๐’ซ ๐‘† โ†” ( ยท๐‘ OLD โ€˜๐‘ค) โŠ† ๐‘†)
30 opelxpi 5675 . . . . . . . . 9 ((( +๐‘ฃ โ€˜๐‘ค) โˆˆ ๐’ซ ๐บ โˆง ( ยท๐‘ OLD โ€˜๐‘ค) โˆˆ ๐’ซ ๐‘†) โ†’ โŸจ( +๐‘ฃ โ€˜๐‘ค), ( ยท๐‘ OLD โ€˜๐‘ค)โŸฉ โˆˆ (๐’ซ ๐บ ร— ๐’ซ ๐‘†))
3127, 29, 30syl2anbr 600 . . . . . . . 8 ((( +๐‘ฃ โ€˜๐‘ค) โŠ† ๐บ โˆง ( ยท๐‘ OLD โ€˜๐‘ค) โŠ† ๐‘†) โ†’ โŸจ( +๐‘ฃ โ€˜๐‘ค), ( ยท๐‘ OLD โ€˜๐‘ค)โŸฉ โˆˆ (๐’ซ ๐บ ร— ๐’ซ ๐‘†))
32 fvex 6860 . . . . . . . . . 10 (normCVโ€˜๐‘ค) โˆˆ V
3332elpw 4569 . . . . . . . . 9 ((normCVโ€˜๐‘ค) โˆˆ ๐’ซ ๐‘ โ†” (normCVโ€˜๐‘ค) โŠ† ๐‘)
3433biimpri 227 . . . . . . . 8 ((normCVโ€˜๐‘ค) โŠ† ๐‘ โ†’ (normCVโ€˜๐‘ค) โˆˆ ๐’ซ ๐‘)
35 opelxpi 5675 . . . . . . . 8 ((โŸจ( +๐‘ฃ โ€˜๐‘ค), ( ยท๐‘ OLD โ€˜๐‘ค)โŸฉ โˆˆ (๐’ซ ๐บ ร— ๐’ซ ๐‘†) โˆง (normCVโ€˜๐‘ค) โˆˆ ๐’ซ ๐‘) โ†’ โŸจโŸจ( +๐‘ฃ โ€˜๐‘ค), ( ยท๐‘ OLD โ€˜๐‘ค)โŸฉ, (normCVโ€˜๐‘ค)โŸฉ โˆˆ ((๐’ซ ๐บ ร— ๐’ซ ๐‘†) ร— ๐’ซ ๐‘))
3631, 34, 35syl2an 597 . . . . . . 7 (((( +๐‘ฃ โ€˜๐‘ค) โŠ† ๐บ โˆง ( ยท๐‘ OLD โ€˜๐‘ค) โŠ† ๐‘†) โˆง (normCVโ€˜๐‘ค) โŠ† ๐‘) โ†’ โŸจโŸจ( +๐‘ฃ โ€˜๐‘ค), ( ยท๐‘ OLD โ€˜๐‘ค)โŸฉ, (normCVโ€˜๐‘ค)โŸฉ โˆˆ ((๐’ซ ๐บ ร— ๐’ซ ๐‘†) ร— ๐’ซ ๐‘))
37363impa 1111 . . . . . 6 ((( +๐‘ฃ โ€˜๐‘ค) โŠ† ๐บ โˆง ( ยท๐‘ OLD โ€˜๐‘ค) โŠ† ๐‘† โˆง (normCVโ€˜๐‘ค) โŠ† ๐‘) โ†’ โŸจโŸจ( +๐‘ฃ โ€˜๐‘ค), ( ยท๐‘ OLD โ€˜๐‘ค)โŸฉ, (normCVโ€˜๐‘ค)โŸฉ โˆˆ ((๐’ซ ๐บ ร— ๐’ซ ๐‘†) ร— ๐’ซ ๐‘))
38 eqid 2737 . . . . . . . 8 ( +๐‘ฃ โ€˜๐‘ค) = ( +๐‘ฃ โ€˜๐‘ค)
39 eqid 2737 . . . . . . . 8 ( ยท๐‘ OLD โ€˜๐‘ค) = ( ยท๐‘ OLD โ€˜๐‘ค)
40 eqid 2737 . . . . . . . 8 (normCVโ€˜๐‘ค) = (normCVโ€˜๐‘ค)
4138, 39, 40nvop 29660 . . . . . . 7 (๐‘ค โˆˆ NrmCVec โ†’ ๐‘ค = โŸจโŸจ( +๐‘ฃ โ€˜๐‘ค), ( ยท๐‘ OLD โ€˜๐‘ค)โŸฉ, (normCVโ€˜๐‘ค)โŸฉ)
4241eleq1d 2823 . . . . . 6 (๐‘ค โˆˆ NrmCVec โ†’ (๐‘ค โˆˆ ((๐’ซ ๐บ ร— ๐’ซ ๐‘†) ร— ๐’ซ ๐‘) โ†” โŸจโŸจ( +๐‘ฃ โ€˜๐‘ค), ( ยท๐‘ OLD โ€˜๐‘ค)โŸฉ, (normCVโ€˜๐‘ค)โŸฉ โˆˆ ((๐’ซ ๐บ ร— ๐’ซ ๐‘†) ร— ๐’ซ ๐‘)))
4337, 42syl5ibr 246 . . . . 5 (๐‘ค โˆˆ NrmCVec โ†’ ((( +๐‘ฃ โ€˜๐‘ค) โŠ† ๐บ โˆง ( ยท๐‘ OLD โ€˜๐‘ค) โŠ† ๐‘† โˆง (normCVโ€˜๐‘ค) โŠ† ๐‘) โ†’ ๐‘ค โˆˆ ((๐’ซ ๐บ ร— ๐’ซ ๐‘†) ร— ๐’ซ ๐‘)))
4425, 43mprgbir 3072 . . . 4 {๐‘ค โˆˆ NrmCVec โˆฃ (( +๐‘ฃ โ€˜๐‘ค) โŠ† ๐บ โˆง ( ยท๐‘ OLD โ€˜๐‘ค) โŠ† ๐‘† โˆง (normCVโ€˜๐‘ค) โŠ† ๐‘)} โŠ† ((๐’ซ ๐บ ร— ๐’ซ ๐‘†) ร— ๐’ซ ๐‘)
4524, 44ssexi 5284 . . 3 {๐‘ค โˆˆ NrmCVec โˆฃ (( +๐‘ฃ โ€˜๐‘ค) โŠ† ๐บ โˆง ( ยท๐‘ OLD โ€˜๐‘ค) โŠ† ๐‘† โˆง (normCVโ€˜๐‘ค) โŠ† ๐‘)} โˆˆ V
4615, 16, 45fvmpt 6953 . 2 (๐‘ˆ โˆˆ NrmCVec โ†’ (SubSpโ€˜๐‘ˆ) = {๐‘ค โˆˆ NrmCVec โˆฃ (( +๐‘ฃ โ€˜๐‘ค) โŠ† ๐บ โˆง ( ยท๐‘ OLD โ€˜๐‘ค) โŠ† ๐‘† โˆง (normCVโ€˜๐‘ค) โŠ† ๐‘)})
471, 46eqtrid 2789 1 (๐‘ˆ โˆˆ NrmCVec โ†’ ๐ป = {๐‘ค โˆˆ NrmCVec โˆฃ (( +๐‘ฃ โ€˜๐‘ค) โŠ† ๐บ โˆง ( ยท๐‘ OLD โ€˜๐‘ค) โŠ† ๐‘† โˆง (normCVโ€˜๐‘ค) โŠ† ๐‘)})
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โˆง wa 397   โˆง w3a 1088   = wceq 1542   โˆˆ wcel 2107  {crab 3410   โŠ† wss 3915  ๐’ซ cpw 4565  โŸจcop 4597   ร— cxp 5636  โ€˜cfv 6501  NrmCVeccnv 29568   +๐‘ฃ cpv 29569   ยท๐‘ OLD cns 29571  normCVcnmcv 29574  SubSpcss 29705
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 2708  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677
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 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-ral 3066  df-rex 3075  df-rab 3411  df-v 3450  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-br 5111  df-opab 5173  df-mpt 5194  df-id 5536  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-fo 6507  df-fv 6509  df-oprab 7366  df-1st 7926  df-2nd 7927  df-vc 29543  df-nv 29576  df-va 29579  df-sm 29581  df-nmcv 29584  df-ssp 29706
This theorem is referenced by:  isssp  29708
  Copyright terms: Public domain W3C validator