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

Theorem mapdpglem25 40210
Description: Lemma for mapdpg 40219. 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 497 . . . 4 (πœ‘ β†’ ((π‘€β€˜(π‘β€˜{π‘Œ})) = (π½β€˜{β„Ž}) ∧ (π‘€β€˜(π‘β€˜{(𝑋 βˆ’ π‘Œ)})) = (π½β€˜{(πΊπ‘…β„Ž)})))
32simpld 496 . . 3 (πœ‘ β†’ (π‘€β€˜(π‘β€˜{π‘Œ})) = (π½β€˜{β„Ž}))
4 mapdpgem25.i1 . . . . 5 (πœ‘ β†’ (𝑖 ∈ 𝐹 ∧ ((π‘€β€˜(π‘β€˜{π‘Œ})) = (π½β€˜{𝑖}) ∧ (π‘€β€˜(π‘β€˜{(𝑋 βˆ’ π‘Œ)})) = (π½β€˜{(𝐺𝑅𝑖)}))))
54simprd 497 . . . 4 (πœ‘ β†’ ((π‘€β€˜(π‘β€˜{π‘Œ})) = (π½β€˜{𝑖}) ∧ (π‘€β€˜(π‘β€˜{(𝑋 βˆ’ π‘Œ)})) = (π½β€˜{(𝐺𝑅𝑖)})))
65simpld 496 . . 3 (πœ‘ β†’ (π‘€β€˜(π‘β€˜{π‘Œ})) = (π½β€˜{𝑖}))
73, 6eqtr3d 2775 . 2 (πœ‘ β†’ (π½β€˜{β„Ž}) = (π½β€˜{𝑖}))
82simprd 497 . . 3 (πœ‘ β†’ (π‘€β€˜(π‘β€˜{(𝑋 βˆ’ π‘Œ)})) = (π½β€˜{(πΊπ‘…β„Ž)}))
95simprd 497 . . 3 (πœ‘ β†’ (π‘€β€˜(π‘β€˜{(𝑋 βˆ’ π‘Œ)})) = (π½β€˜{(𝐺𝑅𝑖)}))
108, 9eqtr3d 2775 . 2 (πœ‘ β†’ (π½β€˜{(πΊπ‘…β„Ž)}) = (π½β€˜{(𝐺𝑅𝑖)}))
117, 10jca 513 1 (πœ‘ β†’ ((π½β€˜{β„Ž}) = (π½β€˜{𝑖}) ∧ (π½β€˜{(πΊπ‘…β„Ž)}) = (π½β€˜{(𝐺𝑅𝑖)})))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ∧ wa 397   = wceq 1542   ∈ wcel 2107   β‰  wne 2940   βˆ– cdif 3911  {csn 4590  β€˜cfv 6500  (class class class)co 7361  Basecbs 17091  0gc0g 17329  -gcsg 18758  LSpanclspn 20476  HLchlt 37862  LHypclh 38497  DVecHcdvh 39591  LCDualclcd 40099  mapdcmpd 40137
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725
This theorem is referenced by:  mapdpglem26  40211  mapdpglem27  40212
  Copyright terms: Public domain W3C validator