lspsolv

Description: If X is in the span of A u. { Y } but not A , then Y is in the span of A u. { X } . (Contributed by Mario Carneiro, 25-Jun-2014)

	Ref	Expression
Hypotheses	lspsolv.v	$⊢ V = {Base}_{W}$
	lspsolv.s	$⊢ S = LSubSp (W)$
	lspsolv.n	$⊢ N = LSpan (W)$
Assertion	lspsolv	$⊢ (W \in LVec \land (A \subseteq V \land Y \in V \land X \in (N (A \cup \{Y\}) ∖ N (A)))) \to Y \in N (A \cup \{X\})$

Proof

Step	Hyp	Ref	Expression
1		lspsolv.v	$⊢ V = {Base}_{W}$
2		lspsolv.s	$⊢ S = LSubSp (W)$
3		lspsolv.n	$⊢ N = LSpan (W)$
4		eqid	$⊢ Scalar (W) = Scalar (W)$
5		eqid	$⊢ {Base}_{Scalar (W)} = {Base}_{Scalar (W)}$
6		eqid	$⊢ +_{W} = +_{W}$
7		eqid	$⊢ \cdot_{W} = \cdot_{W}$
8		eqid	$⊢ \{z \in V \| \exists r \in {Base}_{Scalar (W)} z +_{W} (r \cdot_{W} Y) \in N (A)\} = \{z \in V \| \exists r \in {Base}_{Scalar (W)} z +_{W} (r \cdot_{W} Y) \in N (A)\}$
9		lveclmod	$⊢ W \in LVec \to W \in LMod$
10	9	adantr	$⊢ (W \in LVec \land (A \subseteq V \land Y \in V \land X \in (N (A \cup \{Y\}) ∖ N (A)))) \to W \in LMod$
11		simpr1	$⊢ (W \in LVec \land (A \subseteq V \land Y \in V \land X \in (N (A \cup \{Y\}) ∖ N (A)))) \to A \subseteq V$
12		simpr2	$⊢ (W \in LVec \land (A \subseteq V \land Y \in V \land X \in (N (A \cup \{Y\}) ∖ N (A)))) \to Y \in V$
13		simpr3	$⊢ (W \in LVec \land (A \subseteq V \land Y \in V \land X \in (N (A \cup \{Y\}) ∖ N (A)))) \to X \in (N (A \cup \{Y\}) ∖ N (A))$
14	13	eldifad	$⊢ (W \in LVec \land (A \subseteq V \land Y \in V \land X \in (N (A \cup \{Y\}) ∖ N (A)))) \to X \in N (A \cup \{Y\})$
15	1 2 3 4 5 6 7 8 10 11 12 14	lspsolvlem	$⊢ (W \in LVec \land (A \subseteq V \land Y \in V \land X \in (N (A \cup \{Y\}) ∖ N (A)))) \to \exists r \in {Base}_{Scalar (W)} X +_{W} (r \cdot_{W} Y) \in N (A)$
16	4	lvecdrng	$⊢ W \in LVec \to Scalar (W) \in DivRing$
17	16	ad2antrr	$⊢ ((W \in LVec \land (A \subseteq V \land Y \in V \land X \in (N (A \cup \{Y\}) ∖ N (A)))) \land (r \in {Base}_{Scalar (W)} \land X +_{W} (r \cdot_{W} Y) \in N (A))) \to Scalar (W) \in DivRing$
18		simprl	$⊢ ((W \in LVec \land (A \subseteq V \land Y \in V \land X \in (N (A \cup \{Y\}) ∖ N (A)))) \land (r \in {Base}_{Scalar (W)} \land X +_{W} (r \cdot_{W} Y) \in N (A))) \to r \in {Base}_{Scalar (W)}$
19	10	adantr	$⊢ ((W \in LVec \land (A \subseteq V \land Y \in V \land X \in (N (A \cup \{Y\}) ∖ N (A)))) \land (r \in {Base}_{Scalar (W)} \land X +_{W} (r \cdot_{W} Y) \in N (A))) \to W \in LMod$
20	12	adantr	$⊢ ((W \in LVec \land (A \subseteq V \land Y \in V \land X \in (N (A \cup \{Y\}) ∖ N (A)))) \land (r \in {Base}_{Scalar (W)} \land X +_{W} (r \cdot_{W} Y) \in N (A))) \to Y \in V$
21		eqid	$⊢ 0_{Scalar (W)} = 0_{Scalar (W)}$
22		eqid	$⊢ 0_{W} = 0_{W}$
23	1 4 7 21 22	lmod0vs	$⊢ (W \in LMod \land Y \in V) \to 0_{Scalar (W)} \cdot_{W} Y = 0_{W}$
24	19 20 23	syl2anc	$⊢ ((W \in LVec \land (A \subseteq V \land Y \in V \land X \in (N (A \cup \{Y\}) ∖ N (A)))) \land (r \in {Base}_{Scalar (W)} \land X +_{W} (r \cdot_{W} Y) \in N (A))) \to 0_{Scalar (W)} \cdot_{W} Y = 0_{W}$
25	24	oveq2d	$⊢ ((W \in LVec \land (A \subseteq V \land Y \in V \land X \in (N (A \cup \{Y\}) ∖ N (A)))) \land (r \in {Base}_{Scalar (W)} \land X +_{W} (r \cdot_{W} Y) \in N (A))) \to X +_{W} (0_{Scalar (W)} \cdot_{W} Y) = X +_{W} 0_{W}$
26	11	adantr	$⊢ ((W \in LVec \land (A \subseteq V \land Y \in V \land X \in (N (A \cup \{Y\}) ∖ N (A)))) \land (r \in {Base}_{Scalar (W)} \land X +_{W} (r \cdot_{W} Y) \in N (A))) \to A \subseteq V$
27	20	snssd	$⊢ ((W \in LVec \land (A \subseteq V \land Y \in V \land X \in (N (A \cup \{Y\}) ∖ N (A)))) \land (r \in {Base}_{Scalar (W)} \land X +_{W} (r \cdot_{W} Y) \in N (A))) \to \{Y\} \subseteq V$
28	26 27	unssd	$⊢ ((W \in LVec \land (A \subseteq V \land Y \in V \land X \in (N (A \cup \{Y\}) ∖ N (A)))) \land (r \in {Base}_{Scalar (W)} \land X +_{W} (r \cdot_{W} Y) \in N (A))) \to A \cup \{Y\} \subseteq V$
29	1 3	lspssv	$⊢ (W \in LMod \land A \cup \{Y\} \subseteq V) \to N (A \cup \{Y\}) \subseteq V$
30	19 28 29	syl2anc	$⊢ ((W \in LVec \land (A \subseteq V \land Y \in V \land X \in (N (A \cup \{Y\}) ∖ N (A)))) \land (r \in {Base}_{Scalar (W)} \land X +_{W} (r \cdot_{W} Y) \in N (A))) \to N (A \cup \{Y\}) \subseteq V$
31	30	ssdifssd	$⊢ ((W \in LVec \land (A \subseteq V \land Y \in V \land X \in (N (A \cup \{Y\}) ∖ N (A)))) \land (r \in {Base}_{Scalar (W)} \land X +_{W} (r \cdot_{W} Y) \in N (A))) \to N (A \cup \{Y\}) ∖ N (A) \subseteq V$
32	13	adantr	$⊢ ((W \in LVec \land (A \subseteq V \land Y \in V \land X \in (N (A \cup \{Y\}) ∖ N (A)))) \land (r \in {Base}_{Scalar (W)} \land X +_{W} (r \cdot_{W} Y) \in N (A))) \to X \in (N (A \cup \{Y\}) ∖ N (A))$
33	31 32	sseldd	$⊢ ((W \in LVec \land (A \subseteq V \land Y \in V \land X \in (N (A \cup \{Y\}) ∖ N (A)))) \land (r \in {Base}_{Scalar (W)} \land X +_{W} (r \cdot_{W} Y) \in N (A))) \to X \in V$
34	1 6 22	lmod0vrid	$⊢ (W \in LMod \land X \in V) \to X +_{W} 0_{W} = X$
35	19 33 34	syl2anc	$⊢ ((W \in LVec \land (A \subseteq V \land Y \in V \land X \in (N (A \cup \{Y\}) ∖ N (A)))) \land (r \in {Base}_{Scalar (W)} \land X +_{W} (r \cdot_{W} Y) \in N (A))) \to X +_{W} 0_{W} = X$
36	25 35	eqtrd	$⊢ ((W \in LVec \land (A \subseteq V \land Y \in V \land X \in (N (A \cup \{Y\}) ∖ N (A)))) \land (r \in {Base}_{Scalar (W)} \land X +_{W} (r \cdot_{W} Y) \in N (A))) \to X +_{W} (0_{Scalar (W)} \cdot_{W} Y) = X$
37	36 32	eqeltrd	$⊢ ((W \in LVec \land (A \subseteq V \land Y \in V \land X \in (N (A \cup \{Y\}) ∖ N (A)))) \land (r \in {Base}_{Scalar (W)} \land X +_{W} (r \cdot_{W} Y) \in N (A))) \to X +_{W} (0_{Scalar (W)} \cdot_{W} Y) \in (N (A \cup \{Y\}) ∖ N (A))$
38	37	eldifbd	$⊢ ((W \in LVec \land (A \subseteq V \land Y \in V \land X \in (N (A \cup \{Y\}) ∖ N (A)))) \land (r \in {Base}_{Scalar (W)} \land X +_{W} (r \cdot_{W} Y) \in N (A))) \to \neg X +_{W} (0_{Scalar (W)} \cdot_{W} Y) \in N (A)$
39		simprr	$⊢ ((W \in LVec \land (A \subseteq V \land Y \in V \land X \in (N (A \cup \{Y\}) ∖ N (A)))) \land (r \in {Base}_{Scalar (W)} \land X +_{W} (r \cdot_{W} Y) \in N (A))) \to X +_{W} (r \cdot_{W} Y) \in N (A)$
40		oveq1	$⊢ r = 0_{Scalar (W)} \to r \cdot_{W} Y = 0_{Scalar (W)} \cdot_{W} Y$
41	40	oveq2d	$⊢ r = 0_{Scalar (W)} \to X +_{W} (r \cdot_{W} Y) = X +_{W} (0_{Scalar (W)} \cdot_{W} Y)$
42	41	eleq1d	$⊢ r = 0_{Scalar (W)} \to (X +_{W} (r \cdot_{W} Y) \in N (A) \leftrightarrow X +_{W} (0_{Scalar (W)} \cdot_{W} Y) \in N (A))$
43	39 42	syl5ibcom	$⊢ ((W \in LVec \land (A \subseteq V \land Y \in V \land X \in (N (A \cup \{Y\}) ∖ N (A)))) \land (r \in {Base}_{Scalar (W)} \land X +_{W} (r \cdot_{W} Y) \in N (A))) \to (r = 0_{Scalar (W)} \to X +_{W} (0_{Scalar (W)} \cdot_{W} Y) \in N (A))$
44	43	necon3bd	$⊢ ((W \in LVec \land (A \subseteq V \land Y \in V \land X \in (N (A \cup \{Y\}) ∖ N (A)))) \land (r \in {Base}_{Scalar (W)} \land X +_{W} (r \cdot_{W} Y) \in N (A))) \to (\neg X +_{W} (0_{Scalar (W)} \cdot_{W} Y) \in N (A) \to r \neq 0_{Scalar (W)})$
45	38 44	mpd	$⊢ ((W \in LVec \land (A \subseteq V \land Y \in V \land X \in (N (A \cup \{Y\}) ∖ N (A)))) \land (r \in {Base}_{Scalar (W)} \land X +_{W} (r \cdot_{W} Y) \in N (A))) \to r \neq 0_{Scalar (W)}$
46		eqid	$⊢ \cdot_{Scalar (W)} = \cdot_{Scalar (W)}$
47		eqid	$⊢ 1_{Scalar (W)} = 1_{Scalar (W)}$
48		eqid	$⊢ {inv}_{r} (Scalar (W)) = {inv}_{r} (Scalar (W))$
49	5 21 46 47 48	drnginvrl	$⊢ (Scalar (W) \in DivRing \land r \in {Base}_{Scalar (W)} \land r \neq 0_{Scalar (W)}) \to {inv}_{r} (Scalar (W)) (r) \cdot_{Scalar (W)} r = 1_{Scalar (W)}$
50	17 18 45 49	syl3anc	$⊢ ((W \in LVec \land (A \subseteq V \land Y \in V \land X \in (N (A \cup \{Y\}) ∖ N (A)))) \land (r \in {Base}_{Scalar (W)} \land X +_{W} (r \cdot_{W} Y) \in N (A))) \to {inv}_{r} (Scalar (W)) (r) \cdot_{Scalar (W)} r = 1_{Scalar (W)}$
51	50	oveq1d	$⊢ ((W \in LVec \land (A \subseteq V \land Y \in V \land X \in (N (A \cup \{Y\}) ∖ N (A)))) \land (r \in {Base}_{Scalar (W)} \land X +_{W} (r \cdot_{W} Y) \in N (A))) \to ({inv}_{r} (Scalar (W)) (r) \cdot_{Scalar (W)} r) \cdot_{W} Y = 1_{Scalar (W)} \cdot_{W} Y$
52	5 21 48	drnginvrcl	$⊢ (Scalar (W) \in DivRing \land r \in {Base}_{Scalar (W)} \land r \neq 0_{Scalar (W)}) \to {inv}_{r} (Scalar (W)) (r) \in {Base}_{Scalar (W)}$
53	17 18 45 52	syl3anc	$⊢ ((W \in LVec \land (A \subseteq V \land Y \in V \land X \in (N (A \cup \{Y\}) ∖ N (A)))) \land (r \in {Base}_{Scalar (W)} \land X +_{W} (r \cdot_{W} Y) \in N (A))) \to {inv}_{r} (Scalar (W)) (r) \in {Base}_{Scalar (W)}$
54	1 4 7 5 46	lmodvsass	$⊢ (W \in LMod \land ({inv}_{r} (Scalar (W)) (r) \in {Base}_{Scalar (W)} \land r \in {Base}_{Scalar (W)} \land Y \in V)) \to ({inv}_{r} (Scalar (W)) (r) \cdot_{Scalar (W)} r) \cdot_{W} Y = {inv}_{r} (Scalar (W)) (r) \cdot_{W} (r \cdot_{W} Y)$
55	19 53 18 20 54	syl13anc	$⊢ ((W \in LVec \land (A \subseteq V \land Y \in V \land X \in (N (A \cup \{Y\}) ∖ N (A)))) \land (r \in {Base}_{Scalar (W)} \land X +_{W} (r \cdot_{W} Y) \in N (A))) \to ({inv}_{r} (Scalar (W)) (r) \cdot_{Scalar (W)} r) \cdot_{W} Y = {inv}_{r} (Scalar (W)) (r) \cdot_{W} (r \cdot_{W} Y)$
56	1 4 7 47	lmodvs1	$⊢ (W \in LMod \land Y \in V) \to 1_{Scalar (W)} \cdot_{W} Y = Y$
57	19 20 56	syl2anc	$⊢ ((W \in LVec \land (A \subseteq V \land Y \in V \land X \in (N (A \cup \{Y\}) ∖ N (A)))) \land (r \in {Base}_{Scalar (W)} \land X +_{W} (r \cdot_{W} Y) \in N (A))) \to 1_{Scalar (W)} \cdot_{W} Y = Y$
58	51 55 57	3eqtr3d	$⊢ ((W \in LVec \land (A \subseteq V \land Y \in V \land X \in (N (A \cup \{Y\}) ∖ N (A)))) \land (r \in {Base}_{Scalar (W)} \land X +_{W} (r \cdot_{W} Y) \in N (A))) \to {inv}_{r} (Scalar (W)) (r) \cdot_{W} (r \cdot_{W} Y) = Y$
59	33	snssd	$⊢ ((W \in LVec \land (A \subseteq V \land Y \in V \land X \in (N (A \cup \{Y\}) ∖ N (A)))) \land (r \in {Base}_{Scalar (W)} \land X +_{W} (r \cdot_{W} Y) \in N (A))) \to \{X\} \subseteq V$
60	26 59	unssd	$⊢ ((W \in LVec \land (A \subseteq V \land Y \in V \land X \in (N (A \cup \{Y\}) ∖ N (A)))) \land (r \in {Base}_{Scalar (W)} \land X +_{W} (r \cdot_{W} Y) \in N (A))) \to A \cup \{X\} \subseteq V$
61	1 2 3	lspcl	$⊢ (W \in LMod \land A \cup \{X\} \subseteq V) \to N (A \cup \{X\}) \in S$
62	19 60 61	syl2anc	$⊢ ((W \in LVec \land (A \subseteq V \land Y \in V \land X \in (N (A \cup \{Y\}) ∖ N (A)))) \land (r \in {Base}_{Scalar (W)} \land X +_{W} (r \cdot_{W} Y) \in N (A))) \to N (A \cup \{X\}) \in S$
63	1 4 7 5	lmodvscl	$⊢ (W \in LMod \land r \in {Base}_{Scalar (W)} \land Y \in V) \to r \cdot_{W} Y \in V$
64	19 18 20 63	syl3anc	$⊢ ((W \in LVec \land (A \subseteq V \land Y \in V \land X \in (N (A \cup \{Y\}) ∖ N (A)))) \land (r \in {Base}_{Scalar (W)} \land X +_{W} (r \cdot_{W} Y) \in N (A))) \to r \cdot_{W} Y \in V$
65		eqid	$⊢ -_{W} = -_{W}$
66	1 6 65	lmodvpncan	$⊢ (W \in LMod \land r \cdot_{W} Y \in V \land X \in V) \to ((r \cdot_{W} Y) +_{W} X) -_{W} X = r \cdot_{W} Y$
67	19 64 33 66	syl3anc	$⊢ ((W \in LVec \land (A \subseteq V \land Y \in V \land X \in (N (A \cup \{Y\}) ∖ N (A)))) \land (r \in {Base}_{Scalar (W)} \land X +_{W} (r \cdot_{W} Y) \in N (A))) \to ((r \cdot_{W} Y) +_{W} X) -_{W} X = r \cdot_{W} Y$
68	1 6	lmodcom	$⊢ (W \in LMod \land r \cdot_{W} Y \in V \land X \in V) \to (r \cdot_{W} Y) +_{W} X = X +_{W} (r \cdot_{W} Y)$
69	19 64 33 68	syl3anc	$⊢ ((W \in LVec \land (A \subseteq V \land Y \in V \land X \in (N (A \cup \{Y\}) ∖ N (A)))) \land (r \in {Base}_{Scalar (W)} \land X +_{W} (r \cdot_{W} Y) \in N (A))) \to (r \cdot_{W} Y) +_{W} X = X +_{W} (r \cdot_{W} Y)$
70		ssun1	$⊢ A \subseteq A \cup \{X\}$
71	70	a1i	$⊢ ((W \in LVec \land (A \subseteq V \land Y \in V \land X \in (N (A \cup \{Y\}) ∖ N (A)))) \land (r \in {Base}_{Scalar (W)} \land X +_{W} (r \cdot_{W} Y) \in N (A))) \to A \subseteq A \cup \{X\}$
72	1 3	lspss	$⊢ (W \in LMod \land A \cup \{X\} \subseteq V \land A \subseteq A \cup \{X\}) \to N (A) \subseteq N (A \cup \{X\})$
73	19 60 71 72	syl3anc	$⊢ ((W \in LVec \land (A \subseteq V \land Y \in V \land X \in (N (A \cup \{Y\}) ∖ N (A)))) \land (r \in {Base}_{Scalar (W)} \land X +_{W} (r \cdot_{W} Y) \in N (A))) \to N (A) \subseteq N (A \cup \{X\})$
74	73 39	sseldd	$⊢ ((W \in LVec \land (A \subseteq V \land Y \in V \land X \in (N (A \cup \{Y\}) ∖ N (A)))) \land (r \in {Base}_{Scalar (W)} \land X +_{W} (r \cdot_{W} Y) \in N (A))) \to X +_{W} (r \cdot_{W} Y) \in N (A \cup \{X\})$
75	69 74	eqeltrd	$⊢ ((W \in LVec \land (A \subseteq V \land Y \in V \land X \in (N (A \cup \{Y\}) ∖ N (A)))) \land (r \in {Base}_{Scalar (W)} \land X +_{W} (r \cdot_{W} Y) \in N (A))) \to (r \cdot_{W} Y) +_{W} X \in N (A \cup \{X\})$
76	1 3	lspssid	$⊢ (W \in LMod \land A \cup \{X\} \subseteq V) \to A \cup \{X\} \subseteq N (A \cup \{X\})$
77	19 60 76	syl2anc	$⊢ ((W \in LVec \land (A \subseteq V \land Y \in V \land X \in (N (A \cup \{Y\}) ∖ N (A)))) \land (r \in {Base}_{Scalar (W)} \land X +_{W} (r \cdot_{W} Y) \in N (A))) \to A \cup \{X\} \subseteq N (A \cup \{X\})$
78		snidg	$⊢ X \in V \to X \in \{X\}$
79		elun2	$⊢ X \in \{X\} \to X \in (A \cup \{X\})$
80	33 78 79	3syl	$⊢ ((W \in LVec \land (A \subseteq V \land Y \in V \land X \in (N (A \cup \{Y\}) ∖ N (A)))) \land (r \in {Base}_{Scalar (W)} \land X +_{W} (r \cdot_{W} Y) \in N (A))) \to X \in (A \cup \{X\})$
81	77 80	sseldd	$⊢ ((W \in LVec \land (A \subseteq V \land Y \in V \land X \in (N (A \cup \{Y\}) ∖ N (A)))) \land (r \in {Base}_{Scalar (W)} \land X +_{W} (r \cdot_{W} Y) \in N (A))) \to X \in N (A \cup \{X\})$
82	65 2	lssvsubcl	$⊢ ((W \in LMod \land N (A \cup \{X\}) \in S) \land ((r \cdot_{W} Y) +_{W} X \in N (A \cup \{X\}) \land X \in N (A \cup \{X\}))) \to ((r \cdot_{W} Y) +_{W} X) -_{W} X \in N (A \cup \{X\})$
83	19 62 75 81 82	syl22anc	$⊢ ((W \in LVec \land (A \subseteq V \land Y \in V \land X \in (N (A \cup \{Y\}) ∖ N (A)))) \land (r \in {Base}_{Scalar (W)} \land X +_{W} (r \cdot_{W} Y) \in N (A))) \to ((r \cdot_{W} Y) +_{W} X) -_{W} X \in N (A \cup \{X\})$
84	67 83	eqeltrrd	$⊢ ((W \in LVec \land (A \subseteq V \land Y \in V \land X \in (N (A \cup \{Y\}) ∖ N (A)))) \land (r \in {Base}_{Scalar (W)} \land X +_{W} (r \cdot_{W} Y) \in N (A))) \to r \cdot_{W} Y \in N (A \cup \{X\})$
85	4 7 5 2	lssvscl	$⊢ ((W \in LMod \land N (A \cup \{X\}) \in S) \land ({inv}_{r} (Scalar (W)) (r) \in {Base}_{Scalar (W)} \land r \cdot_{W} Y \in N (A \cup \{X\}))) \to {inv}_{r} (Scalar (W)) (r) \cdot_{W} (r \cdot_{W} Y) \in N (A \cup \{X\})$
86	19 62 53 84 85	syl22anc	$⊢ ((W \in LVec \land (A \subseteq V \land Y \in V \land X \in (N (A \cup \{Y\}) ∖ N (A)))) \land (r \in {Base}_{Scalar (W)} \land X +_{W} (r \cdot_{W} Y) \in N (A))) \to {inv}_{r} (Scalar (W)) (r) \cdot_{W} (r \cdot_{W} Y) \in N (A \cup \{X\})$
87	58 86	eqeltrrd	$⊢ ((W \in LVec \land (A \subseteq V \land Y \in V \land X \in (N (A \cup \{Y\}) ∖ N (A)))) \land (r \in {Base}_{Scalar (W)} \land X +_{W} (r \cdot_{W} Y) \in N (A))) \to Y \in N (A \cup \{X\})$
88	15 87	rexlimddv	$⊢ (W \in LVec \land (A \subseteq V \land Y \in V \land X \in (N (A \cup \{Y\}) ∖ N (A)))) \to Y \in N (A \cup \{X\})$

Metamath Proof Explorer

Theorem lspsolv

Proof