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