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 LVec X V G F ¬ X 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 LVec X V G F G X = 0 Scalar W X V
7 simp3 W LVec X V G F G X = 0 Scalar W G X = 0 Scalar W
8 simp1 W LVec X V G F G X = 0 Scalar W W LVec
9 simp2r W LVec X V G F G X = 0 Scalar W G F
10 eqid Scalar W = Scalar W
11 eqid 0 Scalar W = 0 Scalar W
12 1 10 11 4 5 ellkr W LVec G F X K G X V G X = 0 Scalar W
13 8 9 12 syl2anc W LVec X V G F G X = 0 Scalar W X K G X V G X = 0 Scalar W
14 6 7 13 mpbir2and W LVec X V G F G X = 0 Scalar W X K G
15 14 3expia W LVec X V G F G X = 0 Scalar W X K G
16 15 necon3bd W LVec X V G F ¬ X K G G X 0 Scalar W
17 16 3impia W LVec X V G F ¬ X K G G X 0 Scalar W
18 10 11 1 2 3 4 5 lkrlsp W LVec X V G F G X 0 Scalar W K G ˙ N X = V
19 17 18 syld3an3 W LVec X V G F ¬ X K G K G ˙ N X = V