# Metamath Proof Explorer

## Theorem lsmcv

Description: Subspace sum has the covering property (using spans of singletons to represent atoms). Similar to Exercise 5 of Kalmbach p. 153. ( spansncvi analog.) TODO: ugly proof; can it be shortened? (Contributed by NM, 2-Oct-2014)

Ref Expression
Hypotheses lsmcv.v ${⊢}{V}={\mathrm{Base}}_{{W}}$
lsmcv.s ${⊢}{S}=\mathrm{LSubSp}\left({W}\right)$
lsmcv.n ${⊢}{N}=\mathrm{LSpan}\left({W}\right)$
lsmcv.p
lsmcv.w ${⊢}{\phi }\to {W}\in \mathrm{LVec}$
lsmcv.t ${⊢}{\phi }\to {T}\in {S}$
lsmcv.u ${⊢}{\phi }\to {U}\in {S}$
lsmcv.x ${⊢}{\phi }\to {X}\in {V}$
Assertion lsmcv

### Proof

Step Hyp Ref Expression
1 lsmcv.v ${⊢}{V}={\mathrm{Base}}_{{W}}$
2 lsmcv.s ${⊢}{S}=\mathrm{LSubSp}\left({W}\right)$
3 lsmcv.n ${⊢}{N}=\mathrm{LSpan}\left({W}\right)$
4 lsmcv.p
5 lsmcv.w ${⊢}{\phi }\to {W}\in \mathrm{LVec}$
6 lsmcv.t ${⊢}{\phi }\to {T}\in {S}$
7 lsmcv.u ${⊢}{\phi }\to {U}\in {S}$
8 lsmcv.x ${⊢}{\phi }\to {X}\in {V}$
9 simp3
10 simp2
11 pssss ${⊢}{T}\subset {U}\to {T}\subseteq {U}$
12 10 11 syl
13 pssnel ${⊢}{T}\subset {U}\to \exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {U}\wedge ¬{x}\in {T}\right)$
14 10 13 syl
15 simpl3
16 simprl
17 15 16 sseldd
18 lveclmod ${⊢}{W}\in \mathrm{LVec}\to {W}\in \mathrm{LMod}$
19 5 18 syl ${⊢}{\phi }\to {W}\in \mathrm{LMod}$
20 2 lsssssubg ${⊢}{W}\in \mathrm{LMod}\to {S}\subseteq \mathrm{SubGrp}\left({W}\right)$
21 19 20 syl ${⊢}{\phi }\to {S}\subseteq \mathrm{SubGrp}\left({W}\right)$
22 21 6 sseldd ${⊢}{\phi }\to {T}\in \mathrm{SubGrp}\left({W}\right)$
23 1 2 3 lspsncl ${⊢}\left({W}\in \mathrm{LMod}\wedge {X}\in {V}\right)\to {N}\left(\left\{{X}\right\}\right)\in {S}$
24 19 8 23 syl2anc ${⊢}{\phi }\to {N}\left(\left\{{X}\right\}\right)\in {S}$
25 21 24 sseldd ${⊢}{\phi }\to {N}\left(\left\{{X}\right\}\right)\in \mathrm{SubGrp}\left({W}\right)$
26 eqid ${⊢}{+}_{{W}}={+}_{{W}}$
27 26 4 lsmelval
28 22 25 27 syl2anc
31 17 30 mpbid
32 simp1rr
33 simp2l
34 oveq2 ${⊢}{z}={0}_{{W}}\to {y}{+}_{{W}}{z}={y}{+}_{{W}}{0}_{{W}}$
35 34 eqeq2d ${⊢}{z}={0}_{{W}}\to \left({x}={y}{+}_{{W}}{z}↔{x}={y}{+}_{{W}}{0}_{{W}}\right)$
36 35 biimpac ${⊢}\left({x}={y}{+}_{{W}}{z}\wedge {z}={0}_{{W}}\right)\to {x}={y}{+}_{{W}}{0}_{{W}}$
41 simprl
42 1 2 lssel ${⊢}\left({T}\in {S}\wedge {y}\in {T}\right)\to {y}\in {V}$
43 40 41 42 syl2anc
44 eqid ${⊢}{0}_{{W}}={0}_{{W}}$
45 1 26 44 lmod0vrid ${⊢}\left({W}\in \mathrm{LMod}\wedge {y}\in {V}\right)\to {y}{+}_{{W}}{0}_{{W}}={y}$
46 38 43 45 syl2anc
47 46 eqeq2d
48 47 biimpd
49 48 ex
50 36 49 syl7
51 50 exp4a
52 51 3imp
53 eleq1 ${⊢}{x}={y}\to \left({x}\in {T}↔{y}\in {T}\right)$
54 53 biimparc ${⊢}\left({y}\in {T}\wedge {x}={y}\right)\to {x}\in {T}$
55 33 52 54 syl6an
56 55 necon3bd
57 32 56 mpd
61 lmodabl ${⊢}{W}\in \mathrm{LMod}\to {W}\in \mathrm{Abel}$
62 18 61 syl ${⊢}{W}\in \mathrm{LVec}\to {W}\in \mathrm{Abel}$
63 60 62 syl
64 simp1l1
65 64 6 syl
66 65 33 42 syl2anc
67 60 18 syl
68 64 8 syl
69 67 68 23 syl2anc
70 simp2r
71 1 2 lssel ${⊢}\left({N}\left(\left\{{X}\right\}\right)\in {S}\wedge {z}\in {N}\left(\left\{{X}\right\}\right)\right)\to {z}\in {V}$
72 69 70 71 syl2anc
73 eqid ${⊢}{-}_{{W}}={-}_{{W}}$
74 1 26 73 ablpncan2 ${⊢}\left({W}\in \mathrm{Abel}\wedge {y}\in {V}\wedge {z}\in {V}\right)\to \left({y}{+}_{{W}}{z}\right){-}_{{W}}{y}={z}$
75 63 66 72 74 syl3anc
76 64 7 syl
77 simp3
78 simp1rl
79 77 78 eqeltrrd
80 simp1l2
81 11 sselda ${⊢}\left({T}\subset {U}\wedge {y}\in {T}\right)\to {y}\in {U}$
82 80 33 81 syl2anc
83 73 2 lssvsubcl ${⊢}\left(\left({W}\in \mathrm{LMod}\wedge {U}\in {S}\right)\wedge \left({y}{+}_{{W}}{z}\in {U}\wedge {y}\in {U}\right)\right)\to \left({y}{+}_{{W}}{z}\right){-}_{{W}}{y}\in {U}$
84 67 76 79 82 83 syl22anc
85 75 84 eqeltrrd
88 87 8 syl
89 simp12r
90 simp2
91 1 44 3 86 88 89 90 lspsneleq
92 86 18 syl
93 87 7 syl
94 simp3
95 2 3 92 93 94 lspsnel5a
96 91 95 eqsstrrd
97 57 85 96 mpd3an23
98 97 3exp
99 98 rexlimdvv
100 31 99 mpd
101 14 100 exlimddv
102 21 7 sseldd ${⊢}{\phi }\to {U}\in \mathrm{SubGrp}\left({W}\right)$
103 4 lsmlub
104 22 25 102 103 syl3anc