Description: Part of Part (8) in Baer p. 48. (Contributed by NM, 11-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 ) ) |
||
mapdh8h.f | |- ( ph -> F e. D ) |
||
mapdh8h.mn | |- ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { F } ) ) |
||
mapdh8i.x | |- ( ph -> X e. ( V \ { .0. } ) ) |
||
mapdh8i.y | |- ( ph -> Y e. ( V \ { .0. } ) ) |
||
mapdh8i.z | |- ( ph -> Z e. ( V \ { .0. } ) ) |
||
mapdh8i.xy | |- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) ) |
||
mapdh8i.xz | |- ( ph -> ( N ` { X } ) =/= ( N ` { Z } ) ) |
||
mapdh8i.yt | |- ( ph -> ( N ` { Y } ) =/= ( N ` { T } ) ) |
||
mapdh8i.zt | |- ( ph -> ( N ` { Z } ) =/= ( N ` { T } ) ) |
||
mapdh8i.t | |- ( ph -> T e. ( V \ { .0. } ) ) |
||
mapdh8i.xt | |- ( ph -> ( N ` { X } ) =/= ( N ` { T } ) ) |
||
Assertion | mapdh8i | |- ( ph -> ( I ` <. Y , ( I ` <. X , F , Y >. ) , T >. ) = ( I ` <. Z , ( I ` <. X , F , Z >. ) , T >. ) ) |
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 | mapdh8i.x | |- ( ph -> X e. ( V \ { .0. } ) ) |
|
18 | mapdh8i.y | |- ( ph -> Y e. ( V \ { .0. } ) ) |
|
19 | mapdh8i.z | |- ( ph -> Z e. ( V \ { .0. } ) ) |
|
20 | mapdh8i.xy | |- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) ) |
|
21 | mapdh8i.xz | |- ( ph -> ( N ` { X } ) =/= ( N ` { Z } ) ) |
|
22 | mapdh8i.yt | |- ( ph -> ( N ` { Y } ) =/= ( N ` { T } ) ) |
|
23 | mapdh8i.zt | |- ( ph -> ( N ` { Z } ) =/= ( N ` { T } ) ) |
|
24 | mapdh8i.t | |- ( ph -> T e. ( V \ { .0. } ) ) |
|
25 | mapdh8i.xt | |- ( ph -> ( N ` { X } ) =/= ( N ` { T } ) ) |
|
26 | eqidd | |- ( ph -> ( I ` <. X , F , Y >. ) = ( I ` <. X , F , Y >. ) ) |
|
27 | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 26 17 18 24 20 25 22 | mapdh8g | |- ( ph -> ( I ` <. Y , ( I ` <. X , F , Y >. ) , T >. ) = ( I ` <. X , F , T >. ) ) |
28 | eqidd | |- ( ph -> ( I ` <. X , F , Z >. ) = ( I ` <. X , F , Z >. ) ) |
|
29 | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 28 17 19 24 21 25 23 | mapdh8g | |- ( ph -> ( I ` <. Z , ( I ` <. X , F , Z >. ) , T >. ) = ( I ` <. X , F , T >. ) ) |
30 | 27 29 | eqtr4d | |- ( ph -> ( I ` <. Y , ( I ` <. X , F , Y >. ) , T >. ) = ( I ` <. Z , ( I ` <. X , F , Z >. ) , T >. ) ) |