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

Theorem hdmap1valc 35894
Description: Connect the value of the preliminary map from vectors to functionals 𝐼 to the hypothesis 𝐿 used by earlier theorems. Note: the 𝑋 ∈ (𝑉 ∖ { 0 }) hypothesis could be the more general 𝑋𝑉 but the former will be easier to use. TODO: use the 𝐼 function directly in those theorems, so this theorem becomes unnecessary? TODO: The hdmap1cbv 35893 is probably unnecessary, but it would mean different $d's later on. (Contributed by NM, 15-May-2015.)
Hypotheses
Ref Expression
hdmap1valc.h 𝐻 = (LHyp‘𝐾)
hdmap1valc.u 𝑈 = ((DVecH‘𝐾)‘𝑊)
hdmap1valc.v 𝑉 = (Base‘𝑈)
hdmap1valc.s = (-g𝑈)
hdmap1valc.o 0 = (0g𝑈)
hdmap1valc.n 𝑁 = (LSpan‘𝑈)
hdmap1valc.c 𝐶 = ((LCDual‘𝐾)‘𝑊)
hdmap1valc.d 𝐷 = (Base‘𝐶)
hdmap1valc.r 𝑅 = (-g𝐶)
hdmap1valc.q 𝑄 = (0g𝐶)
hdmap1valc.j 𝐽 = (LSpan‘𝐶)
hdmap1valc.m 𝑀 = ((mapd‘𝐾)‘𝑊)
hdmap1valc.i 𝐼 = ((HDMap1‘𝐾)‘𝑊)
hdmap1valc.k (𝜑 → (𝐾 ∈ HL ∧ 𝑊𝐻))
hdmap1valc.x (𝜑𝑋 ∈ (𝑉 ∖ { 0 }))
hdmap1valc.f (𝜑𝐹𝐷)
hdmap1valc.y (𝜑𝑌𝑉)
hdmap1valc.l 𝐿 = (𝑥 ∈ V ↦ if((2nd𝑥) = 0 , 𝑄, (𝐷 ((𝑀‘(𝑁‘{(2nd𝑥)})) = (𝐽‘{}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st𝑥)) (2nd𝑥))})) = (𝐽‘{((2nd ‘(1st𝑥))𝑅)})))))
Assertion
Ref Expression
hdmap1valc (𝜑 → (𝐼‘⟨𝑋, 𝐹, 𝑌⟩) = (𝐿‘⟨𝑋, 𝐹, 𝑌⟩))
Distinct variable groups:   𝑥, 0   𝑥,,𝐷   ,𝐽,𝑥   ,𝑀,𝑥   ,,𝑥   ,𝑁,𝑥   𝑅,,𝑥   𝑥,𝑄
Allowed substitution hints:   𝜑(𝑥,)   𝐶(𝑥,)   𝑄()   𝑈(𝑥,)   𝐹(𝑥,)   𝐻(𝑥,)   𝐼(𝑥,)   𝐾(𝑥,)   𝐿(𝑥,)   𝑉(𝑥,)   𝑊(𝑥,)   𝑋(𝑥,)   𝑌(𝑥,)   0 ()

Proof of Theorem hdmap1valc
Dummy variables 𝑤 𝑔 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 hdmap1valc.h . . 3 𝐻 = (LHyp‘𝐾)
2 hdmap1valc.u . . 3 𝑈 = ((DVecH‘𝐾)‘𝑊)
3 hdmap1valc.v . . 3 𝑉 = (Base‘𝑈)
4 hdmap1valc.s . . 3 = (-g𝑈)
5 hdmap1valc.o . . 3 0 = (0g𝑈)
6 hdmap1valc.n . . 3 𝑁 = (LSpan‘𝑈)
7 hdmap1valc.c . . 3 𝐶 = ((LCDual‘𝐾)‘𝑊)
8 hdmap1valc.d . . 3 𝐷 = (Base‘𝐶)
9 hdmap1valc.r . . 3 𝑅 = (-g𝐶)
10 hdmap1valc.q . . 3 𝑄 = (0g𝐶)
11 hdmap1valc.j . . 3 𝐽 = (LSpan‘𝐶)
12 hdmap1valc.m . . 3 𝑀 = ((mapd‘𝐾)‘𝑊)
13 hdmap1valc.i . . 3 𝐼 = ((HDMap1‘𝐾)‘𝑊)
14 hdmap1valc.k . . 3 (𝜑 → (𝐾 ∈ HL ∧ 𝑊𝐻))
15 hdmap1valc.x . . . 4 (𝜑𝑋 ∈ (𝑉 ∖ { 0 }))
1615eldifad 3551 . . 3 (𝜑𝑋𝑉)
17 hdmap1valc.f . . 3 (𝜑𝐹𝐷)
18 hdmap1valc.y . . 3 (𝜑𝑌𝑉)
191, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 16, 17, 18hdmap1val 35889 . 2 (𝜑 → (𝐼‘⟨𝑋, 𝐹, 𝑌⟩) = if(𝑌 = 0 , 𝑄, (𝑔𝐷 ((𝑀‘(𝑁‘{𝑌})) = (𝐽‘{𝑔}) ∧ (𝑀‘(𝑁‘{(𝑋 𝑌)})) = (𝐽‘{(𝐹𝑅𝑔)})))))
20 hdmap1valc.l . . . 4 𝐿 = (𝑥 ∈ V ↦ if((2nd𝑥) = 0 , 𝑄, (𝐷 ((𝑀‘(𝑁‘{(2nd𝑥)})) = (𝐽‘{}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st𝑥)) (2nd𝑥))})) = (𝐽‘{((2nd ‘(1st𝑥))𝑅)})))))
2120hdmap1cbv 35893 . . 3 𝐿 = (𝑤 ∈ V ↦ if((2nd𝑤) = 0 , 𝑄, (𝑔𝐷 ((𝑀‘(𝑁‘{(2nd𝑤)})) = (𝐽‘{𝑔}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st𝑤)) (2nd𝑤))})) = (𝐽‘{((2nd ‘(1st𝑤))𝑅𝑔)})))))
2210, 21, 16, 17, 18mapdhval 35814 . 2 (𝜑 → (𝐿‘⟨𝑋, 𝐹, 𝑌⟩) = if(𝑌 = 0 , 𝑄, (𝑔𝐷 ((𝑀‘(𝑁‘{𝑌})) = (𝐽‘{𝑔}) ∧ (𝑀‘(𝑁‘{(𝑋 𝑌)})) = (𝐽‘{(𝐹𝑅𝑔)})))))
2319, 22eqtr4d 2646 1 (𝜑 → (𝐼‘⟨𝑋, 𝐹, 𝑌⟩) = (𝐿‘⟨𝑋, 𝐹, 𝑌⟩))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382   = wceq 1474  wcel 1976  Vcvv 3172  cdif 3536  ifcif 4035  {csn 4124  cotp 4132  cmpt 4637  cfv 5789  crio 6487  (class class class)co 6526  1st c1st 7034  2nd c2nd 7035  Basecbs 15643  0gc0g 15871  -gcsg 17195  LSpanclspn 18740  HLchlt 33438  LHypclh 34071  DVecHcdvh 35168  LCDualclcd 35676  mapdcmpd 35714  HDMap1chdma1 35882
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-rep 4693  ax-sep 4703  ax-nul 4711  ax-pow 4763  ax-pr 4827  ax-un 6824
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-ral 2900  df-rex 2901  df-reu 2902  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-op 4131  df-ot 4133  df-uni 4367  df-iun 4451  df-br 4578  df-opab 4638  df-mpt 4639  df-id 4942  df-xp 5033  df-rel 5034  df-cnv 5035  df-co 5036  df-dm 5037  df-rn 5038  df-res 5039  df-ima 5040  df-iota 5753  df-fun 5791  df-fn 5792  df-f 5793  df-f1 5794  df-fo 5795  df-f1o 5796  df-fv 5797  df-riota 6488  df-ov 6529  df-1st 7036  df-2nd 7037  df-hdmap1 35884
This theorem is referenced by:  hdmap1cl  35895  hdmap1eq2  35896  hdmap1eq4N  35897  hdmap1eulem  35914  hdmap1eulemOLDN  35915
  Copyright terms: Public domain W3C validator