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