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

Theorem dochfln0 38144
Description: The value of a functional is nonzero at a nonzero vector in the orthocomplement of its kernel. (Contributed by NM, 2-Jan-2015.)
Hypotheses
Ref Expression
dochfln0.h 𝐻 = (LHyp‘𝐾)
dochfln0.o = ((ocH‘𝐾)‘𝑊)
dochfln0.u 𝑈 = ((DVecH‘𝐾)‘𝑊)
dochfln0.v 𝑉 = (Base‘𝑈)
dochfln0.r 𝑅 = (Scalar‘𝑈)
dochfln0.n 𝑁 = (0g𝑅)
dochfln0.z 0 = (0g𝑈)
dochfln0.f 𝐹 = (LFnl‘𝑈)
dochfln0.l 𝐿 = (LKer‘𝑈)
dochfln0.k (𝜑 → (𝐾 ∈ HL ∧ 𝑊𝐻))
dochfln0.g (𝜑𝐺𝐹)
dochfln0.x (𝜑𝑋 ∈ (( ‘(𝐿𝐺)) ∖ { 0 }))
Assertion
Ref Expression
dochfln0 (𝜑 → (𝐺𝑋) ≠ 𝑁)

Proof of Theorem dochfln0
StepHypRef Expression
1 dochfln0.h . . 3 𝐻 = (LHyp‘𝐾)
2 dochfln0.o . . 3 = ((ocH‘𝐾)‘𝑊)
3 dochfln0.u . . 3 𝑈 = ((DVecH‘𝐾)‘𝑊)
4 dochfln0.v . . 3 𝑉 = (Base‘𝑈)
5 dochfln0.z . . 3 0 = (0g𝑈)
6 dochfln0.k . . 3 (𝜑 → (𝐾 ∈ HL ∧ 𝑊𝐻))
7 dochfln0.f . . . . . . 7 𝐹 = (LFnl‘𝑈)
8 dochfln0.l . . . . . . 7 𝐿 = (LKer‘𝑈)
91, 3, 6dvhlmod 37777 . . . . . . 7 (𝜑𝑈 ∈ LMod)
10 dochfln0.g . . . . . . 7 (𝜑𝐺𝐹)
114, 7, 8, 9, 10lkrssv 35763 . . . . . 6 (𝜑 → (𝐿𝐺) ⊆ 𝑉)
121, 3, 4, 2dochssv 38022 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐿𝐺) ⊆ 𝑉) → ( ‘(𝐿𝐺)) ⊆ 𝑉)
136, 11, 12syl2anc 584 . . . . 5 (𝜑 → ( ‘(𝐿𝐺)) ⊆ 𝑉)
1413ssdifd 4038 . . . 4 (𝜑 → (( ‘(𝐿𝐺)) ∖ { 0 }) ⊆ (𝑉 ∖ { 0 }))
15 dochfln0.x . . . 4 (𝜑𝑋 ∈ (( ‘(𝐿𝐺)) ∖ { 0 }))
1614, 15sseldd 3890 . . 3 (𝜑𝑋 ∈ (𝑉 ∖ { 0 }))
171, 2, 3, 4, 5, 6, 16dochnel 38060 . 2 (𝜑 → ¬ 𝑋 ∈ ( ‘{𝑋}))
1815eldifad 3871 . . . . . 6 (𝜑𝑋 ∈ ( ‘(𝐿𝐺)))
1913, 18sseldd 3890 . . . . 5 (𝜑𝑋𝑉)
2019biantrurd 533 . . . 4 (𝜑 → ((𝐺𝑋) = 𝑁 ↔ (𝑋𝑉 ∧ (𝐺𝑋) = 𝑁)))
21 dochfln0.r . . . . . 6 𝑅 = (Scalar‘𝑈)
22 dochfln0.n . . . . . 6 𝑁 = (0g𝑅)
234, 21, 22, 7, 8ellkr 35756 . . . . 5 ((𝑈 ∈ LMod ∧ 𝐺𝐹) → (𝑋 ∈ (𝐿𝐺) ↔ (𝑋𝑉 ∧ (𝐺𝑋) = 𝑁)))
249, 10, 23syl2anc 584 . . . 4 (𝜑 → (𝑋 ∈ (𝐿𝐺) ↔ (𝑋𝑉 ∧ (𝐺𝑋) = 𝑁)))
251, 2, 3, 4, 5, 7, 8, 6, 10, 15dochsnkr 38139 . . . . 5 (𝜑 → (𝐿𝐺) = ( ‘{𝑋}))
2625eleq2d 2868 . . . 4 (𝜑 → (𝑋 ∈ (𝐿𝐺) ↔ 𝑋 ∈ ( ‘{𝑋})))
2720, 24, 263bitr2rd 309 . . 3 (𝜑 → (𝑋 ∈ ( ‘{𝑋}) ↔ (𝐺𝑋) = 𝑁))
2827necon3bbid 3021 . 2 (𝜑 → (¬ 𝑋 ∈ ( ‘{𝑋}) ↔ (𝐺𝑋) ≠ 𝑁))
2917, 28mpbid 233 1 (𝜑 → (𝐺𝑋) ≠ 𝑁)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396   = wceq 1522  wcel 2081  wne 2984  cdif 3856  wss 3859  {csn 4472  cfv 6225  Basecbs 16312  Scalarcsca 16397  0gc0g 16542  LModclmod 19324  LFnlclfn 35724  LKerclk 35752  HLchlt 36017  LHypclh 36651  DVecHcdvh 37745  ocHcoch 38014
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-13 2344  ax-ext 2769  ax-rep 5081  ax-sep 5094  ax-nul 5101  ax-pow 5157  ax-pr 5221  ax-un 7319  ax-cnex 10439  ax-resscn 10440  ax-1cn 10441  ax-icn 10442  ax-addcl 10443  ax-addrcl 10444  ax-mulcl 10445  ax-mulrcl 10446  ax-mulcom 10447  ax-addass 10448  ax-mulass 10449  ax-distr 10450  ax-i2m1 10451  ax-1ne0 10452  ax-1rid 10453  ax-rnegex 10454  ax-rrecex 10455  ax-cnre 10456  ax-pre-lttri 10457  ax-pre-lttrn 10458  ax-pre-ltadd 10459  ax-pre-mulgt0 10460  ax-riotaBAD 35620
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1081  df-3an 1082  df-tru 1525  df-fal 1535  df-ex 1762  df-nf 1766  df-sb 2043  df-mo 2576  df-eu 2612  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ne 2985  df-nel 3091  df-ral 3110  df-rex 3111  df-reu 3112  df-rmo 3113  df-rab 3114  df-v 3439  df-sbc 3707  df-csb 3812  df-dif 3862  df-un 3864  df-in 3866  df-ss 3874  df-pss 3876  df-nul 4212  df-if 4382  df-pw 4455  df-sn 4473  df-pr 4475  df-tp 4477  df-op 4479  df-uni 4746  df-int 4783  df-iun 4827  df-iin 4828  df-br 4963  df-opab 5025  df-mpt 5042  df-tr 5064  df-id 5348  df-eprel 5353  df-po 5362  df-so 5363  df-fr 5402  df-we 5404  df-xp 5449  df-rel 5450  df-cnv 5451  df-co 5452  df-dm 5453  df-rn 5454  df-res 5455  df-ima 5456  df-pred 6023  df-ord 6069  df-on 6070  df-lim 6071  df-suc 6072  df-iota 6189  df-fun 6227  df-fn 6228  df-f 6229  df-f1 6230  df-fo 6231  df-f1o 6232  df-fv 6233  df-riota 6977  df-ov 7019  df-oprab 7020  df-mpo 7021  df-om 7437  df-1st 7545  df-2nd 7546  df-tpos 7743  df-undef 7790  df-wrecs 7798  df-recs 7860  df-rdg 7898  df-1o 7953  df-oadd 7957  df-er 8139  df-map 8258  df-en 8358  df-dom 8359  df-sdom 8360  df-fin 8361  df-pnf 10523  df-mnf 10524  df-xr 10525  df-ltxr 10526  df-le 10527  df-sub 10719  df-neg 10720  df-nn 11487  df-2 11548  df-3 11549  df-4 11550  df-5 11551  df-6 11552  df-n0 11746  df-z 11830  df-uz 12094  df-fz 12743  df-struct 16314  df-ndx 16315  df-slot 16316  df-base 16318  df-sets 16319  df-ress 16320  df-plusg 16407  df-mulr 16408  df-sca 16410  df-vsca 16411  df-0g 16544  df-proset 17367  df-poset 17385  df-plt 17397  df-lub 17413  df-glb 17414  df-join 17415  df-meet 17416  df-p0 17478  df-p1 17479  df-lat 17485  df-clat 17547  df-mgm 17681  df-sgrp 17723  df-mnd 17734  df-submnd 17775  df-grp 17864  df-minusg 17865  df-sbg 17866  df-subg 18030  df-cntz 18188  df-lsm 18491  df-cmn 18635  df-abl 18636  df-mgp 18930  df-ur 18942  df-ring 18989  df-oppr 19063  df-dvdsr 19081  df-unit 19082  df-invr 19112  df-dvr 19123  df-drng 19194  df-lmod 19326  df-lss 19394  df-lsp 19434  df-lvec 19565  df-lsatoms 35643  df-lshyp 35644  df-lfl 35725  df-lkr 35753  df-oposet 35843  df-ol 35845  df-oml 35846  df-covers 35933  df-ats 35934  df-atl 35965  df-cvlat 35989  df-hlat 36018  df-llines 36165  df-lplanes 36166  df-lvols 36167  df-lines 36168  df-psubsp 36170  df-pmap 36171  df-padd 36463  df-lhyp 36655  df-laut 36656  df-ldil 36771  df-ltrn 36772  df-trl 36826  df-tgrp 37410  df-tendo 37422  df-edring 37424  df-dveca 37670  df-disoa 37696  df-dvech 37746  df-dib 37806  df-dic 37840  df-dih 37896  df-doch 38015  df-djh 38062
This theorem is referenced by:  dochkr1  38145  dochkr1OLDN  38146  lcfl6lem  38165
  Copyright terms: Public domain W3C validator