Theorem mapdpglem25 39638

Description: Lemma for mapdpg 39647. 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

Step	Hyp	Ref	Expression
1		mapdpgem25.h1	. . . . 5 ⊢ (𝜑 → (ℎ ∈ 𝐹 ∧ ((𝑀‘(𝑁‘{𝑌})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{(𝐺𝑅ℎ)}))))
2	1	simprd 495	. . . 4 ⊢ (𝜑 → ((𝑀‘(𝑁‘{𝑌})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{(𝐺𝑅ℎ)})))
3	2	simpld 494	. . 3 ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑌})) = (𝐽‘{ℎ}))
4		mapdpgem25.i1	. . . . 5 ⊢ (𝜑 → (𝑖 ∈ 𝐹 ∧ ((𝑀‘(𝑁‘{𝑌})) = (𝐽‘{𝑖}) ∧ (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{(𝐺𝑅𝑖)}))))
5	4	simprd 495	. . . 4 ⊢ (𝜑 → ((𝑀‘(𝑁‘{𝑌})) = (𝐽‘{𝑖}) ∧ (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{(𝐺𝑅𝑖)})))
6	5	simpld 494	. . 3 ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑌})) = (𝐽‘{𝑖}))
7	3, 6	eqtr3d 2780	. 2 ⊢ (𝜑 → (𝐽‘{ℎ}) = (𝐽‘{𝑖}))
8	2	simprd 495	. . 3 ⊢ (𝜑 → (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{(𝐺𝑅ℎ)}))
9	5	simprd 495	. . 3 ⊢ (𝜑 → (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{(𝐺𝑅𝑖)}))
10	8, 9	eqtr3d 2780	. 2 ⊢ (𝜑 → (𝐽‘{(𝐺𝑅ℎ)}) = (𝐽‘{(𝐺𝑅𝑖)}))
11	7, 10	jca 511	1 ⊢ (𝜑 → ((𝐽‘{ℎ}) = (𝐽‘{𝑖}) ∧ (𝐽‘{(𝐺𝑅ℎ)}) = (𝐽‘{(𝐺𝑅𝑖)})))

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1539   ∈ wcel 2108   ≠ wne 2942   ∖ cdif 3880  {csn 4558  ‘cfv 6418  (class class class)co 7255  Basecbs 16840  0_gc0g 17067  -_gcsg 18494  LSpanclspn 20148  HLchlt 37291  LHypclh 37925  DVecHcdvh 39019  LCDualclcd 39527  mapdcmpd 39565

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-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-cleq 2730

This theorem is referenced by:  mapdpglem26  39639  mapdpglem27  39640