Metamath Proof Explorer

Theorem lshpkrex

Description: There exists a functional whose kernel equals a given hyperplane. Part of Th. 1.27 of Barbu and Precupanu,Convexity and Optimization in Banach Spaces. (Contributed by NM, 17-Jul-2014)

Ref Expression
Hypotheses lshpkrex.h 
|- H = ( LSHyp ` W )
lshpkrex.f 
|- F = ( LFnl ` W )
lshpkrex.k 
|- K = ( LKer ` W )
Assertion lshpkrex 
|- ( ( W e. LVec /\ U e. H ) -> E. g e. F ( K ` g ) = U )

Proof

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 )