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