Metamath Proof Explorer

Theorem lkrlsp3

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, 29-Jun-2014)

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

Proof

Step Hyp Ref Expression
1 lkrlsp3.v 
 |-  V = ( Base ` W )
2 lkrlsp3.n 
 |-  N = ( LSpan ` W )
3 lkrlsp3.f 
 |-  F = ( LFnl ` W )
4 lkrlsp3.k 
 |-  K = ( LKer ` W )
5 lveclmod 
 |-  ( W e. LVec -> W e. LMod )
6 5 3ad2ant1 
 |-  ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ -. X e. ( K ` G ) ) -> W e. LMod )
7 simp2r 
 |-  ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ -. X e. ( K ` G ) ) -> G e. F )
8 eqid 
 |-  ( LSubSp ` W ) = ( LSubSp ` W )
9 3 4 8 lkrlss 
 |-  ( ( W e. LMod /\ G e. F ) -> ( K ` G ) e. ( LSubSp ` W ) )
10 6 7 9 syl2anc 
 |-  ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ -. X e. ( K ` G ) ) -> ( K ` G ) e. ( LSubSp ` W ) )
11 8 2 lspid 
 |-  ( ( W e. LMod /\ ( K ` G ) e. ( LSubSp ` W ) ) -> ( N ` ( K ` G ) ) = ( K ` G ) )
12 6 10 11 syl2anc 
 |-  ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ -. X e. ( K ` G ) ) -> ( N ` ( K ` G ) ) = ( K ` G ) )
13 12 uneq1d 
 |-  ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ -. X e. ( K ` G ) ) -> ( ( N ` ( K ` G ) ) u. ( N ` { X } ) ) = ( ( K ` G ) u. ( N ` { X } ) ) )
14 13 fveq2d 
 |-  ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ -. X e. ( K ` G ) ) -> ( N ` ( ( N ` ( K ` G ) ) u. ( N ` { X } ) ) ) = ( N ` ( ( K ` G ) u. ( N ` { X } ) ) ) )
15 1 3 4 6 7 lkrssv 
 |-  ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ -. X e. ( K ` G ) ) -> ( K ` G ) C_ V )
16 simp2l 
 |-  ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ -. X e. ( K ` G ) ) -> X e. V )
17 16 snssd 
 |-  ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ -. X e. ( K ` G ) ) -> { X } C_ V )
18 1 2 lspun 
 |-  ( ( W e. LMod /\ ( K ` G ) C_ V /\ { X } C_ V ) -> ( N ` ( ( K ` G ) u. { X } ) ) = ( N ` ( ( N ` ( K ` G ) ) u. ( N ` { X } ) ) ) )
19 6 15 17 18 syl3anc 
 |-  ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ -. X e. ( K ` G ) ) -> ( N ` ( ( K ` G ) u. { X } ) ) = ( N ` ( ( N ` ( K ` G ) ) u. ( N ` { X } ) ) ) )
20 1 8 2 lspsncl 
 |-  ( ( W e. LMod /\ X e. V ) -> ( N ` { X } ) e. ( LSubSp ` W ) )
21 6 16 20 syl2anc 
 |-  ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ -. X e. ( K ` G ) ) -> ( N ` { X } ) e. ( LSubSp ` W ) )
22 eqid 
 |-  ( LSSum ` W ) = ( LSSum ` W )
23 8 2 22 lsmsp 
 |-  ( ( W e. LMod /\ ( K ` G ) e. ( LSubSp ` W ) /\ ( N ` { X } ) e. ( LSubSp ` W ) ) -> ( ( K ` G ) ( LSSum ` W ) ( N ` { X } ) ) = ( N ` ( ( K ` G ) u. ( N ` { X } ) ) ) )
24 6 10 21 23 syl3anc 
 |-  ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ -. X e. ( K ` G ) ) -> ( ( K ` G ) ( LSSum ` W ) ( N ` { X } ) ) = ( N ` ( ( K ` G ) u. ( N ` { X } ) ) ) )
25 14 19 24 3eqtr4d 
 |-  ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ -. X e. ( K ` G ) ) -> ( N ` ( ( K ` G ) u. { X } ) ) = ( ( K ` G ) ( LSSum ` W ) ( N ` { X } ) ) )
26 1 2 22 3 4 lkrlsp2 
 |-  ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ -. X e. ( K ` G ) ) -> ( ( K ` G ) ( LSSum ` W ) ( N ` { X } ) ) = V )
27 25 26 eqtrd 
 |-  ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ -. X e. ( K ` G ) ) -> ( N ` ( ( K ` G ) u. { X } ) ) = V )