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

Theorem mapdindp0 36527
Description: Vector independence lemma. (Contributed by NM, 29-Apr-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 (𝜑 → ¬ 𝑤 ∈ (𝑁‘{𝑋, 𝑌}))
mapdindp1.yz (𝜑 → (𝑌 + 𝑍) ≠ 0 )
Assertion
Ref Expression
mapdindp0 (𝜑 → (𝑁‘{(𝑌 + 𝑍)}) = (𝑁‘{𝑌}))

Proof of Theorem mapdindp0
StepHypRef Expression
1 eqid 2621 . . . 4 (LSubSp‘𝑊) = (LSubSp‘𝑊)
2 mapdindp1.n . . . 4 𝑁 = (LSpan‘𝑊)
3 mapdindp1.w . . . . 5 (𝜑𝑊 ∈ LVec)
4 lveclmod 19046 . . . . 5 (𝑊 ∈ LVec → 𝑊 ∈ LMod)
53, 4syl 17 . . . 4 (𝜑𝑊 ∈ LMod)
6 mapdindp1.y . . . . . . 7 (𝜑𝑌 ∈ (𝑉 ∖ { 0 }))
76eldifad 3572 . . . . . 6 (𝜑𝑌𝑉)
8 mapdindp1.v . . . . . . 7 𝑉 = (Base‘𝑊)
98, 1, 2lspsncl 18917 . . . . . 6 ((𝑊 ∈ LMod ∧ 𝑌𝑉) → (𝑁‘{𝑌}) ∈ (LSubSp‘𝑊))
105, 7, 9syl2anc 692 . . . . 5 (𝜑 → (𝑁‘{𝑌}) ∈ (LSubSp‘𝑊))
11 mapdindp1.e . . . . . 6 (𝜑 → (𝑁‘{𝑌}) = (𝑁‘{𝑍}))
1211, 10eqeltrrd 2699 . . . . 5 (𝜑 → (𝑁‘{𝑍}) ∈ (LSubSp‘𝑊))
13 eqid 2621 . . . . . 6 (LSSum‘𝑊) = (LSSum‘𝑊)
141, 13lsmcl 19023 . . . . 5 ((𝑊 ∈ LMod ∧ (𝑁‘{𝑌}) ∈ (LSubSp‘𝑊) ∧ (𝑁‘{𝑍}) ∈ (LSubSp‘𝑊)) → ((𝑁‘{𝑌})(LSSum‘𝑊)(𝑁‘{𝑍})) ∈ (LSubSp‘𝑊))
155, 10, 12, 14syl3anc 1323 . . . 4 (𝜑 → ((𝑁‘{𝑌})(LSSum‘𝑊)(𝑁‘{𝑍})) ∈ (LSubSp‘𝑊))
161lsssssubg 18898 . . . . . . 7 (𝑊 ∈ LMod → (LSubSp‘𝑊) ⊆ (SubGrp‘𝑊))
175, 16syl 17 . . . . . 6 (𝜑 → (LSubSp‘𝑊) ⊆ (SubGrp‘𝑊))
1817, 10sseldd 3589 . . . . 5 (𝜑 → (𝑁‘{𝑌}) ∈ (SubGrp‘𝑊))
1911, 18eqeltrrd 2699 . . . . 5 (𝜑 → (𝑁‘{𝑍}) ∈ (SubGrp‘𝑊))
208, 2lspsnid 18933 . . . . . 6 ((𝑊 ∈ LMod ∧ 𝑌𝑉) → 𝑌 ∈ (𝑁‘{𝑌}))
215, 7, 20syl2anc 692 . . . . 5 (𝜑𝑌 ∈ (𝑁‘{𝑌}))
22 mapdindp1.z . . . . . . 7 (𝜑𝑍 ∈ (𝑉 ∖ { 0 }))
2322eldifad 3572 . . . . . 6 (𝜑𝑍𝑉)
248, 2lspsnid 18933 . . . . . 6 ((𝑊 ∈ LMod ∧ 𝑍𝑉) → 𝑍 ∈ (𝑁‘{𝑍}))
255, 23, 24syl2anc 692 . . . . 5 (𝜑𝑍 ∈ (𝑁‘{𝑍}))
26 mapdindp1.p . . . . . 6 + = (+g𝑊)
2726, 13lsmelvali 18005 . . . . 5 ((((𝑁‘{𝑌}) ∈ (SubGrp‘𝑊) ∧ (𝑁‘{𝑍}) ∈ (SubGrp‘𝑊)) ∧ (𝑌 ∈ (𝑁‘{𝑌}) ∧ 𝑍 ∈ (𝑁‘{𝑍}))) → (𝑌 + 𝑍) ∈ ((𝑁‘{𝑌})(LSSum‘𝑊)(𝑁‘{𝑍})))
2818, 19, 21, 25, 27syl22anc 1324 . . . 4 (𝜑 → (𝑌 + 𝑍) ∈ ((𝑁‘{𝑌})(LSSum‘𝑊)(𝑁‘{𝑍})))
291, 2, 5, 15, 28lspsnel5a 18936 . . 3 (𝜑 → (𝑁‘{(𝑌 + 𝑍)}) ⊆ ((𝑁‘{𝑌})(LSSum‘𝑊)(𝑁‘{𝑍})))
3011oveq2d 6631 . . . 4 (𝜑 → ((𝑁‘{𝑌})(LSSum‘𝑊)(𝑁‘{𝑌})) = ((𝑁‘{𝑌})(LSSum‘𝑊)(𝑁‘{𝑍})))
3113lsmidm 18017 . . . . 5 ((𝑁‘{𝑌}) ∈ (SubGrp‘𝑊) → ((𝑁‘{𝑌})(LSSum‘𝑊)(𝑁‘{𝑌})) = (𝑁‘{𝑌}))
3218, 31syl 17 . . . 4 (𝜑 → ((𝑁‘{𝑌})(LSSum‘𝑊)(𝑁‘{𝑌})) = (𝑁‘{𝑌}))
3330, 32eqtr3d 2657 . . 3 (𝜑 → ((𝑁‘{𝑌})(LSSum‘𝑊)(𝑁‘{𝑍})) = (𝑁‘{𝑌}))
3429, 33sseqtrd 3626 . 2 (𝜑 → (𝑁‘{(𝑌 + 𝑍)}) ⊆ (𝑁‘{𝑌}))
35 mapdindp1.o . . 3 0 = (0g𝑊)
368, 26lmodvacl 18817 . . . . 5 ((𝑊 ∈ LMod ∧ 𝑌𝑉𝑍𝑉) → (𝑌 + 𝑍) ∈ 𝑉)
375, 7, 23, 36syl3anc 1323 . . . 4 (𝜑 → (𝑌 + 𝑍) ∈ 𝑉)
38 mapdindp1.yz . . . 4 (𝜑 → (𝑌 + 𝑍) ≠ 0 )
39 eldifsn 4294 . . . 4 ((𝑌 + 𝑍) ∈ (𝑉 ∖ { 0 }) ↔ ((𝑌 + 𝑍) ∈ 𝑉 ∧ (𝑌 + 𝑍) ≠ 0 ))
4037, 38, 39sylanbrc 697 . . 3 (𝜑 → (𝑌 + 𝑍) ∈ (𝑉 ∖ { 0 }))
418, 35, 2, 3, 40, 7lspsncmp 19056 . 2 (𝜑 → ((𝑁‘{(𝑌 + 𝑍)}) ⊆ (𝑁‘{𝑌}) ↔ (𝑁‘{(𝑌 + 𝑍)}) = (𝑁‘{𝑌})))
4234, 41mpbid 222 1 (𝜑 → (𝑁‘{(𝑌 + 𝑍)}) = (𝑁‘{𝑌}))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = 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  SubGrpcsubg 17528  LSSumclsm 17989  LModclmod 18803  LSubSpclss 18872  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:  mapdindp1  36528  mapdindp2  36529
  Copyright terms: Public domain W3C validator