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=BaseW
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=BaseW
2 lspsolv.s ⊢S=LSubSp⁡W
3 lspsolv.n ⊢N=LSpan⁡W
4 eqid ⊢Scalar⁡W=Scalar⁡W
5 eqid ⊢BaseScalar⁡W=BaseScalar⁡W
6 eqid ⊢+W=+W
7 eqid ⊢⋅W=⋅W
8 eqid ⊢z∈V|∃r∈BaseScalar⁡Wz+Wr⋅WY∈N⁡A=z∈V|∃r∈BaseScalar⁡Wz+Wr⋅WY∈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∈BaseScalar⁡WX+Wr⋅WY∈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∈BaseScalar⁡W∧X+Wr⋅WY∈N⁡A→Scalar⁡W∈DivRing
18 simprl ⊢W∈LVec∧A⊆V∧Y∈V∧X∈N⁡A∪Y∖N⁡A∧r∈BaseScalar⁡W∧X+Wr⋅WY∈N⁡A→r∈BaseScalar⁡W
19 10 adantr ⊢W∈LVec∧A⊆V∧Y∈V∧X∈N⁡A∪Y∖N⁡A∧r∈BaseScalar⁡W∧X+Wr⋅WY∈N⁡A→W∈LMod
20 12 adantr ⊢W∈LVec∧A⊆V∧Y∈V∧X∈N⁡A∪Y∖N⁡A∧r∈BaseScalar⁡W∧X+Wr⋅WY∈N⁡A→Y∈V
21 eqid ⊢0Scalar⁡W=0Scalar⁡W
22 eqid ⊢0W=0W
23 1 4 7 21 22 lmod0vs ⊢W∈LMod∧Y∈V→0Scalar⁡W⋅WY=0W
24 19 20 23 syl2anc ⊢W∈LVec∧A⊆V∧Y∈V∧X∈N⁡A∪Y∖N⁡A∧r∈BaseScalar⁡W∧X+Wr⋅WY∈N⁡A→0Scalar⁡W⋅WY=0W
25 24 oveq2d ⊢W∈LVec∧A⊆V∧Y∈V∧X∈N⁡A∪Y∖N⁡A∧r∈BaseScalar⁡W∧X+Wr⋅WY∈N⁡A→X+W0Scalar⁡W⋅WY=X+W0W
26 11 adantr ⊢W∈LVec∧A⊆V∧Y∈V∧X∈N⁡A∪Y∖N⁡A∧r∈BaseScalar⁡W∧X+Wr⋅WY∈N⁡A→A⊆V
27 20 snssd ⊢W∈LVec∧A⊆V∧Y∈V∧X∈N⁡A∪Y∖N⁡A∧r∈BaseScalar⁡W∧X+Wr⋅WY∈N⁡A→Y⊆V
28 26 27 unssd ⊢W∈LVec∧A⊆V∧Y∈V∧X∈N⁡A∪Y∖N⁡A∧r∈BaseScalar⁡W∧X+Wr⋅WY∈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∈BaseScalar⁡W∧X+Wr⋅WY∈N⁡A→N⁡A∪Y⊆V
31 30 ssdifssd ⊢W∈LVec∧A⊆V∧Y∈V∧X∈N⁡A∪Y∖N⁡A∧r∈BaseScalar⁡W∧X+Wr⋅WY∈N⁡A→N⁡A∪Y∖N⁡A⊆V
32 13 adantr ⊢W∈LVec∧A⊆V∧Y∈V∧X∈N⁡A∪Y∖N⁡A∧r∈BaseScalar⁡W∧X+Wr⋅WY∈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∈BaseScalar⁡W∧X+Wr⋅WY∈N⁡A→X∈V
34 1 6 22 lmod0vrid ⊢W∈LMod∧X∈V→X+W0W=X
35 19 33 34 syl2anc ⊢W∈LVec∧A⊆V∧Y∈V∧X∈N⁡A∪Y∖N⁡A∧r∈BaseScalar⁡W∧X+Wr⋅WY∈N⁡A→X+W0W=X
36 25 35 eqtrd ⊢W∈LVec∧A⊆V∧Y∈V∧X∈N⁡A∪Y∖N⁡A∧r∈BaseScalar⁡W∧X+Wr⋅WY∈N⁡A→X+W0Scalar⁡W⋅WY=X
37 36 32 eqeltrd ⊢W∈LVec∧A⊆V∧Y∈V∧X∈N⁡A∪Y∖N⁡A∧r∈BaseScalar⁡W∧X+Wr⋅WY∈N⁡A→X+W0Scalar⁡W⋅WY∈N⁡A∪Y∖N⁡A
38 37 eldifbd ⊢W∈LVec∧A⊆V∧Y∈V∧X∈N⁡A∪Y∖N⁡A∧r∈BaseScalar⁡W∧X+Wr⋅WY∈N⁡A→¬X+W0Scalar⁡W⋅WY∈N⁡A
39 simprr ⊢W∈LVec∧A⊆V∧Y∈V∧X∈N⁡A∪Y∖N⁡A∧r∈BaseScalar⁡W∧X+Wr⋅WY∈N⁡A→X+Wr⋅WY∈N⁡A
40 oveq1 ⊢r=0Scalar⁡W→r⋅WY=0Scalar⁡W⋅WY
41 40 oveq2d ⊢r=0Scalar⁡W→X+Wr⋅WY=X+W0Scalar⁡W⋅WY
42 41 eleq1d ⊢r=0Scalar⁡W→X+Wr⋅WY∈N⁡A↔X+W0Scalar⁡W⋅WY∈N⁡A
43 39 42 syl5ibcom ⊢W∈LVec∧A⊆V∧Y∈V∧X∈N⁡A∪Y∖N⁡A∧r∈BaseScalar⁡W∧X+Wr⋅WY∈N⁡A→r=0Scalar⁡W→X+W0Scalar⁡W⋅WY∈N⁡A
44 43 necon3bd ⊢W∈LVec∧A⊆V∧Y∈V∧X∈N⁡A∪Y∖N⁡A∧r∈BaseScalar⁡W∧X+Wr⋅WY∈N⁡A→¬X+W0Scalar⁡W⋅WY∈N⁡A→r≠0Scalar⁡W
45 38 44 mpd ⊢W∈LVec∧A⊆V∧Y∈V∧X∈N⁡A∪Y∖N⁡A∧r∈BaseScalar⁡W∧X+Wr⋅WY∈N⁡A→r≠0Scalar⁡W
46 eqid ⊢⋅Scalar⁡W=⋅Scalar⁡W
47 eqid ⊢1Scalar⁡W=1Scalar⁡W
48 eqid ⊢invr⁡Scalar⁡W=invr⁡Scalar⁡W
49 5 21 46 47 48 drnginvrl ⊢Scalar⁡W∈DivRing∧r∈BaseScalar⁡W∧r≠0Scalar⁡W→invr⁡Scalar⁡W⁡r⋅Scalar⁡Wr=1Scalar⁡W
50 17 18 45 49 syl3anc ⊢W∈LVec∧A⊆V∧Y∈V∧X∈N⁡A∪Y∖N⁡A∧r∈BaseScalar⁡W∧X+Wr⋅WY∈N⁡A→invr⁡Scalar⁡W⁡r⋅Scalar⁡Wr=1Scalar⁡W
51 50 oveq1d ⊢W∈LVec∧A⊆V∧Y∈V∧X∈N⁡A∪Y∖N⁡A∧r∈BaseScalar⁡W∧X+Wr⋅WY∈N⁡A→invr⁡Scalar⁡W⁡r⋅Scalar⁡Wr⋅WY=1Scalar⁡W⋅WY
52 5 21 48 drnginvrcl ⊢Scalar⁡W∈DivRing∧r∈BaseScalar⁡W∧r≠0Scalar⁡W→invr⁡Scalar⁡W⁡r∈BaseScalar⁡W
53 17 18 45 52 syl3anc ⊢W∈LVec∧A⊆V∧Y∈V∧X∈N⁡A∪Y∖N⁡A∧r∈BaseScalar⁡W∧X+Wr⋅WY∈N⁡A→invr⁡Scalar⁡W⁡r∈BaseScalar⁡W
54 1 4 7 5 46 lmodvsass ⊢W∈LMod∧invr⁡Scalar⁡W⁡r∈BaseScalar⁡W∧r∈BaseScalar⁡W∧Y∈V→invr⁡Scalar⁡W⁡r⋅Scalar⁡Wr⋅WY=invr⁡Scalar⁡W⁡r⋅Wr⋅WY
55 19 53 18 20 54 syl13anc ⊢W∈LVec∧A⊆V∧Y∈V∧X∈N⁡A∪Y∖N⁡A∧r∈BaseScalar⁡W∧X+Wr⋅WY∈N⁡A→invr⁡Scalar⁡W⁡r⋅Scalar⁡Wr⋅WY=invr⁡Scalar⁡W⁡r⋅Wr⋅WY
56 1 4 7 47 lmodvs1 ⊢W∈LMod∧Y∈V→1Scalar⁡W⋅WY=Y
57 19 20 56 syl2anc ⊢W∈LVec∧A⊆V∧Y∈V∧X∈N⁡A∪Y∖N⁡A∧r∈BaseScalar⁡W∧X+Wr⋅WY∈N⁡A→1Scalar⁡W⋅WY=Y
58 51 55 57 3eqtr3d ⊢W∈LVec∧A⊆V∧Y∈V∧X∈N⁡A∪Y∖N⁡A∧r∈BaseScalar⁡W∧X+Wr⋅WY∈N⁡A→invr⁡Scalar⁡W⁡r⋅Wr⋅WY=Y
59 33 snssd ⊢W∈LVec∧A⊆V∧Y∈V∧X∈N⁡A∪Y∖N⁡A∧r∈BaseScalar⁡W∧X+Wr⋅WY∈N⁡A→X⊆V
60 26 59 unssd ⊢W∈LVec∧A⊆V∧Y∈V∧X∈N⁡A∪Y∖N⁡A∧r∈BaseScalar⁡W∧X+Wr⋅WY∈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∈BaseScalar⁡W∧X+Wr⋅WY∈N⁡A→N⁡A∪X∈S
63 1 4 7 5 lmodvscl ⊢W∈LMod∧r∈BaseScalar⁡W∧Y∈V→r⋅WY∈V
64 19 18 20 63 syl3anc ⊢W∈LVec∧A⊆V∧Y∈V∧X∈N⁡A∪Y∖N⁡A∧r∈BaseScalar⁡W∧X+Wr⋅WY∈N⁡A→r⋅WY∈V
65 eqid ⊢-W=-W
66 1 6 65 lmodvpncan ⊢W∈LMod∧r⋅WY∈V∧X∈V→r⋅WY+WX-WX=r⋅WY
67 19 64 33 66 syl3anc ⊢W∈LVec∧A⊆V∧Y∈V∧X∈N⁡A∪Y∖N⁡A∧r∈BaseScalar⁡W∧X+Wr⋅WY∈N⁡A→r⋅WY+WX-WX=r⋅WY
68 1 6 lmodcom ⊢W∈LMod∧r⋅WY∈V∧X∈V→r⋅WY+WX=X+Wr⋅WY
69 19 64 33 68 syl3anc ⊢W∈LVec∧A⊆V∧Y∈V∧X∈N⁡A∪Y∖N⁡A∧r∈BaseScalar⁡W∧X+Wr⋅WY∈N⁡A→r⋅WY+WX=X+Wr⋅WY
70 ssun1 ⊢A⊆A∪X
71 70 a1i ⊢W∈LVec∧A⊆V∧Y∈V∧X∈N⁡A∪Y∖N⁡A∧r∈BaseScalar⁡W∧X+Wr⋅WY∈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∈BaseScalar⁡W∧X+Wr⋅WY∈N⁡A→N⁡A⊆N⁡A∪X
74 73 39 sseldd ⊢W∈LVec∧A⊆V∧Y∈V∧X∈N⁡A∪Y∖N⁡A∧r∈BaseScalar⁡W∧X+Wr⋅WY∈N⁡A→X+Wr⋅WY∈N⁡A∪X
75 69 74 eqeltrd ⊢W∈LVec∧A⊆V∧Y∈V∧X∈N⁡A∪Y∖N⁡A∧r∈BaseScalar⁡W∧X+Wr⋅WY∈N⁡A→r⋅WY+WX∈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∈BaseScalar⁡W∧X+Wr⋅WY∈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∈BaseScalar⁡W∧X+Wr⋅WY∈N⁡A→X∈A∪X
81 77 80 sseldd ⊢W∈LVec∧A⊆V∧Y∈V∧X∈N⁡A∪Y∖N⁡A∧r∈BaseScalar⁡W∧X+Wr⋅WY∈N⁡A→X∈N⁡A∪X
82 65 2 lssvsubcl ⊢W∈LMod∧N⁡A∪X∈S∧r⋅WY+WX∈N⁡A∪X∧X∈N⁡A∪X→r⋅WY+WX-WX∈N⁡A∪X
83 19 62 75 81 82 syl22anc ⊢W∈LVec∧A⊆V∧Y∈V∧X∈N⁡A∪Y∖N⁡A∧r∈BaseScalar⁡W∧X+Wr⋅WY∈N⁡A→r⋅WY+WX-WX∈N⁡A∪X
84 67 83 eqeltrrd ⊢W∈LVec∧A⊆V∧Y∈V∧X∈N⁡A∪Y∖N⁡A∧r∈BaseScalar⁡W∧X+Wr⋅WY∈N⁡A→r⋅WY∈N⁡A∪X
85 4 7 5 2 lssvscl ⊢W∈LMod∧N⁡A∪X∈S∧invr⁡Scalar⁡W⁡r∈BaseScalar⁡W∧r⋅WY∈N⁡A∪X→invr⁡Scalar⁡W⁡r⋅Wr⋅WY∈N⁡A∪X
86 19 62 53 84 85 syl22anc ⊢W∈LVec∧A⊆V∧Y∈V∧X∈N⁡A∪Y∖N⁡A∧r∈BaseScalar⁡W∧X+Wr⋅WY∈N⁡A→invr⁡Scalar⁡W⁡r⋅Wr⋅WY∈N⁡A∪X
87 58 86 eqeltrrd ⊢W∈LVec∧A⊆V∧Y∈V∧X∈N⁡A∪Y∖N⁡A∧r∈BaseScalar⁡W∧X+Wr⋅WY∈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