# Metamath Proof Explorer

## Theorem mapdh8aa

Description: Part of Part (8) in Baer p. 48. (Contributed by NM, 12-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 ) )`
mapdh8aa.f
`|- ( ph -> F e. D )`
mapdh8aa.mn
`|- ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { F } ) )`
mapdh8aa.eg
`|- ( ph -> ( I ` <. X , F , Y >. ) = G )`
mapdh8aa.ee
`|- ( ph -> ( I ` <. X , F , Z >. ) = E )`
mapdh8aa.x
`|- ( ph -> X e. ( V \ { .0. } ) )`
mapdh8aa.y
`|- ( ph -> Y e. ( V \ { .0. } ) )`
mapdh8aa.z
`|- ( ph -> Z e. ( V \ { .0. } ) )`
mapdh8aa.zt
`|- ( ph -> ( N ` { Z } ) =/= ( N ` { T } ) )`
mapdh8aa.t
`|- ( ph -> T e. ( V \ { .0. } ) )`
mapdh8aa.yn
`|- ( ph -> -. Y e. ( N ` { Z , T } ) )`
mapdh8aa.xn
`|- ( ph -> -. X e. ( N ` { Y , Z } ) )`
Assertion mapdh8aa
`|- ( 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 mapdh8aa.f
` |-  ( ph -> F e. D )`
16 mapdh8aa.mn
` |-  ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { F } ) )`
17 mapdh8aa.eg
` |-  ( ph -> ( I ` <. X , F , Y >. ) = G )`
18 mapdh8aa.ee
` |-  ( ph -> ( I ` <. X , F , Z >. ) = E )`
19 mapdh8aa.x
` |-  ( ph -> X e. ( V \ { .0. } ) )`
20 mapdh8aa.y
` |-  ( ph -> Y e. ( V \ { .0. } ) )`
21 mapdh8aa.z
` |-  ( ph -> Z e. ( V \ { .0. } ) )`
22 mapdh8aa.zt
` |-  ( ph -> ( N ` { Z } ) =/= ( N ` { T } ) )`
23 mapdh8aa.t
` |-  ( ph -> T e. ( V \ { .0. } ) )`
24 mapdh8aa.yn
` |-  ( ph -> -. Y e. ( N ` { Z , T } ) )`
25 mapdh8aa.xn
` |-  ( ph -> -. X e. ( N ` { Y , Z } ) )`
` |-  ( ph -> Y e. V )`
27 1 2 14 dvhlvec
` |-  ( ph -> U e. LVec )`
` |-  ( ph -> X e. V )`
` |-  ( ph -> Z e. V )`
30 3 6 27 28 26 29 25 lspindpi
` |-  ( ph -> ( ( N ` { X } ) =/= ( N ` { Y } ) /\ ( N ` { X } ) =/= ( N ` { Z } ) ) )`
31 30 simpld
` |-  ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )`
32 10 13 1 12 2 3 4 5 6 7 8 9 11 14 15 16 19 26 31 mapdhcl
` |-  ( ph -> ( I ` <. X , F , Y >. ) e. D )`
33 17 32 eqeltrrd
` |-  ( ph -> G e. D )`
34 10 13 1 12 2 3 4 5 6 7 8 9 11 14 15 16 19 20 33 31 mapdheq
` |-  ( ph -> ( ( I ` <. X , F , Y >. ) = G <-> ( ( M ` ( N ` { Y } ) ) = ( J ` { G } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( F R G ) } ) ) ) )`
35 17 34 mpbid
` |-  ( ph -> ( ( M ` ( N ` { Y } ) ) = ( J ` { G } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( F R G ) } ) ) )`
36 35 simpld
` |-  ( ph -> ( M ` ( N ` { Y } ) ) = ( J ` { G } ) )`
` |-  ( ph -> T e. V )`
` |-  ( ph -> ( ( N ` { Y } ) =/= ( N ` { Z } ) /\ ( N ` { Y } ) =/= ( N ` { T } ) ) )`
` |-  ( ph -> ( N ` { Y } ) =/= ( N ` { Z } ) )`
` |-  ( ph -> ( I ` <. Y , G , Z >. ) = E )`
` |-  ( ph -> ( I ` <. Z , E , T >. ) = ( I ` <. Y , G , T >. ) )`
` |-  ( ph -> ( I ` <. Y , G , T >. ) = ( I ` <. Z , E , T >. ) )`