Description: Kernel of the explicit functional G determined by a nonzero vector X . Compare the more general lshpkr . (Contributed by NM, 27-Oct-2014)
Ref | Expression | ||
---|---|---|---|
Hypotheses | dochsnkr2.h | |- H = ( LHyp ` K ) |
|
dochsnkr2.o | |- ._|_ = ( ( ocH ` K ) ` W ) |
||
dochsnkr2.u | |- U = ( ( DVecH ` K ) ` W ) |
||
dochsnkr2.v | |- V = ( Base ` U ) |
||
dochsnkr2.z | |- .0. = ( 0g ` U ) |
||
dochsnkr2.a | |- .+ = ( +g ` U ) |
||
dochsnkr2.t | |- .x. = ( .s ` U ) |
||
dochsnkr2.l | |- L = ( LKer ` U ) |
||
dochsnkr2.d | |- D = ( Scalar ` U ) |
||
dochsnkr2.r | |- R = ( Base ` D ) |
||
dochsnkr2.g | |- G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { X } ) v = ( w .+ ( k .x. X ) ) ) ) |
||
dochsnkr2.k | |- ( ph -> ( K e. HL /\ W e. H ) ) |
||
dochsnkr2.x | |- ( ph -> X e. ( V \ { .0. } ) ) |
||
Assertion | dochsnkr2 | |- ( ph -> ( L ` G ) = ( ._|_ ` { X } ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dochsnkr2.h | |- H = ( LHyp ` K ) |
|
2 | dochsnkr2.o | |- ._|_ = ( ( ocH ` K ) ` W ) |
|
3 | dochsnkr2.u | |- U = ( ( DVecH ` K ) ` W ) |
|
4 | dochsnkr2.v | |- V = ( Base ` U ) |
|
5 | dochsnkr2.z | |- .0. = ( 0g ` U ) |
|
6 | dochsnkr2.a | |- .+ = ( +g ` U ) |
|
7 | dochsnkr2.t | |- .x. = ( .s ` U ) |
|
8 | dochsnkr2.l | |- L = ( LKer ` U ) |
|
9 | dochsnkr2.d | |- D = ( Scalar ` U ) |
|
10 | dochsnkr2.r | |- R = ( Base ` D ) |
|
11 | dochsnkr2.g | |- G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { X } ) v = ( w .+ ( k .x. X ) ) ) ) |
|
12 | dochsnkr2.k | |- ( ph -> ( K e. HL /\ W e. H ) ) |
|
13 | dochsnkr2.x | |- ( ph -> X e. ( V \ { .0. } ) ) |
|
14 | eqid | |- ( LSpan ` U ) = ( LSpan ` U ) |
|
15 | eqid | |- ( LSSum ` U ) = ( LSSum ` U ) |
|
16 | eqid | |- ( LSHyp ` U ) = ( LSHyp ` U ) |
|
17 | 1 3 12 | dvhlvec | |- ( ph -> U e. LVec ) |
18 | 1 2 3 4 5 16 12 13 | dochsnshp | |- ( ph -> ( ._|_ ` { X } ) e. ( LSHyp ` U ) ) |
19 | 13 | eldifad | |- ( ph -> X e. V ) |
20 | 1 2 3 4 5 14 15 12 13 | dochexmidat | |- ( ph -> ( ( ._|_ ` { X } ) ( LSSum ` U ) ( ( LSpan ` U ) ` { X } ) ) = V ) |
21 | 4 6 14 15 16 17 18 19 20 9 10 7 11 8 | lshpkr | |- ( ph -> ( L ` G ) = ( ._|_ ` { X } ) ) |