# Metamath Proof Explorer

## Theorem lspindpi

Description: Partial independence property. (Contributed by NM, 23-Apr-2015)

Ref Expression
Hypotheses lspindpi.v ${⊢}{V}={\mathrm{Base}}_{{W}}$
lspindpi.n ${⊢}{N}=\mathrm{LSpan}\left({W}\right)$
lspindpi.w ${⊢}{\phi }\to {W}\in \mathrm{LVec}$
lspindpi.x ${⊢}{\phi }\to {X}\in {V}$
lspindpi.y ${⊢}{\phi }\to {Y}\in {V}$
lspindpi.z ${⊢}{\phi }\to {Z}\in {V}$
lspindpi.e ${⊢}{\phi }\to ¬{X}\in {N}\left(\left\{{Y},{Z}\right\}\right)$
Assertion lspindpi ${⊢}{\phi }\to \left({N}\left(\left\{{X}\right\}\right)\ne {N}\left(\left\{{Y}\right\}\right)\wedge {N}\left(\left\{{X}\right\}\right)\ne {N}\left(\left\{{Z}\right\}\right)\right)$

### Proof

Step Hyp Ref Expression
1 lspindpi.v ${⊢}{V}={\mathrm{Base}}_{{W}}$
2 lspindpi.n ${⊢}{N}=\mathrm{LSpan}\left({W}\right)$
3 lspindpi.w ${⊢}{\phi }\to {W}\in \mathrm{LVec}$
4 lspindpi.x ${⊢}{\phi }\to {X}\in {V}$
5 lspindpi.y ${⊢}{\phi }\to {Y}\in {V}$
6 lspindpi.z ${⊢}{\phi }\to {Z}\in {V}$
7 lspindpi.e ${⊢}{\phi }\to ¬{X}\in {N}\left(\left\{{Y},{Z}\right\}\right)$
8 lveclmod ${⊢}{W}\in \mathrm{LVec}\to {W}\in \mathrm{LMod}$
9 3 8 syl ${⊢}{\phi }\to {W}\in \mathrm{LMod}$
10 eqid ${⊢}\mathrm{LSubSp}\left({W}\right)=\mathrm{LSubSp}\left({W}\right)$
11 10 lsssssubg ${⊢}{W}\in \mathrm{LMod}\to \mathrm{LSubSp}\left({W}\right)\subseteq \mathrm{SubGrp}\left({W}\right)$
12 9 11 syl ${⊢}{\phi }\to \mathrm{LSubSp}\left({W}\right)\subseteq \mathrm{SubGrp}\left({W}\right)$
13 1 10 2 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 9 5 13 syl2anc ${⊢}{\phi }\to {N}\left(\left\{{Y}\right\}\right)\in \mathrm{LSubSp}\left({W}\right)$
15 12 14 sseldd ${⊢}{\phi }\to {N}\left(\left\{{Y}\right\}\right)\in \mathrm{SubGrp}\left({W}\right)$
16 1 10 2 lspsncl ${⊢}\left({W}\in \mathrm{LMod}\wedge {Z}\in {V}\right)\to {N}\left(\left\{{Z}\right\}\right)\in \mathrm{LSubSp}\left({W}\right)$
17 9 6 16 syl2anc ${⊢}{\phi }\to {N}\left(\left\{{Z}\right\}\right)\in \mathrm{LSubSp}\left({W}\right)$
18 12 17 sseldd ${⊢}{\phi }\to {N}\left(\left\{{Z}\right\}\right)\in \mathrm{SubGrp}\left({W}\right)$
19 eqid ${⊢}\mathrm{LSSum}\left({W}\right)=\mathrm{LSSum}\left({W}\right)$
20 19 lsmub1 ${⊢}\left({N}\left(\left\{{Y}\right\}\right)\in \mathrm{SubGrp}\left({W}\right)\wedge {N}\left(\left\{{Z}\right\}\right)\in \mathrm{SubGrp}\left({W}\right)\right)\to {N}\left(\left\{{Y}\right\}\right)\subseteq {N}\left(\left\{{Y}\right\}\right)\mathrm{LSSum}\left({W}\right){N}\left(\left\{{Z}\right\}\right)$
21 15 18 20 syl2anc ${⊢}{\phi }\to {N}\left(\left\{{Y}\right\}\right)\subseteq {N}\left(\left\{{Y}\right\}\right)\mathrm{LSSum}\left({W}\right){N}\left(\left\{{Z}\right\}\right)$
22 1 2 19 9 5 6 lsmpr ${⊢}{\phi }\to {N}\left(\left\{{Y},{Z}\right\}\right)={N}\left(\left\{{Y}\right\}\right)\mathrm{LSSum}\left({W}\right){N}\left(\left\{{Z}\right\}\right)$
23 21 22 sseqtrrd ${⊢}{\phi }\to {N}\left(\left\{{Y}\right\}\right)\subseteq {N}\left(\left\{{Y},{Z}\right\}\right)$
24 sseq1 ${⊢}{N}\left(\left\{{X}\right\}\right)={N}\left(\left\{{Y}\right\}\right)\to \left({N}\left(\left\{{X}\right\}\right)\subseteq {N}\left(\left\{{Y},{Z}\right\}\right)↔{N}\left(\left\{{Y}\right\}\right)\subseteq {N}\left(\left\{{Y},{Z}\right\}\right)\right)$
25 23 24 syl5ibrcom ${⊢}{\phi }\to \left({N}\left(\left\{{X}\right\}\right)={N}\left(\left\{{Y}\right\}\right)\to {N}\left(\left\{{X}\right\}\right)\subseteq {N}\left(\left\{{Y},{Z}\right\}\right)\right)$
26 1 10 2 9 5 6 lspprcl ${⊢}{\phi }\to {N}\left(\left\{{Y},{Z}\right\}\right)\in \mathrm{LSubSp}\left({W}\right)$
27 1 10 2 9 26 4 lspsnel5 ${⊢}{\phi }\to \left({X}\in {N}\left(\left\{{Y},{Z}\right\}\right)↔{N}\left(\left\{{X}\right\}\right)\subseteq {N}\left(\left\{{Y},{Z}\right\}\right)\right)$
28 25 27 sylibrd ${⊢}{\phi }\to \left({N}\left(\left\{{X}\right\}\right)={N}\left(\left\{{Y}\right\}\right)\to {X}\in {N}\left(\left\{{Y},{Z}\right\}\right)\right)$
29 28 necon3bd ${⊢}{\phi }\to \left(¬{X}\in {N}\left(\left\{{Y},{Z}\right\}\right)\to {N}\left(\left\{{X}\right\}\right)\ne {N}\left(\left\{{Y}\right\}\right)\right)$
30 7 29 mpd ${⊢}{\phi }\to {N}\left(\left\{{X}\right\}\right)\ne {N}\left(\left\{{Y}\right\}\right)$
31 19 lsmub2 ${⊢}\left({N}\left(\left\{{Y}\right\}\right)\in \mathrm{SubGrp}\left({W}\right)\wedge {N}\left(\left\{{Z}\right\}\right)\in \mathrm{SubGrp}\left({W}\right)\right)\to {N}\left(\left\{{Z}\right\}\right)\subseteq {N}\left(\left\{{Y}\right\}\right)\mathrm{LSSum}\left({W}\right){N}\left(\left\{{Z}\right\}\right)$
32 15 18 31 syl2anc ${⊢}{\phi }\to {N}\left(\left\{{Z}\right\}\right)\subseteq {N}\left(\left\{{Y}\right\}\right)\mathrm{LSSum}\left({W}\right){N}\left(\left\{{Z}\right\}\right)$
33 32 22 sseqtrrd ${⊢}{\phi }\to {N}\left(\left\{{Z}\right\}\right)\subseteq {N}\left(\left\{{Y},{Z}\right\}\right)$
34 sseq1 ${⊢}{N}\left(\left\{{X}\right\}\right)={N}\left(\left\{{Z}\right\}\right)\to \left({N}\left(\left\{{X}\right\}\right)\subseteq {N}\left(\left\{{Y},{Z}\right\}\right)↔{N}\left(\left\{{Z}\right\}\right)\subseteq {N}\left(\left\{{Y},{Z}\right\}\right)\right)$
35 33 34 syl5ibrcom ${⊢}{\phi }\to \left({N}\left(\left\{{X}\right\}\right)={N}\left(\left\{{Z}\right\}\right)\to {N}\left(\left\{{X}\right\}\right)\subseteq {N}\left(\left\{{Y},{Z}\right\}\right)\right)$
36 35 27 sylibrd ${⊢}{\phi }\to \left({N}\left(\left\{{X}\right\}\right)={N}\left(\left\{{Z}\right\}\right)\to {X}\in {N}\left(\left\{{Y},{Z}\right\}\right)\right)$
37 36 necon3bd ${⊢}{\phi }\to \left(¬{X}\in {N}\left(\left\{{Y},{Z}\right\}\right)\to {N}\left(\left\{{X}\right\}\right)\ne {N}\left(\left\{{Z}\right\}\right)\right)$
38 7 37 mpd ${⊢}{\phi }\to {N}\left(\left\{{X}\right\}\right)\ne {N}\left(\left\{{Z}\right\}\right)$
39 30 38 jca ${⊢}{\phi }\to \left({N}\left(\left\{{X}\right\}\right)\ne {N}\left(\left\{{Y}\right\}\right)\wedge {N}\left(\left\{{X}\right\}\right)\ne {N}\left(\left\{{Z}\right\}\right)\right)$