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

Theorem hdmap1val 38491
Description: Value of preliminary map from vectors to functionals in the closed kernel dual space. (Restatement of mapdhval 38417.) TODO: change 𝐼 = (𝑥 ∈ V ↦... to (𝜑 → (𝐼‘⟨𝑋, 𝐹, 𝑌 > ) =... in e.g. mapdh8 38481 to shorten proofs with no $d on 𝑥. (Contributed by NM, 15-May-2015.)
Hypotheses
Ref Expression
hdmap1val.h 𝐻 = (LHyp‘𝐾)
hdmap1fval.u 𝑈 = ((DVecH‘𝐾)‘𝑊)
hdmap1fval.v 𝑉 = (Base‘𝑈)
hdmap1fval.s = (-g𝑈)
hdmap1fval.o 0 = (0g𝑈)
hdmap1fval.n 𝑁 = (LSpan‘𝑈)
hdmap1fval.c 𝐶 = ((LCDual‘𝐾)‘𝑊)
hdmap1fval.d 𝐷 = (Base‘𝐶)
hdmap1fval.r 𝑅 = (-g𝐶)
hdmap1fval.q 𝑄 = (0g𝐶)
hdmap1fval.j 𝐽 = (LSpan‘𝐶)
hdmap1fval.m 𝑀 = ((mapd‘𝐾)‘𝑊)
hdmap1fval.i 𝐼 = ((HDMap1‘𝐾)‘𝑊)
hdmap1fval.k (𝜑 → (𝐾𝐴𝑊𝐻))
hdmap1val.x (𝜑𝑋𝑉)
hdmap1val.f (𝜑𝐹𝐷)
hdmap1val.y (𝜑𝑌𝑉)
Assertion
Ref Expression
hdmap1val (𝜑 → (𝐼‘⟨𝑋, 𝐹, 𝑌⟩) = if(𝑌 = 0 , 𝑄, (𝐷 ((𝑀‘(𝑁‘{𝑌})) = (𝐽‘{}) ∧ (𝑀‘(𝑁‘{(𝑋 𝑌)})) = (𝐽‘{(𝐹𝑅)})))))
Distinct variable groups:   𝐶,   𝐷,   ,𝐽   ,𝑀   ,𝑁   𝑈,   ,𝑉   ,𝐹   ,𝑋   ,𝑌   𝜑,
Allowed substitution hints:   𝐴()   𝑄()   𝑅()   𝐻()   𝐼()   𝐾()   ()   𝑊()   0 ()

Proof of Theorem hdmap1val
StepHypRef Expression
1 hdmap1val.h . . 3 𝐻 = (LHyp‘𝐾)
2 hdmap1fval.u . . 3 𝑈 = ((DVecH‘𝐾)‘𝑊)
3 hdmap1fval.v . . 3 𝑉 = (Base‘𝑈)
4 hdmap1fval.s . . 3 = (-g𝑈)
5 hdmap1fval.o . . 3 0 = (0g𝑈)
6 hdmap1fval.n . . 3 𝑁 = (LSpan‘𝑈)
7 hdmap1fval.c . . 3 𝐶 = ((LCDual‘𝐾)‘𝑊)
8 hdmap1fval.d . . 3 𝐷 = (Base‘𝐶)
9 hdmap1fval.r . . 3 𝑅 = (-g𝐶)
10 hdmap1fval.q . . 3 𝑄 = (0g𝐶)
11 hdmap1fval.j . . 3 𝐽 = (LSpan‘𝐶)
12 hdmap1fval.m . . 3 𝑀 = ((mapd‘𝐾)‘𝑊)
13 hdmap1fval.i . . 3 𝐼 = ((HDMap1‘𝐾)‘𝑊)
14 hdmap1fval.k . . 3 (𝜑 → (𝐾𝐴𝑊𝐻))
15 df-ot 4485 . . . 4 𝑋, 𝐹, 𝑌⟩ = ⟨⟨𝑋, 𝐹⟩, 𝑌
16 hdmap1val.x . . . . . 6 (𝜑𝑋𝑉)
17 hdmap1val.f . . . . . 6 (𝜑𝐹𝐷)
18 opelxp 5484 . . . . . 6 (⟨𝑋, 𝐹⟩ ∈ (𝑉 × 𝐷) ↔ (𝑋𝑉𝐹𝐷))
1916, 17, 18sylanbrc 583 . . . . 5 (𝜑 → ⟨𝑋, 𝐹⟩ ∈ (𝑉 × 𝐷))
20 hdmap1val.y . . . . 5 (𝜑𝑌𝑉)
21 opelxp 5484 . . . . 5 (⟨⟨𝑋, 𝐹⟩, 𝑌⟩ ∈ ((𝑉 × 𝐷) × 𝑉) ↔ (⟨𝑋, 𝐹⟩ ∈ (𝑉 × 𝐷) ∧ 𝑌𝑉))
2219, 20, 21sylanbrc 583 . . . 4 (𝜑 → ⟨⟨𝑋, 𝐹⟩, 𝑌⟩ ∈ ((𝑉 × 𝐷) × 𝑉))
2315, 22syl5eqel 2887 . . 3 (𝜑 → ⟨𝑋, 𝐹, 𝑌⟩ ∈ ((𝑉 × 𝐷) × 𝑉))
241, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 23hdmap1vallem 38490 . 2 (𝜑 → (𝐼‘⟨𝑋, 𝐹, 𝑌⟩) = if((2nd ‘⟨𝑋, 𝐹, 𝑌⟩) = 0 , 𝑄, (𝐷 ((𝑀‘(𝑁‘{(2nd ‘⟨𝑋, 𝐹, 𝑌⟩)})) = (𝐽‘{}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st ‘⟨𝑋, 𝐹, 𝑌⟩)) (2nd ‘⟨𝑋, 𝐹, 𝑌⟩))})) = (𝐽‘{((2nd ‘(1st ‘⟨𝑋, 𝐹, 𝑌⟩))𝑅)})))))
25 ot3rdg 7566 . . . . 5 (𝑌𝑉 → (2nd ‘⟨𝑋, 𝐹, 𝑌⟩) = 𝑌)
2620, 25syl 17 . . . 4 (𝜑 → (2nd ‘⟨𝑋, 𝐹, 𝑌⟩) = 𝑌)
2726eqeq1d 2797 . . 3 (𝜑 → ((2nd ‘⟨𝑋, 𝐹, 𝑌⟩) = 0𝑌 = 0 ))
2826sneqd 4488 . . . . . . 7 (𝜑 → {(2nd ‘⟨𝑋, 𝐹, 𝑌⟩)} = {𝑌})
2928fveq2d 6547 . . . . . 6 (𝜑 → (𝑁‘{(2nd ‘⟨𝑋, 𝐹, 𝑌⟩)}) = (𝑁‘{𝑌}))
3029fveqeq2d 6551 . . . . 5 (𝜑 → ((𝑀‘(𝑁‘{(2nd ‘⟨𝑋, 𝐹, 𝑌⟩)})) = (𝐽‘{}) ↔ (𝑀‘(𝑁‘{𝑌})) = (𝐽‘{})))
31 ot1stg 7564 . . . . . . . . . . 11 ((𝑋𝑉𝐹𝐷𝑌𝑉) → (1st ‘(1st ‘⟨𝑋, 𝐹, 𝑌⟩)) = 𝑋)
3216, 17, 20, 31syl3anc 1364 . . . . . . . . . 10 (𝜑 → (1st ‘(1st ‘⟨𝑋, 𝐹, 𝑌⟩)) = 𝑋)
3332, 26oveq12d 7039 . . . . . . . . 9 (𝜑 → ((1st ‘(1st ‘⟨𝑋, 𝐹, 𝑌⟩)) (2nd ‘⟨𝑋, 𝐹, 𝑌⟩)) = (𝑋 𝑌))
3433sneqd 4488 . . . . . . . 8 (𝜑 → {((1st ‘(1st ‘⟨𝑋, 𝐹, 𝑌⟩)) (2nd ‘⟨𝑋, 𝐹, 𝑌⟩))} = {(𝑋 𝑌)})
3534fveq2d 6547 . . . . . . 7 (𝜑 → (𝑁‘{((1st ‘(1st ‘⟨𝑋, 𝐹, 𝑌⟩)) (2nd ‘⟨𝑋, 𝐹, 𝑌⟩))}) = (𝑁‘{(𝑋 𝑌)}))
3635fveq2d 6547 . . . . . 6 (𝜑 → (𝑀‘(𝑁‘{((1st ‘(1st ‘⟨𝑋, 𝐹, 𝑌⟩)) (2nd ‘⟨𝑋, 𝐹, 𝑌⟩))})) = (𝑀‘(𝑁‘{(𝑋 𝑌)})))
37 ot2ndg 7565 . . . . . . . . . 10 ((𝑋𝑉𝐹𝐷𝑌𝑉) → (2nd ‘(1st ‘⟨𝑋, 𝐹, 𝑌⟩)) = 𝐹)
3816, 17, 20, 37syl3anc 1364 . . . . . . . . 9 (𝜑 → (2nd ‘(1st ‘⟨𝑋, 𝐹, 𝑌⟩)) = 𝐹)
3938oveq1d 7036 . . . . . . . 8 (𝜑 → ((2nd ‘(1st ‘⟨𝑋, 𝐹, 𝑌⟩))𝑅) = (𝐹𝑅))
4039sneqd 4488 . . . . . . 7 (𝜑 → {((2nd ‘(1st ‘⟨𝑋, 𝐹, 𝑌⟩))𝑅)} = {(𝐹𝑅)})
4140fveq2d 6547 . . . . . 6 (𝜑 → (𝐽‘{((2nd ‘(1st ‘⟨𝑋, 𝐹, 𝑌⟩))𝑅)}) = (𝐽‘{(𝐹𝑅)}))
4236, 41eqeq12d 2810 . . . . 5 (𝜑 → ((𝑀‘(𝑁‘{((1st ‘(1st ‘⟨𝑋, 𝐹, 𝑌⟩)) (2nd ‘⟨𝑋, 𝐹, 𝑌⟩))})) = (𝐽‘{((2nd ‘(1st ‘⟨𝑋, 𝐹, 𝑌⟩))𝑅)}) ↔ (𝑀‘(𝑁‘{(𝑋 𝑌)})) = (𝐽‘{(𝐹𝑅)})))
4330, 42anbi12d 630 . . . 4 (𝜑 → (((𝑀‘(𝑁‘{(2nd ‘⟨𝑋, 𝐹, 𝑌⟩)})) = (𝐽‘{}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st ‘⟨𝑋, 𝐹, 𝑌⟩)) (2nd ‘⟨𝑋, 𝐹, 𝑌⟩))})) = (𝐽‘{((2nd ‘(1st ‘⟨𝑋, 𝐹, 𝑌⟩))𝑅)})) ↔ ((𝑀‘(𝑁‘{𝑌})) = (𝐽‘{}) ∧ (𝑀‘(𝑁‘{(𝑋 𝑌)})) = (𝐽‘{(𝐹𝑅)}))))
4443riotabidv 6984 . . 3 (𝜑 → (𝐷 ((𝑀‘(𝑁‘{(2nd ‘⟨𝑋, 𝐹, 𝑌⟩)})) = (𝐽‘{}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st ‘⟨𝑋, 𝐹, 𝑌⟩)) (2nd ‘⟨𝑋, 𝐹, 𝑌⟩))})) = (𝐽‘{((2nd ‘(1st ‘⟨𝑋, 𝐹, 𝑌⟩))𝑅)}))) = (𝐷 ((𝑀‘(𝑁‘{𝑌})) = (𝐽‘{}) ∧ (𝑀‘(𝑁‘{(𝑋 𝑌)})) = (𝐽‘{(𝐹𝑅)}))))
4527, 44ifbieq2d 4410 . 2 (𝜑 → if((2nd ‘⟨𝑋, 𝐹, 𝑌⟩) = 0 , 𝑄, (𝐷 ((𝑀‘(𝑁‘{(2nd ‘⟨𝑋, 𝐹, 𝑌⟩)})) = (𝐽‘{}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st ‘⟨𝑋, 𝐹, 𝑌⟩)) (2nd ‘⟨𝑋, 𝐹, 𝑌⟩))})) = (𝐽‘{((2nd ‘(1st ‘⟨𝑋, 𝐹, 𝑌⟩))𝑅)})))) = if(𝑌 = 0 , 𝑄, (𝐷 ((𝑀‘(𝑁‘{𝑌})) = (𝐽‘{}) ∧ (𝑀‘(𝑁‘{(𝑋 𝑌)})) = (𝐽‘{(𝐹𝑅)})))))
4624, 45eqtrd 2831 1 (𝜑 → (𝐼‘⟨𝑋, 𝐹, 𝑌⟩) = if(𝑌 = 0 , 𝑄, (𝐷 ((𝑀‘(𝑁‘{𝑌})) = (𝐽‘{}) ∧ (𝑀‘(𝑁‘{(𝑋 𝑌)})) = (𝐽‘{(𝐹𝑅)})))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1522  wcel 2081  ifcif 4385  {csn 4476  cop 4482  cotp 4484   × cxp 5446  cfv 6230  crio 6981  (class class class)co 7021  1st c1st 7548  2nd c2nd 7549  Basecbs 16317  0gc0g 16547  -gcsg 17868  LSpanclspn 19438  LHypclh 36677  DVecHcdvh 37771  LCDualclcd 38279  mapdcmpd 38317  HDMap1chdma1 38484
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 5086  ax-sep 5099  ax-nul 5106  ax-pow 5162  ax-pr 5226  ax-un 7324
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1082  df-tru 1525  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-ral 3110  df-rex 3111  df-reu 3112  df-rab 3114  df-v 3439  df-sbc 3710  df-csb 3816  df-dif 3866  df-un 3868  df-in 3870  df-ss 3878  df-nul 4216  df-if 4386  df-pw 4459  df-sn 4477  df-pr 4479  df-op 4483  df-ot 4485  df-uni 4750  df-iun 4831  df-br 4967  df-opab 5029  df-mpt 5046  df-id 5353  df-xp 5454  df-rel 5455  df-cnv 5456  df-co 5457  df-dm 5458  df-rn 5459  df-res 5460  df-ima 5461  df-iota 6194  df-fun 6232  df-fn 6233  df-f 6234  df-f1 6235  df-fo 6236  df-f1o 6237  df-fv 6238  df-riota 6982  df-ov 7024  df-1st 7550  df-2nd 7551  df-hdmap1 38486
This theorem is referenced by:  hdmap1val0  38492  hdmap1val2  38493  hdmap1valc  38496
  Copyright terms: Public domain W3C validator