Metamath Proof Explorer

Theorem mapdh9aOLDN

Description: Lemma for part (9) in Baer p. 48. (Contributed by NM, 14-May-2015) (New usage is discouraged.)

Ref Expression
Hypotheses mapdh8a.h 
|- H = ( LHyp ` K )
mapdh8a.u 
|- U = ( ( DVecH ` K ) ` W )
mapdh8a.v 
|- V = ( Base ` U )
mapdh8a.s 
|- .- = ( -g ` U )
mapdh8a.o 
|- .0. = ( 0g ` U )
mapdh8a.n 
|- N = ( LSpan ` U )
mapdh8a.c 
|- C = ( ( LCDual ` K ) ` W )
mapdh8a.d 
|- D = ( Base ` C )
mapdh8a.r 
|- R = ( -g ` C )
mapdh8a.q 
|- Q = ( 0g ` C )
mapdh8a.j 
|- J = ( LSpan ` C )
mapdh8a.m 
|- M = ( ( mapd ` K ) ` W )
mapdh8a.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 ) } ) ) ) ) )
mapdh8a.k 
|- ( ph -> ( K e. HL /\ W e. H ) )
mapdh8h.f 
|- ( ph -> F e. D )
mapdh8h.mn 
|- ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { F } ) )
mapdh9a.x 
|- ( ph -> X e. ( V \ { .0. } ) )
mapdh9a.t 
|- ( ph -> T e. V )
Assertion mapdh9aOLDN 
|- ( ph -> E! y e. D A. z e. V ( -. z e. ( N ` { X , T } ) -> y = ( I ` <. z , ( I ` <. X , F , z >. ) , T >. ) ) )

Proof

Step Hyp Ref Expression
1 mapdh8a.h 
 |-  H = ( LHyp ` K )
2 mapdh8a.u 
 |-  U = ( ( DVecH ` K ) ` W )
3 mapdh8a.v 
 |-  V = ( Base ` U )
4 mapdh8a.s 
 |-  .- = ( -g ` U )
5 mapdh8a.o 
 |-  .0. = ( 0g ` U )
6 mapdh8a.n 
 |-  N = ( LSpan ` U )
7 mapdh8a.c 
 |-  C = ( ( LCDual ` K ) ` W )
8 mapdh8a.d 
 |-  D = ( Base ` C )
9 mapdh8a.r 
 |-  R = ( -g ` C )
10 mapdh8a.q 
 |-  Q = ( 0g ` C )
11 mapdh8a.j 
 |-  J = ( LSpan ` C )
12 mapdh8a.m 
 |-  M = ( ( mapd ` K ) ` W )
13 mapdh8a.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 mapdh8a.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
15 mapdh8h.f 
 |-  ( ph -> F e. D )
16 mapdh8h.mn 
 |-  ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { F } ) )
17 mapdh9a.x 
 |-  ( ph -> X e. ( V \ { .0. } ) )
18 mapdh9a.t 
 |-  ( ph -> T e. V )
19 14 3ad2ant1 
 |-  ( ( ph /\ ( z e. V /\ w e. V ) /\ ( -. z e. ( N ` { X , T } ) /\ -. w e. ( N ` { X , T } ) ) ) -> ( K e. HL /\ W e. H ) )
20 15 3ad2ant1 
 |-  ( ( ph /\ ( z e. V /\ w e. V ) /\ ( -. z e. ( N ` { X , T } ) /\ -. w e. ( N ` { X , T } ) ) ) -> F e. D )
21 16 3ad2ant1 
 |-  ( ( ph /\ ( z e. V /\ w e. V ) /\ ( -. z e. ( N ` { X , T } ) /\ -. w e. ( N ` { X , T } ) ) ) -> ( M ` ( N ` { X } ) ) = ( J ` { F } ) )
22 17 3ad2ant1 
 |-  ( ( ph /\ ( z e. V /\ w e. V ) /\ ( -. z e. ( N ` { X , T } ) /\ -. w e. ( N ` { X , T } ) ) ) -> X e. ( V \ { .0. } ) )
23 eqid 
 |-  ( LSubSp ` U ) = ( LSubSp ` U )
24 1 2 14 dvhlmod 
 |-  ( ph -> U e. LMod )
25 24 3ad2ant1 
 |-  ( ( ph /\ ( z e. V /\ w e. V ) /\ ( -. z e. ( N ` { X , T } ) /\ -. w e. ( N ` { X , T } ) ) ) -> U e. LMod )
26 17 eldifad 
 |-  ( ph -> X e. V )
27 3 23 6 24 26 18 lspprcl 
 |-  ( ph -> ( N ` { X , T } ) e. ( LSubSp ` U ) )
28 27 3ad2ant1 
 |-  ( ( ph /\ ( z e. V /\ w e. V ) /\ ( -. z e. ( N ` { X , T } ) /\ -. w e. ( N ` { X , T } ) ) ) -> ( N ` { X , T } ) e. ( LSubSp ` U ) )
29 simp2l 
 |-  ( ( ph /\ ( z e. V /\ w e. V ) /\ ( -. z e. ( N ` { X , T } ) /\ -. w e. ( N ` { X , T } ) ) ) -> z e. V )
30 simp3l 
 |-  ( ( ph /\ ( z e. V /\ w e. V ) /\ ( -. z e. ( N ` { X , T } ) /\ -. w e. ( N ` { X , T } ) ) ) -> -. z e. ( N ` { X , T } ) )
31 5 23 25 28 29 30 lssneln0 
 |-  ( ( ph /\ ( z e. V /\ w e. V ) /\ ( -. z e. ( N ` { X , T } ) /\ -. w e. ( N ` { X , T } ) ) ) -> z e. ( V \ { .0. } ) )
32 simp2r 
 |-  ( ( ph /\ ( z e. V /\ w e. V ) /\ ( -. z e. ( N ` { X , T } ) /\ -. w e. ( N ` { X , T } ) ) ) -> w e. V )
33 simp3r 
 |-  ( ( ph /\ ( z e. V /\ w e. V ) /\ ( -. z e. ( N ` { X , T } ) /\ -. w e. ( N ` { X , T } ) ) ) -> -. w e. ( N ` { X , T } ) )
34 5 23 25 28 32 33 lssneln0 
 |-  ( ( ph /\ ( z e. V /\ w e. V ) /\ ( -. z e. ( N ` { X , T } ) /\ -. w e. ( N ` { X , T } ) ) ) -> w e. ( V \ { .0. } ) )
35 1 2 14 dvhlvec 
 |-  ( ph -> U e. LVec )
36 35 3ad2ant1 
 |-  ( ( ph /\ ( z e. V /\ w e. V ) /\ ( -. z e. ( N ` { X , T } ) /\ -. w e. ( N ` { X , T } ) ) ) -> U e. LVec )
37 26 3ad2ant1 
 |-  ( ( ph /\ ( z e. V /\ w e. V ) /\ ( -. z e. ( N ` { X , T } ) /\ -. w e. ( N ` { X , T } ) ) ) -> X e. V )
38 18 3ad2ant1 
 |-  ( ( ph /\ ( z e. V /\ w e. V ) /\ ( -. z e. ( N ` { X , T } ) /\ -. w e. ( N ` { X , T } ) ) ) -> T e. V )
39 3 6 36 29 37 38 30 lspindpi 
 |-  ( ( ph /\ ( z e. V /\ w e. V ) /\ ( -. z e. ( N ` { X , T } ) /\ -. w e. ( N ` { X , T } ) ) ) -> ( ( N ` { z } ) =/= ( N ` { X } ) /\ ( N ` { z } ) =/= ( N ` { T } ) ) )
40 39 simpld 
 |-  ( ( ph /\ ( z e. V /\ w e. V ) /\ ( -. z e. ( N ` { X , T } ) /\ -. w e. ( N ` { X , T } ) ) ) -> ( N ` { z } ) =/= ( N ` { X } ) )
41 40 necomd 
 |-  ( ( ph /\ ( z e. V /\ w e. V ) /\ ( -. z e. ( N ` { X , T } ) /\ -. w e. ( N ` { X , T } ) ) ) -> ( N ` { X } ) =/= ( N ` { z } ) )
42 3 6 36 32 37 38 33 lspindpi 
 |-  ( ( ph /\ ( z e. V /\ w e. V ) /\ ( -. z e. ( N ` { X , T } ) /\ -. w e. ( N ` { X , T } ) ) ) -> ( ( N ` { w } ) =/= ( N ` { X } ) /\ ( N ` { w } ) =/= ( N ` { T } ) ) )
43 42 simpld 
 |-  ( ( ph /\ ( z e. V /\ w e. V ) /\ ( -. z e. ( N ` { X , T } ) /\ -. w e. ( N ` { X , T } ) ) ) -> ( N ` { w } ) =/= ( N ` { X } ) )
44 43 necomd 
 |-  ( ( ph /\ ( z e. V /\ w e. V ) /\ ( -. z e. ( N ` { X , T } ) /\ -. w e. ( N ` { X , T } ) ) ) -> ( N ` { X } ) =/= ( N ` { w } ) )
45 39 simprd 
 |-  ( ( ph /\ ( z e. V /\ w e. V ) /\ ( -. z e. ( N ` { X , T } ) /\ -. w e. ( N ` { X , T } ) ) ) -> ( N ` { z } ) =/= ( N ` { T } ) )
46 42 simprd 
 |-  ( ( ph /\ ( z e. V /\ w e. V ) /\ ( -. z e. ( N ` { X , T } ) /\ -. w e. ( N ` { X , T } ) ) ) -> ( N ` { w } ) =/= ( N ` { T } ) )
47 1 2 3 4 5 6 7 8 9 10 11 12 13 19 20 21 22 31 34 41 44 45 46 38 mapdh8 
 |-  ( ( ph /\ ( z e. V /\ w e. V ) /\ ( -. z e. ( N ` { X , T } ) /\ -. w e. ( N ` { X , T } ) ) ) -> ( I ` <. z , ( I ` <. X , F , z >. ) , T >. ) = ( I ` <. w , ( I ` <. X , F , w >. ) , T >. ) )
48 47 3exp 
 |-  ( ph -> ( ( z e. V /\ w e. V ) -> ( ( -. z e. ( N ` { X , T } ) /\ -. w e. ( N ` { X , T } ) ) -> ( I ` <. z , ( I ` <. X , F , z >. ) , T >. ) = ( I ` <. w , ( I ` <. X , F , w >. ) , T >. ) ) ) )
49 48 ralrimivv 
 |-  ( ph -> A. z e. V A. w e. V ( ( -. z e. ( N ` { X , T } ) /\ -. w e. ( N ` { X , T } ) ) -> ( I ` <. z , ( I ` <. X , F , z >. ) , T >. ) = ( I ` <. w , ( I ` <. X , F , w >. ) , T >. ) ) )
50 1 2 3 6 14 26 18 dvh3dim 
 |-  ( ph -> E. z e. V -. z e. ( N ` { X , T } ) )
51 14 ad2antrr 
 |-  ( ( ( ph /\ z e. V ) /\ -. z e. ( N ` { X , T } ) ) -> ( K e. HL /\ W e. H ) )
52 15 ad2antrr 
 |-  ( ( ( ph /\ z e. V ) /\ -. z e. ( N ` { X , T } ) ) -> F e. D )
53 16 ad2antrr 
 |-  ( ( ( ph /\ z e. V ) /\ -. z e. ( N ` { X , T } ) ) -> ( M ` ( N ` { X } ) ) = ( J ` { F } ) )
54 17 ad2antrr 
 |-  ( ( ( ph /\ z e. V ) /\ -. z e. ( N ` { X , T } ) ) -> X e. ( V \ { .0. } ) )
55 simplr 
 |-  ( ( ( ph /\ z e. V ) /\ -. z e. ( N ` { X , T } ) ) -> z e. V )
56 35 ad2antrr 
 |-  ( ( ( ph /\ z e. V ) /\ -. z e. ( N ` { X , T } ) ) -> U e. LVec )
57 26 ad2antrr 
 |-  ( ( ( ph /\ z e. V ) /\ -. z e. ( N ` { X , T } ) ) -> X e. V )
58 18 ad2antrr 
 |-  ( ( ( ph /\ z e. V ) /\ -. z e. ( N ` { X , T } ) ) -> T e. V )
59 simpr 
 |-  ( ( ( ph /\ z e. V ) /\ -. z e. ( N ` { X , T } ) ) -> -. z e. ( N ` { X , T } ) )
60 3 6 56 55 57 58 59 lspindpi 
 |-  ( ( ( ph /\ z e. V ) /\ -. z e. ( N ` { X , T } ) ) -> ( ( N ` { z } ) =/= ( N ` { X } ) /\ ( N ` { z } ) =/= ( N ` { T } ) ) )
61 60 simpld 
 |-  ( ( ( ph /\ z e. V ) /\ -. z e. ( N ` { X , T } ) ) -> ( N ` { z } ) =/= ( N ` { X } ) )
62 61 necomd 
 |-  ( ( ( ph /\ z e. V ) /\ -. z e. ( N ` { X , T } ) ) -> ( N ` { X } ) =/= ( N ` { z } ) )
63 10 13 1 12 2 3 4 5 6 7 8 9 11 51 52 53 54 55 62 mapdhcl 
 |-  ( ( ( ph /\ z e. V ) /\ -. z e. ( N ` { X , T } ) ) -> ( I ` <. X , F , z >. ) e. D )
64 eqidd 
 |-  ( ( ( ph /\ z e. V ) /\ -. z e. ( N ` { X , T } ) ) -> ( I ` <. X , F , z >. ) = ( I ` <. X , F , z >. ) )
65 24 ad2antrr 
 |-  ( ( ( ph /\ z e. V ) /\ -. z e. ( N ` { X , T } ) ) -> U e. LMod )
66 27 ad2antrr 
 |-  ( ( ( ph /\ z e. V ) /\ -. z e. ( N ` { X , T } ) ) -> ( N ` { X , T } ) e. ( LSubSp ` U ) )
67 5 23 65 66 55 59 lssneln0 
 |-  ( ( ( ph /\ z e. V ) /\ -. z e. ( N ` { X , T } ) ) -> z e. ( V \ { .0. } ) )
68 10 13 1 12 2 3 4 5 6 7 8 9 11 51 52 53 54 67 63 62 mapdheq 
 |-  ( ( ( ph /\ z e. V ) /\ -. z e. ( N ` { X , T } ) ) -> ( ( I ` <. X , F , z >. ) = ( I ` <. X , F , z >. ) <-> ( ( M ` ( N ` { z } ) ) = ( J ` { ( I ` <. X , F , z >. ) } ) /\ ( M ` ( N ` { ( X .- z ) } ) ) = ( J ` { ( F R ( I ` <. X , F , z >. ) ) } ) ) ) )
69 64 68 mpbid 
 |-  ( ( ( ph /\ z e. V ) /\ -. z e. ( N ` { X , T } ) ) -> ( ( M ` ( N ` { z } ) ) = ( J ` { ( I ` <. X , F , z >. ) } ) /\ ( M ` ( N ` { ( X .- z ) } ) ) = ( J ` { ( F R ( I ` <. X , F , z >. ) ) } ) ) )
70 69 simpld 
 |-  ( ( ( ph /\ z e. V ) /\ -. z e. ( N ` { X , T } ) ) -> ( M ` ( N ` { z } ) ) = ( J ` { ( I ` <. X , F , z >. ) } ) )
71 60 simprd 
 |-  ( ( ( ph /\ z e. V ) /\ -. z e. ( N ` { X , T } ) ) -> ( N ` { z } ) =/= ( N ` { T } ) )
72 10 13 1 12 2 3 4 5 6 7 8 9 11 51 63 70 67 58 71 mapdhcl 
 |-  ( ( ( ph /\ z e. V ) /\ -. z e. ( N ` { X , T } ) ) -> ( I ` <. z , ( I ` <. X , F , z >. ) , T >. ) e. D )
73 72 ex 
 |-  ( ( ph /\ z e. V ) -> ( -. z e. ( N ` { X , T } ) -> ( I ` <. z , ( I ` <. X , F , z >. ) , T >. ) e. D ) )
74 73 ancld 
 |-  ( ( ph /\ z e. V ) -> ( -. z e. ( N ` { X , T } ) -> ( -. z e. ( N ` { X , T } ) /\ ( I ` <. z , ( I ` <. X , F , z >. ) , T >. ) e. D ) ) )
75 74 reximdva 
 |-  ( ph -> ( E. z e. V -. z e. ( N ` { X , T } ) -> E. z e. V ( -. z e. ( N ` { X , T } ) /\ ( I ` <. z , ( I ` <. X , F , z >. ) , T >. ) e. D ) ) )
76 50 75 mpd 
 |-  ( ph -> E. z e. V ( -. z e. ( N ` { X , T } ) /\ ( I ` <. z , ( I ` <. X , F , z >. ) , T >. ) e. D ) )
77 eleq1w 
 |-  ( z = w -> ( z e. ( N ` { X , T } ) <-> w e. ( N ` { X , T } ) ) )
78 77 notbid 
 |-  ( z = w -> ( -. z e. ( N ` { X , T } ) <-> -. w e. ( N ` { X , T } ) ) )
79 oteq1 
 |-  ( z = w -> <. z , ( I ` <. X , F , z >. ) , T >. = <. w , ( I ` <. X , F , z >. ) , T >. )
80 oteq3 
 |-  ( z = w -> <. X , F , z >. = <. X , F , w >. )
81 80 fveq2d 
 |-  ( z = w -> ( I ` <. X , F , z >. ) = ( I ` <. X , F , w >. ) )
82 81 oteq2d 
 |-  ( z = w -> <. w , ( I ` <. X , F , z >. ) , T >. = <. w , ( I ` <. X , F , w >. ) , T >. )
83 79 82 eqtrd 
 |-  ( z = w -> <. z , ( I ` <. X , F , z >. ) , T >. = <. w , ( I ` <. X , F , w >. ) , T >. )
84 83 fveq2d 
 |-  ( z = w -> ( I ` <. z , ( I ` <. X , F , z >. ) , T >. ) = ( I ` <. w , ( I ` <. X , F , w >. ) , T >. ) )
85 78 84 reusv3 
 |-  ( E. z e. V ( -. z e. ( N ` { X , T } ) /\ ( I ` <. z , ( I ` <. X , F , z >. ) , T >. ) e. D ) -> ( A. z e. V A. w e. V ( ( -. z e. ( N ` { X , T } ) /\ -. w e. ( N ` { X , T } ) ) -> ( I ` <. z , ( I ` <. X , F , z >. ) , T >. ) = ( I ` <. w , ( I ` <. X , F , w >. ) , T >. ) ) <-> E. y e. D A. z e. V ( -. z e. ( N ` { X , T } ) -> y = ( I ` <. z , ( I ` <. X , F , z >. ) , T >. ) ) ) )
86 76 85 syl 
 |-  ( ph -> ( A. z e. V A. w e. V ( ( -. z e. ( N ` { X , T } ) /\ -. w e. ( N ` { X , T } ) ) -> ( I ` <. z , ( I ` <. X , F , z >. ) , T >. ) = ( I ` <. w , ( I ` <. X , F , w >. ) , T >. ) ) <-> E. y e. D A. z e. V ( -. z e. ( N ` { X , T } ) -> y = ( I ` <. z , ( I ` <. X , F , z >. ) , T >. ) ) ) )
87 49 86 mpbid 
 |-  ( ph -> E. y e. D A. z e. V ( -. z e. ( N ` { X , T } ) -> y = ( I ` <. z , ( I ` <. X , F , z >. ) , T >. ) ) )
88 reusv1 
 |-  ( E. z e. V -. z e. ( N ` { X , T } ) -> ( E! y e. D A. z e. V ( -. z e. ( N ` { X , T } ) -> y = ( I ` <. z , ( I ` <. X , F , z >. ) , T >. ) ) <-> E. y e. D A. z e. V ( -. z e. ( N ` { X , T } ) -> y = ( I ` <. z , ( I ` <. X , F , z >. ) , T >. ) ) ) )
89 50 88 syl 
 |-  ( ph -> ( E! y e. D A. z e. V ( -. z e. ( N ` { X , T } ) -> y = ( I ` <. z , ( I ` <. X , F , z >. ) , T >. ) ) <-> E. y e. D A. z e. V ( -. z e. ( N ` { X , T } ) -> y = ( I ` <. z , ( I ` <. X , F , z >. ) , T >. ) ) ) )
90 87 89 mpbird 
 |-  ( ph -> E! y e. D A. z e. V ( -. z e. ( N ` { X , T } ) -> y = ( I ` <. z , ( I ` <. X , F , z >. ) , T >. ) ) )