Metamath Proof Explorer

Theorem lspprabs

Description: Absorption of vector sum into span of pair. (Contributed by NM, 27-Apr-2015)

Ref Expression
Hypotheses lspprabs.v ${⊢}{V}={\mathrm{Base}}_{{W}}$
lspprabs.p
lspprabs.n ${⊢}{N}=\mathrm{LSpan}\left({W}\right)$
lspprabs.w ${⊢}{\phi }\to {W}\in \mathrm{LMod}$
lspprabs.x ${⊢}{\phi }\to {X}\in {V}$
lspprabs.y ${⊢}{\phi }\to {Y}\in {V}$
Assertion lspprabs

Proof

Step Hyp Ref Expression
1 lspprabs.v ${⊢}{V}={\mathrm{Base}}_{{W}}$
2 lspprabs.p
3 lspprabs.n ${⊢}{N}=\mathrm{LSpan}\left({W}\right)$
4 lspprabs.w ${⊢}{\phi }\to {W}\in \mathrm{LMod}$
5 lspprabs.x ${⊢}{\phi }\to {X}\in {V}$
6 lspprabs.y ${⊢}{\phi }\to {Y}\in {V}$
7 eqid ${⊢}\mathrm{LSubSp}\left({W}\right)=\mathrm{LSubSp}\left({W}\right)$
8 7 lsssssubg ${⊢}{W}\in \mathrm{LMod}\to \mathrm{LSubSp}\left({W}\right)\subseteq \mathrm{SubGrp}\left({W}\right)$
9 4 8 syl ${⊢}{\phi }\to \mathrm{LSubSp}\left({W}\right)\subseteq \mathrm{SubGrp}\left({W}\right)$
10 1 7 3 lspsncl ${⊢}\left({W}\in \mathrm{LMod}\wedge {X}\in {V}\right)\to {N}\left(\left\{{X}\right\}\right)\in \mathrm{LSubSp}\left({W}\right)$
11 4 5 10 syl2anc ${⊢}{\phi }\to {N}\left(\left\{{X}\right\}\right)\in \mathrm{LSubSp}\left({W}\right)$
12 9 11 sseldd ${⊢}{\phi }\to {N}\left(\left\{{X}\right\}\right)\in \mathrm{SubGrp}\left({W}\right)$
13 1 7 3 lspsncl ${⊢}\left({W}\in \mathrm{LMod}\wedge {Y}\in {V}\right)\to {N}\left(\left\{{Y}\right\}\right)\in \mathrm{LSubSp}\left({W}\right)$
14 4 6 13 syl2anc ${⊢}{\phi }\to {N}\left(\left\{{Y}\right\}\right)\in \mathrm{LSubSp}\left({W}\right)$
15 9 14 sseldd ${⊢}{\phi }\to {N}\left(\left\{{Y}\right\}\right)\in \mathrm{SubGrp}\left({W}\right)$
16 eqid ${⊢}\mathrm{LSSum}\left({W}\right)=\mathrm{LSSum}\left({W}\right)$
17 16 lsmub1 ${⊢}\left({N}\left(\left\{{X}\right\}\right)\in \mathrm{SubGrp}\left({W}\right)\wedge {N}\left(\left\{{Y}\right\}\right)\in \mathrm{SubGrp}\left({W}\right)\right)\to {N}\left(\left\{{X}\right\}\right)\subseteq {N}\left(\left\{{X}\right\}\right)\mathrm{LSSum}\left({W}\right){N}\left(\left\{{Y}\right\}\right)$
18 12 15 17 syl2anc ${⊢}{\phi }\to {N}\left(\left\{{X}\right\}\right)\subseteq {N}\left(\left\{{X}\right\}\right)\mathrm{LSSum}\left({W}\right){N}\left(\left\{{Y}\right\}\right)$
19 7 16 lsmcl ${⊢}\left({W}\in \mathrm{LMod}\wedge {N}\left(\left\{{X}\right\}\right)\in \mathrm{LSubSp}\left({W}\right)\wedge {N}\left(\left\{{Y}\right\}\right)\in \mathrm{LSubSp}\left({W}\right)\right)\to {N}\left(\left\{{X}\right\}\right)\mathrm{LSSum}\left({W}\right){N}\left(\left\{{Y}\right\}\right)\in \mathrm{LSubSp}\left({W}\right)$
20 4 11 14 19 syl3anc ${⊢}{\phi }\to {N}\left(\left\{{X}\right\}\right)\mathrm{LSSum}\left({W}\right){N}\left(\left\{{Y}\right\}\right)\in \mathrm{LSubSp}\left({W}\right)$
21 1 3 lspsnid ${⊢}\left({W}\in \mathrm{LMod}\wedge {X}\in {V}\right)\to {X}\in {N}\left(\left\{{X}\right\}\right)$
22 4 5 21 syl2anc ${⊢}{\phi }\to {X}\in {N}\left(\left\{{X}\right\}\right)$
23 1 3 lspsnid ${⊢}\left({W}\in \mathrm{LMod}\wedge {Y}\in {V}\right)\to {Y}\in {N}\left(\left\{{Y}\right\}\right)$
24 4 6 23 syl2anc ${⊢}{\phi }\to {Y}\in {N}\left(\left\{{Y}\right\}\right)$
25 2 16 lsmelvali
26 12 15 22 24 25 syl22anc
27 7 3 4 20 26 lspsnel5a
28 1 2 lmodvacl
29 4 5 6 28 syl3anc
30 1 7 3 lspsncl
31 4 29 30 syl2anc
32 9 31 sseldd
33 9 20 sseldd ${⊢}{\phi }\to {N}\left(\left\{{X}\right\}\right)\mathrm{LSSum}\left({W}\right){N}\left(\left\{{Y}\right\}\right)\in \mathrm{SubGrp}\left({W}\right)$
34 16 lsmlub
35 12 32 33 34 syl3anc
36 18 27 35 mpbi2and
37 16 lsmub1
38 12 32 37 syl2anc
39 7 16 lsmcl
40 4 11 31 39 syl3anc
41 eqid ${⊢}{-}_{{W}}={-}_{{W}}$
42 1 3 lspsnid
43 4 29 42 syl2anc
44 41 16 32 12 43 22 lsmelvalmi
45 lmodabl ${⊢}{W}\in \mathrm{LMod}\to {W}\in \mathrm{Abel}$
46 4 45 syl ${⊢}{\phi }\to {W}\in \mathrm{Abel}$
47 1 2 41 ablpncan2
48 46 5 6 47 syl3anc
49 16 lsmcom
50 46 32 12 49 syl3anc
51 44 48 50 3eltr3d
52 7 3 4 40 51 lspsnel5a
53 9 40 sseldd
54 16 lsmlub
55 12 15 53 54 syl3anc
56 38 52 55 mpbi2and
57 36 56 eqssd
58 1 3 16 4 5 29 lsmpr
59 1 3 16 4 5 6 lsmpr ${⊢}{\phi }\to {N}\left(\left\{{X},{Y}\right\}\right)={N}\left(\left\{{X}\right\}\right)\mathrm{LSSum}\left({W}\right){N}\left(\left\{{Y}\right\}\right)$
60 57 58 59 3eqtr4d