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

Theorem mapdhcl 39710
Description: Lemmma for ~? mapdh . (Contributed by NM, 3-Apr-2015.)
Hypotheses
Ref Expression
mapdh.q 𝑄 = (0g𝐶)
mapdh.i 𝐼 = (𝑥 ∈ V ↦ if((2nd𝑥) = 0 , 𝑄, (𝐷 ((𝑀‘(𝑁‘{(2nd𝑥)})) = (𝐽‘{}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st𝑥)) (2nd𝑥))})) = (𝐽‘{((2nd ‘(1st𝑥))𝑅)})))))
mapdh.h 𝐻 = (LHyp‘𝐾)
mapdh.m 𝑀 = ((mapd‘𝐾)‘𝑊)
mapdh.u 𝑈 = ((DVecH‘𝐾)‘𝑊)
mapdh.v 𝑉 = (Base‘𝑈)
mapdh.s = (-g𝑈)
mapdhc.o 0 = (0g𝑈)
mapdh.n 𝑁 = (LSpan‘𝑈)
mapdh.c 𝐶 = ((LCDual‘𝐾)‘𝑊)
mapdh.d 𝐷 = (Base‘𝐶)
mapdh.r 𝑅 = (-g𝐶)
mapdh.j 𝐽 = (LSpan‘𝐶)
mapdh.k (𝜑 → (𝐾 ∈ HL ∧ 𝑊𝐻))
mapdhc.f (𝜑𝐹𝐷)
mapdh.mn (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐹}))
mapdhcl.x (𝜑𝑋 ∈ (𝑉 ∖ { 0 }))
mapdhc.y (𝜑𝑌𝑉)
mapdh.ne (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))
Assertion
Ref Expression
mapdhcl (𝜑 → (𝐼‘⟨𝑋, 𝐹, 𝑌⟩) ∈ 𝐷)
Distinct variable groups:   𝑥,𝐷,   ,𝐹,𝑥   𝑥,𝐽   𝑥,𝑀   𝑥,𝑁   𝑥, 0   𝑥,𝑄   𝑥,𝑅   𝑥,   ,𝑋,𝑥   ,𝑌,𝑥   𝜑,   0 ,   𝐶,   𝐷,   ,𝐽   ,𝑀   ,𝑁   𝑅,   𝑈,   ,
Allowed substitution hints:   𝜑(𝑥)   𝐶(𝑥)   𝑄()   𝑈(𝑥)   𝐻(𝑥,)   𝐼(𝑥,)   𝐾(𝑥,)   𝑉(𝑥,)   𝑊(𝑥,)

Proof of Theorem mapdhcl
StepHypRef Expression
1 oteq3 4817 . . . 4 (𝑌 = 0 → ⟨𝑋, 𝐹, 𝑌⟩ = ⟨𝑋, 𝐹, 0 ⟩)
21fveq2d 6765 . . 3 (𝑌 = 0 → (𝐼‘⟨𝑋, 𝐹, 𝑌⟩) = (𝐼‘⟨𝑋, 𝐹, 0 ⟩))
32eleq1d 2821 . 2 (𝑌 = 0 → ((𝐼‘⟨𝑋, 𝐹, 𝑌⟩) ∈ 𝐷 ↔ (𝐼‘⟨𝑋, 𝐹, 0 ⟩) ∈ 𝐷))
4 mapdh.q . . . 4 𝑄 = (0g𝐶)
5 mapdh.i . . . 4 𝐼 = (𝑥 ∈ V ↦ if((2nd𝑥) = 0 , 𝑄, (𝐷 ((𝑀‘(𝑁‘{(2nd𝑥)})) = (𝐽‘{}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st𝑥)) (2nd𝑥))})) = (𝐽‘{((2nd ‘(1st𝑥))𝑅)})))))
6 mapdhcl.x . . . . 5 (𝜑𝑋 ∈ (𝑉 ∖ { 0 }))
76adantr 480 . . . 4 ((𝜑𝑌0 ) → 𝑋 ∈ (𝑉 ∖ { 0 }))
8 mapdhc.f . . . . 5 (𝜑𝐹𝐷)
98adantr 480 . . . 4 ((𝜑𝑌0 ) → 𝐹𝐷)
10 mapdhc.y . . . . . 6 (𝜑𝑌𝑉)
1110anim1i 614 . . . . 5 ((𝜑𝑌0 ) → (𝑌𝑉𝑌0 ))
12 eldifsn 4722 . . . . 5 (𝑌 ∈ (𝑉 ∖ { 0 }) ↔ (𝑌𝑉𝑌0 ))
1311, 12sylibr 233 . . . 4 ((𝜑𝑌0 ) → 𝑌 ∈ (𝑉 ∖ { 0 }))
144, 5, 7, 9, 13mapdhval2 39709 . . 3 ((𝜑𝑌0 ) → (𝐼‘⟨𝑋, 𝐹, 𝑌⟩) = (𝐷 ((𝑀‘(𝑁‘{𝑌})) = (𝐽‘{}) ∧ (𝑀‘(𝑁‘{(𝑋 𝑌)})) = (𝐽‘{(𝐹𝑅)}))))
15 mapdh.h . . . . 5 𝐻 = (LHyp‘𝐾)
16 mapdh.m . . . . 5 𝑀 = ((mapd‘𝐾)‘𝑊)
17 mapdh.u . . . . 5 𝑈 = ((DVecH‘𝐾)‘𝑊)
18 mapdh.v . . . . 5 𝑉 = (Base‘𝑈)
19 mapdh.s . . . . 5 = (-g𝑈)
20 mapdhc.o . . . . 5 0 = (0g𝑈)
21 mapdh.n . . . . 5 𝑁 = (LSpan‘𝑈)
22 mapdh.c . . . . 5 𝐶 = ((LCDual‘𝐾)‘𝑊)
23 mapdh.d . . . . 5 𝐷 = (Base‘𝐶)
24 mapdh.r . . . . 5 𝑅 = (-g𝐶)
25 mapdh.j . . . . 5 𝐽 = (LSpan‘𝐶)
26 mapdh.k . . . . . 6 (𝜑 → (𝐾 ∈ HL ∧ 𝑊𝐻))
2726adantr 480 . . . . 5 ((𝜑𝑌0 ) → (𝐾 ∈ HL ∧ 𝑊𝐻))
28 mapdh.ne . . . . . 6 (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))
2928adantr 480 . . . . 5 ((𝜑𝑌0 ) → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))
30 mapdh.mn . . . . . 6 (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐹}))
3130adantr 480 . . . . 5 ((𝜑𝑌0 ) → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐹}))
3215, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 27, 7, 13, 9, 29, 31mapdpg 39689 . . . 4 ((𝜑𝑌0 ) → ∃!𝐷 ((𝑀‘(𝑁‘{𝑌})) = (𝐽‘{}) ∧ (𝑀‘(𝑁‘{(𝑋 𝑌)})) = (𝐽‘{(𝐹𝑅)})))
33 riotacl 7235 . . . 4 (∃!𝐷 ((𝑀‘(𝑁‘{𝑌})) = (𝐽‘{}) ∧ (𝑀‘(𝑁‘{(𝑋 𝑌)})) = (𝐽‘{(𝐹𝑅)})) → (𝐷 ((𝑀‘(𝑁‘{𝑌})) = (𝐽‘{}) ∧ (𝑀‘(𝑁‘{(𝑋 𝑌)})) = (𝐽‘{(𝐹𝑅)}))) ∈ 𝐷)
3432, 33syl 17 . . 3 ((𝜑𝑌0 ) → (𝐷 ((𝑀‘(𝑁‘{𝑌})) = (𝐽‘{}) ∧ (𝑀‘(𝑁‘{(𝑋 𝑌)})) = (𝐽‘{(𝐹𝑅)}))) ∈ 𝐷)
3514, 34eqeltrd 2837 . 2 ((𝜑𝑌0 ) → (𝐼‘⟨𝑋, 𝐹, 𝑌⟩) ∈ 𝐷)
364, 5, 20, 6, 8mapdhval0 39708 . . 3 (𝜑 → (𝐼‘⟨𝑋, 𝐹, 0 ⟩) = 𝑄)
3715, 22, 23, 4, 26lcd0vcl 39597 . . 3 (𝜑𝑄𝐷)
3836, 37eqeltrd 2837 . 2 (𝜑 → (𝐼‘⟨𝑋, 𝐹, 0 ⟩) ∈ 𝐷)
393, 35, 38pm2.61ne 3028 1 (𝜑 → (𝐼‘⟨𝑋, 𝐹, 𝑌⟩) ∈ 𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395   = wceq 1539  wcel 2107  wne 2941  ∃!wreu 3064  Vcvv 3427  cdif 3885  ifcif 4461  {csn 4563  cotp 4571  cmpt 5158  cfv 6423  crio 7216  (class class class)co 7260  1st c1st 7807  2nd c2nd 7808  Basecbs 16856  0gc0g 17094  -gcsg 18523  LSpanclspn 20177  HLchlt 37333  LHypclh 37967  DVecHcdvh 39061  LCDualclcd 39569  mapdcmpd 39607
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-rep 5210  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7571  ax-cnex 10874  ax-resscn 10875  ax-1cn 10876  ax-icn 10877  ax-addcl 10878  ax-addrcl 10879  ax-mulcl 10880  ax-mulrcl 10881  ax-mulcom 10882  ax-addass 10883  ax-mulass 10884  ax-distr 10885  ax-i2m1 10886  ax-1ne0 10887  ax-1rid 10888  ax-rnegex 10889  ax-rrecex 10890  ax-cnre 10891  ax-pre-lttri 10892  ax-pre-lttrn 10893  ax-pre-ltadd 10894  ax-pre-mulgt0 10895  ax-riotaBAD 36936
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3067  df-rex 3068  df-reu 3069  df-rmo 3070  df-rab 3071  df-v 3429  df-sbc 3717  df-csb 3834  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-pss 3907  df-nul 4259  df-if 4462  df-pw 4537  df-sn 4564  df-pr 4566  df-tp 4568  df-op 4570  df-ot 4572  df-uni 4842  df-int 4882  df-iun 4928  df-iin 4929  df-br 5076  df-opab 5138  df-mpt 5159  df-tr 5193  df-id 5485  df-eprel 5491  df-po 5499  df-so 5500  df-fr 5540  df-we 5542  df-xp 5591  df-rel 5592  df-cnv 5593  df-co 5594  df-dm 5595  df-rn 5596  df-res 5597  df-ima 5598  df-pred 6196  df-ord 6259  df-on 6260  df-lim 6261  df-suc 6262  df-iota 6381  df-fun 6425  df-fn 6426  df-f 6427  df-f1 6428  df-fo 6429  df-f1o 6430  df-fv 6431  df-riota 7217  df-ov 7263  df-oprab 7264  df-mpo 7265  df-of 7516  df-om 7693  df-1st 7809  df-2nd 7810  df-tpos 8018  df-undef 8065  df-frecs 8073  df-wrecs 8104  df-recs 8178  df-rdg 8217  df-1o 8272  df-er 8461  df-map 8580  df-en 8697  df-dom 8698  df-sdom 8699  df-fin 8700  df-pnf 10958  df-mnf 10959  df-xr 10960  df-ltxr 10961  df-le 10962  df-sub 11153  df-neg 11154  df-nn 11920  df-2 11982  df-3 11983  df-4 11984  df-5 11985  df-6 11986  df-n0 12180  df-z 12266  df-uz 12528  df-fz 13185  df-struct 16792  df-sets 16809  df-slot 16827  df-ndx 16839  df-base 16857  df-ress 16886  df-plusg 16919  df-mulr 16920  df-sca 16922  df-vsca 16923  df-0g 17096  df-mre 17239  df-mrc 17240  df-acs 17242  df-proset 17957  df-poset 17975  df-plt 17992  df-lub 18008  df-glb 18009  df-join 18010  df-meet 18011  df-p0 18087  df-p1 18088  df-lat 18094  df-clat 18161  df-mgm 18270  df-sgrp 18319  df-mnd 18330  df-submnd 18375  df-grp 18524  df-minusg 18525  df-sbg 18526  df-subg 18696  df-cntz 18867  df-oppg 18894  df-lsm 19185  df-cmn 19332  df-abl 19333  df-mgp 19665  df-ur 19682  df-ring 19729  df-oppr 19806  df-dvdsr 19827  df-unit 19828  df-invr 19858  df-dvr 19869  df-drng 19937  df-lmod 20069  df-lss 20138  df-lsp 20178  df-lvec 20309  df-lsatoms 36959  df-lshyp 36960  df-lcv 37002  df-lfl 37041  df-lkr 37069  df-ldual 37107  df-oposet 37159  df-ol 37161  df-oml 37162  df-covers 37249  df-ats 37250  df-atl 37281  df-cvlat 37305  df-hlat 37334  df-llines 37481  df-lplanes 37482  df-lvols 37483  df-lines 37484  df-psubsp 37486  df-pmap 37487  df-padd 37779  df-lhyp 37971  df-laut 37972  df-ldil 38087  df-ltrn 38088  df-trl 38142  df-tgrp 38726  df-tendo 38738  df-edring 38740  df-dveca 38986  df-disoa 39012  df-dvech 39062  df-dib 39122  df-dic 39156  df-dih 39212  df-doch 39331  df-djh 39378  df-lcdual 39570  df-mapd 39608
This theorem is referenced by:  mapdheq4lem  39714  mapdheq4  39715  mapdh6lem1N  39716  mapdh6lem2N  39717  mapdh6aN  39718  mapdh6bN  39720  mapdh6cN  39721  mapdh6dN  39722  mapdh6hN  39726  mapdh7eN  39731  mapdh7cN  39732  mapdh7fN  39734  mapdh75e  39735  mapdh75fN  39738  mapdh8aa  39759  mapdh8d0N  39765  mapdh8d  39766  mapdh9a  39772  mapdh9aOLDN  39773  hdmap1cl  39787  hdmap1eulem  39805  hdmap1eulemOLDN  39806
  Copyright terms: Public domain W3C validator