Metamath Proof Explorer


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