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

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 ellspsni 
 |-  ( ( ( 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 )