lspindp5

Description: Obtain an independent vector set U , X , Y from a vector U dependent on X and Z and another independent set Z , X , Y . (Here we don't show the ( N{ X } ) =/= ( N{ Y } ) part of the independence, which passes straight through. We also don't show nonzero vector requirements that are redundant for this theorem. Different orderings can be obtained using lspexch and prcom .) (Contributed by NM, 4-May-2015)

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

Proof

Step	Hyp	Ref	Expression
1		lspindp5.v	$⊢ V = {Base}_{W}$
2		lspindp5.n	$⊢ N = LSpan (W)$
3		lspindp5.w	$⊢ φ \to W \in LVec$
4		lspindp5.y	$⊢ φ \to X \in V$
5		lspindp5.x	$⊢ φ \to Y \in V$
6		lspindp5.u	$⊢ φ \to U \in V$
7		lspindp5.e	$⊢ φ \to Z \in N (\{X, U\})$
8		lspindp5.m	$⊢ φ \to \neg Z \in N (\{X, Y\})$
9		ssel	$⊢ N (\{X, U\}) \subseteq N (\{X, Y\}) \to (Z \in N (\{X, U\}) \to Z \in N (\{X, Y\}))$
10	7 9	syl5com	$⊢ φ \to (N (\{X, U\}) \subseteq N (\{X, Y\}) \to Z \in N (\{X, Y\}))$
11	8 10	mtod	$⊢ φ \to \neg N (\{X, U\}) \subseteq N (\{X, Y\})$
12		lveclmod	$⊢ W \in LVec \to W \in LMod$
13	3 12	syl	$⊢ φ \to W \in LMod$
14		prssi	$⊢ (X \in V \land Y \in V) \to \{X, Y\} \subseteq V$
15	4 5 14	syl2anc	$⊢ φ \to \{X, Y\} \subseteq V$
16		snsspr1	$⊢ \{X\} \subseteq \{X, Y\}$
17	16	a1i	$⊢ φ \to \{X\} \subseteq \{X, Y\}$
18	1 2	lspss	$⊢ (W \in LMod \land \{X, Y\} \subseteq V \land \{X\} \subseteq \{X, Y\}) \to N (\{X\}) \subseteq N (\{X, Y\})$
19	13 15 17 18	syl3anc	$⊢ φ \to N (\{X\}) \subseteq N (\{X, Y\})$
20	19	biantrurd	$⊢ φ \to (N (\{U\}) \subseteq N (\{X, Y\}) \leftrightarrow (N (\{X\}) \subseteq N (\{X, Y\}) \land N (\{U\}) \subseteq N (\{X, Y\})))$
21		eqid	$⊢ LSubSp (W) = LSubSp (W)$
22	21	lsssssubg	$⊢ W \in LMod \to LSubSp (W) \subseteq SubGrp (W)$
23	13 22	syl	$⊢ φ \to LSubSp (W) \subseteq SubGrp (W)$
24	1 21 2	lspsncl	$⊢ (W \in LMod \land X \in V) \to N (\{X\}) \in LSubSp (W)$
25	13 4 24	syl2anc	$⊢ φ \to N (\{X\}) \in LSubSp (W)$
26	23 25	sseldd	$⊢ φ \to N (\{X\}) \in SubGrp (W)$
27	1 21 2	lspsncl	$⊢ (W \in LMod \land U \in V) \to N (\{U\}) \in LSubSp (W)$
28	13 6 27	syl2anc	$⊢ φ \to N (\{U\}) \in LSubSp (W)$
29	23 28	sseldd	$⊢ φ \to N (\{U\}) \in SubGrp (W)$
30	1 21 2 13 4 5	lspprcl	$⊢ φ \to N (\{X, Y\}) \in LSubSp (W)$
31	23 30	sseldd	$⊢ φ \to N (\{X, Y\}) \in SubGrp (W)$
32		eqid	$⊢ LSSum (W) = LSSum (W)$
33	32	lsmlub	$⊢ (N (\{X\}) \in SubGrp (W) \land N (\{U\}) \in SubGrp (W) \land N (\{X, Y\}) \in SubGrp (W)) \to ((N (\{X\}) \subseteq N (\{X, Y\}) \land N (\{U\}) \subseteq N (\{X, Y\})) \leftrightarrow N (\{X\}) LSSum (W) N (\{U\}) \subseteq N (\{X, Y\}))$
34	26 29 31 33	syl3anc	$⊢ φ \to ((N (\{X\}) \subseteq N (\{X, Y\}) \land N (\{U\}) \subseteq N (\{X, Y\})) \leftrightarrow N (\{X\}) LSSum (W) N (\{U\}) \subseteq N (\{X, Y\}))$
35	20 34	bitrd	$⊢ φ \to (N (\{U\}) \subseteq N (\{X, Y\}) \leftrightarrow N (\{X\}) LSSum (W) N (\{U\}) \subseteq N (\{X, Y\}))$
36	1 21 2 13 30 6	ellspsn5b	$⊢ φ \to (U \in N (\{X, Y\}) \leftrightarrow N (\{U\}) \subseteq N (\{X, Y\}))$
37	1 2 32 13 4 6	lsmpr	$⊢ φ \to N (\{X, U\}) = N (\{X\}) LSSum (W) N (\{U\})$
38	37	sseq1d	$⊢ φ \to (N (\{X, U\}) \subseteq N (\{X, Y\}) \leftrightarrow N (\{X\}) LSSum (W) N (\{U\}) \subseteq N (\{X, Y\}))$
39	35 36 38	3bitr4d	$⊢ φ \to (U \in N (\{X, Y\}) \leftrightarrow N (\{X, U\}) \subseteq N (\{X, Y\}))$
40	11 39	mtbird	$⊢ φ \to \neg U \in N (\{X, Y\})$

Metamath Proof Explorer

Theorem lspindp5

Proof