| 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 |
|
mapdh8ab.f |
|- ( ph -> F e. D ) |
| 16 |
|
mapdh8ab.mn |
|- ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { F } ) ) |
| 17 |
|
mapdh8ab.eg |
|- ( ph -> ( I ` <. X , F , Y >. ) = G ) |
| 18 |
|
mapdh8ab.ee |
|- ( ph -> ( I ` <. X , F , Z >. ) = E ) |
| 19 |
|
mapdh8ab.x |
|- ( ph -> X e. ( V \ { .0. } ) ) |
| 20 |
|
mapdh8ab.y |
|- ( ph -> Y e. ( V \ { .0. } ) ) |
| 21 |
|
mapdh8ab.z |
|- ( ph -> Z e. ( V \ { .0. } ) ) |
| 22 |
|
mapdh8ab.t |
|- ( ph -> T e. ( V \ { .0. } ) ) |
| 23 |
|
mapdh8ab.yz |
|- ( ph -> ( N ` { Y } ) =/= ( N ` { Z } ) ) |
| 24 |
|
mapdh8ab.xn |
|- ( ph -> -. X e. ( N ` { Y , Z } ) ) |
| 25 |
|
mapdh8ab.yn |
|- ( ph -> ( N ` { X } ) = ( N ` { T } ) ) |
| 26 |
1 2 14
|
dvhlvec |
|- ( ph -> U e. LVec ) |
| 27 |
19
|
eldifad |
|- ( ph -> X e. V ) |
| 28 |
20
|
eldifad |
|- ( ph -> Y e. V ) |
| 29 |
21
|
eldifad |
|- ( ph -> Z e. V ) |
| 30 |
3 6 26 27 28 29 24
|
lspindpi |
|- ( ph -> ( ( N ` { X } ) =/= ( N ` { Y } ) /\ ( N ` { X } ) =/= ( N ` { Z } ) ) ) |
| 31 |
30
|
simprd |
|- ( ph -> ( N ` { X } ) =/= ( N ` { Z } ) ) |
| 32 |
31
|
necomd |
|- ( ph -> ( N ` { Z } ) =/= ( N ` { X } ) ) |
| 33 |
32 25
|
neeqtrd |
|- ( ph -> ( N ` { Z } ) =/= ( N ` { T } ) ) |
| 34 |
25
|
sseq1d |
|- ( ph -> ( ( N ` { X } ) C_ ( N ` { Y , Z } ) <-> ( N ` { T } ) C_ ( N ` { Y , Z } ) ) ) |
| 35 |
|
eqid |
|- ( LSubSp ` U ) = ( LSubSp ` U ) |
| 36 |
1 2 14
|
dvhlmod |
|- ( ph -> U e. LMod ) |
| 37 |
3 35 6 36 28 29
|
lspprcl |
|- ( ph -> ( N ` { Y , Z } ) e. ( LSubSp ` U ) ) |
| 38 |
3 35 6 36 37 27
|
lspsnel5 |
|- ( ph -> ( X e. ( N ` { Y , Z } ) <-> ( N ` { X } ) C_ ( N ` { Y , Z } ) ) ) |
| 39 |
22
|
eldifad |
|- ( ph -> T e. V ) |
| 40 |
3 35 6 36 37 39
|
lspsnel5 |
|- ( ph -> ( T e. ( N ` { Y , Z } ) <-> ( N ` { T } ) C_ ( N ` { Y , Z } ) ) ) |
| 41 |
34 38 40
|
3bitr4d |
|- ( ph -> ( X e. ( N ` { Y , Z } ) <-> T e. ( N ` { Y , Z } ) ) ) |
| 42 |
24 41
|
mtbid |
|- ( ph -> -. T e. ( N ` { Y , Z } ) ) |
| 43 |
26
|
adantr |
|- ( ( ph /\ Y e. ( N ` { Z , T } ) ) -> U e. LVec ) |
| 44 |
20
|
adantr |
|- ( ( ph /\ Y e. ( N ` { Z , T } ) ) -> Y e. ( V \ { .0. } ) ) |
| 45 |
39
|
adantr |
|- ( ( ph /\ Y e. ( N ` { Z , T } ) ) -> T e. V ) |
| 46 |
29
|
adantr |
|- ( ( ph /\ Y e. ( N ` { Z , T } ) ) -> Z e. V ) |
| 47 |
23
|
adantr |
|- ( ( ph /\ Y e. ( N ` { Z , T } ) ) -> ( N ` { Y } ) =/= ( N ` { Z } ) ) |
| 48 |
|
simpr |
|- ( ( ph /\ Y e. ( N ` { Z , T } ) ) -> Y e. ( N ` { Z , T } ) ) |
| 49 |
|
prcom |
|- { Z , T } = { T , Z } |
| 50 |
49
|
fveq2i |
|- ( N ` { Z , T } ) = ( N ` { T , Z } ) |
| 51 |
48 50
|
eleqtrdi |
|- ( ( ph /\ Y e. ( N ` { Z , T } ) ) -> Y e. ( N ` { T , Z } ) ) |
| 52 |
3 5 6 43 44 45 46 47 51
|
lspexch |
|- ( ( ph /\ Y e. ( N ` { Z , T } ) ) -> T e. ( N ` { Y , Z } ) ) |
| 53 |
42 52
|
mtand |
|- ( ph -> -. Y e. ( N ` { Z , T } ) ) |
| 54 |
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 33 22 53 24
|
mapdh8aa |
|- ( ph -> ( I ` <. Y , G , T >. ) = ( I ` <. Z , E , T >. ) ) |