Theorem mapdrn2 40227

Description: Range of the map defined by df-mapd 40201. TODO: this seems to be needed a lot in hdmaprnlem3eN 40434 etc. Would it be better to change df-mapd 40201 theorems to use LSubSp‘𝐶 instead of ran 𝑀? (Contributed by NM, 13-Mar-2015.)

Hypotheses

Ref	Expression
mapdrn2.h	⊢ 𝐻 = (LHyp‘𝐾)
mapdrn2.m	⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)
mapdrn2.c	⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)
mapdrn2.t	⊢ 𝑇 = (LSubSp‘𝐶)
mapdrn2.k	⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))

Assertion

Ref	Expression
mapdrn2	⊢ (𝜑 → ran 𝑀 = 𝑇)

Proof of Theorem mapdrn2

Dummy variable 𝑓 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		mapdrn2.h	. . 3 ⊢ 𝐻 = (LHyp‘𝐾)
2		eqid 2731	. . 3 ⊢ ((ocH‘𝐾)‘𝑊) = ((ocH‘𝐾)‘𝑊)
3		mapdrn2.m	. . 3 ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)
4		eqid 2731	. . 3 ⊢ ((DVecH‘𝐾)‘𝑊) = ((DVecH‘𝐾)‘𝑊)
5		eqid 2731	. . 3 ⊢ (LFnl‘((DVecH‘𝐾)‘𝑊)) = (LFnl‘((DVecH‘𝐾)‘𝑊))
6		eqid 2731	. . 3 ⊢ (LKer‘((DVecH‘𝐾)‘𝑊)) = (LKer‘((DVecH‘𝐾)‘𝑊))
7		eqid 2731	. . 3 ⊢ (LDual‘((DVecH‘𝐾)‘𝑊)) = (LDual‘((DVecH‘𝐾)‘𝑊))
8		eqid 2731	. . 3 ⊢ (LSubSp‘(LDual‘((DVecH‘𝐾)‘𝑊))) = (LSubSp‘(LDual‘((DVecH‘𝐾)‘𝑊)))
9		eqid 2731	. . 3 ⊢ {𝑓 ∈ (LFnl‘((DVecH‘𝐾)‘𝑊)) ∣ (((ocH‘𝐾)‘𝑊)‘(((ocH‘𝐾)‘𝑊)‘((LKer‘((DVecH‘𝐾)‘𝑊))‘𝑓))) = ((LKer‘((DVecH‘𝐾)‘𝑊))‘𝑓)} = {𝑓 ∈ (LFnl‘((DVecH‘𝐾)‘𝑊)) ∣ (((ocH‘𝐾)‘𝑊)‘(((ocH‘𝐾)‘𝑊)‘((LKer‘((DVecH‘𝐾)‘𝑊))‘𝑓))) = ((LKer‘((DVecH‘𝐾)‘𝑊))‘𝑓)}
10		mapdrn2.k	. . 3 ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
11	1, 2, 3, 4, 5, 6, 7, 8, 9, 10	mapdrn 40225	. 2 ⊢ (𝜑 → ran 𝑀 = ((LSubSp‘(LDual‘((DVecH‘𝐾)‘𝑊))) ∩ 𝒫 {𝑓 ∈ (LFnl‘((DVecH‘𝐾)‘𝑊)) ∣ (((ocH‘𝐾)‘𝑊)‘(((ocH‘𝐾)‘𝑊)‘((LKer‘((DVecH‘𝐾)‘𝑊))‘𝑓))) = ((LKer‘((DVecH‘𝐾)‘𝑊))‘𝑓)}))
12		mapdrn2.c	. . 3 ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)
13		mapdrn2.t	. . 3 ⊢ 𝑇 = (LSubSp‘𝐶)
14	1, 2, 12, 13, 4, 5, 6, 7, 8, 9, 10	lcdlss 40195	. 2 ⊢ (𝜑 → 𝑇 = ((LSubSp‘(LDual‘((DVecH‘𝐾)‘𝑊))) ∩ 𝒫 {𝑓 ∈ (LFnl‘((DVecH‘𝐾)‘𝑊)) ∣ (((ocH‘𝐾)‘𝑊)‘(((ocH‘𝐾)‘𝑊)‘((LKer‘((DVecH‘𝐾)‘𝑊))‘𝑓))) = ((LKer‘((DVecH‘𝐾)‘𝑊))‘𝑓)}))
15	11, 14	eqtr4d 2774	1 ⊢ (𝜑 → ran 𝑀 = 𝑇)

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1541   ∈ wcel 2106  {crab 3425   ∩ cin 3934  𝒫 cpw 4587  ran crn 5661  ‘cfv 6523  LSubSpclss 20471  LFnlclfn 37632  LKerclk 37660  LDualcld 37698  HLchlt 37925  LHypclh 38560  DVecHcdvh 39654  ocHcoch 39923  LCDualclcd 40162  mapdcmpd 40200

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702  ax-rep 5269  ax-sep 5283  ax-nul 5290  ax-pow 5347  ax-pr 5411  ax-un 7699  ax-cnex 11138  ax-resscn 11139  ax-1cn 11140  ax-icn 11141  ax-addcl 11142  ax-addrcl 11143  ax-mulcl 11144  ax-mulrcl 11145  ax-mulcom 11146  ax-addass 11147  ax-mulass 11148  ax-distr 11149  ax-i2m1 11150  ax-1ne0 11151  ax-1rid 11152  ax-rnegex 11153  ax-rrecex 11154  ax-cnre 11155  ax-pre-lttri 11156  ax-pre-lttrn 11157  ax-pre-ltadd 11158  ax-pre-mulgt0 11159  ax-riotaBAD 37528

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rmo 3371  df-reu 3372  df-rab 3426  df-v 3468  df-sbc 3765  df-csb 3881  df-dif 3938  df-un 3940  df-in 3942  df-ss 3952  df-pss 3954  df-nul 4310  df-if 4514  df-pw 4589  df-sn 4614  df-pr 4616  df-tp 4618  df-op 4620  df-uni 4893  df-int 4935  df-iun 4983  df-iin 4984  df-br 5133  df-opab 5195  df-mpt 5216  df-tr 5250  df-id 5558  df-eprel 5564  df-po 5572  df-so 5573  df-fr 5615  df-we 5617  df-xp 5666  df-rel 5667  df-cnv 5668  df-co 5669  df-dm 5670  df-rn 5671  df-res 5672  df-ima 5673  df-pred 6280  df-ord 6347  df-on 6348  df-lim 6349  df-suc 6350  df-iota 6475  df-fun 6525  df-fn 6526  df-f 6527  df-f1 6528  df-fo 6529  df-f1o 6530  df-fv 6531  df-riota 7340  df-ov 7387  df-oprab 7388  df-mpo 7389  df-of 7644  df-om 7830  df-1st 7948  df-2nd 7949  df-tpos 8184  df-undef 8231  df-frecs 8239  df-wrecs 8270  df-recs 8344  df-rdg 8383  df-1o 8439  df-er 8677  df-map 8796  df-en 8913  df-dom 8914  df-sdom 8915  df-fin 8916  df-pnf 11222  df-mnf 11223  df-xr 11224  df-ltxr 11225  df-le 11226  df-sub 11418  df-neg 11419  df-nn 12185  df-2 12247  df-3 12248  df-4 12249  df-5 12250  df-6 12251  df-n0 12445  df-z 12531  df-uz 12795  df-fz 13457  df-struct 17052  df-sets 17069  df-slot 17087  df-ndx 17099  df-base 17117  df-ress 17146  df-plusg 17182  df-mulr 17183  df-sca 17185  df-vsca 17186  df-0g 17359  df-mre 17502  df-mrc 17503  df-acs 17505  df-proset 18220  df-poset 18238  df-plt 18255  df-lub 18271  df-glb 18272  df-join 18273  df-meet 18274  df-p0 18350  df-p1 18351  df-lat 18357  df-clat 18424  df-mgm 18533  df-sgrp 18582  df-mnd 18593  df-submnd 18638  df-grp 18787  df-minusg 18788  df-sbg 18789  df-subg 18961  df-cntz 19133  df-oppg 19160  df-lsm 19454  df-cmn 19600  df-abl 19601  df-mgp 19933  df-ur 19950  df-ring 20002  df-oppr 20085  df-dvdsr 20106  df-unit 20107  df-invr 20137  df-dvr 20148  df-drng 20249  df-lmod 20402  df-lss 20472  df-lsp 20512  df-lvec 20643  df-lsatoms 37551  df-lshyp 37552  df-lcv 37594  df-lfl 37633  df-lkr 37661  df-ldual 37699  df-oposet 37751  df-ol 37753  df-oml 37754  df-covers 37841  df-ats 37842  df-atl 37873  df-cvlat 37897  df-hlat 37926  df-llines 38074  df-lplanes 38075  df-lvols 38076  df-lines 38077  df-psubsp 38079  df-pmap 38080  df-padd 38372  df-lhyp 38564  df-laut 38565  df-ldil 38680  df-ltrn 38681  df-trl 38735  df-tgrp 39319  df-tendo 39331  df-edring 39333  df-dveca 39579  df-disoa 39605  df-dvech 39655  df-dib 39715  df-dic 39749  df-dih 39805  df-doch 39924  df-djh 39971  df-lcdual 40163  df-mapd 40201

This theorem is referenced by:  mapdcl2  40232  mapdcv  40236  mapdincl  40237  mapdin  40238  mapdlsmcl  40239  mapdcnvatN  40242  hdmaprnlem3N  40426  hdmaprnlem3uN  40427  hdmaprnlem9N  40433  hdmaprnlem3eN  40434  hdmaprnlem16N  40438