Step |
Hyp |
Ref |
Expression |
1 |
|
lshpkrex.h |
|- H = ( LSHyp ` W ) |
2 |
|
lshpkrex.f |
|- F = ( LFnl ` W ) |
3 |
|
lshpkrex.k |
|- K = ( LKer ` W ) |
4 |
|
eqid |
|- ( Base ` W ) = ( Base ` W ) |
5 |
|
eqid |
|- ( LSpan ` W ) = ( LSpan ` W ) |
6 |
|
eqid |
|- ( LSubSp ` W ) = ( LSubSp ` W ) |
7 |
|
eqid |
|- ( LSSum ` W ) = ( LSSum ` W ) |
8 |
|
lveclmod |
|- ( W e. LVec -> W e. LMod ) |
9 |
4 5 6 7 1 8
|
islshpsm |
|- ( W e. LVec -> ( U e. H <-> ( U e. ( LSubSp ` W ) /\ U =/= ( Base ` W ) /\ E. z e. ( Base ` W ) ( U ( LSSum ` W ) ( ( LSpan ` W ) ` { z } ) ) = ( Base ` W ) ) ) ) |
10 |
|
simp3 |
|- ( ( U e. ( LSubSp ` W ) /\ U =/= ( Base ` W ) /\ E. z e. ( Base ` W ) ( U ( LSSum ` W ) ( ( LSpan ` W ) ` { z } ) ) = ( Base ` W ) ) -> E. z e. ( Base ` W ) ( U ( LSSum ` W ) ( ( LSpan ` W ) ` { z } ) ) = ( Base ` W ) ) |
11 |
9 10
|
syl6bi |
|- ( W e. LVec -> ( U e. H -> E. z e. ( Base ` W ) ( U ( LSSum ` W ) ( ( LSpan ` W ) ` { z } ) ) = ( Base ` W ) ) ) |
12 |
11
|
imp |
|- ( ( W e. LVec /\ U e. H ) -> E. z e. ( Base ` W ) ( U ( LSSum ` W ) ( ( LSpan ` W ) ` { z } ) ) = ( Base ` W ) ) |
13 |
|
eqid |
|- ( +g ` W ) = ( +g ` W ) |
14 |
|
simp1l |
|- ( ( ( W e. LVec /\ U e. H ) /\ z e. ( Base ` W ) /\ ( U ( LSSum ` W ) ( ( LSpan ` W ) ` { z } ) ) = ( Base ` W ) ) -> W e. LVec ) |
15 |
|
simp1r |
|- ( ( ( W e. LVec /\ U e. H ) /\ z e. ( Base ` W ) /\ ( U ( LSSum ` W ) ( ( LSpan ` W ) ` { z } ) ) = ( Base ` W ) ) -> U e. H ) |
16 |
|
simp2 |
|- ( ( ( W e. LVec /\ U e. H ) /\ z e. ( Base ` W ) /\ ( U ( LSSum ` W ) ( ( LSpan ` W ) ` { z } ) ) = ( Base ` W ) ) -> z e. ( Base ` W ) ) |
17 |
|
simp3 |
|- ( ( ( W e. LVec /\ U e. H ) /\ z e. ( Base ` W ) /\ ( U ( LSSum ` W ) ( ( LSpan ` W ) ` { z } ) ) = ( Base ` W ) ) -> ( U ( LSSum ` W ) ( ( LSpan ` W ) ` { z } ) ) = ( Base ` W ) ) |
18 |
|
eqid |
|- ( Scalar ` W ) = ( Scalar ` W ) |
19 |
|
eqid |
|- ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) ) |
20 |
|
eqid |
|- ( .s ` W ) = ( .s ` W ) |
21 |
|
eqid |
|- ( x e. ( Base ` W ) |-> ( iota_ k e. ( Base ` ( Scalar ` W ) ) E. y e. U x = ( y ( +g ` W ) ( k ( .s ` W ) z ) ) ) ) = ( x e. ( Base ` W ) |-> ( iota_ k e. ( Base ` ( Scalar ` W ) ) E. y e. U x = ( y ( +g ` W ) ( k ( .s ` W ) z ) ) ) ) |
22 |
4 13 5 7 1 14 15 16 17 18 19 20 21 2
|
lshpkrcl |
|- ( ( ( W e. LVec /\ U e. H ) /\ z e. ( Base ` W ) /\ ( U ( LSSum ` W ) ( ( LSpan ` W ) ` { z } ) ) = ( Base ` W ) ) -> ( x e. ( Base ` W ) |-> ( iota_ k e. ( Base ` ( Scalar ` W ) ) E. y e. U x = ( y ( +g ` W ) ( k ( .s ` W ) z ) ) ) ) e. F ) |
23 |
4 13 5 7 1 14 15 16 17 18 19 20 21 3
|
lshpkr |
|- ( ( ( W e. LVec /\ U e. H ) /\ z e. ( Base ` W ) /\ ( U ( LSSum ` W ) ( ( LSpan ` W ) ` { z } ) ) = ( Base ` W ) ) -> ( K ` ( x e. ( Base ` W ) |-> ( iota_ k e. ( Base ` ( Scalar ` W ) ) E. y e. U x = ( y ( +g ` W ) ( k ( .s ` W ) z ) ) ) ) ) = U ) |
24 |
|
fveqeq2 |
|- ( g = ( x e. ( Base ` W ) |-> ( iota_ k e. ( Base ` ( Scalar ` W ) ) E. y e. U x = ( y ( +g ` W ) ( k ( .s ` W ) z ) ) ) ) -> ( ( K ` g ) = U <-> ( K ` ( x e. ( Base ` W ) |-> ( iota_ k e. ( Base ` ( Scalar ` W ) ) E. y e. U x = ( y ( +g ` W ) ( k ( .s ` W ) z ) ) ) ) ) = U ) ) |
25 |
24
|
rspcev |
|- ( ( ( x e. ( Base ` W ) |-> ( iota_ k e. ( Base ` ( Scalar ` W ) ) E. y e. U x = ( y ( +g ` W ) ( k ( .s ` W ) z ) ) ) ) e. F /\ ( K ` ( x e. ( Base ` W ) |-> ( iota_ k e. ( Base ` ( Scalar ` W ) ) E. y e. U x = ( y ( +g ` W ) ( k ( .s ` W ) z ) ) ) ) ) = U ) -> E. g e. F ( K ` g ) = U ) |
26 |
22 23 25
|
syl2anc |
|- ( ( ( W e. LVec /\ U e. H ) /\ z e. ( Base ` W ) /\ ( U ( LSSum ` W ) ( ( LSpan ` W ) ` { z } ) ) = ( Base ` W ) ) -> E. g e. F ( K ` g ) = U ) |
27 |
26
|
rexlimdv3a |
|- ( ( W e. LVec /\ U e. H ) -> ( E. z e. ( Base ` W ) ( U ( LSSum ` W ) ( ( LSpan ` W ) ` { z } ) ) = ( Base ` W ) -> E. g e. F ( K ` g ) = U ) ) |
28 |
12 27
|
mpd |
|- ( ( W e. LVec /\ U e. H ) -> E. g e. F ( K ` g ) = U ) |