Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  lclkr Structured version   Unicode version

Theorem lclkr 37708
Description: The set of functionals with closed kernels is a subspace. Part of proof of Theorem 3.6 of [Holland95] p. 218, line 20, stating "The fM that arise this way generate a subspace F of E'". Our proof was suggested by Mario Carneiro, 5-Jan-2015. (Contributed by NM, 18-Jan-2015.)
Hypotheses
Ref Expression
lclkr.h  |-  H  =  ( LHyp `  K
)
lclkr.u  |-  U  =  ( ( DVecH `  K
) `  W )
lclkr.o  |-  ._|_  =  ( ( ocH `  K
) `  W )
lclkr.f  |-  F  =  (LFnl `  U )
lclkr.l  |-  L  =  (LKer `  U )
lclkr.d  |-  D  =  (LDual `  U )
lclkr.s  |-  S  =  ( LSubSp `  D )
lclkr.c  |-  C  =  { f  e.  F  |  (  ._|_  `  (  ._|_  `  ( L `  f ) ) )  =  ( L `  f ) }
lclkr.k  |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )
Assertion
Ref Expression
lclkr  |-  ( ph  ->  C  e.  S )
Distinct variable groups:    ._|_ , f    D, f    f, F    f, L    U, f
Allowed substitution hints:    ph( f)    C( f)    S( f)    H( f)    K( f)    W( f)

Proof of Theorem lclkr
Dummy variables  a 
b  x are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ssrab2 3512 . . . 4  |-  { f  e.  F  |  ( 
._|_  `  (  ._|_  `  ( L `  f )
) )  =  ( L `  f ) }  C_  F
21a1i 11 . . 3  |-  ( ph  ->  { f  e.  F  |  (  ._|_  `  (  ._|_  `  ( L `  f ) ) )  =  ( L `  f ) }  C_  F )
3 lclkr.c . . . 4  |-  C  =  { f  e.  F  |  (  ._|_  `  (  ._|_  `  ( L `  f ) ) )  =  ( L `  f ) }
43a1i 11 . . 3  |-  ( ph  ->  C  =  { f  e.  F  |  ( 
._|_  `  (  ._|_  `  ( L `  f )
) )  =  ( L `  f ) } )
5 lclkr.f . . . 4  |-  F  =  (LFnl `  U )
6 lclkr.d . . . 4  |-  D  =  (LDual `  U )
7 eqid 2392 . . . 4  |-  ( Base `  D )  =  (
Base `  D )
8 lclkr.h . . . . 5  |-  H  =  ( LHyp `  K
)
9 lclkr.u . . . . 5  |-  U  =  ( ( DVecH `  K
) `  W )
10 lclkr.k . . . . 5  |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )
118, 9, 10dvhlmod 37285 . . . 4  |-  ( ph  ->  U  e.  LMod )
125, 6, 7, 11ldualvbase 35299 . . 3  |-  ( ph  ->  ( Base `  D
)  =  F )
132, 4, 123sstr4d 3473 . 2  |-  ( ph  ->  C  C_  ( Base `  D ) )
14 eqid 2392 . . . . . 6  |-  (Scalar `  U )  =  (Scalar `  U )
15 eqid 2392 . . . . . 6  |-  ( 0g
`  (Scalar `  U )
)  =  ( 0g
`  (Scalar `  U )
)
16 eqid 2392 . . . . . 6  |-  ( Base `  U )  =  (
Base `  U )
1714, 15, 16, 5lfl0f 35242 . . . . 5  |-  ( U  e.  LMod  ->  ( (
Base `  U )  X.  { ( 0g `  (Scalar `  U ) ) } )  e.  F
)
1811, 17syl 16 . . . 4  |-  ( ph  ->  ( ( Base `  U
)  X.  { ( 0g `  (Scalar `  U ) ) } )  e.  F )
19 lclkr.o . . . . . 6  |-  ._|_  =  ( ( ocH `  K
) `  W )
208, 9, 19, 16, 10dochoc1 37536 . . . . 5  |-  ( ph  ->  (  ._|_  `  (  ._|_  `  ( Base `  U
) ) )  =  ( Base `  U
) )
21 eqid 2392 . . . . . . . 8  |-  ( (
Base `  U )  X.  { ( 0g `  (Scalar `  U ) ) } )  =  ( ( Base `  U
)  X.  { ( 0g `  (Scalar `  U ) ) } )
22 lclkr.l . . . . . . . . . 10  |-  L  =  (LKer `  U )
2314, 15, 16, 5, 22lkr0f 35267 . . . . . . . . 9  |-  ( ( U  e.  LMod  /\  (
( Base `  U )  X.  { ( 0g `  (Scalar `  U ) ) } )  e.  F
)  ->  ( ( L `  ( ( Base `  U )  X. 
{ ( 0g `  (Scalar `  U ) ) } ) )  =  ( Base `  U
)  <->  ( ( Base `  U )  X.  {
( 0g `  (Scalar `  U ) ) } )  =  ( (
Base `  U )  X.  { ( 0g `  (Scalar `  U ) ) } ) ) )
2411, 18, 23syl2anc 659 . . . . . . . 8  |-  ( ph  ->  ( ( L `  ( ( Base `  U
)  X.  { ( 0g `  (Scalar `  U ) ) } ) )  =  (
Base `  U )  <->  ( ( Base `  U
)  X.  { ( 0g `  (Scalar `  U ) ) } )  =  ( (
Base `  U )  X.  { ( 0g `  (Scalar `  U ) ) } ) ) )
2521, 24mpbiri 233 . . . . . . 7  |-  ( ph  ->  ( L `  (
( Base `  U )  X.  { ( 0g `  (Scalar `  U ) ) } ) )  =  ( Base `  U
) )
2625fveq2d 5791 . . . . . 6  |-  ( ph  ->  (  ._|_  `  ( L `
 ( ( Base `  U )  X.  {
( 0g `  (Scalar `  U ) ) } ) ) )  =  (  ._|_  `  ( Base `  U ) ) )
2726fveq2d 5791 . . . . 5  |-  ( ph  ->  (  ._|_  `  (  ._|_  `  ( L `  (
( Base `  U )  X.  { ( 0g `  (Scalar `  U ) ) } ) ) ) )  =  (  ._|_  `  (  ._|_  `  ( Base `  U ) ) ) )
2820, 27, 253eqtr4d 2443 . . . 4  |-  ( ph  ->  (  ._|_  `  (  ._|_  `  ( L `  (
( Base `  U )  X.  { ( 0g `  (Scalar `  U ) ) } ) ) ) )  =  ( L `
 ( ( Base `  U )  X.  {
( 0g `  (Scalar `  U ) ) } ) ) )
293lcfl1lem 37666 . . . 4  |-  ( ( ( Base `  U
)  X.  { ( 0g `  (Scalar `  U ) ) } )  e.  C  <->  ( (
( Base `  U )  X.  { ( 0g `  (Scalar `  U ) ) } )  e.  F  /\  (  ._|_  `  (  ._|_  `  ( L `  ( ( Base `  U
)  X.  { ( 0g `  (Scalar `  U ) ) } ) ) ) )  =  ( L `  ( ( Base `  U
)  X.  { ( 0g `  (Scalar `  U ) ) } ) ) ) )
3018, 28, 29sylanbrc 662 . . 3  |-  ( ph  ->  ( ( Base `  U
)  X.  { ( 0g `  (Scalar `  U ) ) } )  e.  C )
31 ne0i 3730 . . 3  |-  ( ( ( Base `  U
)  X.  { ( 0g `  (Scalar `  U ) ) } )  e.  C  ->  C  =/=  (/) )
3230, 31syl 16 . 2  |-  ( ph  ->  C  =/=  (/) )
33 eqid 2392 . . . 4  |-  ( +g  `  D )  =  ( +g  `  D )
3410adantr 463 . . . 4  |-  ( (
ph  /\  ( x  e.  ( Base `  (Scalar `  D ) )  /\  a  e.  C  /\  b  e.  C )
)  ->  ( K  e.  HL  /\  W  e.  H ) )
35 eqid 2392 . . . . 5  |-  ( Base `  (Scalar `  U )
)  =  ( Base `  (Scalar `  U )
)
36 eqid 2392 . . . . 5  |-  ( .s
`  D )  =  ( .s `  D
)
37 simpr1 1000 . . . . . 6  |-  ( (
ph  /\  ( x  e.  ( Base `  (Scalar `  D ) )  /\  a  e.  C  /\  b  e.  C )
)  ->  x  e.  ( Base `  (Scalar `  D
) ) )
38 eqid 2392 . . . . . . . 8  |-  (Scalar `  D )  =  (Scalar `  D )
39 eqid 2392 . . . . . . . 8  |-  ( Base `  (Scalar `  D )
)  =  ( Base `  (Scalar `  D )
)
4014, 35, 6, 38, 39, 11ldualsbase 35306 . . . . . . 7  |-  ( ph  ->  ( Base `  (Scalar `  D ) )  =  ( Base `  (Scalar `  U ) ) )
4140adantr 463 . . . . . 6  |-  ( (
ph  /\  ( x  e.  ( Base `  (Scalar `  D ) )  /\  a  e.  C  /\  b  e.  C )
)  ->  ( Base `  (Scalar `  D )
)  =  ( Base `  (Scalar `  U )
) )
4237, 41eleqtrd 2482 . . . . 5  |-  ( (
ph  /\  ( x  e.  ( Base `  (Scalar `  D ) )  /\  a  e.  C  /\  b  e.  C )
)  ->  x  e.  ( Base `  (Scalar `  U
) ) )
43 simpr2 1001 . . . . 5  |-  ( (
ph  /\  ( x  e.  ( Base `  (Scalar `  D ) )  /\  a  e.  C  /\  b  e.  C )
)  ->  a  e.  C )
448, 19, 9, 5, 22, 6, 14, 35, 36, 3, 34, 42, 43lclkrlem1 37681 . . . 4  |-  ( (
ph  /\  ( x  e.  ( Base `  (Scalar `  D ) )  /\  a  e.  C  /\  b  e.  C )
)  ->  ( x
( .s `  D
) a )  e.  C )
45 simpr3 1002 . . . 4  |-  ( (
ph  /\  ( x  e.  ( Base `  (Scalar `  D ) )  /\  a  e.  C  /\  b  e.  C )
)  ->  b  e.  C )
468, 19, 9, 5, 22, 6, 33, 3, 34, 44, 45lclkrlem2 37707 . . 3  |-  ( (
ph  /\  ( x  e.  ( Base `  (Scalar `  D ) )  /\  a  e.  C  /\  b  e.  C )
)  ->  ( (
x ( .s `  D ) a ) ( +g  `  D
) b )  e.  C )
4746ralrimivvva 2814 . 2  |-  ( ph  ->  A. x  e.  (
Base `  (Scalar `  D
) ) A. a  e.  C  A. b  e.  C  ( (
x ( .s `  D ) a ) ( +g  `  D
) b )  e.  C )
48 lclkr.s . . 3  |-  S  =  ( LSubSp `  D )
4938, 39, 7, 33, 36, 48islss 17713 . 2  |-  ( C  e.  S  <->  ( C  C_  ( Base `  D
)  /\  C  =/=  (/) 
/\  A. x  e.  (
Base `  (Scalar `  D
) ) A. a  e.  C  A. b  e.  C  ( (
x ( .s `  D ) a ) ( +g  `  D
) b )  e.  C ) )
5013, 32, 47, 49syl3anbrc 1178 1  |-  ( ph  ->  C  e.  S )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 367    /\ w3a 971    = wceq 1399    e. wcel 1836    =/= wne 2587   A.wral 2742   {crab 2746    C_ wss 3402   (/)c0 3724   {csn 3957    X. cxp 4924   ` cfv 5509  (class class class)co 6214   Basecbs 14653   +g cplusg 14721  Scalarcsca 14724   .scvsca 14725   0gc0g 14866   LModclmod 17644   LSubSpclss 17710  LFnlclfn 35230  LKerclk 35258  LDualcld 35296   HLchlt 35523   LHypclh 36156   DVecHcdvh 37253   ocHcoch 37522
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1633  ax-4 1646  ax-5 1719  ax-6 1765  ax-7 1808  ax-8 1838  ax-9 1840  ax-10 1855  ax-11 1860  ax-12 1872  ax-13 2016  ax-ext 2370  ax-rep 4491  ax-sep 4501  ax-nul 4509  ax-pow 4556  ax-pr 4614  ax-un 6509  ax-cnex 9477  ax-resscn 9478  ax-1cn 9479  ax-icn 9480  ax-addcl 9481  ax-addrcl 9482  ax-mulcl 9483  ax-mulrcl 9484  ax-mulcom 9485  ax-addass 9486  ax-mulass 9487  ax-distr 9488  ax-i2m1 9489  ax-1ne0 9490  ax-1rid 9491  ax-rnegex 9492  ax-rrecex 9493  ax-cnre 9494  ax-pre-lttri 9495  ax-pre-lttrn 9496  ax-pre-ltadd 9497  ax-pre-mulgt0 9498  ax-riotaBAD 35132
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-tru 1402  df-fal 1405  df-ex 1628  df-nf 1632  df-sb 1758  df-eu 2232  df-mo 2233  df-clab 2378  df-cleq 2384  df-clel 2387  df-nfc 2542  df-ne 2589  df-nel 2590  df-ral 2747  df-rex 2748  df-reu 2749  df-rmo 2750  df-rab 2751  df-v 3049  df-sbc 3266  df-csb 3362  df-dif 3405  df-un 3407  df-in 3409  df-ss 3416  df-pss 3418  df-nul 3725  df-if 3871  df-pw 3942  df-sn 3958  df-pr 3960  df-tp 3962  df-op 3964  df-uni 4177  df-int 4213  df-iun 4258  df-iin 4259  df-br 4381  df-opab 4439  df-mpt 4440  df-tr 4474  df-eprel 4718  df-id 4722  df-po 4727  df-so 4728  df-fr 4765  df-we 4767  df-ord 4808  df-on 4809  df-lim 4810  df-suc 4811  df-xp 4932  df-rel 4933  df-cnv 4934  df-co 4935  df-dm 4936  df-rn 4937  df-res 4938  df-ima 4939  df-iota 5473  df-fun 5511  df-fn 5512  df-f 5513  df-f1 5514  df-fo 5515  df-f1o 5516  df-fv 5517  df-riota 6176  df-ov 6217  df-oprab 6218  df-mpt2 6219  df-of 6457  df-om 6618  df-1st 6717  df-2nd 6718  df-tpos 6891  df-undef 6938  df-recs 6978  df-rdg 7012  df-1o 7066  df-oadd 7070  df-er 7247  df-map 7358  df-en 7454  df-dom 7455  df-sdom 7456  df-fin 7457  df-pnf 9559  df-mnf 9560  df-xr 9561  df-ltxr 9562  df-le 9563  df-sub 9738  df-neg 9739  df-nn 10471  df-2 10529  df-3 10530  df-4 10531  df-5 10532  df-6 10533  df-n0 10731  df-z 10800  df-uz 11020  df-fz 11612  df-struct 14655  df-ndx 14656  df-slot 14657  df-base 14658  df-sets 14659  df-ress 14660  df-plusg 14734  df-mulr 14735  df-sca 14737  df-vsca 14738  df-0g 14868  df-mre 15012  df-mrc 15013  df-acs 15015  df-preset 15693  df-poset 15711  df-plt 15724  df-lub 15740  df-glb 15741  df-join 15742  df-meet 15743  df-p0 15805  df-p1 15806  df-lat 15812  df-clat 15874  df-mgm 16008  df-sgrp 16047  df-mnd 16057  df-submnd 16103  df-grp 16193  df-minusg 16194  df-sbg 16195  df-subg 16334  df-cntz 16491  df-oppg 16517  df-lsm 16792  df-cmn 16936  df-abl 16937  df-mgp 17274  df-ur 17286  df-ring 17332  df-oppr 17404  df-dvdsr 17422  df-unit 17423  df-invr 17453  df-dvr 17464  df-drng 17530  df-lmod 17646  df-lss 17711  df-lsp 17750  df-lvec 17881  df-lsatoms 35149  df-lshyp 35150  df-lcv 35192  df-lfl 35231  df-lkr 35259  df-ldual 35297  df-oposet 35349  df-ol 35351  df-oml 35352  df-covers 35439  df-ats 35440  df-atl 35471  df-cvlat 35495  df-hlat 35524  df-llines 35670  df-lplanes 35671  df-lvols 35672  df-lines 35673  df-psubsp 35675  df-pmap 35676  df-padd 35968  df-lhyp 36160  df-laut 36161  df-ldil 36276  df-ltrn 36277  df-trl 36332  df-tgrp 36917  df-tendo 36929  df-edring 36931  df-dveca 37177  df-disoa 37204  df-dvech 37254  df-dib 37314  df-dic 37348  df-dih 37404  df-doch 37523  df-djh 37570
This theorem is referenced by:  lcdlvec  37766  lcd0v  37786  lcdlss  37794  lcdlsp  37796  mapdunirnN  37825
  Copyright terms: Public domain W3C validator