Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  lspfixed Structured version   Unicode version

Theorem lspfixed 18094
 Description: Show membership in the span of the sum of two vectors, one of which () is fixed in advance. (Contributed by NM, 27-May-2015.)
Hypotheses
Ref Expression
lspfixed.v
lspfixed.p
lspfixed.o
lspfixed.n
lspfixed.w
lspfixed.x
lspfixed.y
lspfixed.z
lspfixed.e
lspfixed.f
lspfixed.g
Assertion
Ref Expression
lspfixed
Distinct variable groups:   ,   ,   ,   ,   ,   ,   ,
Allowed substitution hints:   ()   ()

Proof of Theorem lspfixed
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 lspfixed.g . . 3
2 lspfixed.v . . . 4
3 lspfixed.p . . . 4
4 eqid 2402 . . . 4 Scalar Scalar
5 eqid 2402 . . . 4 Scalar Scalar
6 eqid 2402 . . . 4
7 lspfixed.n . . . 4
8 lspfixed.w . . . . 5
9 lveclmod 18072 . . . . 5
108, 9syl 17 . . . 4
11 lspfixed.y . . . 4
12 lspfixed.z . . . 4
132, 3, 4, 5, 6, 7, 10, 11, 12lspprel 18060 . . 3 Scalar Scalar
141, 13mpbid 210 . 2 Scalar Scalar
15103ad2ant1 1018 . . . . . . 7 Scalar Scalar
16 eqid 2402 . . . . . . . . . 10
172, 16, 7lspsncl 17943 . . . . . . . . 9
1810, 12, 17syl2anc 659 . . . . . . . 8
19183ad2ant1 1018 . . . . . . 7 Scalar Scalar
2083ad2ant1 1018 . . . . . . . . 9 Scalar Scalar
214lvecdrng 18071 . . . . . . . . 9 Scalar
2220, 21syl 17 . . . . . . . 8 Scalar Scalar Scalar
23 simp2l 1023 . . . . . . . 8 Scalar Scalar Scalar
24 lspfixed.f . . . . . . . . . 10
25243ad2ant1 1018 . . . . . . . . 9 Scalar Scalar
26 simpl3 1002 . . . . . . . . . . . . 13 Scalar Scalar Scalar
27 simpr 459 . . . . . . . . . . . . . . . 16 Scalar Scalar Scalar Scalar
2827oveq1d 6293 . . . . . . . . . . . . . . 15 Scalar Scalar Scalar Scalar
29 simpl1 1000 . . . . . . . . . . . . . . . . 17 Scalar Scalar Scalar
3029, 10syl 17 . . . . . . . . . . . . . . . 16 Scalar Scalar Scalar
3129, 11syl 17 . . . . . . . . . . . . . . . 16 Scalar Scalar Scalar
32 eqid 2402 . . . . . . . . . . . . . . . . 17 Scalar Scalar
33 lspfixed.o . . . . . . . . . . . . . . . . 17
342, 4, 6, 32, 33lmod0vs 17865 . . . . . . . . . . . . . . . 16 Scalar
3530, 31, 34syl2anc 659 . . . . . . . . . . . . . . 15 Scalar Scalar Scalar Scalar
3628, 35eqtrd 2443 . . . . . . . . . . . . . 14 Scalar Scalar Scalar
3736oveq1d 6293 . . . . . . . . . . . . 13 Scalar Scalar Scalar
38 simp2r 1024 . . . . . . . . . . . . . . . 16 Scalar Scalar Scalar
39123ad2ant1 1018 . . . . . . . . . . . . . . . 16 Scalar Scalar
402, 4, 6, 5lmodvscl 17849 . . . . . . . . . . . . . . . 16 Scalar
4115, 38, 39, 40syl3anc 1230 . . . . . . . . . . . . . . 15 Scalar Scalar
4241adantr 463 . . . . . . . . . . . . . 14 Scalar Scalar Scalar
432, 3, 33lmod0vlid 17862 . . . . . . . . . . . . . 14
4430, 42, 43syl2anc 659 . . . . . . . . . . . . 13 Scalar Scalar Scalar
4526, 37, 443eqtrd 2447 . . . . . . . . . . . 12 Scalar Scalar Scalar
4629, 18syl 17 . . . . . . . . . . . . 13 Scalar Scalar Scalar
47 simpl2r 1051 . . . . . . . . . . . . 13 Scalar Scalar Scalar Scalar
482, 7lspsnid 17959 . . . . . . . . . . . . . . 15
4910, 12, 48syl2anc 659 . . . . . . . . . . . . . 14
5029, 49syl 17 . . . . . . . . . . . . 13 Scalar Scalar Scalar
514, 6, 5, 16lssvscl 17921 . . . . . . . . . . . . 13 Scalar
5230, 46, 47, 50, 51syl22anc 1231 . . . . . . . . . . . 12 Scalar Scalar Scalar
5345, 52eqeltrd 2490 . . . . . . . . . . 11 Scalar Scalar Scalar
5453ex 432 . . . . . . . . . 10 Scalar Scalar Scalar
5554necon3bd 2615 . . . . . . . . 9 Scalar Scalar Scalar
5625, 55mpd 15 . . . . . . . 8 Scalar Scalar Scalar
57 eqid 2402 . . . . . . . . 9 Scalar Scalar
585, 32, 57drnginvrcl 17733 . . . . . . . 8 Scalar Scalar Scalar Scalar Scalar
5922, 23, 56, 58syl3anc 1230 . . . . . . 7 Scalar Scalar Scalar Scalar
60493ad2ant1 1018 . . . . . . . 8 Scalar Scalar
6115, 19, 38, 60, 51syl22anc 1231 . . . . . . 7 Scalar Scalar
624, 6, 5, 16lssvscl 17921 . . . . . . 7 Scalar Scalar Scalar
6315, 19, 59, 61, 62syl22anc 1231 . . . . . 6 Scalar Scalar Scalar
645, 32, 57drnginvrn0 17734 . . . . . . . 8 Scalar Scalar Scalar Scalar Scalar
6522, 23, 56, 64syl3anc 1230 . . . . . . 7 Scalar Scalar Scalar Scalar
66 lspfixed.e . . . . . . . . . 10
67663ad2ant1 1018 . . . . . . . . 9 Scalar Scalar
68 simpl3 1002 . . . . . . . . . . . . 13 Scalar Scalar Scalar
69 oveq1 6285 . . . . . . . . . . . . . . 15 Scalar Scalar
702, 4, 6, 32, 33lmod0vs 17865 . . . . . . . . . . . . . . . 16 Scalar
7115, 39, 70syl2anc 659 . . . . . . . . . . . . . . 15 Scalar Scalar Scalar
7269, 71sylan9eqr 2465 . . . . . . . . . . . . . 14 Scalar Scalar Scalar
7372oveq2d 6294 . . . . . . . . . . . . 13 Scalar Scalar Scalar
74113ad2ant1 1018 . . . . . . . . . . . . . . . 16 Scalar Scalar
752, 4, 6, 5lmodvscl 17849 . . . . . . . . . . . . . . . 16 Scalar
7615, 23, 74, 75syl3anc 1230 . . . . . . . . . . . . . . 15 Scalar Scalar
772, 3, 33lmod0vrid 17863 . . . . . . . . . . . . . . 15
7815, 76, 77syl2anc 659 . . . . . . . . . . . . . 14 Scalar Scalar
7978adantr 463 . . . . . . . . . . . . 13 Scalar Scalar Scalar
8068, 73, 793eqtrd 2447 . . . . . . . . . . . 12 Scalar Scalar Scalar
812, 16, 7lspsncl 17943 . . . . . . . . . . . . . . . 16
8210, 11, 81syl2anc 659 . . . . . . . . . . . . . . 15
83823ad2ant1 1018 . . . . . . . . . . . . . 14 Scalar Scalar
842, 7lspsnid 17959 . . . . . . . . . . . . . . . 16
8510, 11, 84syl2anc 659 . . . . . . . . . . . . . . 15
86853ad2ant1 1018 . . . . . . . . . . . . . 14 Scalar Scalar
874, 6, 5, 16lssvscl 17921 . . . . . . . . . . . . . 14 Scalar
8815, 83, 23, 86, 87syl22anc 1231 . . . . . . . . . . . . 13 Scalar Scalar
8988adantr 463 . . . . . . . . . . . 12 Scalar Scalar Scalar
9080, 89eqeltrd 2490 . . . . . . . . . . 11 Scalar Scalar Scalar
9190ex 432 . . . . . . . . . 10 Scalar Scalar Scalar
9291necon3bd 2615 . . . . . . . . 9 Scalar Scalar Scalar
9367, 92mpd 15 . . . . . . . 8 Scalar Scalar Scalar
94 simpl1 1000 . . . . . . . . . . . . 13 Scalar Scalar
9594, 1syl 17 . . . . . . . . . . . 12 Scalar Scalar
96 preq2 4052 . . . . . . . . . . . . . 14
9796fveq2d 5853 . . . . . . . . . . . . 13
982, 33, 7, 15, 74lsppr0 18058 . . . . . . . . . . . . 13 Scalar Scalar
9997, 98sylan9eqr 2465 . . . . . . . . . . . 12 Scalar Scalar
10095, 99eleqtrd 2492 . . . . . . . . . . 11 Scalar Scalar
101100ex 432 . . . . . . . . . 10 Scalar Scalar
102101necon3bd 2615 . . . . . . . . 9 Scalar Scalar
10367, 102mpd 15 . . . . . . . 8 Scalar Scalar
1042, 6, 4, 5, 32, 33, 20, 38, 39lvecvsn0 18075 . . . . . . . 8 Scalar Scalar Scalar
10593, 103, 104mpbir2and 923 . . . . . . 7 Scalar Scalar
1062, 6, 4, 5, 32, 33, 20, 59, 41lvecvsn0 18075 . . . . . . 7 Scalar Scalar Scalar Scalar Scalar
10765, 105, 106mpbir2and 923 . . . . . 6 Scalar Scalar Scalar
108 eldifsn 4097 . . . . . 6 Scalar Scalar Scalar
10963, 107, 108sylanbrc 662 . . . . 5 Scalar Scalar Scalar
110 simp3 999 . . . . . . 7 Scalar Scalar
1112, 3lmodvacl 17846 . . . . . . . . 9
11215, 76, 41, 111syl3anc 1230 . . . . . . . 8 Scalar Scalar
1132, 7lspsnid 17959 . . . . . . . 8
11415, 112, 113syl2anc 659 . . . . . . 7 Scalar Scalar
115110, 114eqeltrd 2490 . . . . . 6 Scalar Scalar
1162, 4, 6, 5, 32, 7lspsnvs 18080 . . . . . . . 8 Scalar Scalar Scalar Scalar Scalar
11720, 59, 65, 112, 116syl121anc 1235 . . . . . . 7 Scalar Scalar Scalar
1182, 3, 4, 6, 5lmodvsdi 17855 . . . . . . . . . . 11 Scalar Scalar Scalar Scalar Scalar
11915, 59, 76, 41, 118syl13anc 1232 . . . . . . . . . 10 Scalar Scalar Scalar Scalar Scalar
120 eqid 2402 . . . . . . . . . . . . . . 15 Scalar Scalar
121 eqid 2402 . . . . . . . . . . . . . . 15 Scalar Scalar
1225, 32, 120, 121, 57drnginvrl 17735 . . . . . . . . . . . . . 14 Scalar Scalar Scalar ScalarScalar Scalar
12322, 23, 56, 122syl3anc 1230 . . . . . . . . . . . . 13 Scalar Scalar ScalarScalar Scalar
124123oveq1d 6293 . . . . . . . . . . . 12 Scalar Scalar ScalarScalar Scalar
1252, 4, 6, 5, 120lmodvsass 17857 . . . . . . . . . . . . 13 Scalar Scalar Scalar ScalarScalar Scalar
12615, 59, 23, 74, 125syl13anc 1232 . . . . . . . . . . . 12 Scalar Scalar ScalarScalar Scalar
1272, 4, 6, 121lmodvs1 17860 . . . . . . . . . . . . 13 Scalar
12815, 74, 127syl2anc 659 . . . . . . . . . . . 12 Scalar Scalar Scalar
129124, 126, 1283eqtr3d 2451 . . . . . . . . . . 11 Scalar Scalar Scalar
130129oveq1d 6293 . . . . . . . . . 10 Scalar Scalar Scalar Scalar Scalar
131119, 130eqtrd 2443 . . . . . . . . 9 Scalar Scalar Scalar Scalar
132131sneqd 3984 . . . . . . . 8 Scalar Scalar Scalar Scalar
133132fveq2d 5853 . . . . . . 7 Scalar Scalar Scalar Scalar
134117, 133eqtr3d 2445 . . . . . 6 Scalar Scalar Scalar
135115, 134eleqtrd 2492 . . . . 5 Scalar Scalar Scalar
136 oveq2 6286 . . . . . . . . 9 Scalar Scalar
137136sneqd 3984 . . . . . . . 8 Scalar Scalar
138137fveq2d 5853 . . . . . . 7 Scalar Scalar
139138eleq2d 2472 . . . . . 6 Scalar Scalar
140139rspcev 3160 . . . . 5 Scalar Scalar
141109, 135, 140syl2anc 659 . . . 4 Scalar Scalar
1421413exp 1196 . . 3 Scalar Scalar
143142rexlimdvv 2902 . 2 Scalar Scalar
14414, 143mpd 15 1
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wa 367   w3a 974   wceq 1405   wcel 1842   wne 2598  wrex 2755   cdif 3411  csn 3972  cpr 3974  cfv 5569  (class class class)co 6278  cbs 14841   cplusg 14909  cmulr 14910  Scalarcsca 14912  cvsca 14913  c0g 15054  cur 17473  cinvr 17640  cdr 17716  clmod 17832  clss 17898  clspn 17937  clvec 18068 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-8 1844  ax-9 1846  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-rep 4507  ax-sep 4517  ax-nul 4525  ax-pow 4572  ax-pr 4630  ax-un 6574  ax-cnex 9578  ax-resscn 9579  ax-1cn 9580  ax-icn 9581  ax-addcl 9582  ax-addrcl 9583  ax-mulcl 9584  ax-mulrcl 9585  ax-mulcom 9586  ax-addass 9587  ax-mulass 9588  ax-distr 9589  ax-i2m1 9590  ax-1ne0 9591  ax-1rid 9592  ax-rnegex 9593  ax-rrecex 9594  ax-cnre 9595  ax-pre-lttri 9596  ax-pre-lttrn 9597  ax-pre-ltadd 9598  ax-pre-mulgt0 9599 This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 975  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-eu 2242  df-mo 2243  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ne 2600  df-nel 2601  df-ral 2759  df-rex 2760  df-reu 2761  df-rmo 2762  df-rab 2763  df-v 3061  df-sbc 3278  df-csb 3374  df-dif 3417  df-un 3419  df-in 3421  df-ss 3428  df-pss 3430  df-nul 3739  df-if 3886  df-pw 3957  df-sn 3973  df-pr 3975  df-tp 3977  df-op 3979  df-uni 4192  df-int 4228  df-iun 4273  df-br 4396  df-opab 4454  df-mpt 4455  df-tr 4490  df-eprel 4734  df-id 4738  df-po 4744  df-so 4745  df-fr 4782  df-we 4784  df-xp 4829  df-rel 4830  df-cnv 4831  df-co 4832  df-dm 4833  df-rn 4834  df-res 4835  df-ima 4836  df-pred 5367  df-ord 5413  df-on 5414  df-lim 5415  df-suc 5416  df-iota 5533  df-fun 5571  df-fn 5572  df-f 5573  df-f1 5574  df-fo 5575  df-f1o 5576  df-fv 5577  df-riota 6240  df-ov 6281  df-oprab 6282  df-mpt2 6283  df-om 6684  df-1st 6784  df-2nd 6785  df-tpos 6958  df-wrecs 7013  df-recs 7075  df-rdg 7113  df-er 7348  df-en 7555  df-dom 7556  df-sdom 7557  df-pnf 9660  df-mnf 9661  df-xr 9662  df-ltxr 9663  df-le 9664  df-sub 9843  df-neg 9844  df-nn 10577  df-2 10635  df-3 10636  df-ndx 14844  df-slot 14845  df-base 14846  df-sets 14847  df-ress 14848  df-plusg 14922  df-mulr 14923  df-0g 15056  df-mgm 16196  df-sgrp 16235  df-mnd 16245  df-submnd 16291  df-grp 16381  df-minusg 16382  df-sbg 16383  df-subg 16522  df-cntz 16679  df-lsm 16980  df-cmn 17124  df-abl 17125  df-mgp 17462  df-ur 17474  df-ring 17520  df-oppr 17592  df-dvdsr 17610  df-unit 17611  df-invr 17641  df-drng 17718  df-lmod 17834  df-lss 17899  df-lsp 17938  df-lvec 18069 This theorem is referenced by:  lsatfixedN  32027
 Copyright terms: Public domain W3C validator