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

Theorem dochlkr 37405
Description: Equivalent conditions for the closure of a kernel to be a hyperplane. (Contributed by NM, 29-Oct-2014.)
Hypotheses
Ref Expression
dochlkr.h 𝐻 = (LHyp‘𝐾)
dochlkr.o = ((ocH‘𝐾)‘𝑊)
dochlkr.u 𝑈 = ((DVecH‘𝐾)‘𝑊)
dochlkr.f 𝐹 = (LFnl‘𝑈)
dochlkr.y 𝑌 = (LSHyp‘𝑈)
dochlkr.l 𝐿 = (LKer‘𝑈)
dochlkr.k (𝜑 → (𝐾 ∈ HL ∧ 𝑊𝐻))
dochlkr.g (𝜑𝐺𝐹)
Assertion
Ref Expression
dochlkr (𝜑 → (( ‘( ‘(𝐿𝐺))) ∈ 𝑌 ↔ (( ‘( ‘(𝐿𝐺))) = (𝐿𝐺) ∧ (𝐿𝐺) ∈ 𝑌)))

Proof of Theorem dochlkr
StepHypRef Expression
1 dochlkr.k . . . . . . . 8 (𝜑 → (𝐾 ∈ HL ∧ 𝑊𝐻))
2 eqid 2800 . . . . . . . . 9 (Base‘𝑈) = (Base‘𝑈)
3 dochlkr.f . . . . . . . . 9 𝐹 = (LFnl‘𝑈)
4 dochlkr.l . . . . . . . . 9 𝐿 = (LKer‘𝑈)
5 dochlkr.h . . . . . . . . . 10 𝐻 = (LHyp‘𝐾)
6 dochlkr.u . . . . . . . . . 10 𝑈 = ((DVecH‘𝐾)‘𝑊)
75, 6, 1dvhlmod 37130 . . . . . . . . 9 (𝜑𝑈 ∈ LMod)
8 dochlkr.g . . . . . . . . 9 (𝜑𝐺𝐹)
92, 3, 4, 7, 8lkrssv 35116 . . . . . . . 8 (𝜑 → (𝐿𝐺) ⊆ (Base‘𝑈))
10 dochlkr.o . . . . . . . . 9 = ((ocH‘𝐾)‘𝑊)
115, 6, 2, 10dochocss 37386 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐿𝐺) ⊆ (Base‘𝑈)) → (𝐿𝐺) ⊆ ( ‘( ‘(𝐿𝐺))))
121, 9, 11syl2anc 580 . . . . . . 7 (𝜑 → (𝐿𝐺) ⊆ ( ‘( ‘(𝐿𝐺))))
1312adantr 473 . . . . . 6 ((𝜑 ∧ ( ‘( ‘(𝐿𝐺))) ∈ 𝑌) → (𝐿𝐺) ⊆ ( ‘( ‘(𝐿𝐺))))
14 dochlkr.y . . . . . . 7 𝑌 = (LSHyp‘𝑈)
155, 6, 1dvhlvec 37129 . . . . . . . 8 (𝜑𝑈 ∈ LVec)
1615adantr 473 . . . . . . 7 ((𝜑 ∧ ( ‘( ‘(𝐿𝐺))) ∈ 𝑌) → 𝑈 ∈ LVec)
177adantr 473 . . . . . . . . . . 11 ((𝜑 ∧ ( ‘( ‘(𝐿𝐺))) ∈ 𝑌) → 𝑈 ∈ LMod)
18 simpr 478 . . . . . . . . . . 11 ((𝜑 ∧ ( ‘( ‘(𝐿𝐺))) ∈ 𝑌) → ( ‘( ‘(𝐿𝐺))) ∈ 𝑌)
192, 14, 17, 18lshpne 35002 . . . . . . . . . 10 ((𝜑 ∧ ( ‘( ‘(𝐿𝐺))) ∈ 𝑌) → ( ‘( ‘(𝐿𝐺))) ≠ (Base‘𝑈))
2019ex 402 . . . . . . . . 9 (𝜑 → (( ‘( ‘(𝐿𝐺))) ∈ 𝑌 → ( ‘( ‘(𝐿𝐺))) ≠ (Base‘𝑈)))
212, 14, 3, 4, 15, 8lkrshpor 35127 . . . . . . . . . . . 12 (𝜑 → ((𝐿𝐺) ∈ 𝑌 ∨ (𝐿𝐺) = (Base‘𝑈)))
2221ord 891 . . . . . . . . . . 11 (𝜑 → (¬ (𝐿𝐺) ∈ 𝑌 → (𝐿𝐺) = (Base‘𝑈)))
23 2fveq3 6417 . . . . . . . . . . . . . 14 ((𝐿𝐺) = (Base‘𝑈) → ( ‘( ‘(𝐿𝐺))) = ( ‘( ‘(Base‘𝑈))))
2423adantl 474 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝐿𝐺) = (Base‘𝑈)) → ( ‘( ‘(𝐿𝐺))) = ( ‘( ‘(Base‘𝑈))))
251adantr 473 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝐿𝐺) = (Base‘𝑈)) → (𝐾 ∈ HL ∧ 𝑊𝐻))
265, 6, 10, 2, 25dochoc1 37381 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝐿𝐺) = (Base‘𝑈)) → ( ‘( ‘(Base‘𝑈))) = (Base‘𝑈))
2724, 26eqtrd 2834 . . . . . . . . . . . 12 ((𝜑 ∧ (𝐿𝐺) = (Base‘𝑈)) → ( ‘( ‘(𝐿𝐺))) = (Base‘𝑈))
2827ex 402 . . . . . . . . . . 11 (𝜑 → ((𝐿𝐺) = (Base‘𝑈) → ( ‘( ‘(𝐿𝐺))) = (Base‘𝑈)))
2922, 28syld 47 . . . . . . . . . 10 (𝜑 → (¬ (𝐿𝐺) ∈ 𝑌 → ( ‘( ‘(𝐿𝐺))) = (Base‘𝑈)))
3029necon1ad 2989 . . . . . . . . 9 (𝜑 → (( ‘( ‘(𝐿𝐺))) ≠ (Base‘𝑈) → (𝐿𝐺) ∈ 𝑌))
3120, 30syld 47 . . . . . . . 8 (𝜑 → (( ‘( ‘(𝐿𝐺))) ∈ 𝑌 → (𝐿𝐺) ∈ 𝑌))
3231imp 396 . . . . . . 7 ((𝜑 ∧ ( ‘( ‘(𝐿𝐺))) ∈ 𝑌) → (𝐿𝐺) ∈ 𝑌)
3314, 16, 32, 18lshpcmp 35008 . . . . . 6 ((𝜑 ∧ ( ‘( ‘(𝐿𝐺))) ∈ 𝑌) → ((𝐿𝐺) ⊆ ( ‘( ‘(𝐿𝐺))) ↔ (𝐿𝐺) = ( ‘( ‘(𝐿𝐺)))))
3413, 33mpbid 224 . . . . 5 ((𝜑 ∧ ( ‘( ‘(𝐿𝐺))) ∈ 𝑌) → (𝐿𝐺) = ( ‘( ‘(𝐿𝐺))))
3534eqcomd 2806 . . . 4 ((𝜑 ∧ ( ‘( ‘(𝐿𝐺))) ∈ 𝑌) → ( ‘( ‘(𝐿𝐺))) = (𝐿𝐺))
3635, 32jca 508 . . 3 ((𝜑 ∧ ( ‘( ‘(𝐿𝐺))) ∈ 𝑌) → (( ‘( ‘(𝐿𝐺))) = (𝐿𝐺) ∧ (𝐿𝐺) ∈ 𝑌))
3736ex 402 . 2 (𝜑 → (( ‘( ‘(𝐿𝐺))) ∈ 𝑌 → (( ‘( ‘(𝐿𝐺))) = (𝐿𝐺) ∧ (𝐿𝐺) ∈ 𝑌)))
38 eleq1 2867 . . 3 (( ‘( ‘(𝐿𝐺))) = (𝐿𝐺) → (( ‘( ‘(𝐿𝐺))) ∈ 𝑌 ↔ (𝐿𝐺) ∈ 𝑌))
3938biimpar 470 . 2 ((( ‘( ‘(𝐿𝐺))) = (𝐿𝐺) ∧ (𝐿𝐺) ∈ 𝑌) → ( ‘( ‘(𝐿𝐺))) ∈ 𝑌)
4037, 39impbid1 217 1 (𝜑 → (( ‘( ‘(𝐿𝐺))) ∈ 𝑌 ↔ (( ‘( ‘(𝐿𝐺))) = (𝐿𝐺) ∧ (𝐿𝐺) ∈ 𝑌)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 198  wa 385   = wceq 1653  wcel 2157  wne 2972  wss 3770  cfv 6102  Basecbs 16183  LModclmod 19180  LVecclvec 19422  LSHypclsh 34995  LFnlclfn 35077  LKerclk 35105  HLchlt 35370  LHypclh 36004  DVecHcdvh 37098  ocHcoch 37367
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-8 2159  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2378  ax-ext 2778  ax-rep 4965  ax-sep 4976  ax-nul 4984  ax-pow 5036  ax-pr 5098  ax-un 7184  ax-cnex 10281  ax-resscn 10282  ax-1cn 10283  ax-icn 10284  ax-addcl 10285  ax-addrcl 10286  ax-mulcl 10287  ax-mulrcl 10288  ax-mulcom 10289  ax-addass 10290  ax-mulass 10291  ax-distr 10292  ax-i2m1 10293  ax-1ne0 10294  ax-1rid 10295  ax-rnegex 10296  ax-rrecex 10297  ax-cnre 10298  ax-pre-lttri 10299  ax-pre-lttrn 10300  ax-pre-ltadd 10301  ax-pre-mulgt0 10302  ax-riotaBAD 34973
This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-3or 1109  df-3an 1110  df-tru 1657  df-fal 1667  df-ex 1876  df-nf 1880  df-sb 2065  df-mo 2592  df-eu 2610  df-clab 2787  df-cleq 2793  df-clel 2796  df-nfc 2931  df-ne 2973  df-nel 3076  df-ral 3095  df-rex 3096  df-reu 3097  df-rmo 3098  df-rab 3099  df-v 3388  df-sbc 3635  df-csb 3730  df-dif 3773  df-un 3775  df-in 3777  df-ss 3784  df-pss 3786  df-nul 4117  df-if 4279  df-pw 4352  df-sn 4370  df-pr 4372  df-tp 4374  df-op 4376  df-uni 4630  df-int 4669  df-iun 4713  df-iin 4714  df-br 4845  df-opab 4907  df-mpt 4924  df-tr 4947  df-id 5221  df-eprel 5226  df-po 5234  df-so 5235  df-fr 5272  df-we 5274  df-xp 5319  df-rel 5320  df-cnv 5321  df-co 5322  df-dm 5323  df-rn 5324  df-res 5325  df-ima 5326  df-pred 5899  df-ord 5945  df-on 5946  df-lim 5947  df-suc 5948  df-iota 6065  df-fun 6104  df-fn 6105  df-f 6106  df-f1 6107  df-fo 6108  df-f1o 6109  df-fv 6110  df-riota 6840  df-ov 6882  df-oprab 6883  df-mpt2 6884  df-om 7301  df-1st 7402  df-2nd 7403  df-tpos 7591  df-undef 7638  df-wrecs 7646  df-recs 7708  df-rdg 7746  df-1o 7800  df-oadd 7804  df-er 7983  df-map 8098  df-en 8197  df-dom 8198  df-sdom 8199  df-fin 8200  df-pnf 10366  df-mnf 10367  df-xr 10368  df-ltxr 10369  df-le 10370  df-sub 10559  df-neg 10560  df-nn 11314  df-2 11375  df-3 11376  df-4 11377  df-5 11378  df-6 11379  df-n0 11580  df-z 11666  df-uz 11930  df-fz 12580  df-struct 16185  df-ndx 16186  df-slot 16187  df-base 16189  df-sets 16190  df-ress 16191  df-plusg 16279  df-mulr 16280  df-sca 16282  df-vsca 16283  df-0g 16416  df-proset 17242  df-poset 17260  df-plt 17272  df-lub 17288  df-glb 17289  df-join 17290  df-meet 17291  df-p0 17353  df-p1 17354  df-lat 17360  df-clat 17422  df-mgm 17556  df-sgrp 17598  df-mnd 17609  df-submnd 17650  df-grp 17740  df-minusg 17741  df-sbg 17742  df-subg 17903  df-cntz 18061  df-lsm 18363  df-cmn 18509  df-abl 18510  df-mgp 18805  df-ur 18817  df-ring 18864  df-oppr 18938  df-dvdsr 18956  df-unit 18957  df-invr 18987  df-dvr 18998  df-drng 19066  df-lmod 19182  df-lss 19250  df-lsp 19292  df-lvec 19423  df-lsatoms 34996  df-lshyp 34997  df-lfl 35078  df-lkr 35106  df-oposet 35196  df-ol 35198  df-oml 35199  df-covers 35286  df-ats 35287  df-atl 35318  df-cvlat 35342  df-hlat 35371  df-llines 35518  df-lplanes 35519  df-lvols 35520  df-lines 35521  df-psubsp 35523  df-pmap 35524  df-padd 35816  df-lhyp 36008  df-laut 36009  df-ldil 36124  df-ltrn 36125  df-trl 36179  df-tendo 36775  df-edring 36777  df-disoa 37049  df-dvech 37099  df-dib 37159  df-dic 37193  df-dih 37249  df-doch 37368
This theorem is referenced by:  dochkrshp  37406  dochkrshp2  37407  mapdordlem1a  37654  mapdordlem2  37657
  Copyright terms: Public domain W3C validator