Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  mapdindp2 Structured version   Visualization version   GIF version

Theorem mapdindp2 36529
Description: Vector independence lemma. (Contributed by NM, 1-May-2015.)
Hypotheses
Ref Expression
mapdindp1.v 𝑉 = (Base‘𝑊)
mapdindp1.p + = (+g𝑊)
mapdindp1.o 0 = (0g𝑊)
mapdindp1.n 𝑁 = (LSpan‘𝑊)
mapdindp1.w (𝜑𝑊 ∈ LVec)
mapdindp1.x (𝜑𝑋 ∈ (𝑉 ∖ { 0 }))
mapdindp1.y (𝜑𝑌 ∈ (𝑉 ∖ { 0 }))
mapdindp1.z (𝜑𝑍 ∈ (𝑉 ∖ { 0 }))
mapdindp1.W (𝜑𝑤 ∈ (𝑉 ∖ { 0 }))
mapdindp1.e (𝜑 → (𝑁‘{𝑌}) = (𝑁‘{𝑍}))
mapdindp1.ne (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))
mapdindp1.f (𝜑 → ¬ 𝑤 ∈ (𝑁‘{𝑋, 𝑌}))
Assertion
Ref Expression
mapdindp2 (𝜑 → ¬ 𝑤 ∈ (𝑁‘{𝑋, (𝑌 + 𝑍)}))

Proof of Theorem mapdindp2
StepHypRef Expression
1 preq2 4246 . . . . . 6 ((𝑌 + 𝑍) = 0 → {𝑋, (𝑌 + 𝑍)} = {𝑋, 0 })
21fveq2d 6162 . . . . 5 ((𝑌 + 𝑍) = 0 → (𝑁‘{𝑋, (𝑌 + 𝑍)}) = (𝑁‘{𝑋, 0 }))
3 mapdindp1.v . . . . . 6 𝑉 = (Base‘𝑊)
4 mapdindp1.o . . . . . 6 0 = (0g𝑊)
5 mapdindp1.n . . . . . 6 𝑁 = (LSpan‘𝑊)
6 mapdindp1.w . . . . . . 7 (𝜑𝑊 ∈ LVec)
7 lveclmod 19046 . . . . . . 7 (𝑊 ∈ LVec → 𝑊 ∈ LMod)
86, 7syl 17 . . . . . 6 (𝜑𝑊 ∈ LMod)
9 mapdindp1.x . . . . . . 7 (𝜑𝑋 ∈ (𝑉 ∖ { 0 }))
109eldifad 3572 . . . . . 6 (𝜑𝑋𝑉)
113, 4, 5, 8, 10lsppr0 19032 . . . . 5 (𝜑 → (𝑁‘{𝑋, 0 }) = (𝑁‘{𝑋}))
122, 11sylan9eqr 2677 . . . 4 ((𝜑 ∧ (𝑌 + 𝑍) = 0 ) → (𝑁‘{𝑋, (𝑌 + 𝑍)}) = (𝑁‘{𝑋}))
13 mapdindp1.y . . . . . . . 8 (𝜑𝑌 ∈ (𝑉 ∖ { 0 }))
1413eldifad 3572 . . . . . . 7 (𝜑𝑌𝑉)
15 prssi 4328 . . . . . . 7 ((𝑋𝑉𝑌𝑉) → {𝑋, 𝑌} ⊆ 𝑉)
1610, 14, 15syl2anc 692 . . . . . 6 (𝜑 → {𝑋, 𝑌} ⊆ 𝑉)
17 snsspr1 4320 . . . . . . 7 {𝑋} ⊆ {𝑋, 𝑌}
1817a1i 11 . . . . . 6 (𝜑 → {𝑋} ⊆ {𝑋, 𝑌})
193, 5lspss 18924 . . . . . 6 ((𝑊 ∈ LMod ∧ {𝑋, 𝑌} ⊆ 𝑉 ∧ {𝑋} ⊆ {𝑋, 𝑌}) → (𝑁‘{𝑋}) ⊆ (𝑁‘{𝑋, 𝑌}))
208, 16, 18, 19syl3anc 1323 . . . . 5 (𝜑 → (𝑁‘{𝑋}) ⊆ (𝑁‘{𝑋, 𝑌}))
2120adantr 481 . . . 4 ((𝜑 ∧ (𝑌 + 𝑍) = 0 ) → (𝑁‘{𝑋}) ⊆ (𝑁‘{𝑋, 𝑌}))
2212, 21eqsstrd 3624 . . 3 ((𝜑 ∧ (𝑌 + 𝑍) = 0 ) → (𝑁‘{𝑋, (𝑌 + 𝑍)}) ⊆ (𝑁‘{𝑋, 𝑌}))
23 mapdindp1.f . . . 4 (𝜑 → ¬ 𝑤 ∈ (𝑁‘{𝑋, 𝑌}))
2423adantr 481 . . 3 ((𝜑 ∧ (𝑌 + 𝑍) = 0 ) → ¬ 𝑤 ∈ (𝑁‘{𝑋, 𝑌}))
2522, 24ssneldd 3591 . 2 ((𝜑 ∧ (𝑌 + 𝑍) = 0 ) → ¬ 𝑤 ∈ (𝑁‘{𝑋, (𝑌 + 𝑍)}))
2623adantr 481 . . 3 ((𝜑 ∧ (𝑌 + 𝑍) ≠ 0 ) → ¬ 𝑤 ∈ (𝑁‘{𝑋, 𝑌}))
27 mapdindp1.p . . . . . 6 + = (+g𝑊)
286adantr 481 . . . . . 6 ((𝜑 ∧ (𝑌 + 𝑍) ≠ 0 ) → 𝑊 ∈ LVec)
299adantr 481 . . . . . 6 ((𝜑 ∧ (𝑌 + 𝑍) ≠ 0 ) → 𝑋 ∈ (𝑉 ∖ { 0 }))
3013adantr 481 . . . . . 6 ((𝜑 ∧ (𝑌 + 𝑍) ≠ 0 ) → 𝑌 ∈ (𝑉 ∖ { 0 }))
31 mapdindp1.z . . . . . . 7 (𝜑𝑍 ∈ (𝑉 ∖ { 0 }))
3231adantr 481 . . . . . 6 ((𝜑 ∧ (𝑌 + 𝑍) ≠ 0 ) → 𝑍 ∈ (𝑉 ∖ { 0 }))
33 mapdindp1.W . . . . . . 7 (𝜑𝑤 ∈ (𝑉 ∖ { 0 }))
3433adantr 481 . . . . . 6 ((𝜑 ∧ (𝑌 + 𝑍) ≠ 0 ) → 𝑤 ∈ (𝑉 ∖ { 0 }))
35 mapdindp1.e . . . . . . 7 (𝜑 → (𝑁‘{𝑌}) = (𝑁‘{𝑍}))
3635adantr 481 . . . . . 6 ((𝜑 ∧ (𝑌 + 𝑍) ≠ 0 ) → (𝑁‘{𝑌}) = (𝑁‘{𝑍}))
37 mapdindp1.ne . . . . . . 7 (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))
3837adantr 481 . . . . . 6 ((𝜑 ∧ (𝑌 + 𝑍) ≠ 0 ) → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))
39 simpr 477 . . . . . 6 ((𝜑 ∧ (𝑌 + 𝑍) ≠ 0 ) → (𝑌 + 𝑍) ≠ 0 )
403, 27, 4, 5, 28, 29, 30, 32, 34, 36, 38, 26, 39mapdindp0 36527 . . . . 5 ((𝜑 ∧ (𝑌 + 𝑍) ≠ 0 ) → (𝑁‘{(𝑌 + 𝑍)}) = (𝑁‘{𝑌}))
4140oveq2d 6631 . . . 4 ((𝜑 ∧ (𝑌 + 𝑍) ≠ 0 ) → ((𝑁‘{𝑋})(LSSum‘𝑊)(𝑁‘{(𝑌 + 𝑍)})) = ((𝑁‘{𝑋})(LSSum‘𝑊)(𝑁‘{𝑌})))
42 eqid 2621 . . . . . 6 (LSSum‘𝑊) = (LSSum‘𝑊)
4331eldifad 3572 . . . . . . 7 (𝜑𝑍𝑉)
443, 27lmodvacl 18817 . . . . . . 7 ((𝑊 ∈ LMod ∧ 𝑌𝑉𝑍𝑉) → (𝑌 + 𝑍) ∈ 𝑉)
458, 14, 43, 44syl3anc 1323 . . . . . 6 (𝜑 → (𝑌 + 𝑍) ∈ 𝑉)
463, 5, 42, 8, 10, 45lsmpr 19029 . . . . 5 (𝜑 → (𝑁‘{𝑋, (𝑌 + 𝑍)}) = ((𝑁‘{𝑋})(LSSum‘𝑊)(𝑁‘{(𝑌 + 𝑍)})))
4746adantr 481 . . . 4 ((𝜑 ∧ (𝑌 + 𝑍) ≠ 0 ) → (𝑁‘{𝑋, (𝑌 + 𝑍)}) = ((𝑁‘{𝑋})(LSSum‘𝑊)(𝑁‘{(𝑌 + 𝑍)})))
483, 5, 42, 8, 10, 14lsmpr 19029 . . . . 5 (𝜑 → (𝑁‘{𝑋, 𝑌}) = ((𝑁‘{𝑋})(LSSum‘𝑊)(𝑁‘{𝑌})))
4948adantr 481 . . . 4 ((𝜑 ∧ (𝑌 + 𝑍) ≠ 0 ) → (𝑁‘{𝑋, 𝑌}) = ((𝑁‘{𝑋})(LSSum‘𝑊)(𝑁‘{𝑌})))
5041, 47, 493eqtr4d 2665 . . 3 ((𝜑 ∧ (𝑌 + 𝑍) ≠ 0 ) → (𝑁‘{𝑋, (𝑌 + 𝑍)}) = (𝑁‘{𝑋, 𝑌}))
5126, 50neleqtrrd 2720 . 2 ((𝜑 ∧ (𝑌 + 𝑍) ≠ 0 ) → ¬ 𝑤 ∈ (𝑁‘{𝑋, (𝑌 + 𝑍)}))
5225, 51pm2.61dane 2877 1 (𝜑 → ¬ 𝑤 ∈ (𝑁‘{𝑋, (𝑌 + 𝑍)}))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 384   = wceq 1480  wcel 1987  wne 2790  cdif 3557  wss 3560  {csn 4155  {cpr 4157  cfv 5857  (class class class)co 6615  Basecbs 15800  +gcplusg 15881  0gc0g 16040  LSSumclsm 17989  LModclmod 18803  LSpanclspn 18911  LVecclvec 19042
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4741  ax-sep 4751  ax-nul 4759  ax-pow 4813  ax-pr 4877  ax-un 6914  ax-cnex 9952  ax-resscn 9953  ax-1cn 9954  ax-icn 9955  ax-addcl 9956  ax-addrcl 9957  ax-mulcl 9958  ax-mulrcl 9959  ax-mulcom 9960  ax-addass 9961  ax-mulass 9962  ax-distr 9963  ax-i2m1 9964  ax-1ne0 9965  ax-1rid 9966  ax-rnegex 9967  ax-rrecex 9968  ax-cnre 9969  ax-pre-lttri 9970  ax-pre-lttrn 9971  ax-pre-ltadd 9972  ax-pre-mulgt0 9973
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2913  df-rex 2914  df-reu 2915  df-rmo 2916  df-rab 2917  df-v 3192  df-sbc 3423  df-csb 3520  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-pss 3576  df-nul 3898  df-if 4065  df-pw 4138  df-sn 4156  df-pr 4158  df-tp 4160  df-op 4162  df-uni 4410  df-int 4448  df-iun 4494  df-br 4624  df-opab 4684  df-mpt 4685  df-tr 4723  df-eprel 4995  df-id 4999  df-po 5005  df-so 5006  df-fr 5043  df-we 5045  df-xp 5090  df-rel 5091  df-cnv 5092  df-co 5093  df-dm 5094  df-rn 5095  df-res 5096  df-ima 5097  df-pred 5649  df-ord 5695  df-on 5696  df-lim 5697  df-suc 5698  df-iota 5820  df-fun 5859  df-fn 5860  df-f 5861  df-f1 5862  df-fo 5863  df-f1o 5864  df-fv 5865  df-riota 6576  df-ov 6618  df-oprab 6619  df-mpt2 6620  df-om 7028  df-1st 7128  df-2nd 7129  df-tpos 7312  df-wrecs 7367  df-recs 7428  df-rdg 7466  df-er 7702  df-en 7916  df-dom 7917  df-sdom 7918  df-pnf 10036  df-mnf 10037  df-xr 10038  df-ltxr 10039  df-le 10040  df-sub 10228  df-neg 10229  df-nn 10981  df-2 11039  df-3 11040  df-ndx 15803  df-slot 15804  df-base 15805  df-sets 15806  df-ress 15807  df-plusg 15894  df-mulr 15895  df-0g 16042  df-mgm 17182  df-sgrp 17224  df-mnd 17235  df-submnd 17276  df-grp 17365  df-minusg 17366  df-sbg 17367  df-subg 17531  df-cntz 17690  df-lsm 17991  df-cmn 18135  df-abl 18136  df-mgp 18430  df-ur 18442  df-ring 18489  df-oppr 18563  df-dvdsr 18581  df-unit 18582  df-invr 18612  df-drng 18689  df-lmod 18805  df-lss 18873  df-lsp 18912  df-lvec 19043
This theorem is referenced by:  mapdh6dN  36547  hdmap1l6d  36622
  Copyright terms: Public domain W3C validator