lsatfixedN

Description: Show equality with the span of the sum of two vectors, one of which ( X ) is fixed in advance. Compare lspfixed . (Contributed by NM, 29-May-2015) (New usage is discouraged.)

	Ref	Expression
Hypotheses	lsatfixed.v	$⊢ V = {Base}_{W}$
	lsatfixed.p	$⊢ \underset{˙}{+} = +_{W}$
	lsatfixed.o	$⊢ \underset{˙}{0} = 0_{W}$
	lsatfixed.n	$⊢ N = LSpan (W)$
	lsatfixed.a	$⊢ A = LSAtoms (W)$
	lsatfixed.w	$⊢ φ \to W \in LVec$
	lsatfixed.q	$⊢ φ \to Q \in A$
	lsatfixed.x	$⊢ φ \to X \in V$
	lsatfixed.y	$⊢ φ \to Y \in V$
	lsatfixed.e	$⊢ φ \to Q \neq N (\{X\})$
	lsatfixed.f	$⊢ φ \to Q \neq N (\{Y\})$
	lsatfixed.g	$⊢ φ \to Q \subseteq N (\{X, Y\})$
Assertion	lsatfixedN	$⊢ φ \to \exists z \in (N (\{Y\}) ∖ \{\underset{˙}{0}\}) Q = N (\{X \underset{˙}{+} z\})$

Proof

Step	Hyp	Ref	Expression
1		lsatfixed.v	$⊢ V = {Base}_{W}$
2		lsatfixed.p	$⊢ \underset{˙}{+} = +_{W}$
3		lsatfixed.o	$⊢ \underset{˙}{0} = 0_{W}$
4		lsatfixed.n	$⊢ N = LSpan (W)$
5		lsatfixed.a	$⊢ A = LSAtoms (W)$
6		lsatfixed.w	$⊢ φ \to W \in LVec$
7		lsatfixed.q	$⊢ φ \to Q \in A$
8		lsatfixed.x	$⊢ φ \to X \in V$
9		lsatfixed.y	$⊢ φ \to Y \in V$
10		lsatfixed.e	$⊢ φ \to Q \neq N (\{X\})$
11		lsatfixed.f	$⊢ φ \to Q \neq N (\{Y\})$
12		lsatfixed.g	$⊢ φ \to Q \subseteq N (\{X, Y\})$
13	1 4 3 5	islsat	$⊢ W \in LVec \to (Q \in A \leftrightarrow \exists w \in (V ∖ \{\underset{˙}{0}\}) Q = N (\{w\}))$
14	6 13	syl	$⊢ φ \to (Q \in A \leftrightarrow \exists w \in (V ∖ \{\underset{˙}{0}\}) Q = N (\{w\}))$
15	7 14	mpbid	$⊢ φ \to \exists w \in (V ∖ \{\underset{˙}{0}\}) Q = N (\{w\})$
16	6	3ad2ant1	$⊢ (φ \land w \in (V ∖ \{\underset{˙}{0}\}) \land Q = N (\{w\})) \to W \in LVec$
17	8	3ad2ant1	$⊢ (φ \land w \in (V ∖ \{\underset{˙}{0}\}) \land Q = N (\{w\})) \to X \in V$
18	9	3ad2ant1	$⊢ (φ \land w \in (V ∖ \{\underset{˙}{0}\}) \land Q = N (\{w\})) \to Y \in V$
19		simp2	$⊢ (φ \land w \in (V ∖ \{\underset{˙}{0}\}) \land Q = N (\{w\})) \to w \in (V ∖ \{\underset{˙}{0}\})$
20		simp3	$⊢ (φ \land w \in (V ∖ \{\underset{˙}{0}\}) \land Q = N (\{w\})) \to Q = N (\{w\})$
21	20	eqcomd	$⊢ (φ \land w \in (V ∖ \{\underset{˙}{0}\}) \land Q = N (\{w\})) \to N (\{w\}) = Q$
22	10	3ad2ant1	$⊢ (φ \land w \in (V ∖ \{\underset{˙}{0}\}) \land Q = N (\{w\})) \to Q \neq N (\{X\})$
23	21 22	eqnetrd	$⊢ (φ \land w \in (V ∖ \{\underset{˙}{0}\}) \land Q = N (\{w\})) \to N (\{w\}) \neq N (\{X\})$
24	1 3 4 16 19 17 23	lspsnne1	$⊢ (φ \land w \in (V ∖ \{\underset{˙}{0}\}) \land Q = N (\{w\})) \to \neg w \in N (\{X\})$
25	11	3ad2ant1	$⊢ (φ \land w \in (V ∖ \{\underset{˙}{0}\}) \land Q = N (\{w\})) \to Q \neq N (\{Y\})$
26	21 25	eqnetrd	$⊢ (φ \land w \in (V ∖ \{\underset{˙}{0}\}) \land Q = N (\{w\})) \to N (\{w\}) \neq N (\{Y\})$
27	1 3 4 16 19 18 26	lspsnne1	$⊢ (φ \land w \in (V ∖ \{\underset{˙}{0}\}) \land Q = N (\{w\})) \to \neg w \in N (\{Y\})$
28	12	3ad2ant1	$⊢ (φ \land w \in (V ∖ \{\underset{˙}{0}\}) \land Q = N (\{w\})) \to Q \subseteq N (\{X, Y\})$
29	21 28	eqsstrd	$⊢ (φ \land w \in (V ∖ \{\underset{˙}{0}\}) \land Q = N (\{w\})) \to N (\{w\}) \subseteq N (\{X, Y\})$
30		eqid	$⊢ LSubSp (W) = LSubSp (W)$
31		lveclmod	$⊢ W \in LVec \to W \in LMod$
32	6 31	syl	$⊢ φ \to W \in LMod$
33	32	3ad2ant1	$⊢ (φ \land w \in (V ∖ \{\underset{˙}{0}\}) \land Q = N (\{w\})) \to W \in LMod$
34	1 30 4 32 8 9	lspprcl	$⊢ φ \to N (\{X, Y\}) \in LSubSp (W)$
35	34	3ad2ant1	$⊢ (φ \land w \in (V ∖ \{\underset{˙}{0}\}) \land Q = N (\{w\})) \to N (\{X, Y\}) \in LSubSp (W)$
36	19	eldifad	$⊢ (φ \land w \in (V ∖ \{\underset{˙}{0}\}) \land Q = N (\{w\})) \to w \in V$
37	1 30 4 33 35 36	lspsnel5	$⊢ (φ \land w \in (V ∖ \{\underset{˙}{0}\}) \land Q = N (\{w\})) \to (w \in N (\{X, Y\}) \leftrightarrow N (\{w\}) \subseteq N (\{X, Y\}))$
38	29 37	mpbird	$⊢ (φ \land w \in (V ∖ \{\underset{˙}{0}\}) \land Q = N (\{w\})) \to w \in N (\{X, Y\})$
39	1 2 3 4 16 17 18 24 27 38	lspfixed	$⊢ (φ \land w \in (V ∖ \{\underset{˙}{0}\}) \land Q = N (\{w\})) \to \exists z \in (N (\{Y\}) ∖ \{\underset{˙}{0}\}) w \in N (\{X \underset{˙}{+} z\})$
40		simpl1	$⊢ ((φ \land w \in (V ∖ \{\underset{˙}{0}\}) \land Q = N (\{w\})) \land z \in (N (\{Y\}) ∖ \{\underset{˙}{0}\})) \to φ$
41	40 6	syl	$⊢ ((φ \land w \in (V ∖ \{\underset{˙}{0}\}) \land Q = N (\{w\})) \land z \in (N (\{Y\}) ∖ \{\underset{˙}{0}\})) \to W \in LVec$
42		simpl2	$⊢ ((φ \land w \in (V ∖ \{\underset{˙}{0}\}) \land Q = N (\{w\})) \land z \in (N (\{Y\}) ∖ \{\underset{˙}{0}\})) \to w \in (V ∖ \{\underset{˙}{0}\})$
43	40 32	syl	$⊢ ((φ \land w \in (V ∖ \{\underset{˙}{0}\}) \land Q = N (\{w\})) \land z \in (N (\{Y\}) ∖ \{\underset{˙}{0}\})) \to W \in LMod$
44	40 8	syl	$⊢ ((φ \land w \in (V ∖ \{\underset{˙}{0}\}) \land Q = N (\{w\})) \land z \in (N (\{Y\}) ∖ \{\underset{˙}{0}\})) \to X \in V$
45	9	snssd	$⊢ φ \to \{Y\} \subseteq V$
46	1 4	lspssv	$⊢ (W \in LMod \land \{Y\} \subseteq V) \to N (\{Y\}) \subseteq V$
47	32 45 46	syl2anc	$⊢ φ \to N (\{Y\}) \subseteq V$
48	47	ssdifssd	$⊢ φ \to N (\{Y\}) ∖ \{\underset{˙}{0}\} \subseteq V$
49	48	3ad2ant1	$⊢ (φ \land w \in (V ∖ \{\underset{˙}{0}\}) \land Q = N (\{w\})) \to N (\{Y\}) ∖ \{\underset{˙}{0}\} \subseteq V$
50	49	sselda	$⊢ ((φ \land w \in (V ∖ \{\underset{˙}{0}\}) \land Q = N (\{w\})) \land z \in (N (\{Y\}) ∖ \{\underset{˙}{0}\})) \to z \in V$
51	1 2	lmodvacl	$⊢ (W \in LMod \land X \in V \land z \in V) \to X \underset{˙}{+} z \in V$
52	43 44 50 51	syl3anc	$⊢ ((φ \land w \in (V ∖ \{\underset{˙}{0}\}) \land Q = N (\{w\})) \land z \in (N (\{Y\}) ∖ \{\underset{˙}{0}\})) \to X \underset{˙}{+} z \in V$
53	1 3 4 41 42 52	lspsncmp	$⊢ ((φ \land w \in (V ∖ \{\underset{˙}{0}\}) \land Q = N (\{w\})) \land z \in (N (\{Y\}) ∖ \{\underset{˙}{0}\})) \to (N (\{w\}) \subseteq N (\{X \underset{˙}{+} z\}) \leftrightarrow N (\{w\}) = N (\{X \underset{˙}{+} z\}))$
54	1 30 4	lspsncl	$⊢ (W \in LMod \land X \underset{˙}{+} z \in V) \to N (\{X \underset{˙}{+} z\}) \in LSubSp (W)$
55	43 52 54	syl2anc	$⊢ ((φ \land w \in (V ∖ \{\underset{˙}{0}\}) \land Q = N (\{w\})) \land z \in (N (\{Y\}) ∖ \{\underset{˙}{0}\})) \to N (\{X \underset{˙}{+} z\}) \in LSubSp (W)$
56	42	eldifad	$⊢ ((φ \land w \in (V ∖ \{\underset{˙}{0}\}) \land Q = N (\{w\})) \land z \in (N (\{Y\}) ∖ \{\underset{˙}{0}\})) \to w \in V$
57	1 30 4 43 55 56	lspsnel5	$⊢ ((φ \land w \in (V ∖ \{\underset{˙}{0}\}) \land Q = N (\{w\})) \land z \in (N (\{Y\}) ∖ \{\underset{˙}{0}\})) \to (w \in N (\{X \underset{˙}{+} z\}) \leftrightarrow N (\{w\}) \subseteq N (\{X \underset{˙}{+} z\}))$
58		simpl3	$⊢ ((φ \land w \in (V ∖ \{\underset{˙}{0}\}) \land Q = N (\{w\})) \land z \in (N (\{Y\}) ∖ \{\underset{˙}{0}\})) \to Q = N (\{w\})$
59	58	eqeq1d	$⊢ ((φ \land w \in (V ∖ \{\underset{˙}{0}\}) \land Q = N (\{w\})) \land z \in (N (\{Y\}) ∖ \{\underset{˙}{0}\})) \to (Q = N (\{X \underset{˙}{+} z\}) \leftrightarrow N (\{w\}) = N (\{X \underset{˙}{+} z\}))$
60	53 57 59	3bitr4rd	$⊢ ((φ \land w \in (V ∖ \{\underset{˙}{0}\}) \land Q = N (\{w\})) \land z \in (N (\{Y\}) ∖ \{\underset{˙}{0}\})) \to (Q = N (\{X \underset{˙}{+} z\}) \leftrightarrow w \in N (\{X \underset{˙}{+} z\}))$
61	60	rexbidva	$⊢ (φ \land w \in (V ∖ \{\underset{˙}{0}\}) \land Q = N (\{w\})) \to (\exists z \in (N (\{Y\}) ∖ \{\underset{˙}{0}\}) Q = N (\{X \underset{˙}{+} z\}) \leftrightarrow \exists z \in (N (\{Y\}) ∖ \{\underset{˙}{0}\}) w \in N (\{X \underset{˙}{+} z\}))$
62	39 61	mpbird	$⊢ (φ \land w \in (V ∖ \{\underset{˙}{0}\}) \land Q = N (\{w\})) \to \exists z \in (N (\{Y\}) ∖ \{\underset{˙}{0}\}) Q = N (\{X \underset{˙}{+} z\})$
63	62	rexlimdv3a	$⊢ φ \to (\exists w \in (V ∖ \{\underset{˙}{0}\}) Q = N (\{w\}) \to \exists z \in (N (\{Y\}) ∖ \{\underset{˙}{0}\}) Q = N (\{X \underset{˙}{+} z\}))$
64	15 63	mpd	$⊢ φ \to \exists z \in (N (\{Y\}) ∖ \{\underset{˙}{0}\}) Q = N (\{X \underset{˙}{+} z\})$

Metamath Proof Explorer

Theorem lsatfixedN

Proof