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

Theorem lcfl6 35035
 Description: Property of a functional with a closed kernel. Note that means the functional is zero by lkr0f 32627. (Contributed by NM, 3-Jan-2015.)
Hypotheses
Ref Expression
lcfl6.h
lcfl6.o
lcfl6.u
lcfl6.v
lcfl6.a
lcfl6.t
lcfl6.s Scalar
lcfl6.r
lcfl6.z
lcfl6.f LFnl
lcfl6.l LKer
lcfl6.c
lcfl6.k
lcfl6.g
Assertion
Ref Expression
lcfl6
Distinct variable groups:   ,,,   ,,,,,   , ,   ,   ,,   ,   ,,   ,   ,,   ,,,   ,,   ,   ,,,
Allowed substitution hints:   (,,,)   (,,,)   (,)   (,,)   (,)   (,)   (,,,)   (,,,)   (,,)   (,,,,)   (,,,,)   (,,)   (,,)   (,,,,)   (,,)

Proof of Theorem lcfl6
StepHypRef Expression
1 df-ne 2621 . . . . 5
2 lcfl6.h . . . . . . . 8
3 lcfl6.o . . . . . . . 8
4 lcfl6.u . . . . . . . 8
5 lcfl6.v . . . . . . . 8
6 lcfl6.s . . . . . . . 8 Scalar
7 lcfl6.z . . . . . . . 8
8 eqid 2423 . . . . . . . 8
9 lcfl6.f . . . . . . . 8 LFnl
10 lcfl6.l . . . . . . . 8 LKer
11 lcfl6.k . . . . . . . . 9
1211ad2antrr 731 . . . . . . . 8
13 lcfl6.g . . . . . . . . 9
1413ad2antrr 731 . . . . . . . 8
15 lcfl6.c . . . . . . . . . . . . . 14
162, 3, 4, 5, 9, 10, 15, 11, 13lcfl2 35028 . . . . . . . . . . . . 13
1716biimpa 487 . . . . . . . . . . . 12
1817orcomd 390 . . . . . . . . . . 11
1918ord 379 . . . . . . . . . 10
201, 19syl5bi 221 . . . . . . . . 9
2120imp 431 . . . . . . . 8
222, 3, 4, 5, 6, 7, 8, 9, 10, 12, 14, 21dochkr1 35013 . . . . . . 7
232, 4, 11dvhlmod 34645 . . . . . . . . . . . . . . 15
245, 9, 10, 23, 13lkrssv 32629 . . . . . . . . . . . . . 14
252, 4, 5, 3dochssv 34890 . . . . . . . . . . . . . 14
2611, 24, 25syl2anc 666 . . . . . . . . . . . . 13
2726ssdifd 3603 . . . . . . . . . . . 12
2827ad3antrrr 735 . . . . . . . . . . 11
29 simprl 763 . . . . . . . . . . 11
3028, 29sseldd 3467 . . . . . . . . . 10
31 lcfl6.a . . . . . . . . . . 11
32 lcfl6.t . . . . . . . . . . 11
33 lcfl6.r . . . . . . . . . . 11
3411ad3antrrr 735 . . . . . . . . . . 11
3513ad3antrrr 735 . . . . . . . . . . 11
36 simprr 765 . . . . . . . . . . 11
372, 3, 4, 5, 31, 32, 6, 8, 33, 7, 9, 10, 34, 35, 29, 36lcfl6lem 35033 . . . . . . . . . 10
3830, 37jca 535 . . . . . . . . 9
3938ex 436 . . . . . . . 8
4039reximdv2 2897 . . . . . . 7
4122, 40mpd 15 . . . . . 6
4241ex 436 . . . . 5
431, 42syl5bir 222 . . . 4
4443orrd 380 . . 3
4544ex 436 . 2
46 olc 386 . . . 4
4746, 16syl5ibr 225 . . 3
4811adantr 467 . . . . . . . 8
49 eldifi 3589 . . . . . . . . . . 11
5049adantl 468 . . . . . . . . . 10
5150snssd 4144 . . . . . . . . 9
52 eqid 2423 . . . . . . . . . 10
532, 52, 4, 5, 3dochcl 34888 . . . . . . . . 9
5448, 51, 53syl2anc 666 . . . . . . . 8
552, 52, 3dochoc 34902 . . . . . . . 8
5648, 54, 55syl2anc 666 . . . . . . 7
57563adant3 1026 . . . . . 6
58 simp3 1008 . . . . . . . . . 10
5958fveq2d 5884 . . . . . . . . 9
60 eqid 2423 . . . . . . . . . . 11
61 simpr 463 . . . . . . . . . . 11
622, 3, 4, 5, 7, 31, 32, 10, 6, 33, 60, 48, 61dochsnkr2 35008 . . . . . . . . . 10
63623adant3 1026 . . . . . . . . 9
6459, 63eqtrd 2464 . . . . . . . 8
6564fveq2d 5884 . . . . . . 7
6665fveq2d 5884 . . . . . 6
6757, 66, 643eqtr4d 2474 . . . . 5
68133ad2ant1 1027 . . . . . 6
6915, 68lcfl1 35027 . . . . 5
7067, 69mpbird 236 . . . 4
7170rexlimdv3a 2920 . . 3
7247, 71jaod 382 . 2
7345, 72impbid 194 1
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wb 188   wo 370   wa 371   w3a 983   wceq 1438   wcel 1869   wne 2619  wrex 2777  crab 2780   cdif 3435   wss 3438  csn 3998   cmpt 4481   crn 4853  cfv 5600  crio 6265  (class class class)co 6304  cbs 15118   cplusg 15187  Scalarcsca 15190  cvsca 15191  c0g 15335  cur 17732  LFnlclfn 32590  LKerclk 32618  chlt 32883  clh 33516  cdvh 34613  cdih 34763  coch 34882 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-8 1871  ax-9 1873  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401  ax-rep 4535  ax-sep 4545  ax-nul 4554  ax-pow 4601  ax-pr 4659  ax-un 6596  ax-cnex 9601  ax-resscn 9602  ax-1cn 9603  ax-icn 9604  ax-addcl 9605  ax-addrcl 9606  ax-mulcl 9607  ax-mulrcl 9608  ax-mulcom 9609  ax-addass 9610  ax-mulass 9611  ax-distr 9612  ax-i2m1 9613  ax-1ne0 9614  ax-1rid 9615  ax-rnegex 9616  ax-rrecex 9617  ax-cnre 9618  ax-pre-lttri 9619  ax-pre-lttrn 9620  ax-pre-ltadd 9621  ax-pre-mulgt0 9622  ax-riotaBAD 32492 This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 984  df-3an 985  df-tru 1441  df-fal 1444  df-ex 1661  df-nf 1665  df-sb 1788  df-eu 2270  df-mo 2271  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-ne 2621  df-nel 2622  df-ral 2781  df-rex 2782  df-reu 2783  df-rmo 2784  df-rab 2785  df-v 3084  df-sbc 3302  df-csb 3398  df-dif 3441  df-un 3443  df-in 3445  df-ss 3452  df-pss 3454  df-nul 3764  df-if 3912  df-pw 3983  df-sn 3999  df-pr 4001  df-tp 4003  df-op 4005  df-uni 4219  df-int 4255  df-iun 4300  df-iin 4301  df-br 4423  df-opab 4482  df-mpt 4483  df-tr 4518  df-eprel 4763  df-id 4767  df-po 4773  df-so 4774  df-fr 4811  df-we 4813  df-xp 4858  df-rel 4859  df-cnv 4860  df-co 4861  df-dm 4862  df-rn 4863  df-res 4864  df-ima 4865  df-pred 5398  df-ord 5444  df-on 5445  df-lim 5446  df-suc 5447  df-iota 5564  df-fun 5602  df-fn 5603  df-f 5604  df-f1 5605  df-fo 5606  df-f1o 5607  df-fv 5608  df-riota 6266  df-ov 6307  df-oprab 6308  df-mpt2 6309  df-om 6706  df-1st 6806  df-2nd 6807  df-tpos 6983  df-undef 7030  df-wrecs 7038  df-recs 7100  df-rdg 7138  df-1o 7192  df-oadd 7196  df-er 7373  df-map 7484  df-en 7580  df-dom 7581  df-sdom 7582  df-fin 7583  df-pnf 9683  df-mnf 9684  df-xr 9685  df-ltxr 9686  df-le 9687  df-sub 9868  df-neg 9869  df-nn 10616  df-2 10674  df-3 10675  df-4 10676  df-5 10677  df-6 10678  df-n0 10876  df-z 10944  df-uz 11166  df-fz 11791  df-struct 15120  df-ndx 15121  df-slot 15122  df-base 15123  df-sets 15124  df-ress 15125  df-plusg 15200  df-mulr 15201  df-sca 15203  df-vsca 15204  df-0g 15337  df-preset 16170  df-poset 16188  df-plt 16201  df-lub 16217  df-glb 16218  df-join 16219  df-meet 16220  df-p0 16282  df-p1 16283  df-lat 16289  df-clat 16351  df-mgm 16485  df-sgrp 16524  df-mnd 16534  df-submnd 16580  df-grp 16670  df-minusg 16671  df-sbg 16672  df-subg 16811  df-cntz 16968  df-lsm 17285  df-cmn 17429  df-abl 17430  df-mgp 17721  df-ur 17733  df-ring 17779  df-oppr 17848  df-dvdsr 17866  df-unit 17867  df-invr 17897  df-dvr 17908  df-drng 17974  df-lmod 18090  df-lss 18153  df-lsp 18192  df-lvec 18323  df-lsatoms 32509  df-lshyp 32510  df-lfl 32591  df-lkr 32619  df-oposet 32709  df-ol 32711  df-oml 32712  df-covers 32799  df-ats 32800  df-atl 32831  df-cvlat 32855  df-hlat 32884  df-llines 33030  df-lplanes 33031  df-lvols 33032  df-lines 33033  df-psubsp 33035  df-pmap 33036  df-padd 33328  df-lhyp 33520  df-laut 33521  df-ldil 33636  df-ltrn 33637  df-trl 33692  df-tgrp 34277  df-tendo 34289  df-edring 34291  df-dveca 34537  df-disoa 34564  df-dvech 34614  df-dib 34674  df-dic 34708  df-dih 34764  df-doch 34883  df-djh 34930 This theorem is referenced by:  lcfl7N  35036  lcfrlem9  35085
 Copyright terms: Public domain W3C validator