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

Theorem mapdpglem25 39307
 Description: Lemma for mapdpg 39316. Baer p. 45 line 12: "Then we have Gy' = Gy'' and G(x'-y') = G(x'-y'')." (Contributed by NM, 21-Mar-2015.)
Hypotheses
Ref Expression
mapdpg.h 𝐻 = (LHyp‘𝐾)
mapdpg.m 𝑀 = ((mapd‘𝐾)‘𝑊)
mapdpg.u 𝑈 = ((DVecH‘𝐾)‘𝑊)
mapdpg.v 𝑉 = (Base‘𝑈)
mapdpg.s = (-g𝑈)
mapdpg.z 0 = (0g𝑈)
mapdpg.n 𝑁 = (LSpan‘𝑈)
mapdpg.c 𝐶 = ((LCDual‘𝐾)‘𝑊)
mapdpg.f 𝐹 = (Base‘𝐶)
mapdpg.r 𝑅 = (-g𝐶)
mapdpg.j 𝐽 = (LSpan‘𝐶)
mapdpg.k (𝜑 → (𝐾 ∈ HL ∧ 𝑊𝐻))
mapdpg.x (𝜑𝑋 ∈ (𝑉 ∖ { 0 }))
mapdpg.y (𝜑𝑌 ∈ (𝑉 ∖ { 0 }))
mapdpg.g (𝜑𝐺𝐹)
mapdpg.ne (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))
mapdpg.e (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐺}))
mapdpgem25.h1 (𝜑 → (𝐹 ∧ ((𝑀‘(𝑁‘{𝑌})) = (𝐽‘{}) ∧ (𝑀‘(𝑁‘{(𝑋 𝑌)})) = (𝐽‘{(𝐺𝑅)}))))
mapdpgem25.i1 (𝜑 → (𝑖𝐹 ∧ ((𝑀‘(𝑁‘{𝑌})) = (𝐽‘{𝑖}) ∧ (𝑀‘(𝑁‘{(𝑋 𝑌)})) = (𝐽‘{(𝐺𝑅𝑖)}))))
Assertion
Ref Expression
mapdpglem25 (𝜑 → ((𝐽‘{}) = (𝐽‘{𝑖}) ∧ (𝐽‘{(𝐺𝑅)}) = (𝐽‘{(𝐺𝑅𝑖)})))

Proof of Theorem mapdpglem25
StepHypRef Expression
1 mapdpgem25.h1 . . . . 5 (𝜑 → (𝐹 ∧ ((𝑀‘(𝑁‘{𝑌})) = (𝐽‘{}) ∧ (𝑀‘(𝑁‘{(𝑋 𝑌)})) = (𝐽‘{(𝐺𝑅)}))))
21simprd 499 . . . 4 (𝜑 → ((𝑀‘(𝑁‘{𝑌})) = (𝐽‘{}) ∧ (𝑀‘(𝑁‘{(𝑋 𝑌)})) = (𝐽‘{(𝐺𝑅)})))
32simpld 498 . . 3 (𝜑 → (𝑀‘(𝑁‘{𝑌})) = (𝐽‘{}))
4 mapdpgem25.i1 . . . . 5 (𝜑 → (𝑖𝐹 ∧ ((𝑀‘(𝑁‘{𝑌})) = (𝐽‘{𝑖}) ∧ (𝑀‘(𝑁‘{(𝑋 𝑌)})) = (𝐽‘{(𝐺𝑅𝑖)}))))
54simprd 499 . . . 4 (𝜑 → ((𝑀‘(𝑁‘{𝑌})) = (𝐽‘{𝑖}) ∧ (𝑀‘(𝑁‘{(𝑋 𝑌)})) = (𝐽‘{(𝐺𝑅𝑖)})))
65simpld 498 . . 3 (𝜑 → (𝑀‘(𝑁‘{𝑌})) = (𝐽‘{𝑖}))
73, 6eqtr3d 2795 . 2 (𝜑 → (𝐽‘{}) = (𝐽‘{𝑖}))
82simprd 499 . . 3 (𝜑 → (𝑀‘(𝑁‘{(𝑋 𝑌)})) = (𝐽‘{(𝐺𝑅)}))
95simprd 499 . . 3 (𝜑 → (𝑀‘(𝑁‘{(𝑋 𝑌)})) = (𝐽‘{(𝐺𝑅𝑖)}))
108, 9eqtr3d 2795 . 2 (𝜑 → (𝐽‘{(𝐺𝑅)}) = (𝐽‘{(𝐺𝑅𝑖)}))
117, 10jca 515 1 (𝜑 → ((𝐽‘{}) = (𝐽‘{𝑖}) ∧ (𝐽‘{(𝐺𝑅)}) = (𝐽‘{(𝐺𝑅𝑖)})))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   = wceq 1538   ∈ wcel 2111   ≠ wne 2951   ∖ cdif 3857  {csn 4525  ‘cfv 6340  (class class class)co 7156  Basecbs 16554  0gc0g 16784  -gcsg 18184  LSpanclspn 19824  HLchlt 36960  LHypclh 37594  DVecHcdvh 38688  LCDualclcd 39196  mapdcmpd 39234 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2121  ax-ext 2729 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2750 This theorem is referenced by:  mapdpglem26  39308  mapdpglem27  39309
 Copyright terms: Public domain W3C validator