Theorem mapdh7fN

Description: Part (7) of Baer p. 48 line 10 (6 of 6 cases). (Contributed by NM, 2-May-2015) (New usage is discouraged.)

	Ref	Expression
Hypotheses	mapdh7.h	|- H = ( LHyp ` K )
	mapdh7.u	|- U = ( ( DVecH ` K ) ` W )
	mapdh7.v	|- V = ( Base ` U )
	mapdh7.s	|- .- = ( -g ` U )
	mapdh7.o	|- .0. = ( 0g ` U )
	mapdh7.n	|- N = ( LSpan ` U )
	mapdh7.c	|- C = ( ( LCDual ` K ) ` W )
	mapdh7.d	|- D = ( Base ` C )
	mapdh7.r	|- R = ( -g ` C )
	mapdh7.q	|- Q = ( 0g ` C )
	mapdh7.j	|- J = ( LSpan ` C )
	mapdh7.m	|- M = ( ( mapd ` K ) ` W )
	mapdh7.i	|- I = ( x e. _V |-> if ( ( 2nd ` x ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) ) ) )
	mapdh7.k	|- ( ph -> ( K e. HL /\ W e. H ) )
	mapdh7.f	|- ( ph -> F e. D )
	mapdh7.mn	|- ( ph -> ( M ` ( N ` { u } ) ) = ( J ` { F } ) )
	mapdh7.x	|- ( ph -> u e. ( V \ { .0. } ) )
	mapdh7.y	|- ( ph -> v e. ( V \ { .0. } ) )
	mapdh7.z	|- ( ph -> w e. ( V \ { .0. } ) )
	mapdh7.ne	|- ( ph -> ( N ` { u } ) =/= ( N ` { v } ) )
	mapdh7.wn	|- ( ph -> -. w e. ( N ` { u , v } ) )
	mapdh7a	|- ( ph -> ( I ` <. u , F , v >. ) = G )
	mapdh7.b	|- ( ph -> ( I ` <. u , F , w >. ) = E )
Assertion	mapdh7fN	|- ( ph -> ( I ` <. w , E , v >. ) = G )

Proof

Step	Hyp	Ref	Expression
1		mapdh7.h	|- H = ( LHyp ` K )
2		mapdh7.u	|- U = ( ( DVecH ` K ) ` W )
3		mapdh7.v	|- V = ( Base ` U )
4		mapdh7.s	|- .- = ( -g ` U )
5		mapdh7.o	|- .0. = ( 0g ` U )
6		mapdh7.n	|- N = ( LSpan ` U )
7		mapdh7.c	|- C = ( ( LCDual ` K ) ` W )
8		mapdh7.d	|- D = ( Base ` C )
9		mapdh7.r	|- R = ( -g ` C )
10		mapdh7.q	|- Q = ( 0g ` C )
11		mapdh7.j	|- J = ( LSpan ` C )
12		mapdh7.m	|- M = ( ( mapd ` K ) ` W )
13		mapdh7.i	|- I = ( x e. _V |-> if ( ( 2nd ` x ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) ) ) )
14		mapdh7.k	|- ( ph -> ( K e. HL /\ W e. H ) )
15		mapdh7.f	|- ( ph -> F e. D )
16		mapdh7.mn	|- ( ph -> ( M ` ( N ` { u } ) ) = ( J ` { F } ) )
17		mapdh7.x	|- ( ph -> u e. ( V \ { .0. } ) )
18		mapdh7.y	|- ( ph -> v e. ( V \ { .0. } ) )
19		mapdh7.z	|- ( ph -> w e. ( V \ { .0. } ) )
20		mapdh7.ne	|- ( ph -> ( N ` { u } ) =/= ( N ` { v } ) )
21		mapdh7.wn	|- ( ph -> -. w e. ( N ` { u , v } ) )
22		mapdh7a	|- ( ph -> ( I ` <. u , F , v >. ) = G )
23		mapdh7.b	|- ( ph -> ( I ` <. u , F , w >. ) = E )
24	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23	mapdh7dN	|- ( ph -> ( I ` <. v , G , w >. ) = E )
25	18	eldifad	|- ( ph -> v e. V )
26	10 13 1 12 2 3 4 5 6 7 8 9 11 14 15 16 17 25 20	mapdhcl	|- ( ph -> ( I ` <. u , F , v >. ) e. D )
27	22 26	eqeltrrd	|- ( ph -> G e. D )
28	10 13 1 12 2 3 4 5 6 7 8 9 11 14 15 16 17 18 27 20	mapdheq	|- ( ph -> ( ( I ` <. u , F , v >. ) = G <-> ( ( M ` ( N ` { v } ) ) = ( J ` { G } ) /\ ( M ` ( N ` { ( u .- v ) } ) ) = ( J ` { ( F R G ) } ) ) ) )
29	22 28	mpbid	|- ( ph -> ( ( M ` ( N ` { v } ) ) = ( J ` { G } ) /\ ( M ` ( N ` { ( u .- v ) } ) ) = ( J ` { ( F R G ) } ) ) )
30	29	simpld	|- ( ph -> ( M ` ( N ` { v } ) ) = ( J ` { G } ) )
31	19	eldifad	|- ( ph -> w e. V )
32	1 2 14	dvhlvec	|- ( ph -> U e. LVec )
33	17	eldifad	|- ( ph -> u e. V )
34	3 6 32 31 33 25 21	lspindpi	|- ( ph -> ( ( N ` { w } ) =/= ( N ` { u } ) /\ ( N ` { w } ) =/= ( N ` { v } ) ) )
35	34	simpld	|- ( ph -> ( N ` { w } ) =/= ( N ` { u } ) )
36	35	necomd	|- ( ph -> ( N ` { u } ) =/= ( N ` { w } ) )
37	10 13 1 12 2 3 4 5 6 7 8 9 11 14 15 16 17 31 36	mapdhcl	|- ( ph -> ( I ` <. u , F , w >. ) e. D )
38	23 37	eqeltrrd	|- ( ph -> E e. D )
39	34	simprd	|- ( ph -> ( N ` { w } ) =/= ( N ` { v } ) )
40	39	necomd	|- ( ph -> ( N ` { v } ) =/= ( N ` { w } ) )
41	10 13 1 12 2 3 4 5 6 7 8 9 11 14 27 30 18 19 38 40	mapdheq2	|- ( ph -> ( ( I ` <. v , G , w >. ) = E -> ( I ` <. w , E , v >. ) = G ) )
42	24 41	mpd	|- ( ph -> ( I ` <. w , E , v >. ) = G )