This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lshpkr

Description: The kernel of functional G is the hyperplane defining it. (Contributed by NM, 17-Jul-2014)

Ref Expression
Hypotheses lshpkr.v 
|- V = ( Base ` W )
lshpkr.a 
|- .+ = ( +g ` W )
lshpkr.n 
|- N = ( LSpan ` W )
lshpkr.p 
|- .(+) = ( LSSum ` W )
lshpkr.h 
|- H = ( LSHyp ` W )
lshpkr.w 
|- ( ph -> W e. LVec )
lshpkr.u 
|- ( ph -> U e. H )
lshpkr.z 
|- ( ph -> Z e. V )
lshpkr.e 
|- ( ph -> ( U .(+) ( N ` { Z } ) ) = V )
lshpkr.d 
|- D = ( Scalar ` W )
lshpkr.k 
|- K = ( Base ` D )
lshpkr.t 
|- .x. = ( .s ` W )
lshpkr.g 
|- G = ( x e. V |-> ( iota_ k e. K E. y e. U x = ( y .+ ( k .x. Z ) ) ) )
lshpkr.l 
|- L = ( LKer ` W )
Assertion lshpkr 
|- ( ph -> ( L ` G ) = U )

Proof

Step Hyp Ref Expression
1 lshpkr.v 
 |-  V = ( Base ` W )
2 lshpkr.a 
 |-  .+ = ( +g ` W )
3 lshpkr.n 
 |-  N = ( LSpan ` W )
4 lshpkr.p 
 |-  .(+) = ( LSSum ` W )
5 lshpkr.h 
 |-  H = ( LSHyp ` W )
6 lshpkr.w 
 |-  ( ph -> W e. LVec )
7 lshpkr.u 
 |-  ( ph -> U e. H )
8 lshpkr.z 
 |-  ( ph -> Z e. V )
9 lshpkr.e 
 |-  ( ph -> ( U .(+) ( N ` { Z } ) ) = V )
10 lshpkr.d 
 |-  D = ( Scalar ` W )
11 lshpkr.k 
 |-  K = ( Base ` D )
12 lshpkr.t 
 |-  .x. = ( .s ` W )
13 lshpkr.g 
 |-  G = ( x e. V |-> ( iota_ k e. K E. y e. U x = ( y .+ ( k .x. Z ) ) ) )
14 lshpkr.l 
 |-  L = ( LKer ` W )
15 eqid 
 |-  ( LFnl ` W ) = ( LFnl ` W )
16 lveclmod 
 |-  ( W e. LVec -> W e. LMod )
17 6 16 syl 
 |-  ( ph -> W e. LMod )
18 1 2 3 4 5 6 7 8 9 10 11 12 13 15 lshpkrcl 
 |-  ( ph -> G e. ( LFnl ` W ) )
19 1 15 14 17 18 lkrssv 
 |-  ( ph -> ( L ` G ) C_ V )
20 19 sseld 
 |-  ( ph -> ( v e. ( L ` G ) -> v e. V ) )
21 eqid 
 |-  ( LSubSp ` W ) = ( LSubSp ` W )
22 21 5 17 7 lshplss 
 |-  ( ph -> U e. ( LSubSp ` W ) )
23 1 21 lssel 
 |-  ( ( U e. ( LSubSp ` W ) /\ v e. U ) -> v e. V )
24 22 23 sylan 
 |-  ( ( ph /\ v e. U ) -> v e. V )
25 24 ex 
 |-  ( ph -> ( v e. U -> v e. V ) )
26 eqid 
 |-  ( 0g ` D ) = ( 0g ` D )
27 1 10 26 15 14 ellkr 
 |-  ( ( W e. LVec /\ G e. ( LFnl ` W ) ) -> ( v e. ( L ` G ) <-> ( v e. V /\ ( G ` v ) = ( 0g ` D ) ) ) )
28 6 18 27 syl2anc 
 |-  ( ph -> ( v e. ( L ` G ) <-> ( v e. V /\ ( G ` v ) = ( 0g ` D ) ) ) )
29 28 baibd 
 |-  ( ( ph /\ v e. V ) -> ( v e. ( L ` G ) <-> ( G ` v ) = ( 0g ` D ) ) )
30 6 adantr 
 |-  ( ( ph /\ v e. V ) -> W e. LVec )
31 7 adantr 
 |-  ( ( ph /\ v e. V ) -> U e. H )
32 8 adantr 
 |-  ( ( ph /\ v e. V ) -> Z e. V )
33 simpr 
 |-  ( ( ph /\ v e. V ) -> v e. V )
34 9 adantr 
 |-  ( ( ph /\ v e. V ) -> ( U .(+) ( N ` { Z } ) ) = V )
35 1 2 3 4 5 30 31 32 33 34 10 11 12 26 13 lshpkrlem1 
 |-  ( ( ph /\ v e. V ) -> ( v e. U <-> ( G ` v ) = ( 0g ` D ) ) )
36 29 35 bitr4d 
 |-  ( ( ph /\ v e. V ) -> ( v e. ( L ` G ) <-> v e. U ) )
37 36 ex 
 |-  ( ph -> ( v e. V -> ( v e. ( L ` G ) <-> v e. U ) ) )
38 20 25 37 pm5.21ndd 
 |-  ( ph -> ( v e. ( L ` G ) <-> v e. U ) )
39 38 eqrdv 
 |-  ( ph -> ( L ` G ) = U )