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 ˙ = 0 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 ∈ LVec ∧ X ∈ V ∧ G ∈ F ∧ G ⁡ X ≠ 0 ˙ → K ⁡ G ⊕ ˙ N ⁡ X = V

Proof

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