Metamath Proof Explorer

Theorem lkrlsp2

Description: The subspace sum of a kernel and the span of a vector not in the kernel is the whole vector space. (Contributed by NM, 12-May-2014)

Ref Expression
Hypotheses lkrlsp2.v 
|- V = ( Base ` W )
lkrlsp2.n 
|- N = ( LSpan ` W )
lkrlsp2.p 
|- .(+) = ( LSSum ` W )
lkrlsp2.f 
|- F = ( LFnl ` W )
lkrlsp2.k 
|- K = ( LKer ` W )
Assertion lkrlsp2 
|- ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ -. X e. ( K ` G ) ) -> ( ( K ` G ) .(+) ( N ` { X } ) ) = V )

Proof

Step Hyp Ref Expression
1 lkrlsp2.v 
 |-  V = ( Base ` W )
2 lkrlsp2.n 
 |-  N = ( LSpan ` W )
3 lkrlsp2.p 
 |-  .(+) = ( LSSum ` W )
4 lkrlsp2.f 
 |-  F = ( LFnl ` W )
5 lkrlsp2.k 
 |-  K = ( LKer ` W )
6 simp2l 
 |-  ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ ( G ` X ) = ( 0g ` ( Scalar ` W ) ) ) -> X e. V )
7 simp3 
 |-  ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ ( G ` X ) = ( 0g ` ( Scalar ` W ) ) ) -> ( G ` X ) = ( 0g ` ( Scalar ` W ) ) )
8 simp1 
 |-  ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ ( G ` X ) = ( 0g ` ( Scalar ` W ) ) ) -> W e. LVec )
9 simp2r 
 |-  ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ ( G ` X ) = ( 0g ` ( Scalar ` W ) ) ) -> G e. F )
10 eqid 
 |-  ( Scalar ` W ) = ( Scalar ` W )
11 eqid 
 |-  ( 0g ` ( Scalar ` W ) ) = ( 0g ` ( Scalar ` W ) )
12 1 10 11 4 5 ellkr 
 |-  ( ( W e. LVec /\ G e. F ) -> ( X e. ( K ` G ) <-> ( X e. V /\ ( G ` X ) = ( 0g ` ( Scalar ` W ) ) ) ) )
13 8 9 12 syl2anc 
 |-  ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ ( G ` X ) = ( 0g ` ( Scalar ` W ) ) ) -> ( X e. ( K ` G ) <-> ( X e. V /\ ( G ` X ) = ( 0g ` ( Scalar ` W ) ) ) ) )
14 6 7 13 mpbir2and 
 |-  ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ ( G ` X ) = ( 0g ` ( Scalar ` W ) ) ) -> X e. ( K ` G ) )
15 14 3expia 
 |-  ( ( W e. LVec /\ ( X e. V /\ G e. F ) ) -> ( ( G ` X ) = ( 0g ` ( Scalar ` W ) ) -> X e. ( K ` G ) ) )
16 15 necon3bd 
 |-  ( ( W e. LVec /\ ( X e. V /\ G e. F ) ) -> ( -. X e. ( K ` G ) -> ( G ` X ) =/= ( 0g ` ( Scalar ` W ) ) ) )
17 16 3impia 
 |-  ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ -. X e. ( K ` G ) ) -> ( G ` X ) =/= ( 0g ` ( Scalar ` W ) ) )
18 10 11 1 2 3 4 5 lkrlsp 
 |-  ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ ( G ` X ) =/= ( 0g ` ( Scalar ` W ) ) ) -> ( ( K ` G ) .(+) ( N ` { X } ) ) = V )
19 17 18 syld3an3 
 |-  ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ -. X e. ( K ` G ) ) -> ( ( K ` G ) .(+) ( N ` { X } ) ) = V )