Metamath Proof Explorer

Theorem mapdh8ac

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 ) )`
mapdh8ac.f
`|- ( ph -> F e. D )`
mapdh8ac.mn
`|- ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { F } ) )`
mapdh8ac.eg
`|- ( ph -> ( I ` <. X , F , Y >. ) = G )`
mapdh8ac.ee
`|- ( ph -> ( I ` <. X , F , Z >. ) = E )`
mapdh8ac.x
`|- ( ph -> X e. ( V \ { .0. } ) )`
mapdh8ac.y
`|- ( ph -> Y e. ( V \ { .0. } ) )`
mapdh8ac.z
`|- ( ph -> Z e. ( V \ { .0. } ) )`
mapdh8ac.t
`|- ( ph -> T e. ( V \ { .0. } ) )`
mapdh8ac.yn
`|- ( ph -> ( N ` { X } ) = ( N ` { T } ) )`
mapdh8ac.ew
`|- ( ph -> ( I ` <. X , F , w >. ) = B )`
mapdh8ac.w
`|- ( ph -> w e. ( V \ { .0. } ) )`
mapdh8ac.yw
`|- ( ph -> ( N ` { Y } ) =/= ( N ` { w } ) )`
mapdh8ac.xy
`|- ( ph -> -. X e. ( N ` { Y , w } ) )`
mapdh8ac.wz
`|- ( ph -> ( N ` { w } ) =/= ( N ` { Z } ) )`
mapdh8ac.xz
`|- ( ph -> -. X e. ( N ` { w , Z } ) )`
Assertion mapdh8ac
`|- ( 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 mapdh8ac.f
` |-  ( ph -> F e. D )`
16 mapdh8ac.mn
` |-  ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { F } ) )`
17 mapdh8ac.eg
` |-  ( ph -> ( I ` <. X , F , Y >. ) = G )`
18 mapdh8ac.ee
` |-  ( ph -> ( I ` <. X , F , Z >. ) = E )`
19 mapdh8ac.x
` |-  ( ph -> X e. ( V \ { .0. } ) )`
20 mapdh8ac.y
` |-  ( ph -> Y e. ( V \ { .0. } ) )`
21 mapdh8ac.z
` |-  ( ph -> Z e. ( V \ { .0. } ) )`
22 mapdh8ac.t
` |-  ( ph -> T e. ( V \ { .0. } ) )`
23 mapdh8ac.yn
` |-  ( ph -> ( N ` { X } ) = ( N ` { T } ) )`
24 mapdh8ac.ew
` |-  ( ph -> ( I ` <. X , F , w >. ) = B )`
25 mapdh8ac.w
` |-  ( ph -> w e. ( V \ { .0. } ) )`
26 mapdh8ac.yw
` |-  ( ph -> ( N ` { Y } ) =/= ( N ` { w } ) )`
27 mapdh8ac.xy
` |-  ( ph -> -. X e. ( N ` { Y , w } ) )`
28 mapdh8ac.wz
` |-  ( ph -> ( N ` { w } ) =/= ( N ` { Z } ) )`
29 mapdh8ac.xz
` |-  ( ph -> -. X e. ( N ` { w , Z } ) )`
30 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 24 19 20 25 22 26 27 23 mapdh8ab
` |-  ( ph -> ( I ` <. Y , G , T >. ) = ( I ` <. w , B , T >. ) )`
31 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 24 18 19 25 21 22 28 29 23 mapdh8ab
` |-  ( ph -> ( I ` <. w , B , T >. ) = ( I ` <. Z , E , T >. ) )`
32 30 31 eqtrd
` |-  ( ph -> ( I ` <. Y , G , T >. ) = ( I ` <. Z , E , T >. ) )`