Metamath Proof Explorer


Theorem lkrlsp

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

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

Proof

Step Hyp Ref Expression
1 lkrlsp.d
 |-  D = ( Scalar ` W )
2 lkrlsp.o
 |-  .0. = ( 0g ` D )
3 lkrlsp.v
 |-  V = ( Base ` W )
4 lkrlsp.n
 |-  N = ( LSpan ` W )
5 lkrlsp.p
 |-  .(+) = ( LSSum ` W )
6 lkrlsp.f
 |-  F = ( LFnl ` W )
7 lkrlsp.k
 |-  K = ( LKer ` W )
8 lveclmod
 |-  ( W e. LVec -> W e. LMod )
9 8 3ad2ant1
 |-  ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ ( G ` X ) =/= .0. ) -> W e. LMod )
10 simp2r
 |-  ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ ( G ` X ) =/= .0. ) -> G e. F )
11 eqid
 |-  ( LSubSp ` W ) = ( LSubSp ` W )
12 6 7 11 lkrlss
 |-  ( ( W e. LMod /\ G e. F ) -> ( K ` G ) e. ( LSubSp ` W ) )
13 9 10 12 syl2anc
 |-  ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ ( G ` X ) =/= .0. ) -> ( K ` G ) e. ( LSubSp ` W ) )
14 simp2l
 |-  ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ ( G ` X ) =/= .0. ) -> X e. V )
15 3 11 4 lspsncl
 |-  ( ( W e. LMod /\ X e. V ) -> ( N ` { X } ) e. ( LSubSp ` W ) )
16 9 14 15 syl2anc
 |-  ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ ( G ` X ) =/= .0. ) -> ( N ` { X } ) e. ( LSubSp ` W ) )
17 11 5 lsmcl
 |-  ( ( W e. LMod /\ ( K ` G ) e. ( LSubSp ` W ) /\ ( N ` { X } ) e. ( LSubSp ` W ) ) -> ( ( K ` G ) .(+) ( N ` { X } ) ) e. ( LSubSp ` W ) )
18 9 13 16 17 syl3anc
 |-  ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ ( G ` X ) =/= .0. ) -> ( ( K ` G ) .(+) ( N ` { X } ) ) e. ( LSubSp ` W ) )
19 3 11 lssss
 |-  ( ( ( K ` G ) .(+) ( N ` { X } ) ) e. ( LSubSp ` W ) -> ( ( K ` G ) .(+) ( N ` { X } ) ) C_ V )
20 18 19 syl
 |-  ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ ( G ` X ) =/= .0. ) -> ( ( K ` G ) .(+) ( N ` { X } ) ) C_ V )
21 simpl1
 |-  ( ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ ( G ` X ) =/= .0. ) /\ u e. V ) -> W e. LVec )
22 21 8 syl
 |-  ( ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ ( G ` X ) =/= .0. ) /\ u e. V ) -> W e. LMod )
23 simpr
 |-  ( ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ ( G ` X ) =/= .0. ) /\ u e. V ) -> u e. V )
24 1 lmodring
 |-  ( W e. LMod -> D e. Ring )
25 22 24 syl
 |-  ( ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ ( G ` X ) =/= .0. ) /\ u e. V ) -> D e. Ring )
26 simpl2r
 |-  ( ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ ( G ` X ) =/= .0. ) /\ u e. V ) -> G e. F )
27 eqid
 |-  ( Base ` D ) = ( Base ` D )
28 1 27 3 6 lflcl
 |-  ( ( W e. LVec /\ G e. F /\ u e. V ) -> ( G ` u ) e. ( Base ` D ) )
29 21 26 23 28 syl3anc
 |-  ( ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ ( G ` X ) =/= .0. ) /\ u e. V ) -> ( G ` u ) e. ( Base ` D ) )
30 1 lvecdrng
 |-  ( W e. LVec -> D e. DivRing )
31 21 30 syl
 |-  ( ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ ( G ` X ) =/= .0. ) /\ u e. V ) -> D e. DivRing )
32 simpl2l
 |-  ( ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ ( G ` X ) =/= .0. ) /\ u e. V ) -> X e. V )
33 1 27 3 6 lflcl
 |-  ( ( W e. LVec /\ G e. F /\ X e. V ) -> ( G ` X ) e. ( Base ` D ) )
34 21 26 32 33 syl3anc
 |-  ( ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ ( G ` X ) =/= .0. ) /\ u e. V ) -> ( G ` X ) e. ( Base ` D ) )
35 simpl3
 |-  ( ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ ( G ` X ) =/= .0. ) /\ u e. V ) -> ( G ` X ) =/= .0. )
36 eqid
 |-  ( invr ` D ) = ( invr ` D )
37 27 2 36 drnginvrcl
 |-  ( ( D e. DivRing /\ ( G ` X ) e. ( Base ` D ) /\ ( G ` X ) =/= .0. ) -> ( ( invr ` D ) ` ( G ` X ) ) e. ( Base ` D ) )
38 31 34 35 37 syl3anc
 |-  ( ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ ( G ` X ) =/= .0. ) /\ u e. V ) -> ( ( invr ` D ) ` ( G ` X ) ) e. ( Base ` D ) )
39 eqid
 |-  ( .r ` D ) = ( .r ` D )
40 27 39 ringcl
 |-  ( ( D e. Ring /\ ( G ` u ) e. ( Base ` D ) /\ ( ( invr ` D ) ` ( G ` X ) ) e. ( Base ` D ) ) -> ( ( G ` u ) ( .r ` D ) ( ( invr ` D ) ` ( G ` X ) ) ) e. ( Base ` D ) )
41 25 29 38 40 syl3anc
 |-  ( ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ ( G ` X ) =/= .0. ) /\ u e. V ) -> ( ( G ` u ) ( .r ` D ) ( ( invr ` D ) ` ( G ` X ) ) ) e. ( Base ` D ) )
42 eqid
 |-  ( .s ` W ) = ( .s ` W )
43 3 1 42 27 lmodvscl
 |-  ( ( W e. LMod /\ ( ( G ` u ) ( .r ` D ) ( ( invr ` D ) ` ( G ` X ) ) ) e. ( Base ` D ) /\ X e. V ) -> ( ( ( G ` u ) ( .r ` D ) ( ( invr ` D ) ` ( G ` X ) ) ) ( .s ` W ) X ) e. V )
44 22 41 32 43 syl3anc
 |-  ( ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ ( G ` X ) =/= .0. ) /\ u e. V ) -> ( ( ( G ` u ) ( .r ` D ) ( ( invr ` D ) ` ( G ` X ) ) ) ( .s ` W ) X ) e. V )
45 eqid
 |-  ( +g ` W ) = ( +g ` W )
46 eqid
 |-  ( -g ` W ) = ( -g ` W )
47 3 45 46 lmodvnpcan
 |-  ( ( W e. LMod /\ u e. V /\ ( ( ( G ` u ) ( .r ` D ) ( ( invr ` D ) ` ( G ` X ) ) ) ( .s ` W ) X ) e. V ) -> ( ( u ( -g ` W ) ( ( ( G ` u ) ( .r ` D ) ( ( invr ` D ) ` ( G ` X ) ) ) ( .s ` W ) X ) ) ( +g ` W ) ( ( ( G ` u ) ( .r ` D ) ( ( invr ` D ) ` ( G ` X ) ) ) ( .s ` W ) X ) ) = u )
48 22 23 44 47 syl3anc
 |-  ( ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ ( G ` X ) =/= .0. ) /\ u e. V ) -> ( ( u ( -g ` W ) ( ( ( G ` u ) ( .r ` D ) ( ( invr ` D ) ` ( G ` X ) ) ) ( .s ` W ) X ) ) ( +g ` W ) ( ( ( G ` u ) ( .r ` D ) ( ( invr ` D ) ` ( G ` X ) ) ) ( .s ` W ) X ) ) = u )
49 11 lsssssubg
 |-  ( W e. LMod -> ( LSubSp ` W ) C_ ( SubGrp ` W ) )
50 22 49 syl
 |-  ( ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ ( G ` X ) =/= .0. ) /\ u e. V ) -> ( LSubSp ` W ) C_ ( SubGrp ` W ) )
51 13 adantr
 |-  ( ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ ( G ` X ) =/= .0. ) /\ u e. V ) -> ( K ` G ) e. ( LSubSp ` W ) )
52 50 51 sseldd
 |-  ( ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ ( G ` X ) =/= .0. ) /\ u e. V ) -> ( K ` G ) e. ( SubGrp ` W ) )
53 16 adantr
 |-  ( ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ ( G ` X ) =/= .0. ) /\ u e. V ) -> ( N ` { X } ) e. ( LSubSp ` W ) )
54 50 53 sseldd
 |-  ( ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ ( G ` X ) =/= .0. ) /\ u e. V ) -> ( N ` { X } ) e. ( SubGrp ` W ) )
55 3 46 lmodvsubcl
 |-  ( ( W e. LMod /\ u e. V /\ ( ( ( G ` u ) ( .r ` D ) ( ( invr ` D ) ` ( G ` X ) ) ) ( .s ` W ) X ) e. V ) -> ( u ( -g ` W ) ( ( ( G ` u ) ( .r ` D ) ( ( invr ` D ) ` ( G ` X ) ) ) ( .s ` W ) X ) ) e. V )
56 22 23 44 55 syl3anc
 |-  ( ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ ( G ` X ) =/= .0. ) /\ u e. V ) -> ( u ( -g ` W ) ( ( ( G ` u ) ( .r ` D ) ( ( invr ` D ) ` ( G ` X ) ) ) ( .s ` W ) X ) ) e. V )
57 eqid
 |-  ( -g ` D ) = ( -g ` D )
58 1 57 3 46 6 lflsub
 |-  ( ( W e. LMod /\ G e. F /\ ( u e. V /\ ( ( ( G ` u ) ( .r ` D ) ( ( invr ` D ) ` ( G ` X ) ) ) ( .s ` W ) X ) e. V ) ) -> ( G ` ( u ( -g ` W ) ( ( ( G ` u ) ( .r ` D ) ( ( invr ` D ) ` ( G ` X ) ) ) ( .s ` W ) X ) ) ) = ( ( G ` u ) ( -g ` D ) ( G ` ( ( ( G ` u ) ( .r ` D ) ( ( invr ` D ) ` ( G ` X ) ) ) ( .s ` W ) X ) ) ) )
59 22 26 23 44 58 syl112anc
 |-  ( ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ ( G ` X ) =/= .0. ) /\ u e. V ) -> ( G ` ( u ( -g ` W ) ( ( ( G ` u ) ( .r ` D ) ( ( invr ` D ) ` ( G ` X ) ) ) ( .s ` W ) X ) ) ) = ( ( G ` u ) ( -g ` D ) ( G ` ( ( ( G ` u ) ( .r ` D ) ( ( invr ` D ) ` ( G ` X ) ) ) ( .s ` W ) X ) ) ) )
60 1 27 39 3 42 6 lflmul
 |-  ( ( W e. LMod /\ G e. F /\ ( ( ( G ` u ) ( .r ` D ) ( ( invr ` D ) ` ( G ` X ) ) ) e. ( Base ` D ) /\ X e. V ) ) -> ( G ` ( ( ( G ` u ) ( .r ` D ) ( ( invr ` D ) ` ( G ` X ) ) ) ( .s ` W ) X ) ) = ( ( ( G ` u ) ( .r ` D ) ( ( invr ` D ) ` ( G ` X ) ) ) ( .r ` D ) ( G ` X ) ) )
61 22 26 41 32 60 syl112anc
 |-  ( ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ ( G ` X ) =/= .0. ) /\ u e. V ) -> ( G ` ( ( ( G ` u ) ( .r ` D ) ( ( invr ` D ) ` ( G ` X ) ) ) ( .s ` W ) X ) ) = ( ( ( G ` u ) ( .r ` D ) ( ( invr ` D ) ` ( G ` X ) ) ) ( .r ` D ) ( G ` X ) ) )
62 27 39 ringass
 |-  ( ( D e. Ring /\ ( ( G ` u ) e. ( Base ` D ) /\ ( ( invr ` D ) ` ( G ` X ) ) e. ( Base ` D ) /\ ( G ` X ) e. ( Base ` D ) ) ) -> ( ( ( G ` u ) ( .r ` D ) ( ( invr ` D ) ` ( G ` X ) ) ) ( .r ` D ) ( G ` X ) ) = ( ( G ` u ) ( .r ` D ) ( ( ( invr ` D ) ` ( G ` X ) ) ( .r ` D ) ( G ` X ) ) ) )
63 25 29 38 34 62 syl13anc
 |-  ( ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ ( G ` X ) =/= .0. ) /\ u e. V ) -> ( ( ( G ` u ) ( .r ` D ) ( ( invr ` D ) ` ( G ` X ) ) ) ( .r ` D ) ( G ` X ) ) = ( ( G ` u ) ( .r ` D ) ( ( ( invr ` D ) ` ( G ` X ) ) ( .r ` D ) ( G ` X ) ) ) )
64 eqid
 |-  ( 1r ` D ) = ( 1r ` D )
65 27 2 39 64 36 drnginvrl
 |-  ( ( D e. DivRing /\ ( G ` X ) e. ( Base ` D ) /\ ( G ` X ) =/= .0. ) -> ( ( ( invr ` D ) ` ( G ` X ) ) ( .r ` D ) ( G ` X ) ) = ( 1r ` D ) )
66 31 34 35 65 syl3anc
 |-  ( ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ ( G ` X ) =/= .0. ) /\ u e. V ) -> ( ( ( invr ` D ) ` ( G ` X ) ) ( .r ` D ) ( G ` X ) ) = ( 1r ` D ) )
67 66 oveq2d
 |-  ( ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ ( G ` X ) =/= .0. ) /\ u e. V ) -> ( ( G ` u ) ( .r ` D ) ( ( ( invr ` D ) ` ( G ` X ) ) ( .r ` D ) ( G ` X ) ) ) = ( ( G ` u ) ( .r ` D ) ( 1r ` D ) ) )
68 27 39 64 ringridm
 |-  ( ( D e. Ring /\ ( G ` u ) e. ( Base ` D ) ) -> ( ( G ` u ) ( .r ` D ) ( 1r ` D ) ) = ( G ` u ) )
69 25 29 68 syl2anc
 |-  ( ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ ( G ` X ) =/= .0. ) /\ u e. V ) -> ( ( G ` u ) ( .r ` D ) ( 1r ` D ) ) = ( G ` u ) )
70 67 69 eqtrd
 |-  ( ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ ( G ` X ) =/= .0. ) /\ u e. V ) -> ( ( G ` u ) ( .r ` D ) ( ( ( invr ` D ) ` ( G ` X ) ) ( .r ` D ) ( G ` X ) ) ) = ( G ` u ) )
71 61 63 70 3eqtrd
 |-  ( ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ ( G ` X ) =/= .0. ) /\ u e. V ) -> ( G ` ( ( ( G ` u ) ( .r ` D ) ( ( invr ` D ) ` ( G ` X ) ) ) ( .s ` W ) X ) ) = ( G ` u ) )
72 71 oveq2d
 |-  ( ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ ( G ` X ) =/= .0. ) /\ u e. V ) -> ( ( G ` u ) ( -g ` D ) ( G ` ( ( ( G ` u ) ( .r ` D ) ( ( invr ` D ) ` ( G ` X ) ) ) ( .s ` W ) X ) ) ) = ( ( G ` u ) ( -g ` D ) ( G ` u ) ) )
73 1 lmodfgrp
 |-  ( W e. LMod -> D e. Grp )
74 22 73 syl
 |-  ( ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ ( G ` X ) =/= .0. ) /\ u e. V ) -> D e. Grp )
75 27 2 57 grpsubid
 |-  ( ( D e. Grp /\ ( G ` u ) e. ( Base ` D ) ) -> ( ( G ` u ) ( -g ` D ) ( G ` u ) ) = .0. )
76 74 29 75 syl2anc
 |-  ( ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ ( G ` X ) =/= .0. ) /\ u e. V ) -> ( ( G ` u ) ( -g ` D ) ( G ` u ) ) = .0. )
77 59 72 76 3eqtrd
 |-  ( ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ ( G ` X ) =/= .0. ) /\ u e. V ) -> ( G ` ( u ( -g ` W ) ( ( ( G ` u ) ( .r ` D ) ( ( invr ` D ) ` ( G ` X ) ) ) ( .s ` W ) X ) ) ) = .0. )
78 3 1 2 6 7 ellkr
 |-  ( ( W e. LVec /\ G e. F ) -> ( ( u ( -g ` W ) ( ( ( G ` u ) ( .r ` D ) ( ( invr ` D ) ` ( G ` X ) ) ) ( .s ` W ) X ) ) e. ( K ` G ) <-> ( ( u ( -g ` W ) ( ( ( G ` u ) ( .r ` D ) ( ( invr ` D ) ` ( G ` X ) ) ) ( .s ` W ) X ) ) e. V /\ ( G ` ( u ( -g ` W ) ( ( ( G ` u ) ( .r ` D ) ( ( invr ` D ) ` ( G ` X ) ) ) ( .s ` W ) X ) ) ) = .0. ) ) )
79 21 26 78 syl2anc
 |-  ( ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ ( G ` X ) =/= .0. ) /\ u e. V ) -> ( ( u ( -g ` W ) ( ( ( G ` u ) ( .r ` D ) ( ( invr ` D ) ` ( G ` X ) ) ) ( .s ` W ) X ) ) e. ( K ` G ) <-> ( ( u ( -g ` W ) ( ( ( G ` u ) ( .r ` D ) ( ( invr ` D ) ` ( G ` X ) ) ) ( .s ` W ) X ) ) e. V /\ ( G ` ( u ( -g ` W ) ( ( ( G ` u ) ( .r ` D ) ( ( invr ` D ) ` ( G ` X ) ) ) ( .s ` W ) X ) ) ) = .0. ) ) )
80 56 77 79 mpbir2and
 |-  ( ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ ( G ` X ) =/= .0. ) /\ u e. V ) -> ( u ( -g ` W ) ( ( ( G ` u ) ( .r ` D ) ( ( invr ` D ) ` ( G ` X ) ) ) ( .s ` W ) X ) ) e. ( K ` G ) )
81 3 42 1 27 4 22 41 32 lspsneli
 |-  ( ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ ( G ` X ) =/= .0. ) /\ u e. V ) -> ( ( ( G ` u ) ( .r ` D ) ( ( invr ` D ) ` ( G ` X ) ) ) ( .s ` W ) X ) e. ( N ` { X } ) )
82 45 5 lsmelvali
 |-  ( ( ( ( K ` G ) e. ( SubGrp ` W ) /\ ( N ` { X } ) e. ( SubGrp ` W ) ) /\ ( ( u ( -g ` W ) ( ( ( G ` u ) ( .r ` D ) ( ( invr ` D ) ` ( G ` X ) ) ) ( .s ` W ) X ) ) e. ( K ` G ) /\ ( ( ( G ` u ) ( .r ` D ) ( ( invr ` D ) ` ( G ` X ) ) ) ( .s ` W ) X ) e. ( N ` { X } ) ) ) -> ( ( u ( -g ` W ) ( ( ( G ` u ) ( .r ` D ) ( ( invr ` D ) ` ( G ` X ) ) ) ( .s ` W ) X ) ) ( +g ` W ) ( ( ( G ` u ) ( .r ` D ) ( ( invr ` D ) ` ( G ` X ) ) ) ( .s ` W ) X ) ) e. ( ( K ` G ) .(+) ( N ` { X } ) ) )
83 52 54 80 81 82 syl22anc
 |-  ( ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ ( G ` X ) =/= .0. ) /\ u e. V ) -> ( ( u ( -g ` W ) ( ( ( G ` u ) ( .r ` D ) ( ( invr ` D ) ` ( G ` X ) ) ) ( .s ` W ) X ) ) ( +g ` W ) ( ( ( G ` u ) ( .r ` D ) ( ( invr ` D ) ` ( G ` X ) ) ) ( .s ` W ) X ) ) e. ( ( K ` G ) .(+) ( N ` { X } ) ) )
84 48 83 eqeltrrd
 |-  ( ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ ( G ` X ) =/= .0. ) /\ u e. V ) -> u e. ( ( K ` G ) .(+) ( N ` { X } ) ) )
85 20 84 eqelssd
 |-  ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ ( G ` X ) =/= .0. ) -> ( ( K ` G ) .(+) ( N ` { X } ) ) = V )