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

Theorem lspexch 16203
 Description: Exchange property for span of a pair. TODO: see if a version with Y,Z and X,Z reversed will shorten proofs (analogous to lspexchn1 16204 vs. lspexchn2 16205); look for lspexch 16203 and prcom 3884 in same proof. TODO: would a hypothesis of instead of { Z } ) ` be better overall? This would be shorter and also satisfy the condition. Here and also lspindp* and all proofs affected by them (all in NM's mathbox); there are 58 hypotheses with the pattern as of 24-May-2015. (Contributed by NM, 11-Apr-2015.)
Hypotheses
Ref Expression
lspexch.v
lspexch.o
lspexch.n
lspexch.w
lspexch.x
lspexch.y
lspexch.z
lspexch.q
lspexch.e
Assertion
Ref Expression
lspexch

Proof of Theorem lspexch
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 lspexch.e . . 3
2 lspexch.v . . . 4
3 eqid 2438 . . . 4
4 eqid 2438 . . . 4 Scalar Scalar
5 eqid 2438 . . . 4 Scalar Scalar
6 eqid 2438 . . . 4
7 lspexch.n . . . 4
8 lspexch.w . . . . 5
9 lveclmod 16180 . . . . 5
108, 9syl 16 . . . 4
11 lspexch.y . . . 4
12 lspexch.z . . . 4
132, 3, 4, 5, 6, 7, 10, 11, 12lspprel 16168 . . 3 Scalar Scalar
141, 13mpbid 203 . 2 Scalar Scalar
15 eqid 2438 . . . . . . . 8
16 eqid 2438 . . . . . . . 8 Scalar Scalar
1783ad2ant1 979 . . . . . . . . 9 Scalar Scalar
1817, 9syl 16 . . . . . . . 8 Scalar Scalar
19 simp2r 985 . . . . . . . 8 Scalar Scalar Scalar
20 lspexch.x . . . . . . . . . 10
21203ad2ant1 979 . . . . . . . . 9 Scalar Scalar
2221eldifad 3334 . . . . . . . 8 Scalar Scalar
23123ad2ant1 979 . . . . . . . 8 Scalar Scalar
242, 3, 15, 6, 4, 5, 16, 18, 19, 22, 23lmodsubvs 16002 . . . . . . 7 Scalar Scalar Scalar
25 simp3 960 . . . . . . . . 9 Scalar Scalar
2625eqcomd 2443 . . . . . . . 8 Scalar Scalar
27103ad2ant1 979 . . . . . . . . . 10 Scalar Scalar
28 lmodgrp 15959 . . . . . . . . . 10
2927, 28syl 16 . . . . . . . . 9 Scalar Scalar
302, 4, 6, 5lmodvscl 15969 . . . . . . . . . 10 Scalar
3118, 19, 23, 30syl3anc 1185 . . . . . . . . 9 Scalar Scalar
32 simp2l 984 . . . . . . . . . 10 Scalar Scalar Scalar
33113ad2ant1 979 . . . . . . . . . 10 Scalar Scalar
342, 4, 6, 5lmodvscl 15969 . . . . . . . . . 10 Scalar
3518, 32, 33, 34syl3anc 1185 . . . . . . . . 9 Scalar Scalar
362, 3, 15grpsubadd 14878 . . . . . . . . 9
3729, 22, 31, 35, 36syl13anc 1187 . . . . . . . 8 Scalar Scalar
3826, 37mpbird 225 . . . . . . 7 Scalar Scalar
3924, 38eqtr3d 2472 . . . . . 6 Scalar Scalar Scalar
40 eqid 2438 . . . . . . 7 Scalar Scalar
41 eqid 2438 . . . . . . 7 Scalar Scalar
42 lspexch.q . . . . . . . . . 10
43423ad2ant1 979 . . . . . . . . 9 Scalar Scalar
44 lspexch.o . . . . . . . . . . . 12
4517adantr 453 . . . . . . . . . . . 12 Scalar Scalar Scalar
4623adantr 453 . . . . . . . . . . . 12 Scalar Scalar Scalar
4725adantr 453 . . . . . . . . . . . . . 14 Scalar Scalar Scalar
48 oveq1 6090 . . . . . . . . . . . . . . . 16 Scalar Scalar
4948oveq1d 6098 . . . . . . . . . . . . . . 15 Scalar Scalar
502, 4, 6, 40, 44lmod0vs 15985 . . . . . . . . . . . . . . . . . 18 Scalar
5118, 33, 50syl2anc 644 . . . . . . . . . . . . . . . . 17 Scalar Scalar Scalar
5251oveq1d 6098 . . . . . . . . . . . . . . . 16 Scalar Scalar Scalar
532, 3, 44lmod0vlid 15982 . . . . . . . . . . . . . . . . 17
5418, 31, 53syl2anc 644 . . . . . . . . . . . . . . . 16 Scalar Scalar
5552, 54eqtrd 2470 . . . . . . . . . . . . . . 15 Scalar Scalar Scalar
5649, 55sylan9eqr 2492 . . . . . . . . . . . . . 14 Scalar Scalar Scalar
5747, 56eqtrd 2470 . . . . . . . . . . . . 13 Scalar Scalar Scalar
582, 6, 4, 5, 7, 18, 19, 23lspsneli 16079 . . . . . . . . . . . . . 14 Scalar Scalar
5958adantr 453 . . . . . . . . . . . . 13 Scalar Scalar Scalar
6057, 59eqeltrd 2512 . . . . . . . . . . . 12 Scalar Scalar Scalar
61 eldifsni 3930 . . . . . . . . . . . . . 14
6221, 61syl 16 . . . . . . . . . . . . 13 Scalar Scalar
6362adantr 453 . . . . . . . . . . . 12 Scalar Scalar Scalar
642, 44, 7, 45, 46, 60, 63lspsneleq 16189 . . . . . . . . . . 11 Scalar Scalar Scalar
6564ex 425 . . . . . . . . . 10 Scalar Scalar Scalar
6665necon3d 2641 . . . . . . . . 9 Scalar Scalar Scalar
6743, 66mpd 15 . . . . . . . 8 Scalar Scalar Scalar
68 eldifsn 3929 . . . . . . . 8 Scalar Scalar Scalar Scalar
6932, 67, 68sylanbrc 647 . . . . . . 7 Scalar Scalar Scalar Scalar
704lmodfgrp 15961 . . . . . . . . . . 11 Scalar
7127, 70syl 16 . . . . . . . . . 10 Scalar Scalar Scalar
725, 16grpinvcl 14852 . . . . . . . . . 10 Scalar Scalar Scalar Scalar
7371, 19, 72syl2anc 644 . . . . . . . . 9 Scalar Scalar Scalar Scalar
742, 4, 6, 5lmodvscl 15969 . . . . . . . . 9 Scalar Scalar Scalar
7518, 73, 23, 74syl3anc 1185 . . . . . . . 8 Scalar Scalar Scalar
762, 3lmodvacl 15966 . . . . . . . 8 Scalar Scalar
7718, 22, 75, 76syl3anc 1185 . . . . . . 7 Scalar Scalar Scalar
782, 6, 4, 5, 40, 41, 17, 69, 77, 33lvecinv 16187 . . . . . 6 Scalar Scalar Scalar Scalar Scalar
7939, 78mpbid 203 . . . . 5 Scalar Scalar Scalar Scalar
80 eqid 2438 . . . . . . 7
812, 80, 7, 18, 22, 23lspprcl 16056 . . . . . 6 Scalar Scalar
824lvecdrng 16179 . . . . . . . 8 Scalar
8317, 82syl 16 . . . . . . 7 Scalar Scalar Scalar
845, 40, 41drnginvrcl 15854 . . . . . . 7 Scalar Scalar Scalar Scalar Scalar
8583, 32, 67, 84syl3anc 1185 . . . . . 6 Scalar Scalar Scalar Scalar
86 eqid 2438 . . . . . . . . . 10 Scalar Scalar
872, 4, 6, 86lmodvs1 15980 . . . . . . . . 9 Scalar
8818, 22, 87syl2anc 644 . . . . . . . 8 Scalar Scalar Scalar
8988oveq1d 6098 . . . . . . 7 Scalar Scalar Scalar Scalar Scalar
904lmodrng 15960 . . . . . . . . 9 Scalar
915, 86rngidcl 15686 . . . . . . . . 9 Scalar Scalar Scalar
9218, 90, 913syl 19 . . . . . . . 8 Scalar Scalar Scalar Scalar
932, 3, 6, 4, 5, 7, 18, 92, 73, 22, 23lsppreli 16164 . . . . . . 7 Scalar Scalar Scalar Scalar
9489, 93eqeltrrd 2513 . . . . . 6 Scalar Scalar Scalar
954, 6, 5, 80lssvscl 16033 . . . . . 6 Scalar Scalar Scalar Scalar Scalar
9618, 81, 85, 94, 95syl22anc 1186 . . . . 5 Scalar Scalar Scalar Scalar
9779, 96eqeltrd 2512 . . . 4 Scalar Scalar
98973exp 1153 . . 3 Scalar Scalar
9998rexlimdvv 2838 . 2 Scalar Scalar
10014, 99mpd 15 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 178   wa 360   w3a 937   wceq 1653   wcel 1726   wne 2601  wrex 2708   cdif 3319  csn 3816  cpr 3817  cfv 5456  (class class class)co 6083  cbs 13471   cplusg 13531  Scalarcsca 13534  cvsca 13535  c0g 13725  cgrp 14687  cminusg 14688  csg 14690  crg 15662  cur 15664  cinvr 15778  cdr 15837  clmod 15952  clss 16010  clspn 16049  clvec 16176 This theorem is referenced by:  lspexchn1  16204  lspindp1  16207  mapdh8ab  32637  mapdh8ad  32639  mapdh8b  32640  mapdh8c  32641  mapdh8e  32644 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-13 1728  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-rep 4322  ax-sep 4332  ax-nul 4340  ax-pow 4379  ax-pr 4405  ax-un 4703  ax-cnex 9048  ax-resscn 9049  ax-1cn 9050  ax-icn 9051  ax-addcl 9052  ax-addrcl 9053  ax-mulcl 9054  ax-mulrcl 9055  ax-mulcom 9056  ax-addass 9057  ax-mulass 9058  ax-distr 9059  ax-i2m1 9060  ax-1ne0 9061  ax-1rid 9062  ax-rnegex 9063  ax-rrecex 9064  ax-cnre 9065  ax-pre-lttri 9066  ax-pre-lttrn 9067  ax-pre-ltadd 9068  ax-pre-mulgt0 9069 This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 938  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2287  df-mo 2288  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-nel 2604  df-ral 2712  df-rex 2713  df-reu 2714  df-rmo 2715  df-rab 2716  df-v 2960  df-sbc 3164  df-csb 3254  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-pss 3338  df-nul 3631  df-if 3742  df-pw 3803  df-sn 3822  df-pr 3823  df-tp 3824  df-op 3825  df-uni 4018  df-int 4053  df-iun 4097  df-br 4215  df-opab 4269  df-mpt 4270  df-tr 4305  df-eprel 4496  df-id 4500  df-po 4505  df-so 4506  df-fr 4543  df-we 4545  df-ord 4586  df-on 4587  df-lim 4588  df-suc 4589  df-om 4848  df-xp 4886  df-rel 4887  df-cnv 4888  df-co 4889  df-dm 4890  df-rn 4891  df-res 4892  df-ima 4893  df-iota 5420  df-fun 5458  df-fn 5459  df-f 5460  df-f1 5461  df-fo 5462  df-f1o 5463  df-fv 5464  df-ov 6086  df-oprab 6087  df-mpt2 6088  df-1st 6351  df-2nd 6352  df-tpos 6481  df-riota 6551  df-recs 6635  df-rdg 6670  df-er 6907  df-en 7112  df-dom 7113  df-sdom 7114  df-pnf 9124  df-mnf 9125  df-xr 9126  df-ltxr 9127  df-le 9128  df-sub 9295  df-neg 9296  df-nn 10003  df-2 10060  df-3 10061  df-ndx 13474  df-slot 13475  df-base 13476  df-sets 13477  df-ress 13478  df-plusg 13544  df-mulr 13545  df-0g 13729  df-mnd 14692  df-submnd 14741  df-grp 14814  df-minusg 14815  df-sbg 14816  df-subg 14943  df-cntz 15118  df-lsm 15272  df-cmn 15416  df-abl 15417  df-mgp 15651  df-rng 15665  df-ur 15667  df-oppr 15730  df-dvdsr 15748  df-unit 15749  df-invr 15779  df-drng 15839  df-lmod 15954  df-lss 16011  df-lsp 16050  df-lvec 16177
 Copyright terms: Public domain W3C validator