Description: Lemmma for mapdh6N . (Contributed by NM, 23-Apr-2015) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | mapdh.q | |- Q = ( 0g ` C ) |
|
mapdh.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 ) } ) ) ) ) ) |
||
mapdh.h | |- H = ( LHyp ` K ) |
||
mapdh.m | |- M = ( ( mapd ` K ) ` W ) |
||
mapdh.u | |- U = ( ( DVecH ` K ) ` W ) |
||
mapdh.v | |- V = ( Base ` U ) |
||
mapdh.s | |- .- = ( -g ` U ) |
||
mapdhc.o | |- .0. = ( 0g ` U ) |
||
mapdh.n | |- N = ( LSpan ` U ) |
||
mapdh.c | |- C = ( ( LCDual ` K ) ` W ) |
||
mapdh.d | |- D = ( Base ` C ) |
||
mapdh.r | |- R = ( -g ` C ) |
||
mapdh.j | |- J = ( LSpan ` C ) |
||
mapdh.k | |- ( ph -> ( K e. HL /\ W e. H ) ) |
||
mapdhc.f | |- ( ph -> F e. D ) |
||
mapdh.mn | |- ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { F } ) ) |
||
mapdhcl.x | |- ( ph -> X e. ( V \ { .0. } ) ) |
||
mapdh.p | |- .+ = ( +g ` U ) |
||
mapdh.a | |- .+b = ( +g ` C ) |
||
mapdh6b0.y | |- ( ph -> Y e. V ) |
||
mapdh6b0.z | |- ( ph -> Z e. V ) |
||
mapdh6b0.ne | |- ( ph -> ( ( N ` { X } ) i^i ( N ` { Y , Z } ) ) = { .0. } ) |
||
Assertion | mapdh6b0N | |- ( ph -> -. X e. ( N ` { Y , Z } ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mapdh.q | |- Q = ( 0g ` C ) |
|
2 | mapdh.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 ) } ) ) ) ) ) |
|
3 | mapdh.h | |- H = ( LHyp ` K ) |
|
4 | mapdh.m | |- M = ( ( mapd ` K ) ` W ) |
|
5 | mapdh.u | |- U = ( ( DVecH ` K ) ` W ) |
|
6 | mapdh.v | |- V = ( Base ` U ) |
|
7 | mapdh.s | |- .- = ( -g ` U ) |
|
8 | mapdhc.o | |- .0. = ( 0g ` U ) |
|
9 | mapdh.n | |- N = ( LSpan ` U ) |
|
10 | mapdh.c | |- C = ( ( LCDual ` K ) ` W ) |
|
11 | mapdh.d | |- D = ( Base ` C ) |
|
12 | mapdh.r | |- R = ( -g ` C ) |
|
13 | mapdh.j | |- J = ( LSpan ` C ) |
|
14 | mapdh.k | |- ( ph -> ( K e. HL /\ W e. H ) ) |
|
15 | mapdhc.f | |- ( ph -> F e. D ) |
|
16 | mapdh.mn | |- ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { F } ) ) |
|
17 | mapdhcl.x | |- ( ph -> X e. ( V \ { .0. } ) ) |
|
18 | mapdh.p | |- .+ = ( +g ` U ) |
|
19 | mapdh.a | |- .+b = ( +g ` C ) |
|
20 | mapdh6b0.y | |- ( ph -> Y e. V ) |
|
21 | mapdh6b0.z | |- ( ph -> Z e. V ) |
|
22 | mapdh6b0.ne | |- ( ph -> ( ( N ` { X } ) i^i ( N ` { Y , Z } ) ) = { .0. } ) |
|
23 | eqid | |- ( LSubSp ` U ) = ( LSubSp ` U ) |
|
24 | 3 5 14 | dvhlvec | |- ( ph -> U e. LVec ) |
25 | 3 5 14 | dvhlmod | |- ( ph -> U e. LMod ) |
26 | 6 23 9 25 20 21 | lspprcl | |- ( ph -> ( N ` { Y , Z } ) e. ( LSubSp ` U ) ) |
27 | 6 8 9 23 24 26 17 | lspdisjb | |- ( ph -> ( -. X e. ( N ` { Y , Z } ) <-> ( ( N ` { X } ) i^i ( N ` { Y , Z } ) ) = { .0. } ) ) |
28 | 22 27 | mpbird | |- ( ph -> -. X e. ( N ` { Y , Z } ) ) |