Theorem hdmap1eq

Description: The defining equation for h(x,x',y)=y' in part (2) in Baer p. 45 line 24. (Contributed by NM, 16-May-2015)

	Ref	Expression
Hypotheses	hdmap1val2.h	|- H = ( LHyp ` K )
	hdmap1val2.u	|- U = ( ( DVecH ` K ) ` W )
	hdmap1val2.v	|- V = ( Base ` U )
	hdmap1val2.s	|- .- = ( -g ` U )
	hdmap1val2.o	|- .0. = ( 0g ` U )
	hdmap1val2.n	|- N = ( LSpan ` U )
	hdmap1val2.c	|- C = ( ( LCDual ` K ) ` W )
	hdmap1val2.d	|- D = ( Base ` C )
	hdmap1val2.r	|- R = ( -g ` C )
	hdmap1val2.l	|- L = ( LSpan ` C )
	hdmap1val2.m	|- M = ( ( mapd ` K ) ` W )
	hdmap1val2.i	|- I = ( ( HDMap1 ` K ) ` W )
	hdmap1val2.k	|- ( ph -> ( K e. HL /\ W e. H ) )
	hdmap1eq.x	|- ( ph -> X e. ( V \ { .0. } ) )
	hdmap1eq.f	|- ( ph -> F e. D )
	hdmap1eq.y	|- ( ph -> Y e. ( V \ { .0. } ) )
	hdmap1eq.g	|- ( ph -> G e. D )
	hdmap1eq.e	|- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )
	hdmap1eq.mn	|- ( ph -> ( M ` ( N ` { X } ) ) = ( L ` { F } ) )
Assertion	hdmap1eq	|- ( ph -> ( ( I ` <. X , F , Y >. ) = G <-> ( ( M ` ( N ` { Y } ) ) = ( L ` { G } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( L ` { ( F R G ) } ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		hdmap1val2.h	|- H = ( LHyp ` K )
2		hdmap1val2.u	|- U = ( ( DVecH ` K ) ` W )
3		hdmap1val2.v	|- V = ( Base ` U )
4		hdmap1val2.s	|- .- = ( -g ` U )
5		hdmap1val2.o	|- .0. = ( 0g ` U )
6		hdmap1val2.n	|- N = ( LSpan ` U )
7		hdmap1val2.c	|- C = ( ( LCDual ` K ) ` W )
8		hdmap1val2.d	|- D = ( Base ` C )
9		hdmap1val2.r	|- R = ( -g ` C )
10		hdmap1val2.l	|- L = ( LSpan ` C )
11		hdmap1val2.m	|- M = ( ( mapd ` K ) ` W )
12		hdmap1val2.i	|- I = ( ( HDMap1 ` K ) ` W )
13		hdmap1val2.k	|- ( ph -> ( K e. HL /\ W e. H ) )
14		hdmap1eq.x	|- ( ph -> X e. ( V \ { .0. } ) )
15		hdmap1eq.f	|- ( ph -> F e. D )
16		hdmap1eq.y	|- ( ph -> Y e. ( V \ { .0. } ) )
17		hdmap1eq.g	|- ( ph -> G e. D )
18		hdmap1eq.e	|- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )
19		hdmap1eq.mn	|- ( ph -> ( M ` ( N ` { X } ) ) = ( L ` { F } ) )
20	14	eldifad	|- ( ph -> X e. V )
21	1 2 3 4 5 6 7 8 9 10 11 12 13 20 15 16	hdmap1val2	|- ( ph -> ( I ` <. X , F , Y >. ) = ( iota_ h e. D ( ( M ` ( N ` { Y } ) ) = ( L ` { h } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( L ` { ( F R h ) } ) ) ) )
22	21	eqeq1d	|- ( ph -> ( ( I ` <. X , F , Y >. ) = G <-> ( iota_ h e. D ( ( M ` ( N ` { Y } ) ) = ( L ` { h } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( L ` { ( F R h ) } ) ) ) = G ) )
23	1 11 2 3 4 5 6 7 8 9 10 13 14 16 15 18 19	mapdpg	|- ( ph -> E! h e. D ( ( M ` ( N ` { Y } ) ) = ( L ` { h } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( L ` { ( F R h ) } ) ) )
24		nfv	|- F/ h ph
25		nfcvd	|- ( ph -> F/_ h G )
26		nfvd	|- ( ph -> F/ h ( ( M ` ( N ` { Y } ) ) = ( L ` { G } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( L ` { ( F R G ) } ) ) )
27		sneq	|- ( h = G -> { h } = { G } )
28	27	fveq2d	|- ( h = G -> ( L ` { h } ) = ( L ` { G } ) )
29	28	eqeq2d	|- ( h = G -> ( ( M ` ( N ` { Y } ) ) = ( L ` { h } ) <-> ( M ` ( N ` { Y } ) ) = ( L ` { G } ) ) )
30		oveq2	|- ( h = G -> ( F R h ) = ( F R G ) )
31	30	sneqd	|- ( h = G -> { ( F R h ) } = { ( F R G ) } )
32	31	fveq2d	|- ( h = G -> ( L ` { ( F R h ) } ) = ( L ` { ( F R G ) } ) )
33	32	eqeq2d	|- ( h = G -> ( ( M ` ( N ` { ( X .- Y ) } ) ) = ( L ` { ( F R h ) } ) <-> ( M ` ( N ` { ( X .- Y ) } ) ) = ( L ` { ( F R G ) } ) ) )
34	29 33	anbi12d	|- ( h = G -> ( ( ( M ` ( N ` { Y } ) ) = ( L ` { h } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( L ` { ( F R h ) } ) ) <-> ( ( M ` ( N ` { Y } ) ) = ( L ` { G } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( L ` { ( F R G ) } ) ) ) )
35	34	adantl	|- ( ( ph /\ h = G ) -> ( ( ( M ` ( N ` { Y } ) ) = ( L ` { h } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( L ` { ( F R h ) } ) ) <-> ( ( M ` ( N ` { Y } ) ) = ( L ` { G } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( L ` { ( F R G ) } ) ) ) )
36	24 25 26 17 35	riota2df	|- ( ( ph /\ E! h e. D ( ( M ` ( N ` { Y } ) ) = ( L ` { h } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( L ` { ( F R h ) } ) ) ) -> ( ( ( M ` ( N ` { Y } ) ) = ( L ` { G } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( L ` { ( F R G ) } ) ) <-> ( iota_ h e. D ( ( M ` ( N ` { Y } ) ) = ( L ` { h } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( L ` { ( F R h ) } ) ) ) = G ) )
37	23 36	mpdan	|- ( ph -> ( ( ( M ` ( N ` { Y } ) ) = ( L ` { G } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( L ` { ( F R G ) } ) ) <-> ( iota_ h e. D ( ( M ` ( N ` { Y } ) ) = ( L ` { h } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( L ` { ( F R h ) } ) ) ) = G ) )
38	22 37	bitr4d	|- ( ph -> ( ( I ` <. X , F , Y >. ) = G <-> ( ( M ` ( N ` { Y } ) ) = ( L ` { G } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( L ` { ( F R G ) } ) ) ) )