lspindpi

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

	Ref	Expression
Hypotheses	lspindpi.v	$⊢ V = {Base}_{W}$
	lspindpi.n	$⊢ N = LSpan (W)$
	lspindpi.w	$⊢ φ \to W \in LVec$
	lspindpi.x	$⊢ φ \to X \in V$
	lspindpi.y	$⊢ φ \to Y \in V$
	lspindpi.z	$⊢ φ \to Z \in V$
	lspindpi.e	$⊢ φ \to \neg X \in N (\{Y, Z\})$
Assertion	lspindpi	$⊢ φ \to (N (\{X\}) \neq N (\{Y\}) \land N (\{X\}) \neq N (\{Z\}))$

Proof

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

Metamath Proof Explorer

Theorem lspindpi

Proof