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

Theorem lspexch 17643
 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 17644 vs. lspexchn2 17645); look for lspexch 17643 and prcom 4089 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 2441 . . . 4
4 eqid 2441 . . . 4 Scalar Scalar
5 eqid 2441 . . . 4 Scalar Scalar
6 eqid 2441 . . . 4
7 lspexch.n . . . 4
8 lspexch.w . . . . 5
9 lveclmod 17620 . . . . 5
108, 9syl 16 . . . 4
11 lspexch.y . . . 4
12 lspexch.z . . . 4
132, 3, 4, 5, 6, 7, 10, 11, 12lspprel 17608 . . 3 Scalar Scalar
141, 13mpbid 210 . 2 Scalar Scalar
15 eqid 2441 . . . . . . . 8
16 eqid 2441 . . . . . . . 8 Scalar Scalar
1783ad2ant1 1016 . . . . . . . . 9 Scalar Scalar
1817, 9syl 16 . . . . . . . 8 Scalar Scalar
19 simp2r 1022 . . . . . . . 8 Scalar Scalar Scalar
20 lspexch.x . . . . . . . . . 10
21203ad2ant1 1016 . . . . . . . . 9 Scalar Scalar
2221eldifad 3470 . . . . . . . 8 Scalar Scalar
23123ad2ant1 1016 . . . . . . . 8 Scalar Scalar
242, 3, 15, 6, 4, 5, 16, 18, 19, 22, 23lmodsubvs 17434 . . . . . . 7 Scalar Scalar Scalar
25 simp3 997 . . . . . . . . 9 Scalar Scalar
2625eqcomd 2449 . . . . . . . 8 Scalar Scalar
27103ad2ant1 1016 . . . . . . . . . 10 Scalar Scalar
28 lmodgrp 17387 . . . . . . . . . 10
2927, 28syl 16 . . . . . . . . 9 Scalar Scalar
302, 4, 6, 5lmodvscl 17397 . . . . . . . . . 10 Scalar
3118, 19, 23, 30syl3anc 1227 . . . . . . . . 9 Scalar Scalar
32 simp2l 1021 . . . . . . . . . 10 Scalar Scalar Scalar
33113ad2ant1 1016 . . . . . . . . . 10 Scalar Scalar
342, 4, 6, 5lmodvscl 17397 . . . . . . . . . 10 Scalar
3518, 32, 33, 34syl3anc 1227 . . . . . . . . 9 Scalar Scalar
362, 3, 15grpsubadd 15995 . . . . . . . . 9
3729, 22, 31, 35, 36syl13anc 1229 . . . . . . . 8 Scalar Scalar
3826, 37mpbird 232 . . . . . . 7 Scalar Scalar
3924, 38eqtr3d 2484 . . . . . 6 Scalar Scalar Scalar
40 eqid 2441 . . . . . . 7 Scalar Scalar
41 eqid 2441 . . . . . . 7 Scalar Scalar
42 lspexch.q . . . . . . . . . 10
43423ad2ant1 1016 . . . . . . . . 9 Scalar Scalar
44 lspexch.o . . . . . . . . . . . 12
4517adantr 465 . . . . . . . . . . . 12 Scalar Scalar Scalar
4623adantr 465 . . . . . . . . . . . 12 Scalar Scalar Scalar
4725adantr 465 . . . . . . . . . . . . . 14 Scalar Scalar Scalar
48 oveq1 6284 . . . . . . . . . . . . . . . 16 Scalar Scalar
4948oveq1d 6292 . . . . . . . . . . . . . . 15 Scalar Scalar
502, 4, 6, 40, 44lmod0vs 17413 . . . . . . . . . . . . . . . . . 18 Scalar
5118, 33, 50syl2anc 661 . . . . . . . . . . . . . . . . 17 Scalar Scalar Scalar
5251oveq1d 6292 . . . . . . . . . . . . . . . 16 Scalar Scalar Scalar
532, 3, 44lmod0vlid 17410 . . . . . . . . . . . . . . . . 17
5418, 31, 53syl2anc 661 . . . . . . . . . . . . . . . 16 Scalar Scalar
5552, 54eqtrd 2482 . . . . . . . . . . . . . . 15 Scalar Scalar Scalar
5649, 55sylan9eqr 2504 . . . . . . . . . . . . . 14 Scalar Scalar Scalar
5747, 56eqtrd 2482 . . . . . . . . . . . . 13 Scalar Scalar Scalar
582, 6, 4, 5, 7, 18, 19, 23lspsneli 17515 . . . . . . . . . . . . . 14 Scalar Scalar
5958adantr 465 . . . . . . . . . . . . 13 Scalar Scalar Scalar
6057, 59eqeltrd 2529 . . . . . . . . . . . 12 Scalar Scalar Scalar
61 eldifsni 4137 . . . . . . . . . . . . . 14
6221, 61syl 16 . . . . . . . . . . . . 13 Scalar Scalar
6362adantr 465 . . . . . . . . . . . 12 Scalar Scalar Scalar
642, 44, 7, 45, 46, 60, 63lspsneleq 17629 . . . . . . . . . . 11 Scalar Scalar Scalar
6564ex 434 . . . . . . . . . 10 Scalar Scalar Scalar
6665necon3d 2665 . . . . . . . . 9 Scalar Scalar Scalar
6743, 66mpd 15 . . . . . . . 8 Scalar Scalar Scalar
68 eldifsn 4136 . . . . . . . 8 Scalar Scalar Scalar Scalar
6932, 67, 68sylanbrc 664 . . . . . . 7 Scalar Scalar Scalar Scalar
704lmodfgrp 17389 . . . . . . . . . . 11 Scalar
7127, 70syl 16 . . . . . . . . . 10 Scalar Scalar Scalar
725, 16grpinvcl 15964 . . . . . . . . . 10 Scalar Scalar Scalar Scalar
7371, 19, 72syl2anc 661 . . . . . . . . 9 Scalar Scalar Scalar Scalar
742, 4, 6, 5lmodvscl 17397 . . . . . . . . 9 Scalar Scalar Scalar
7518, 73, 23, 74syl3anc 1227 . . . . . . . 8 Scalar Scalar Scalar
762, 3lmodvacl 17394 . . . . . . . 8 Scalar Scalar
7718, 22, 75, 76syl3anc 1227 . . . . . . 7 Scalar Scalar Scalar
782, 6, 4, 5, 40, 41, 17, 69, 77, 33lvecinv 17627 . . . . . 6 Scalar Scalar Scalar Scalar Scalar
7939, 78mpbid 210 . . . . 5 Scalar Scalar Scalar Scalar
80 eqid 2441 . . . . . . 7
812, 80, 7, 18, 22, 23lspprcl 17492 . . . . . 6 Scalar Scalar
824lvecdrng 17619 . . . . . . . 8 Scalar
8317, 82syl 16 . . . . . . 7 Scalar Scalar Scalar
845, 40, 41drnginvrcl 17281 . . . . . . 7 Scalar Scalar Scalar Scalar Scalar
8583, 32, 67, 84syl3anc 1227 . . . . . 6 Scalar Scalar Scalar Scalar
86 eqid 2441 . . . . . . . . . 10 Scalar Scalar
872, 4, 6, 86lmodvs1 17408 . . . . . . . . 9 Scalar
8818, 22, 87syl2anc 661 . . . . . . . 8 Scalar Scalar Scalar
8988oveq1d 6292 . . . . . . 7 Scalar Scalar Scalar Scalar Scalar
904lmodring 17388 . . . . . . . . 9 Scalar
915, 86ringidcl 17087 . . . . . . . . 9 Scalar Scalar Scalar
9218, 90, 913syl 20 . . . . . . . 8 Scalar Scalar Scalar Scalar
932, 3, 6, 4, 5, 7, 18, 92, 73, 22, 23lsppreli 17604 . . . . . . 7 Scalar Scalar Scalar Scalar
9489, 93eqeltrrd 2530 . . . . . 6 Scalar Scalar Scalar
954, 6, 5, 80lssvscl 17469 . . . . . 6 Scalar Scalar Scalar Scalar Scalar
9618, 81, 85, 94, 95syl22anc 1228 . . . . 5 Scalar Scalar Scalar Scalar
9779, 96eqeltrd 2529 . . . 4 Scalar Scalar
98973exp 1194 . . 3 Scalar Scalar
9998rexlimdvv 2939 . 2 Scalar Scalar
10014, 99mpd 15 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 184   wa 369   w3a 972   wceq 1381   wcel 1802   wne 2636  wrex 2792   cdif 3455  csn 4010  cpr 4012  cfv 5574  (class class class)co 6277  cbs 14504   cplusg 14569  Scalarcsca 14572  cvsca 14573  c0g 14709  cgrp 15922  cminusg 15923  csg 15924  cur 17021  crg 17066  cinvr 17188  cdr 17264  clmod 17380  clss 17446  clspn 17485  clvec 17616 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-8 1804  ax-9 1806  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419  ax-rep 4544  ax-sep 4554  ax-nul 4562  ax-pow 4611  ax-pr 4672  ax-un 6573  ax-cnex 9546  ax-resscn 9547  ax-1cn 9548  ax-icn 9549  ax-addcl 9550  ax-addrcl 9551  ax-mulcl 9552  ax-mulrcl 9553  ax-mulcom 9554  ax-addass 9555  ax-mulass 9556  ax-distr 9557  ax-i2m1 9558  ax-1ne0 9559  ax-1rid 9560  ax-rnegex 9561  ax-rrecex 9562  ax-cnre 9563  ax-pre-lttri 9564  ax-pre-lttrn 9565  ax-pre-ltadd 9566  ax-pre-mulgt0 9567 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 973  df-3an 974  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-eu 2270  df-mo 2271  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-ne 2638  df-nel 2639  df-ral 2796  df-rex 2797  df-reu 2798  df-rmo 2799  df-rab 2800  df-v 3095  df-sbc 3312  df-csb 3418  df-dif 3461  df-un 3463  df-in 3465  df-ss 3472  df-pss 3474  df-nul 3768  df-if 3923  df-pw 3995  df-sn 4011  df-pr 4013  df-tp 4015  df-op 4017  df-uni 4231  df-int 4268  df-iun 4313  df-br 4434  df-opab 4492  df-mpt 4493  df-tr 4527  df-eprel 4777  df-id 4781  df-po 4786  df-so 4787  df-fr 4824  df-we 4826  df-ord 4867  df-on 4868  df-lim 4869  df-suc 4870  df-xp 4991  df-rel 4992  df-cnv 4993  df-co 4994  df-dm 4995  df-rn 4996  df-res 4997  df-ima 4998  df-iota 5537  df-fun 5576  df-fn 5577  df-f 5578  df-f1 5579  df-fo 5580  df-f1o 5581  df-fv 5582  df-riota 6238  df-ov 6280  df-oprab 6281  df-mpt2 6282  df-om 6682  df-1st 6781  df-2nd 6782  df-tpos 6953  df-recs 7040  df-rdg 7074  df-er 7309  df-en 7515  df-dom 7516  df-sdom 7517  df-pnf 9628  df-mnf 9629  df-xr 9630  df-ltxr 9631  df-le 9632  df-sub 9807  df-neg 9808  df-nn 10538  df-2 10595  df-3 10596  df-ndx 14507  df-slot 14508  df-base 14509  df-sets 14510  df-ress 14511  df-plusg 14582  df-mulr 14583  df-0g 14711  df-mgm 15741  df-sgrp 15780  df-mnd 15790  df-submnd 15836  df-grp 15926  df-minusg 15927  df-sbg 15928  df-subg 16067  df-cntz 16224  df-lsm 16525  df-cmn 16669  df-abl 16670  df-mgp 17010  df-ur 17022  df-ring 17068  df-oppr 17140  df-dvdsr 17158  df-unit 17159  df-invr 17189  df-drng 17266  df-lmod 17382  df-lss 17447  df-lsp 17486  df-lvec 17617 This theorem is referenced by:  lspexchn1  17644  lspindp1  17647  mapdh8ab  37206  mapdh8ad  37208  mapdh8b  37209  mapdh8c  37210  mapdh8e  37213
 Copyright terms: Public domain W3C validator