Mathbox for Norm Megill < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  lfl1 Structured version   Visualization version   GIF version

Theorem lfl1 36682
 Description: A nonzero functional has a value of 1 at some argument. (Contributed by NM, 16-Apr-2014.)
Hypotheses
Ref Expression
lfl1.d 𝐷 = (Scalar‘𝑊)
lfl1.o 0 = (0g𝐷)
lfl1.u 1 = (1r𝐷)
lfl1.v 𝑉 = (Base‘𝑊)
lfl1.f 𝐹 = (LFnl‘𝑊)
Assertion
Ref Expression
lfl1 ((𝑊 ∈ LVec ∧ 𝐺𝐹𝐺 ≠ (𝑉 × { 0 })) → ∃𝑥𝑉 (𝐺𝑥) = 1 )
Distinct variable groups:   𝑥,𝐷   𝑥,𝐺   𝑥, 1   𝑥,𝑉   𝑥,𝑊
Allowed substitution hints:   𝐹(𝑥)   0 (𝑥)

Proof of Theorem lfl1
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 nne 2956 . . . . . . 7 (¬ (𝐺𝑧) ≠ 0 ↔ (𝐺𝑧) = 0 )
21ralbii 3098 . . . . . 6 (∀𝑧𝑉 ¬ (𝐺𝑧) ≠ 0 ↔ ∀𝑧𝑉 (𝐺𝑧) = 0 )
3 lfl1.d . . . . . . . . . 10 𝐷 = (Scalar‘𝑊)
4 eqid 2759 . . . . . . . . . 10 (Base‘𝐷) = (Base‘𝐷)
5 lfl1.v . . . . . . . . . 10 𝑉 = (Base‘𝑊)
6 lfl1.f . . . . . . . . . 10 𝐹 = (LFnl‘𝑊)
73, 4, 5, 6lflf 36675 . . . . . . . . 9 ((𝑊 ∈ LVec ∧ 𝐺𝐹) → 𝐺:𝑉⟶(Base‘𝐷))
87ffnd 6505 . . . . . . . 8 ((𝑊 ∈ LVec ∧ 𝐺𝐹) → 𝐺 Fn 𝑉)
9 fconstfv 6973 . . . . . . . . 9 (𝐺:𝑉⟶{ 0 } ↔ (𝐺 Fn 𝑉 ∧ ∀𝑧𝑉 (𝐺𝑧) = 0 ))
109simplbi2 504 . . . . . . . 8 (𝐺 Fn 𝑉 → (∀𝑧𝑉 (𝐺𝑧) = 0𝐺:𝑉⟶{ 0 }))
118, 10syl 17 . . . . . . 7 ((𝑊 ∈ LVec ∧ 𝐺𝐹) → (∀𝑧𝑉 (𝐺𝑧) = 0𝐺:𝑉⟶{ 0 }))
12 lfl1.o . . . . . . . . 9 0 = (0g𝐷)
1312fvexi 6678 . . . . . . . 8 0 ∈ V
1413fconst2 6965 . . . . . . 7 (𝐺:𝑉⟶{ 0 } ↔ 𝐺 = (𝑉 × { 0 }))
1511, 14syl6ib 254 . . . . . 6 ((𝑊 ∈ LVec ∧ 𝐺𝐹) → (∀𝑧𝑉 (𝐺𝑧) = 0𝐺 = (𝑉 × { 0 })))
162, 15syl5bi 245 . . . . 5 ((𝑊 ∈ LVec ∧ 𝐺𝐹) → (∀𝑧𝑉 ¬ (𝐺𝑧) ≠ 0𝐺 = (𝑉 × { 0 })))
1716necon3ad 2965 . . . 4 ((𝑊 ∈ LVec ∧ 𝐺𝐹) → (𝐺 ≠ (𝑉 × { 0 }) → ¬ ∀𝑧𝑉 ¬ (𝐺𝑧) ≠ 0 ))
18 dfrex2 3167 . . . 4 (∃𝑧𝑉 (𝐺𝑧) ≠ 0 ↔ ¬ ∀𝑧𝑉 ¬ (𝐺𝑧) ≠ 0 )
1917, 18syl6ibr 255 . . 3 ((𝑊 ∈ LVec ∧ 𝐺𝐹) → (𝐺 ≠ (𝑉 × { 0 }) → ∃𝑧𝑉 (𝐺𝑧) ≠ 0 ))
20193impia 1115 . 2 ((𝑊 ∈ LVec ∧ 𝐺𝐹𝐺 ≠ (𝑉 × { 0 })) → ∃𝑧𝑉 (𝐺𝑧) ≠ 0 )
21 simp1l 1195 . . . . . . 7 (((𝑊 ∈ LVec ∧ 𝐺𝐹) ∧ 𝑧𝑉 ∧ (𝐺𝑧) ≠ 0 ) → 𝑊 ∈ LVec)
22 lveclmod 19961 . . . . . . 7 (𝑊 ∈ LVec → 𝑊 ∈ LMod)
2321, 22syl 17 . . . . . 6 (((𝑊 ∈ LVec ∧ 𝐺𝐹) ∧ 𝑧𝑉 ∧ (𝐺𝑧) ≠ 0 ) → 𝑊 ∈ LMod)
243lvecdrng 19960 . . . . . . . 8 (𝑊 ∈ LVec → 𝐷 ∈ DivRing)
2521, 24syl 17 . . . . . . 7 (((𝑊 ∈ LVec ∧ 𝐺𝐹) ∧ 𝑧𝑉 ∧ (𝐺𝑧) ≠ 0 ) → 𝐷 ∈ DivRing)
26 simp1r 1196 . . . . . . . 8 (((𝑊 ∈ LVec ∧ 𝐺𝐹) ∧ 𝑧𝑉 ∧ (𝐺𝑧) ≠ 0 ) → 𝐺𝐹)
27 simp2 1135 . . . . . . . 8 (((𝑊 ∈ LVec ∧ 𝐺𝐹) ∧ 𝑧𝑉 ∧ (𝐺𝑧) ≠ 0 ) → 𝑧𝑉)
283, 4, 5, 6lflcl 36676 . . . . . . . 8 ((𝑊 ∈ LVec ∧ 𝐺𝐹𝑧𝑉) → (𝐺𝑧) ∈ (Base‘𝐷))
2921, 26, 27, 28syl3anc 1369 . . . . . . 7 (((𝑊 ∈ LVec ∧ 𝐺𝐹) ∧ 𝑧𝑉 ∧ (𝐺𝑧) ≠ 0 ) → (𝐺𝑧) ∈ (Base‘𝐷))
30 simp3 1136 . . . . . . 7 (((𝑊 ∈ LVec ∧ 𝐺𝐹) ∧ 𝑧𝑉 ∧ (𝐺𝑧) ≠ 0 ) → (𝐺𝑧) ≠ 0 )
31 eqid 2759 . . . . . . . 8 (invr𝐷) = (invr𝐷)
324, 12, 31drnginvrcl 19602 . . . . . . 7 ((𝐷 ∈ DivRing ∧ (𝐺𝑧) ∈ (Base‘𝐷) ∧ (𝐺𝑧) ≠ 0 ) → ((invr𝐷)‘(𝐺𝑧)) ∈ (Base‘𝐷))
3325, 29, 30, 32syl3anc 1369 . . . . . 6 (((𝑊 ∈ LVec ∧ 𝐺𝐹) ∧ 𝑧𝑉 ∧ (𝐺𝑧) ≠ 0 ) → ((invr𝐷)‘(𝐺𝑧)) ∈ (Base‘𝐷))
34 eqid 2759 . . . . . . 7 ( ·𝑠𝑊) = ( ·𝑠𝑊)
355, 3, 34, 4lmodvscl 19734 . . . . . 6 ((𝑊 ∈ LMod ∧ ((invr𝐷)‘(𝐺𝑧)) ∈ (Base‘𝐷) ∧ 𝑧𝑉) → (((invr𝐷)‘(𝐺𝑧))( ·𝑠𝑊)𝑧) ∈ 𝑉)
3623, 33, 27, 35syl3anc 1369 . . . . 5 (((𝑊 ∈ LVec ∧ 𝐺𝐹) ∧ 𝑧𝑉 ∧ (𝐺𝑧) ≠ 0 ) → (((invr𝐷)‘(𝐺𝑧))( ·𝑠𝑊)𝑧) ∈ 𝑉)
37 eqid 2759 . . . . . . . 8 (.r𝐷) = (.r𝐷)
383, 4, 37, 5, 34, 6lflmul 36680 . . . . . . 7 ((𝑊 ∈ LMod ∧ 𝐺𝐹 ∧ (((invr𝐷)‘(𝐺𝑧)) ∈ (Base‘𝐷) ∧ 𝑧𝑉)) → (𝐺‘(((invr𝐷)‘(𝐺𝑧))( ·𝑠𝑊)𝑧)) = (((invr𝐷)‘(𝐺𝑧))(.r𝐷)(𝐺𝑧)))
3923, 26, 33, 27, 38syl112anc 1372 . . . . . 6 (((𝑊 ∈ LVec ∧ 𝐺𝐹) ∧ 𝑧𝑉 ∧ (𝐺𝑧) ≠ 0 ) → (𝐺‘(((invr𝐷)‘(𝐺𝑧))( ·𝑠𝑊)𝑧)) = (((invr𝐷)‘(𝐺𝑧))(.r𝐷)(𝐺𝑧)))
40 lfl1.u . . . . . . . 8 1 = (1r𝐷)
414, 12, 37, 40, 31drnginvrl 19604 . . . . . . 7 ((𝐷 ∈ DivRing ∧ (𝐺𝑧) ∈ (Base‘𝐷) ∧ (𝐺𝑧) ≠ 0 ) → (((invr𝐷)‘(𝐺𝑧))(.r𝐷)(𝐺𝑧)) = 1 )
4225, 29, 30, 41syl3anc 1369 . . . . . 6 (((𝑊 ∈ LVec ∧ 𝐺𝐹) ∧ 𝑧𝑉 ∧ (𝐺𝑧) ≠ 0 ) → (((invr𝐷)‘(𝐺𝑧))(.r𝐷)(𝐺𝑧)) = 1 )
4339, 42eqtrd 2794 . . . . 5 (((𝑊 ∈ LVec ∧ 𝐺𝐹) ∧ 𝑧𝑉 ∧ (𝐺𝑧) ≠ 0 ) → (𝐺‘(((invr𝐷)‘(𝐺𝑧))( ·𝑠𝑊)𝑧)) = 1 )
44 fveqeq2 6673 . . . . . 6 (𝑥 = (((invr𝐷)‘(𝐺𝑧))( ·𝑠𝑊)𝑧) → ((𝐺𝑥) = 1 ↔ (𝐺‘(((invr𝐷)‘(𝐺𝑧))( ·𝑠𝑊)𝑧)) = 1 ))
4544rspcev 3544 . . . . 5 (((((invr𝐷)‘(𝐺𝑧))( ·𝑠𝑊)𝑧) ∈ 𝑉 ∧ (𝐺‘(((invr𝐷)‘(𝐺𝑧))( ·𝑠𝑊)𝑧)) = 1 ) → ∃𝑥𝑉 (𝐺𝑥) = 1 )
4636, 43, 45syl2anc 587 . . . 4 (((𝑊 ∈ LVec ∧ 𝐺𝐹) ∧ 𝑧𝑉 ∧ (𝐺𝑧) ≠ 0 ) → ∃𝑥𝑉 (𝐺𝑥) = 1 )
4746rexlimdv3a 3211 . . 3 ((𝑊 ∈ LVec ∧ 𝐺𝐹) → (∃𝑧𝑉 (𝐺𝑧) ≠ 0 → ∃𝑥𝑉 (𝐺𝑥) = 1 ))
48473adant3 1130 . 2 ((𝑊 ∈ LVec ∧ 𝐺𝐹𝐺 ≠ (𝑉 × { 0 })) → (∃𝑧𝑉 (𝐺𝑧) ≠ 0 → ∃𝑥𝑉 (𝐺𝑥) = 1 ))
4920, 48mpd 15 1 ((𝑊 ∈ LVec ∧ 𝐺𝐹𝐺 ≠ (𝑉 × { 0 })) → ∃𝑥𝑉 (𝐺𝑥) = 1 )
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 399   ∧ w3a 1085   = wceq 1539   ∈ wcel 2112   ≠ wne 2952  ∀wral 3071  ∃wrex 3072  {csn 4526   × cxp 5527   Fn wfn 6336  ⟶wf 6337  ‘cfv 6341  (class class class)co 7157  Basecbs 16556  .rcmulr 16639  Scalarcsca 16641   ·𝑠 cvsca 16642  0gc0g 16786  1rcur 19334  invrcinvr 19507  DivRingcdr 19585  LModclmod 19717  LVecclvec 19957  LFnlclfn 36669 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 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730  ax-rep 5161  ax-sep 5174  ax-nul 5181  ax-pow 5239  ax-pr 5303  ax-un 7466  ax-cnex 10645  ax-resscn 10646  ax-1cn 10647  ax-icn 10648  ax-addcl 10649  ax-addrcl 10650  ax-mulcl 10651  ax-mulrcl 10652  ax-mulcom 10653  ax-addass 10654  ax-mulass 10655  ax-distr 10656  ax-i2m1 10657  ax-1ne0 10658  ax-1rid 10659  ax-rnegex 10660  ax-rrecex 10661  ax-cnre 10662  ax-pre-lttri 10663  ax-pre-lttrn 10664  ax-pre-ltadd 10665  ax-pre-mulgt0 10666 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2071  df-mo 2558  df-eu 2589  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2902  df-ne 2953  df-nel 3057  df-ral 3076  df-rex 3077  df-reu 3078  df-rmo 3079  df-rab 3080  df-v 3412  df-sbc 3700  df-csb 3809  df-dif 3864  df-un 3866  df-in 3868  df-ss 3878  df-pss 3880  df-nul 4229  df-if 4425  df-pw 4500  df-sn 4527  df-pr 4529  df-tp 4531  df-op 4533  df-uni 4803  df-iun 4889  df-br 5038  df-opab 5100  df-mpt 5118  df-tr 5144  df-id 5435  df-eprel 5440  df-po 5448  df-so 5449  df-fr 5488  df-we 5490  df-xp 5535  df-rel 5536  df-cnv 5537  df-co 5538  df-dm 5539  df-rn 5540  df-res 5541  df-ima 5542  df-pred 6132  df-ord 6178  df-on 6179  df-lim 6180  df-suc 6181  df-iota 6300  df-fun 6343  df-fn 6344  df-f 6345  df-f1 6346  df-fo 6347  df-f1o 6348  df-fv 6349  df-riota 7115  df-ov 7160  df-oprab 7161  df-mpo 7162  df-om 7587  df-1st 7700  df-2nd 7701  df-tpos 7909  df-wrecs 7964  df-recs 8025  df-rdg 8063  df-er 8306  df-map 8425  df-en 8542  df-dom 8543  df-sdom 8544  df-pnf 10729  df-mnf 10730  df-xr 10731  df-ltxr 10732  df-le 10733  df-sub 10924  df-neg 10925  df-nn 11689  df-2 11751  df-3 11752  df-ndx 16559  df-slot 16560  df-base 16562  df-sets 16563  df-ress 16564  df-plusg 16651  df-mulr 16652  df-0g 16788  df-mgm 17933  df-sgrp 17982  df-mnd 17993  df-grp 18187  df-minusg 18188  df-sbg 18189  df-mgp 19323  df-ur 19335  df-ring 19382  df-oppr 19459  df-dvdsr 19477  df-unit 19478  df-invr 19508  df-drng 19587  df-lmod 19719  df-lvec 19958  df-lfl 36670 This theorem is referenced by:  eqlkr  36711  lkrshp  36717
 Copyright terms: Public domain W3C validator