Theorem mapdpglem25 36986

Description: Lemma for mapdpg 36995. 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	|- H = ( LHyp ` K )
mapdpg.m	|- M = ( (mapd ` K ) ` W )
mapdpg.u	|- U = ( ( DVecH ` K ) ` W )
mapdpg.v	|- V = ( Base ` U )
mapdpg.s	|- .- = ( -g ` U )
mapdpg.z	|- .0. = ( 0g ` U )
mapdpg.n	|- N = ( LSpan ` U )
mapdpg.c	|- C = ( (LCDual ` K ) ` W )
mapdpg.f	|- F = ( Base ` C )
mapdpg.r	|- R = ( -g ` C )
mapdpg.j	|- J = ( LSpan ` C )
mapdpg.k	|- ( ph -> ( K e. HL /\ W e. H ) )
mapdpg.x	|- ( ph -> X e. ( V \ { .0. } ) )
mapdpg.y	|- ( ph -> Y e. ( V \ { .0. } ) )
mapdpg.g	|- ( ph -> G e. F )
mapdpg.ne	|- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )
mapdpg.e	|- ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { G } ) )
mapdpgem25.h1	|- ( ph -> ( h e. F /\ ( ( M ` ( N ` { Y } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R h ) } ) ) ) )
mapdpgem25.i1	|- ( ph -> ( i e. F /\ ( ( M ` ( N ` { Y } ) ) = ( J ` { i } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R i ) } ) ) ) )

Assertion

Ref	Expression
mapdpglem25	|- ( ph -> ( ( J ` { h } ) = ( J ` { i } ) /\ ( J ` { ( G R h ) } ) = ( J ` { ( G R i ) } ) ) )

Proof of Theorem mapdpglem25

Step	Hyp	Ref	Expression
1		mapdpgem25.h1	. . . . 5 |- ( ph -> ( h e. F /\ ( ( M ` ( N ` { Y } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R h ) } ) ) ) )
2	1	simprd 479	. . . 4 |- ( ph -> ( ( M ` ( N ` { Y } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R h ) } ) ) )
3	2	simpld 475	. . 3 |- ( ph -> ( M ` ( N ` { Y } ) ) = ( J ` { h } ) )
4		mapdpgem25.i1	. . . . 5 |- ( ph -> ( i e. F /\ ( ( M ` ( N ` { Y } ) ) = ( J ` { i } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R i ) } ) ) ) )
5	4	simprd 479	. . . 4 |- ( ph -> ( ( M ` ( N ` { Y } ) ) = ( J ` { i } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R i ) } ) ) )
6	5	simpld 475	. . 3 |- ( ph -> ( M ` ( N ` { Y } ) ) = ( J ` { i } ) )
7	3, 6	eqtr3d 2658	. 2 |- ( ph -> ( J ` { h } ) = ( J ` { i } ) )
8	2	simprd 479	. . 3 |- ( ph -> ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R h ) } ) )
9	5	simprd 479	. . 3 |- ( ph -> ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R i ) } ) )
10	8, 9	eqtr3d 2658	. 2 |- ( ph -> ( J ` { ( G R h ) } ) = ( J ` { ( G R i ) } ) )
11	7, 10	jca 554	1 |- ( ph -> ( ( J ` { h } ) = ( J ` { i } ) /\ ( J ` { ( G R h ) } ) = ( J ` { ( G R i ) } ) ) )

Syntax hints:   -> wi 4   /\ wa 384   = wceq 1483   e. wcel 1990   =/= wne 2794   \ cdif 3571   {csn 4177   ` cfv 5888  (class class class)co 6650   Basecbs 15857   0gc0g 16100   -gcsg 17424   LSpanclspn 18971   HLchlt 34637   LHypclh 35270   DVecHcdvh 36367  LCDualclcd 36875  mapdcmpd 36913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615

This theorem is referenced by:  mapdpglem26  36987  mapdpglem27  36988