lspfixed

Description: Show membership in the span of the sum of two vectors, one of which ( Y ) is fixed in advance. (Contributed by NM, 27-May-2015) (Revised by AV, 12-Jul-2022)

	Ref	Expression
Hypotheses	lspfixed.v	$⊢ V = {Base}_{W}$
	lspfixed.p	$⊢ \underset{˙}{+} = +_{W}$
	lspfixed.o	$⊢ \underset{˙}{0} = 0_{W}$
	lspfixed.n	$⊢ N = LSpan (W)$
	lspfixed.w	$⊢ φ \to W \in LVec$
	lspfixed.y	$⊢ φ \to Y \in V$
	lspfixed.z	$⊢ φ \to Z \in V$
	lspfixed.e	$⊢ φ \to \neg X \in N (\{Y\})$
	lspfixed.f	$⊢ φ \to \neg X \in N (\{Z\})$
	lspfixed.g	$⊢ φ \to X \in N (\{Y, Z\})$
Assertion	lspfixed	$⊢ φ \to \exists z \in (N (\{Z\}) ∖ \{\underset{˙}{0}\}) X \in N (\{Y \underset{˙}{+} z\})$

Proof

Step	Hyp	Ref	Expression
1		lspfixed.v	$⊢ V = {Base}_{W}$
2		lspfixed.p	$⊢ \underset{˙}{+} = +_{W}$
3		lspfixed.o	$⊢ \underset{˙}{0} = 0_{W}$
4		lspfixed.n	$⊢ N = LSpan (W)$
5		lspfixed.w	$⊢ φ \to W \in LVec$
6		lspfixed.y	$⊢ φ \to Y \in V$
7		lspfixed.z	$⊢ φ \to Z \in V$
8		lspfixed.e	$⊢ φ \to \neg X \in N (\{Y\})$
9		lspfixed.f	$⊢ φ \to \neg X \in N (\{Z\})$
10		lspfixed.g	$⊢ φ \to X \in N (\{Y, Z\})$
11		eqid	$⊢ Scalar (W) = Scalar (W)$
12		eqid	$⊢ {Base}_{Scalar (W)} = {Base}_{Scalar (W)}$
13		eqid	$⊢ \cdot_{W} = \cdot_{W}$
14		lveclmod	$⊢ W \in LVec \to W \in LMod$
15	5 14	syl	$⊢ φ \to W \in LMod$
16	1 2 11 12 13 4 15 6 7	lspprel	$⊢ φ \to (X \in N (\{Y, Z\}) \leftrightarrow \exists k \in {Base}_{Scalar (W)} \exists l \in {Base}_{Scalar (W)} X = (k \cdot_{W} Y) \underset{˙}{+} (l \cdot_{W} Z))$
17	10 16	mpbid	$⊢ φ \to \exists k \in {Base}_{Scalar (W)} \exists l \in {Base}_{Scalar (W)} X = (k \cdot_{W} Y) \underset{˙}{+} (l \cdot_{W} Z)$
18	15	3ad2ant1	$⊢ (φ \land (k \in {Base}_{Scalar (W)} \land l \in {Base}_{Scalar (W)}) \land X = (k \cdot_{W} Y) \underset{˙}{+} (l \cdot_{W} Z)) \to W \in LMod$
19		eqid	$⊢ LSubSp (W) = LSubSp (W)$
20	1 19 4	lspsncl	$⊢ (W \in LMod \land Z \in V) \to N (\{Z\}) \in LSubSp (W)$
21	15 7 20	syl2anc	$⊢ φ \to N (\{Z\}) \in LSubSp (W)$
22	21	3ad2ant1	$⊢ (φ \land (k \in {Base}_{Scalar (W)} \land l \in {Base}_{Scalar (W)}) \land X = (k \cdot_{W} Y) \underset{˙}{+} (l \cdot_{W} Z)) \to N (\{Z\}) \in LSubSp (W)$
23	5	3ad2ant1	$⊢ (φ \land (k \in {Base}_{Scalar (W)} \land l \in {Base}_{Scalar (W)}) \land X = (k \cdot_{W} Y) \underset{˙}{+} (l \cdot_{W} Z)) \to W \in LVec$
24	11	lvecdrng	$⊢ W \in LVec \to Scalar (W) \in DivRing$
25	23 24	syl	$⊢ (φ \land (k \in {Base}_{Scalar (W)} \land l \in {Base}_{Scalar (W)}) \land X = (k \cdot_{W} Y) \underset{˙}{+} (l \cdot_{W} Z)) \to Scalar (W) \in DivRing$
26		simp2l	$⊢ (φ \land (k \in {Base}_{Scalar (W)} \land l \in {Base}_{Scalar (W)}) \land X = (k \cdot_{W} Y) \underset{˙}{+} (l \cdot_{W} Z)) \to k \in {Base}_{Scalar (W)}$
27	9	3ad2ant1	$⊢ (φ \land (k \in {Base}_{Scalar (W)} \land l \in {Base}_{Scalar (W)}) \land X = (k \cdot_{W} Y) \underset{˙}{+} (l \cdot_{W} Z)) \to \neg X \in N (\{Z\})$
28		simpl3	$⊢ ((φ \land (k \in {Base}_{Scalar (W)} \land l \in {Base}_{Scalar (W)}) \land X = (k \cdot_{W} Y) \underset{˙}{+} (l \cdot_{W} Z)) \land k = 0_{Scalar (W)}) \to X = (k \cdot_{W} Y) \underset{˙}{+} (l \cdot_{W} Z)$
29		simpr	$⊢ ((φ \land (k \in {Base}_{Scalar (W)} \land l \in {Base}_{Scalar (W)}) \land X = (k \cdot_{W} Y) \underset{˙}{+} (l \cdot_{W} Z)) \land k = 0_{Scalar (W)}) \to k = 0_{Scalar (W)}$
30	29	oveq1d	$⊢ ((φ \land (k \in {Base}_{Scalar (W)} \land l \in {Base}_{Scalar (W)}) \land X = (k \cdot_{W} Y) \underset{˙}{+} (l \cdot_{W} Z)) \land k = 0_{Scalar (W)}) \to k \cdot_{W} Y = 0_{Scalar (W)} \cdot_{W} Y$
31		simpl1	$⊢ ((φ \land (k \in {Base}_{Scalar (W)} \land l \in {Base}_{Scalar (W)}) \land X = (k \cdot_{W} Y) \underset{˙}{+} (l \cdot_{W} Z)) \land k = 0_{Scalar (W)}) \to φ$
32	31 15	syl	$⊢ ((φ \land (k \in {Base}_{Scalar (W)} \land l \in {Base}_{Scalar (W)}) \land X = (k \cdot_{W} Y) \underset{˙}{+} (l \cdot_{W} Z)) \land k = 0_{Scalar (W)}) \to W \in LMod$
33	31 6	syl	$⊢ ((φ \land (k \in {Base}_{Scalar (W)} \land l \in {Base}_{Scalar (W)}) \land X = (k \cdot_{W} Y) \underset{˙}{+} (l \cdot_{W} Z)) \land k = 0_{Scalar (W)}) \to Y \in V$
34		eqid	$⊢ 0_{Scalar (W)} = 0_{Scalar (W)}$
35	1 11 13 34 3	lmod0vs	$⊢ (W \in LMod \land Y \in V) \to 0_{Scalar (W)} \cdot_{W} Y = \underset{˙}{0}$
36	32 33 35	syl2anc	$⊢ ((φ \land (k \in {Base}_{Scalar (W)} \land l \in {Base}_{Scalar (W)}) \land X = (k \cdot_{W} Y) \underset{˙}{+} (l \cdot_{W} Z)) \land k = 0_{Scalar (W)}) \to 0_{Scalar (W)} \cdot_{W} Y = \underset{˙}{0}$
37	30 36	eqtrd	$⊢ ((φ \land (k \in {Base}_{Scalar (W)} \land l \in {Base}_{Scalar (W)}) \land X = (k \cdot_{W} Y) \underset{˙}{+} (l \cdot_{W} Z)) \land k = 0_{Scalar (W)}) \to k \cdot_{W} Y = \underset{˙}{0}$
38	37	oveq1d	$⊢ ((φ \land (k \in {Base}_{Scalar (W)} \land l \in {Base}_{Scalar (W)}) \land X = (k \cdot_{W} Y) \underset{˙}{+} (l \cdot_{W} Z)) \land k = 0_{Scalar (W)}) \to (k \cdot_{W} Y) \underset{˙}{+} (l \cdot_{W} Z) = \underset{˙}{0} \underset{˙}{+} (l \cdot_{W} Z)$
39		simp2r	$⊢ (φ \land (k \in {Base}_{Scalar (W)} \land l \in {Base}_{Scalar (W)}) \land X = (k \cdot_{W} Y) \underset{˙}{+} (l \cdot_{W} Z)) \to l \in {Base}_{Scalar (W)}$
40	7	3ad2ant1	$⊢ (φ \land (k \in {Base}_{Scalar (W)} \land l \in {Base}_{Scalar (W)}) \land X = (k \cdot_{W} Y) \underset{˙}{+} (l \cdot_{W} Z)) \to Z \in V$
41	1 11 13 12	lmodvscl	$⊢ (W \in LMod \land l \in {Base}_{Scalar (W)} \land Z \in V) \to l \cdot_{W} Z \in V$
42	18 39 40 41	syl3anc	$⊢ (φ \land (k \in {Base}_{Scalar (W)} \land l \in {Base}_{Scalar (W)}) \land X = (k \cdot_{W} Y) \underset{˙}{+} (l \cdot_{W} Z)) \to l \cdot_{W} Z \in V$
43	42	adantr	$⊢ ((φ \land (k \in {Base}_{Scalar (W)} \land l \in {Base}_{Scalar (W)}) \land X = (k \cdot_{W} Y) \underset{˙}{+} (l \cdot_{W} Z)) \land k = 0_{Scalar (W)}) \to l \cdot_{W} Z \in V$
44	1 2 3	lmod0vlid	$⊢ (W \in LMod \land l \cdot_{W} Z \in V) \to \underset{˙}{0} \underset{˙}{+} (l \cdot_{W} Z) = l \cdot_{W} Z$
45	32 43 44	syl2anc	$⊢ ((φ \land (k \in {Base}_{Scalar (W)} \land l \in {Base}_{Scalar (W)}) \land X = (k \cdot_{W} Y) \underset{˙}{+} (l \cdot_{W} Z)) \land k = 0_{Scalar (W)}) \to \underset{˙}{0} \underset{˙}{+} (l \cdot_{W} Z) = l \cdot_{W} Z$
46	28 38 45	3eqtrd	$⊢ ((φ \land (k \in {Base}_{Scalar (W)} \land l \in {Base}_{Scalar (W)}) \land X = (k \cdot_{W} Y) \underset{˙}{+} (l \cdot_{W} Z)) \land k = 0_{Scalar (W)}) \to X = l \cdot_{W} Z$
47	31 21	syl	$⊢ ((φ \land (k \in {Base}_{Scalar (W)} \land l \in {Base}_{Scalar (W)}) \land X = (k \cdot_{W} Y) \underset{˙}{+} (l \cdot_{W} Z)) \land k = 0_{Scalar (W)}) \to N (\{Z\}) \in LSubSp (W)$
48		simpl2r	$⊢ ((φ \land (k \in {Base}_{Scalar (W)} \land l \in {Base}_{Scalar (W)}) \land X = (k \cdot_{W} Y) \underset{˙}{+} (l \cdot_{W} Z)) \land k = 0_{Scalar (W)}) \to l \in {Base}_{Scalar (W)}$
49	1 4	lspsnid	$⊢ (W \in LMod \land Z \in V) \to Z \in N (\{Z\})$
50	15 7 49	syl2anc	$⊢ φ \to Z \in N (\{Z\})$
51	31 50	syl	$⊢ ((φ \land (k \in {Base}_{Scalar (W)} \land l \in {Base}_{Scalar (W)}) \land X = (k \cdot_{W} Y) \underset{˙}{+} (l \cdot_{W} Z)) \land k = 0_{Scalar (W)}) \to Z \in N (\{Z\})$
52	11 13 12 19	lssvscl	$⊢ ((W \in LMod \land N (\{Z\}) \in LSubSp (W)) \land (l \in {Base}_{Scalar (W)} \land Z \in N (\{Z\}))) \to l \cdot_{W} Z \in N (\{Z\})$
53	32 47 48 51 52	syl22anc	$⊢ ((φ \land (k \in {Base}_{Scalar (W)} \land l \in {Base}_{Scalar (W)}) \land X = (k \cdot_{W} Y) \underset{˙}{+} (l \cdot_{W} Z)) \land k = 0_{Scalar (W)}) \to l \cdot_{W} Z \in N (\{Z\})$
54	46 53	eqeltrd	$⊢ ((φ \land (k \in {Base}_{Scalar (W)} \land l \in {Base}_{Scalar (W)}) \land X = (k \cdot_{W} Y) \underset{˙}{+} (l \cdot_{W} Z)) \land k = 0_{Scalar (W)}) \to X \in N (\{Z\})$
55	54	ex	$⊢ (φ \land (k \in {Base}_{Scalar (W)} \land l \in {Base}_{Scalar (W)}) \land X = (k \cdot_{W} Y) \underset{˙}{+} (l \cdot_{W} Z)) \to (k = 0_{Scalar (W)} \to X \in N (\{Z\}))$
56	55	necon3bd	$⊢ (φ \land (k \in {Base}_{Scalar (W)} \land l \in {Base}_{Scalar (W)}) \land X = (k \cdot_{W} Y) \underset{˙}{+} (l \cdot_{W} Z)) \to (\neg X \in N (\{Z\}) \to k \neq 0_{Scalar (W)})$
57	27 56	mpd	$⊢ (φ \land (k \in {Base}_{Scalar (W)} \land l \in {Base}_{Scalar (W)}) \land X = (k \cdot_{W} Y) \underset{˙}{+} (l \cdot_{W} Z)) \to k \neq 0_{Scalar (W)}$
58		eqid	$⊢ {inv}_{r} (Scalar (W)) = {inv}_{r} (Scalar (W))$
59	12 34 58	drnginvrcl	$⊢ (Scalar (W) \in DivRing \land k \in {Base}_{Scalar (W)} \land k \neq 0_{Scalar (W)}) \to {inv}_{r} (Scalar (W)) (k) \in {Base}_{Scalar (W)}$
60	25 26 57 59	syl3anc	$⊢ (φ \land (k \in {Base}_{Scalar (W)} \land l \in {Base}_{Scalar (W)}) \land X = (k \cdot_{W} Y) \underset{˙}{+} (l \cdot_{W} Z)) \to {inv}_{r} (Scalar (W)) (k) \in {Base}_{Scalar (W)}$
61	50	3ad2ant1	$⊢ (φ \land (k \in {Base}_{Scalar (W)} \land l \in {Base}_{Scalar (W)}) \land X = (k \cdot_{W} Y) \underset{˙}{+} (l \cdot_{W} Z)) \to Z \in N (\{Z\})$
62	18 22 39 61 52	syl22anc	$⊢ (φ \land (k \in {Base}_{Scalar (W)} \land l \in {Base}_{Scalar (W)}) \land X = (k \cdot_{W} Y) \underset{˙}{+} (l \cdot_{W} Z)) \to l \cdot_{W} Z \in N (\{Z\})$
63	11 13 12 19	lssvscl	$⊢ ((W \in LMod \land N (\{Z\}) \in LSubSp (W)) \land ({inv}_{r} (Scalar (W)) (k) \in {Base}_{Scalar (W)} \land l \cdot_{W} Z \in N (\{Z\}))) \to {inv}_{r} (Scalar (W)) (k) \cdot_{W} (l \cdot_{W} Z) \in N (\{Z\})$
64	18 22 60 62 63	syl22anc	$⊢ (φ \land (k \in {Base}_{Scalar (W)} \land l \in {Base}_{Scalar (W)}) \land X = (k \cdot_{W} Y) \underset{˙}{+} (l \cdot_{W} Z)) \to {inv}_{r} (Scalar (W)) (k) \cdot_{W} (l \cdot_{W} Z) \in N (\{Z\})$
65	12 34 58	drnginvrn0	$⊢ (Scalar (W) \in DivRing \land k \in {Base}_{Scalar (W)} \land k \neq 0_{Scalar (W)}) \to {inv}_{r} (Scalar (W)) (k) \neq 0_{Scalar (W)}$
66	25 26 57 65	syl3anc	$⊢ (φ \land (k \in {Base}_{Scalar (W)} \land l \in {Base}_{Scalar (W)}) \land X = (k \cdot_{W} Y) \underset{˙}{+} (l \cdot_{W} Z)) \to {inv}_{r} (Scalar (W)) (k) \neq 0_{Scalar (W)}$
67	8	3ad2ant1	$⊢ (φ \land (k \in {Base}_{Scalar (W)} \land l \in {Base}_{Scalar (W)}) \land X = (k \cdot_{W} Y) \underset{˙}{+} (l \cdot_{W} Z)) \to \neg X \in N (\{Y\})$
68		simpl3	$⊢ ((φ \land (k \in {Base}_{Scalar (W)} \land l \in {Base}_{Scalar (W)}) \land X = (k \cdot_{W} Y) \underset{˙}{+} (l \cdot_{W} Z)) \land l = 0_{Scalar (W)}) \to X = (k \cdot_{W} Y) \underset{˙}{+} (l \cdot_{W} Z)$
69		oveq1	$⊢ l = 0_{Scalar (W)} \to l \cdot_{W} Z = 0_{Scalar (W)} \cdot_{W} Z$
70	1 11 13 34 3	lmod0vs	$⊢ (W \in LMod \land Z \in V) \to 0_{Scalar (W)} \cdot_{W} Z = \underset{˙}{0}$
71	18 40 70	syl2anc	$⊢ (φ \land (k \in {Base}_{Scalar (W)} \land l \in {Base}_{Scalar (W)}) \land X = (k \cdot_{W} Y) \underset{˙}{+} (l \cdot_{W} Z)) \to 0_{Scalar (W)} \cdot_{W} Z = \underset{˙}{0}$
72	69 71	sylan9eqr	$⊢ ((φ \land (k \in {Base}_{Scalar (W)} \land l \in {Base}_{Scalar (W)}) \land X = (k \cdot_{W} Y) \underset{˙}{+} (l \cdot_{W} Z)) \land l = 0_{Scalar (W)}) \to l \cdot_{W} Z = \underset{˙}{0}$
73	72	oveq2d	$⊢ ((φ \land (k \in {Base}_{Scalar (W)} \land l \in {Base}_{Scalar (W)}) \land X = (k \cdot_{W} Y) \underset{˙}{+} (l \cdot_{W} Z)) \land l = 0_{Scalar (W)}) \to (k \cdot_{W} Y) \underset{˙}{+} (l \cdot_{W} Z) = (k \cdot_{W} Y) \underset{˙}{+} \underset{˙}{0}$
74	6	3ad2ant1	$⊢ (φ \land (k \in {Base}_{Scalar (W)} \land l \in {Base}_{Scalar (W)}) \land X = (k \cdot_{W} Y) \underset{˙}{+} (l \cdot_{W} Z)) \to Y \in V$
75	1 11 13 12	lmodvscl	$⊢ (W \in LMod \land k \in {Base}_{Scalar (W)} \land Y \in V) \to k \cdot_{W} Y \in V$
76	18 26 74 75	syl3anc	$⊢ (φ \land (k \in {Base}_{Scalar (W)} \land l \in {Base}_{Scalar (W)}) \land X = (k \cdot_{W} Y) \underset{˙}{+} (l \cdot_{W} Z)) \to k \cdot_{W} Y \in V$
77	1 2 3	lmod0vrid	$⊢ (W \in LMod \land k \cdot_{W} Y \in V) \to (k \cdot_{W} Y) \underset{˙}{+} \underset{˙}{0} = k \cdot_{W} Y$
78	18 76 77	syl2anc	$⊢ (φ \land (k \in {Base}_{Scalar (W)} \land l \in {Base}_{Scalar (W)}) \land X = (k \cdot_{W} Y) \underset{˙}{+} (l \cdot_{W} Z)) \to (k \cdot_{W} Y) \underset{˙}{+} \underset{˙}{0} = k \cdot_{W} Y$
79	78	adantr	$⊢ ((φ \land (k \in {Base}_{Scalar (W)} \land l \in {Base}_{Scalar (W)}) \land X = (k \cdot_{W} Y) \underset{˙}{+} (l \cdot_{W} Z)) \land l = 0_{Scalar (W)}) \to (k \cdot_{W} Y) \underset{˙}{+} \underset{˙}{0} = k \cdot_{W} Y$
80	68 73 79	3eqtrd	$⊢ ((φ \land (k \in {Base}_{Scalar (W)} \land l \in {Base}_{Scalar (W)}) \land X = (k \cdot_{W} Y) \underset{˙}{+} (l \cdot_{W} Z)) \land l = 0_{Scalar (W)}) \to X = k \cdot_{W} Y$
81	1 19 4	lspsncl	$⊢ (W \in LMod \land Y \in V) \to N (\{Y\}) \in LSubSp (W)$
82	15 6 81	syl2anc	$⊢ φ \to N (\{Y\}) \in LSubSp (W)$
83	82	3ad2ant1	$⊢ (φ \land (k \in {Base}_{Scalar (W)} \land l \in {Base}_{Scalar (W)}) \land X = (k \cdot_{W} Y) \underset{˙}{+} (l \cdot_{W} Z)) \to N (\{Y\}) \in LSubSp (W)$
84	1 4	lspsnid	$⊢ (W \in LMod \land Y \in V) \to Y \in N (\{Y\})$
85	15 6 84	syl2anc	$⊢ φ \to Y \in N (\{Y\})$
86	85	3ad2ant1	$⊢ (φ \land (k \in {Base}_{Scalar (W)} \land l \in {Base}_{Scalar (W)}) \land X = (k \cdot_{W} Y) \underset{˙}{+} (l \cdot_{W} Z)) \to Y \in N (\{Y\})$
87	11 13 12 19	lssvscl	$⊢ ((W \in LMod \land N (\{Y\}) \in LSubSp (W)) \land (k \in {Base}_{Scalar (W)} \land Y \in N (\{Y\}))) \to k \cdot_{W} Y \in N (\{Y\})$
88	18 83 26 86 87	syl22anc	$⊢ (φ \land (k \in {Base}_{Scalar (W)} \land l \in {Base}_{Scalar (W)}) \land X = (k \cdot_{W} Y) \underset{˙}{+} (l \cdot_{W} Z)) \to k \cdot_{W} Y \in N (\{Y\})$
89	88	adantr	$⊢ ((φ \land (k \in {Base}_{Scalar (W)} \land l \in {Base}_{Scalar (W)}) \land X = (k \cdot_{W} Y) \underset{˙}{+} (l \cdot_{W} Z)) \land l = 0_{Scalar (W)}) \to k \cdot_{W} Y \in N (\{Y\})$
90	80 89	eqeltrd	$⊢ ((φ \land (k \in {Base}_{Scalar (W)} \land l \in {Base}_{Scalar (W)}) \land X = (k \cdot_{W} Y) \underset{˙}{+} (l \cdot_{W} Z)) \land l = 0_{Scalar (W)}) \to X \in N (\{Y\})$
91	90	ex	$⊢ (φ \land (k \in {Base}_{Scalar (W)} \land l \in {Base}_{Scalar (W)}) \land X = (k \cdot_{W} Y) \underset{˙}{+} (l \cdot_{W} Z)) \to (l = 0_{Scalar (W)} \to X \in N (\{Y\}))$
92	91	necon3bd	$⊢ (φ \land (k \in {Base}_{Scalar (W)} \land l \in {Base}_{Scalar (W)}) \land X = (k \cdot_{W} Y) \underset{˙}{+} (l \cdot_{W} Z)) \to (\neg X \in N (\{Y\}) \to l \neq 0_{Scalar (W)})$
93	67 92	mpd	$⊢ (φ \land (k \in {Base}_{Scalar (W)} \land l \in {Base}_{Scalar (W)}) \land X = (k \cdot_{W} Y) \underset{˙}{+} (l \cdot_{W} Z)) \to l \neq 0_{Scalar (W)}$
94		simpl1	$⊢ ((φ \land (k \in {Base}_{Scalar (W)} \land l \in {Base}_{Scalar (W)}) \land X = (k \cdot_{W} Y) \underset{˙}{+} (l \cdot_{W} Z)) \land Z = \underset{˙}{0}) \to φ$
95	94 10	syl	$⊢ ((φ \land (k \in {Base}_{Scalar (W)} \land l \in {Base}_{Scalar (W)}) \land X = (k \cdot_{W} Y) \underset{˙}{+} (l \cdot_{W} Z)) \land Z = \underset{˙}{0}) \to X \in N (\{Y, Z\})$
96		preq2	$⊢ Z = \underset{˙}{0} \to \{Y, Z\} = \{Y, \underset{˙}{0}\}$
97	96	fveq2d	$⊢ Z = \underset{˙}{0} \to N (\{Y, Z\}) = N (\{Y, \underset{˙}{0}\})$
98	1 3 4 18 74	lsppr0	$⊢ (φ \land (k \in {Base}_{Scalar (W)} \land l \in {Base}_{Scalar (W)}) \land X = (k \cdot_{W} Y) \underset{˙}{+} (l \cdot_{W} Z)) \to N (\{Y, \underset{˙}{0}\}) = N (\{Y\})$
99	97 98	sylan9eqr	$⊢ ((φ \land (k \in {Base}_{Scalar (W)} \land l \in {Base}_{Scalar (W)}) \land X = (k \cdot_{W} Y) \underset{˙}{+} (l \cdot_{W} Z)) \land Z = \underset{˙}{0}) \to N (\{Y, Z\}) = N (\{Y\})$
100	95 99	eleqtrd	$⊢ ((φ \land (k \in {Base}_{Scalar (W)} \land l \in {Base}_{Scalar (W)}) \land X = (k \cdot_{W} Y) \underset{˙}{+} (l \cdot_{W} Z)) \land Z = \underset{˙}{0}) \to X \in N (\{Y\})$
101	100	ex	$⊢ (φ \land (k \in {Base}_{Scalar (W)} \land l \in {Base}_{Scalar (W)}) \land X = (k \cdot_{W} Y) \underset{˙}{+} (l \cdot_{W} Z)) \to (Z = \underset{˙}{0} \to X \in N (\{Y\}))$
102	101	necon3bd	$⊢ (φ \land (k \in {Base}_{Scalar (W)} \land l \in {Base}_{Scalar (W)}) \land X = (k \cdot_{W} Y) \underset{˙}{+} (l \cdot_{W} Z)) \to (\neg X \in N (\{Y\}) \to Z \neq \underset{˙}{0})$
103	67 102	mpd	$⊢ (φ \land (k \in {Base}_{Scalar (W)} \land l \in {Base}_{Scalar (W)}) \land X = (k \cdot_{W} Y) \underset{˙}{+} (l \cdot_{W} Z)) \to Z \neq \underset{˙}{0}$
104	1 13 11 12 34 3 23 39 40	lvecvsn0	$⊢ (φ \land (k \in {Base}_{Scalar (W)} \land l \in {Base}_{Scalar (W)}) \land X = (k \cdot_{W} Y) \underset{˙}{+} (l \cdot_{W} Z)) \to (l \cdot_{W} Z \neq \underset{˙}{0} \leftrightarrow (l \neq 0_{Scalar (W)} \land Z \neq \underset{˙}{0}))$
105	93 103 104	mpbir2and	$⊢ (φ \land (k \in {Base}_{Scalar (W)} \land l \in {Base}_{Scalar (W)}) \land X = (k \cdot_{W} Y) \underset{˙}{+} (l \cdot_{W} Z)) \to l \cdot_{W} Z \neq \underset{˙}{0}$
106	1 13 11 12 34 3 23 60 42	lvecvsn0	$⊢ (φ \land (k \in {Base}_{Scalar (W)} \land l \in {Base}_{Scalar (W)}) \land X = (k \cdot_{W} Y) \underset{˙}{+} (l \cdot_{W} Z)) \to ({inv}_{r} (Scalar (W)) (k) \cdot_{W} (l \cdot_{W} Z) \neq \underset{˙}{0} \leftrightarrow ({inv}_{r} (Scalar (W)) (k) \neq 0_{Scalar (W)} \land l \cdot_{W} Z \neq \underset{˙}{0}))$
107	66 105 106	mpbir2and	$⊢ (φ \land (k \in {Base}_{Scalar (W)} \land l \in {Base}_{Scalar (W)}) \land X = (k \cdot_{W} Y) \underset{˙}{+} (l \cdot_{W} Z)) \to {inv}_{r} (Scalar (W)) (k) \cdot_{W} (l \cdot_{W} Z) \neq \underset{˙}{0}$
108		eldifsn	$⊢ {inv}_{r} (Scalar (W)) (k) \cdot_{W} (l \cdot_{W} Z) \in (N (\{Z\}) ∖ \{\underset{˙}{0}\}) \leftrightarrow ({inv}_{r} (Scalar (W)) (k) \cdot_{W} (l \cdot_{W} Z) \in N (\{Z\}) \land {inv}_{r} (Scalar (W)) (k) \cdot_{W} (l \cdot_{W} Z) \neq \underset{˙}{0})$
109	64 107 108	sylanbrc	$⊢ (φ \land (k \in {Base}_{Scalar (W)} \land l \in {Base}_{Scalar (W)}) \land X = (k \cdot_{W} Y) \underset{˙}{+} (l \cdot_{W} Z)) \to {inv}_{r} (Scalar (W)) (k) \cdot_{W} (l \cdot_{W} Z) \in (N (\{Z\}) ∖ \{\underset{˙}{0}\})$
110		simp3	$⊢ (φ \land (k \in {Base}_{Scalar (W)} \land l \in {Base}_{Scalar (W)}) \land X = (k \cdot_{W} Y) \underset{˙}{+} (l \cdot_{W} Z)) \to X = (k \cdot_{W} Y) \underset{˙}{+} (l \cdot_{W} Z)$
111	1 2	lmodvacl	$⊢ (W \in LMod \land k \cdot_{W} Y \in V \land l \cdot_{W} Z \in V) \to (k \cdot_{W} Y) \underset{˙}{+} (l \cdot_{W} Z) \in V$
112	18 76 42 111	syl3anc	$⊢ (φ \land (k \in {Base}_{Scalar (W)} \land l \in {Base}_{Scalar (W)}) \land X = (k \cdot_{W} Y) \underset{˙}{+} (l \cdot_{W} Z)) \to (k \cdot_{W} Y) \underset{˙}{+} (l \cdot_{W} Z) \in V$
113	1 4	lspsnid	$⊢ (W \in LMod \land (k \cdot_{W} Y) \underset{˙}{+} (l \cdot_{W} Z) \in V) \to (k \cdot_{W} Y) \underset{˙}{+} (l \cdot_{W} Z) \in N (\{(k \cdot_{W} Y) \underset{˙}{+} (l \cdot_{W} Z)\})$
114	18 112 113	syl2anc	$⊢ (φ \land (k \in {Base}_{Scalar (W)} \land l \in {Base}_{Scalar (W)}) \land X = (k \cdot_{W} Y) \underset{˙}{+} (l \cdot_{W} Z)) \to (k \cdot_{W} Y) \underset{˙}{+} (l \cdot_{W} Z) \in N (\{(k \cdot_{W} Y) \underset{˙}{+} (l \cdot_{W} Z)\})$
115	110 114	eqeltrd	$⊢ (φ \land (k \in {Base}_{Scalar (W)} \land l \in {Base}_{Scalar (W)}) \land X = (k \cdot_{W} Y) \underset{˙}{+} (l \cdot_{W} Z)) \to X \in N (\{(k \cdot_{W} Y) \underset{˙}{+} (l \cdot_{W} Z)\})$
116	1 11 13 12 34 4	lspsnvs	$⊢ (W \in LVec \land ({inv}_{r} (Scalar (W)) (k) \in {Base}_{Scalar (W)} \land {inv}_{r} (Scalar (W)) (k) \neq 0_{Scalar (W)}) \land (k \cdot_{W} Y) \underset{˙}{+} (l \cdot_{W} Z) \in V) \to N (\{{inv}_{r} (Scalar (W)) (k) \cdot_{W} ((k \cdot_{W} Y) \underset{˙}{+} (l \cdot_{W} Z))\}) = N (\{(k \cdot_{W} Y) \underset{˙}{+} (l \cdot_{W} Z)\})$
117	23 60 66 112 116	syl121anc	$⊢ (φ \land (k \in {Base}_{Scalar (W)} \land l \in {Base}_{Scalar (W)}) \land X = (k \cdot_{W} Y) \underset{˙}{+} (l \cdot_{W} Z)) \to N (\{{inv}_{r} (Scalar (W)) (k) \cdot_{W} ((k \cdot_{W} Y) \underset{˙}{+} (l \cdot_{W} Z))\}) = N (\{(k \cdot_{W} Y) \underset{˙}{+} (l \cdot_{W} Z)\})$
118	1 2 11 13 12	lmodvsdi	$⊢ (W \in LMod \land ({inv}_{r} (Scalar (W)) (k) \in {Base}_{Scalar (W)} \land k \cdot_{W} Y \in V \land l \cdot_{W} Z \in V)) \to {inv}_{r} (Scalar (W)) (k) \cdot_{W} ((k \cdot_{W} Y) \underset{˙}{+} (l \cdot_{W} Z)) = ({inv}_{r} (Scalar (W)) (k) \cdot_{W} (k \cdot_{W} Y)) \underset{˙}{+} ({inv}_{r} (Scalar (W)) (k) \cdot_{W} (l \cdot_{W} Z))$
119	18 60 76 42 118	syl13anc	$⊢ (φ \land (k \in {Base}_{Scalar (W)} \land l \in {Base}_{Scalar (W)}) \land X = (k \cdot_{W} Y) \underset{˙}{+} (l \cdot_{W} Z)) \to {inv}_{r} (Scalar (W)) (k) \cdot_{W} ((k \cdot_{W} Y) \underset{˙}{+} (l \cdot_{W} Z)) = ({inv}_{r} (Scalar (W)) (k) \cdot_{W} (k \cdot_{W} Y)) \underset{˙}{+} ({inv}_{r} (Scalar (W)) (k) \cdot_{W} (l \cdot_{W} Z))$
120		eqid	$⊢ \cdot_{Scalar (W)} = \cdot_{Scalar (W)}$
121		eqid	$⊢ 1_{Scalar (W)} = 1_{Scalar (W)}$
122	12 34 120 121 58	drnginvrl	$⊢ (Scalar (W) \in DivRing \land k \in {Base}_{Scalar (W)} \land k \neq 0_{Scalar (W)}) \to {inv}_{r} (Scalar (W)) (k) \cdot_{Scalar (W)} k = 1_{Scalar (W)}$
123	25 26 57 122	syl3anc	$⊢ (φ \land (k \in {Base}_{Scalar (W)} \land l \in {Base}_{Scalar (W)}) \land X = (k \cdot_{W} Y) \underset{˙}{+} (l \cdot_{W} Z)) \to {inv}_{r} (Scalar (W)) (k) \cdot_{Scalar (W)} k = 1_{Scalar (W)}$
124	123	oveq1d	$⊢ (φ \land (k \in {Base}_{Scalar (W)} \land l \in {Base}_{Scalar (W)}) \land X = (k \cdot_{W} Y) \underset{˙}{+} (l \cdot_{W} Z)) \to ({inv}_{r} (Scalar (W)) (k) \cdot_{Scalar (W)} k) \cdot_{W} Y = 1_{Scalar (W)} \cdot_{W} Y$
125	1 11 13 12 120	lmodvsass	$⊢ (W \in LMod \land ({inv}_{r} (Scalar (W)) (k) \in {Base}_{Scalar (W)} \land k \in {Base}_{Scalar (W)} \land Y \in V)) \to ({inv}_{r} (Scalar (W)) (k) \cdot_{Scalar (W)} k) \cdot_{W} Y = {inv}_{r} (Scalar (W)) (k) \cdot_{W} (k \cdot_{W} Y)$
126	18 60 26 74 125	syl13anc	$⊢ (φ \land (k \in {Base}_{Scalar (W)} \land l \in {Base}_{Scalar (W)}) \land X = (k \cdot_{W} Y) \underset{˙}{+} (l \cdot_{W} Z)) \to ({inv}_{r} (Scalar (W)) (k) \cdot_{Scalar (W)} k) \cdot_{W} Y = {inv}_{r} (Scalar (W)) (k) \cdot_{W} (k \cdot_{W} Y)$
127	1 11 13 121	lmodvs1	$⊢ (W \in LMod \land Y \in V) \to 1_{Scalar (W)} \cdot_{W} Y = Y$
128	18 74 127	syl2anc	$⊢ (φ \land (k \in {Base}_{Scalar (W)} \land l \in {Base}_{Scalar (W)}) \land X = (k \cdot_{W} Y) \underset{˙}{+} (l \cdot_{W} Z)) \to 1_{Scalar (W)} \cdot_{W} Y = Y$
129	124 126 128	3eqtr3d	$⊢ (φ \land (k \in {Base}_{Scalar (W)} \land l \in {Base}_{Scalar (W)}) \land X = (k \cdot_{W} Y) \underset{˙}{+} (l \cdot_{W} Z)) \to {inv}_{r} (Scalar (W)) (k) \cdot_{W} (k \cdot_{W} Y) = Y$
130	129	oveq1d	$⊢ (φ \land (k \in {Base}_{Scalar (W)} \land l \in {Base}_{Scalar (W)}) \land X = (k \cdot_{W} Y) \underset{˙}{+} (l \cdot_{W} Z)) \to ({inv}_{r} (Scalar (W)) (k) \cdot_{W} (k \cdot_{W} Y)) \underset{˙}{+} ({inv}_{r} (Scalar (W)) (k) \cdot_{W} (l \cdot_{W} Z)) = Y \underset{˙}{+} ({inv}_{r} (Scalar (W)) (k) \cdot_{W} (l \cdot_{W} Z))$
131	119 130	eqtrd	$⊢ (φ \land (k \in {Base}_{Scalar (W)} \land l \in {Base}_{Scalar (W)}) \land X = (k \cdot_{W} Y) \underset{˙}{+} (l \cdot_{W} Z)) \to {inv}_{r} (Scalar (W)) (k) \cdot_{W} ((k \cdot_{W} Y) \underset{˙}{+} (l \cdot_{W} Z)) = Y \underset{˙}{+} ({inv}_{r} (Scalar (W)) (k) \cdot_{W} (l \cdot_{W} Z))$
132	131	sneqd	$⊢ (φ \land (k \in {Base}_{Scalar (W)} \land l \in {Base}_{Scalar (W)}) \land X = (k \cdot_{W} Y) \underset{˙}{+} (l \cdot_{W} Z)) \to \{{inv}_{r} (Scalar (W)) (k) \cdot_{W} ((k \cdot_{W} Y) \underset{˙}{+} (l \cdot_{W} Z))\} = \{Y \underset{˙}{+} ({inv}_{r} (Scalar (W)) (k) \cdot_{W} (l \cdot_{W} Z))\}$
133	132	fveq2d	$⊢ (φ \land (k \in {Base}_{Scalar (W)} \land l \in {Base}_{Scalar (W)}) \land X = (k \cdot_{W} Y) \underset{˙}{+} (l \cdot_{W} Z)) \to N (\{{inv}_{r} (Scalar (W)) (k) \cdot_{W} ((k \cdot_{W} Y) \underset{˙}{+} (l \cdot_{W} Z))\}) = N (\{Y \underset{˙}{+} ({inv}_{r} (Scalar (W)) (k) \cdot_{W} (l \cdot_{W} Z))\})$
134	117 133	eqtr3d	$⊢ (φ \land (k \in {Base}_{Scalar (W)} \land l \in {Base}_{Scalar (W)}) \land X = (k \cdot_{W} Y) \underset{˙}{+} (l \cdot_{W} Z)) \to N (\{(k \cdot_{W} Y) \underset{˙}{+} (l \cdot_{W} Z)\}) = N (\{Y \underset{˙}{+} ({inv}_{r} (Scalar (W)) (k) \cdot_{W} (l \cdot_{W} Z))\})$
135	115 134	eleqtrd	$⊢ (φ \land (k \in {Base}_{Scalar (W)} \land l \in {Base}_{Scalar (W)}) \land X = (k \cdot_{W} Y) \underset{˙}{+} (l \cdot_{W} Z)) \to X \in N (\{Y \underset{˙}{+} ({inv}_{r} (Scalar (W)) (k) \cdot_{W} (l \cdot_{W} Z))\})$
136		oveq2	$⊢ z = {inv}_{r} (Scalar (W)) (k) \cdot_{W} (l \cdot_{W} Z) \to Y \underset{˙}{+} z = Y \underset{˙}{+} ({inv}_{r} (Scalar (W)) (k) \cdot_{W} (l \cdot_{W} Z))$
137	136	sneqd	$⊢ z = {inv}_{r} (Scalar (W)) (k) \cdot_{W} (l \cdot_{W} Z) \to \{Y \underset{˙}{+} z\} = \{Y \underset{˙}{+} ({inv}_{r} (Scalar (W)) (k) \cdot_{W} (l \cdot_{W} Z))\}$
138	137	fveq2d	$⊢ z = {inv}_{r} (Scalar (W)) (k) \cdot_{W} (l \cdot_{W} Z) \to N (\{Y \underset{˙}{+} z\}) = N (\{Y \underset{˙}{+} ({inv}_{r} (Scalar (W)) (k) \cdot_{W} (l \cdot_{W} Z))\})$
139	138	eleq2d	$⊢ z = {inv}_{r} (Scalar (W)) (k) \cdot_{W} (l \cdot_{W} Z) \to (X \in N (\{Y \underset{˙}{+} z\}) \leftrightarrow X \in N (\{Y \underset{˙}{+} ({inv}_{r} (Scalar (W)) (k) \cdot_{W} (l \cdot_{W} Z))\}))$
140	139	rspcev	$⊢ ({inv}_{r} (Scalar (W)) (k) \cdot_{W} (l \cdot_{W} Z) \in (N (\{Z\}) ∖ \{\underset{˙}{0}\}) \land X \in N (\{Y \underset{˙}{+} ({inv}_{r} (Scalar (W)) (k) \cdot_{W} (l \cdot_{W} Z))\})) \to \exists z \in (N (\{Z\}) ∖ \{\underset{˙}{0}\}) X \in N (\{Y \underset{˙}{+} z\})$
141	109 135 140	syl2anc	$⊢ (φ \land (k \in {Base}_{Scalar (W)} \land l \in {Base}_{Scalar (W)}) \land X = (k \cdot_{W} Y) \underset{˙}{+} (l \cdot_{W} Z)) \to \exists z \in (N (\{Z\}) ∖ \{\underset{˙}{0}\}) X \in N (\{Y \underset{˙}{+} z\})$
142	141	3exp	$⊢ φ \to ((k \in {Base}_{Scalar (W)} \land l \in {Base}_{Scalar (W)}) \to (X = (k \cdot_{W} Y) \underset{˙}{+} (l \cdot_{W} Z) \to \exists z \in (N (\{Z\}) ∖ \{\underset{˙}{0}\}) X \in N (\{Y \underset{˙}{+} z\})))$
143	142	rexlimdvv	$⊢ φ \to (\exists k \in {Base}_{Scalar (W)} \exists l \in {Base}_{Scalar (W)} X = (k \cdot_{W} Y) \underset{˙}{+} (l \cdot_{W} Z) \to \exists z \in (N (\{Z\}) ∖ \{\underset{˙}{0}\}) X \in N (\{Y \underset{˙}{+} z\}))$
144	17 143	mpd	$⊢ φ \to \exists z \in (N (\{Z\}) ∖ \{\underset{˙}{0}\}) X \in N (\{Y \underset{˙}{+} z\})$

Metamath Proof Explorer

Theorem lspfixed

Proof