# Metamath Proof Explorer

## Theorem mapdh8ab

Description: Part of Part (8) in Baer p. 48. (Contributed by NM, 13-May-2015)

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 ) )`
mapdh8ab.f
`|- ( ph -> F e. D )`
mapdh8ab.mn
`|- ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { F } ) )`
mapdh8ab.eg
`|- ( ph -> ( I ` <. X , F , Y >. ) = G )`
mapdh8ab.ee
`|- ( ph -> ( I ` <. X , F , Z >. ) = E )`
mapdh8ab.x
`|- ( ph -> X e. ( V \ { .0. } ) )`
mapdh8ab.y
`|- ( ph -> Y e. ( V \ { .0. } ) )`
mapdh8ab.z
`|- ( ph -> Z e. ( V \ { .0. } ) )`
mapdh8ab.t
`|- ( ph -> T e. ( V \ { .0. } ) )`
mapdh8ab.yz
`|- ( ph -> ( N ` { Y } ) =/= ( N ` { Z } ) )`
mapdh8ab.xn
`|- ( ph -> -. X e. ( N ` { Y , Z } ) )`
mapdh8ab.yn
`|- ( ph -> ( N ` { X } ) = ( N ` { T } ) )`
Assertion mapdh8ab
`|- ( ph -> ( I ` <. Y , G , T >. ) = ( I ` <. Z , E , 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 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 )`
` |-  ( ph -> X e. V )`
` |-  ( ph -> Y e. V )`
` |-  ( 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 } ) ) )`
` |-  ( 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 } ) )`
` |-  ( ( ph /\ Y e. ( N ` { Z , T } ) ) -> U e. LVec )`
` |-  ( ( ph /\ Y e. ( N ` { Z , T } ) ) -> Y e. ( V \ { .0. } ) )`
` |-  ( ( ph /\ Y e. ( N ` { Z , T } ) ) -> T e. V )`
` |-  ( ( ph /\ Y e. ( N ` { Z , T } ) ) -> Z e. V )`
` |-  ( ( 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 >. ) )`