mapdcnvid2 - Mathbox for Norm Megill

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

Theorem mapdcnvid2 37417

Description: Value of the converse of the map defined by df-mapd 37385. (Contributed by NM, 13-Mar-2015.)

**Hypotheses**
Ref	Expression
mapdcnvid2.h	⊢ 𝐻 = (LHyp‘𝐾)
mapdcnvid2.m	⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)
mapdcnvid2.k	⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
mapdcnvid2.x	⊢ (𝜑 → 𝑋 ∈ ran 𝑀)

**Assertion**
Ref	Expression
mapdcnvid2	⊢ (𝜑 → (𝑀‘(^◡𝑀‘𝑋)) = 𝑋)

Proof of Theorem mapdcnvid2 Dummy variable 𝑔 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		mapdcnvid2.h	. . . 4 ⊢ 𝐻 = (LHyp‘𝐾)
2		eqid 2748	. . . 4 ⊢ ((ocH‘𝐾)‘𝑊) = ((ocH‘𝐾)‘𝑊)
3		mapdcnvid2.m	. . . 4 ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)
4		eqid 2748	. . . 4 ⊢ ((DVecH‘𝐾)‘𝑊) = ((DVecH‘𝐾)‘𝑊)
5		eqid 2748	. . . 4 ⊢ (LSubSp‘((DVecH‘𝐾)‘𝑊)) = (LSubSp‘((DVecH‘𝐾)‘𝑊))
6		eqid 2748	. . . 4 ⊢ (LFnl‘((DVecH‘𝐾)‘𝑊)) = (LFnl‘((DVecH‘𝐾)‘𝑊))
7		eqid 2748	. . . 4 ⊢ (LKer‘((DVecH‘𝐾)‘𝑊)) = (LKer‘((DVecH‘𝐾)‘𝑊))
8		eqid 2748	. . . 4 ⊢ (LDual‘((DVecH‘𝐾)‘𝑊)) = (LDual‘((DVecH‘𝐾)‘𝑊))
9		eqid 2748	. . . 4 ⊢ (LSubSp‘(LDual‘((DVecH‘𝐾)‘𝑊))) = (LSubSp‘(LDual‘((DVecH‘𝐾)‘𝑊)))
10		eqid 2748	. . . 4 ⊢ {𝑔 ∈ (LFnl‘((DVecH‘𝐾)‘𝑊)) ∣ (((ocH‘𝐾)‘𝑊)‘(((ocH‘𝐾)‘𝑊)‘((LKer‘((DVecH‘𝐾)‘𝑊))‘𝑔))) = ((LKer‘((DVecH‘𝐾)‘𝑊))‘𝑔)} = {𝑔 ∈ (LFnl‘((DVecH‘𝐾)‘𝑊)) ∣ (((ocH‘𝐾)‘𝑊)‘(((ocH‘𝐾)‘𝑊)‘((LKer‘((DVecH‘𝐾)‘𝑊))‘𝑔))) = ((LKer‘((DVecH‘𝐾)‘𝑊))‘𝑔)}
11		mapdcnvid2.k	. . . 4 ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
12	1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11	mapd1o 37408	. . 3 ⊢ (𝜑 → 𝑀:(LSubSp‘((DVecH‘𝐾)‘𝑊))–1-1-onto→((LSubSp‘(LDual‘((DVecH‘𝐾)‘𝑊))) ∩ 𝒫 {𝑔 ∈ (LFnl‘((DVecH‘𝐾)‘𝑊)) ∣ (((ocH‘𝐾)‘𝑊)‘(((ocH‘𝐾)‘𝑊)‘((LKer‘((DVecH‘𝐾)‘𝑊))‘𝑔))) = ((LKer‘((DVecH‘𝐾)‘𝑊))‘𝑔)}))
13		f1of1 6285	. . 3 ⊢ (𝑀:(LSubSp‘((DVecH‘𝐾)‘𝑊))–1-1-onto→((LSubSp‘(LDual‘((DVecH‘𝐾)‘𝑊))) ∩ 𝒫 {𝑔 ∈ (LFnl‘((DVecH‘𝐾)‘𝑊)) ∣ (((ocH‘𝐾)‘𝑊)‘(((ocH‘𝐾)‘𝑊)‘((LKer‘((DVecH‘𝐾)‘𝑊))‘𝑔))) = ((LKer‘((DVecH‘𝐾)‘𝑊))‘𝑔)}) → 𝑀:(LSubSp‘((DVecH‘𝐾)‘𝑊))–1-1→((LSubSp‘(LDual‘((DVecH‘𝐾)‘𝑊))) ∩ 𝒫 {𝑔 ∈ (LFnl‘((DVecH‘𝐾)‘𝑊)) ∣ (((ocH‘𝐾)‘𝑊)‘(((ocH‘𝐾)‘𝑊)‘((LKer‘((DVecH‘𝐾)‘𝑊))‘𝑔))) = ((LKer‘((DVecH‘𝐾)‘𝑊))‘𝑔)}))
14		f1f1orn 6297	. . 3 ⊢ (𝑀:(LSubSp‘((DVecH‘𝐾)‘𝑊))–1-1→((LSubSp‘(LDual‘((DVecH‘𝐾)‘𝑊))) ∩ 𝒫 {𝑔 ∈ (LFnl‘((DVecH‘𝐾)‘𝑊)) ∣ (((ocH‘𝐾)‘𝑊)‘(((ocH‘𝐾)‘𝑊)‘((LKer‘((DVecH‘𝐾)‘𝑊))‘𝑔))) = ((LKer‘((DVecH‘𝐾)‘𝑊))‘𝑔)}) → 𝑀:(LSubSp‘((DVecH‘𝐾)‘𝑊))–1-1-onto→ran 𝑀)
15	12, 13, 14	3syl 18	. 2 ⊢ (𝜑 → 𝑀:(LSubSp‘((DVecH‘𝐾)‘𝑊))–1-1-onto→ran 𝑀)
16		mapdcnvid2.x	. 2 ⊢ (𝜑 → 𝑋 ∈ ran 𝑀)
17		f1ocnvfv2 6684	. 2 ⊢ ((𝑀:(LSubSp‘((DVecH‘𝐾)‘𝑊))–1-1-onto→ran 𝑀 ∧ 𝑋 ∈ ran 𝑀) → (𝑀‘(^◡𝑀‘𝑋)) = 𝑋)
18	15, 16, 17	syl2anc 696	1 ⊢ (𝜑 → (𝑀‘(^◡𝑀‘𝑋)) = 𝑋)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 383 = wceq 1620 ∈ wcel 2127 {crab 3042 ∩ cin 3702 𝒫 cpw 4290 ^◡ccnv 5253 ran crn 5255 –1-1→wf1 6034 –1-1-onto→wf1o 6036 ‘cfv 6037 LSubSpclss 19105 LFnlclfn 34816 LKerclk 34844 LDualcld 34882 HLchlt 35109 LHypclh 35742 DVecHcdvh 36838 ocHcoch 37107 mapdcmpd 37384

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1859 ax-4 1874 ax-5 1976 ax-6 2042 ax-7 2078 ax-8 2129 ax-9 2136 ax-10 2156 ax-11 2171 ax-12 2184 ax-13 2379 ax-ext 2728 ax-rep 4911 ax-sep 4921 ax-nul 4929 ax-pow 4980 ax-pr 5043 ax-un 7102 ax-cnex 10155 ax-resscn 10156 ax-1cn 10157 ax-icn 10158 ax-addcl 10159 ax-addrcl 10160 ax-mulcl 10161 ax-mulrcl 10162 ax-mulcom 10163 ax-addass 10164 ax-mulass 10165 ax-distr 10166 ax-i2m1 10167 ax-1ne0 10168 ax-1rid 10169 ax-rnegex 10170 ax-rrecex 10171 ax-cnre 10172 ax-pre-lttri 10173 ax-pre-lttrn 10174 ax-pre-ltadd 10175 ax-pre-mulgt0 10176 ax-riotaBAD 34711

This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3or 1073 df-3an 1074 df-tru 1623 df-fal 1626 df-ex 1842 df-nf 1847 df-sb 2035 df-eu 2599 df-mo 2600 df-clab 2735 df-cleq 2741 df-clel 2744 df-nfc 2879 df-ne 2921 df-nel 3024 df-ral 3043 df-rex 3044 df-reu 3045 df-rmo 3046 df-rab 3047 df-v 3330 df-sbc 3565 df-csb 3663 df-dif 3706 df-un 3708 df-in 3710 df-ss 3717 df-pss 3719 df-nul 4047 df-if 4219 df-pw 4292 df-sn 4310 df-pr 4312 df-tp 4314 df-op 4316 df-uni 4577 df-int 4616 df-iun 4662 df-iin 4663 df-br 4793 df-opab 4853 df-mpt 4870 df-tr 4893 df-id 5162 df-eprel 5167 df-po 5175 df-so 5176 df-fr 5213 df-we 5215 df-xp 5260 df-rel 5261 df-cnv 5262 df-co 5263 df-dm 5264 df-rn 5265 df-res 5266 df-ima 5267 df-pred 5829 df-ord 5875 df-on 5876 df-lim 5877 df-suc 5878 df-iota 6000 df-fun 6039 df-fn 6040 df-f 6041 df-f1 6042 df-fo 6043 df-f1o 6044 df-fv 6045 df-riota 6762 df-ov 6804 df-oprab 6805 df-mpt2 6806 df-of 7050 df-om 7219 df-1st 7321 df-2nd 7322 df-tpos 7509 df-undef 7556 df-wrecs 7564 df-recs 7625 df-rdg 7663 df-1o 7717 df-oadd 7721 df-er 7899 df-map 8013 df-en 8110 df-dom 8111 df-sdom 8112 df-fin 8113 df-pnf 10239 df-mnf 10240 df-xr 10241 df-ltxr 10242 df-le 10243 df-sub 10431 df-neg 10432 df-nn 11184 df-2 11242 df-3 11243 df-4 11244 df-5 11245 df-6 11246 df-n0 11456 df-z 11541 df-uz 11851 df-fz 12491 df-struct 16032 df-ndx 16033 df-slot 16034 df-base 16036 df-sets 16037 df-ress 16038 df-plusg 16127 df-mulr 16128 df-sca 16130 df-vsca 16131 df-0g 16275 df-mre 16419 df-mrc 16420 df-acs 16422 df-preset 17100 df-poset 17118 df-plt 17130 df-lub 17146 df-glb 17147 df-join 17148 df-meet 17149 df-p0 17211 df-p1 17212 df-lat 17218 df-clat 17280 df-mgm 17414 df-sgrp 17456 df-mnd 17467 df-submnd 17508 df-grp 17597 df-minusg 17598 df-sbg 17599 df-subg 17763 df-cntz 17921 df-oppg 17947 df-lsm 18222 df-cmn 18366 df-abl 18367 df-mgp 18661 df-ur 18673 df-ring 18720 df-oppr 18794 df-dvdsr 18812 df-unit 18813 df-invr 18843 df-dvr 18854 df-drng 18922 df-lmod 19038 df-lss 19106 df-lsp 19145 df-lvec 19276 df-lsatoms 34735 df-lshyp 34736 df-lcv 34778 df-lfl 34817 df-lkr 34845 df-ldual 34883 df-oposet 34935 df-ol 34937 df-oml 34938 df-covers 35025 df-ats 35026 df-atl 35057 df-cvlat 35081 df-hlat 35110 df-llines 35256 df-lplanes 35257 df-lvols 35258 df-lines 35259 df-psubsp 35261 df-pmap 35262 df-padd 35554 df-lhyp 35746 df-laut 35747 df-ldil 35862 df-ltrn 35863 df-trl 35918 df-tgrp 36502 df-tendo 36514 df-edring 36516 df-dveca 36762 df-disoa 36789 df-dvech 36839 df-dib 36899 df-dic 36933 df-dih 36989 df-doch 37108 df-djh 37155 df-mapd 37385

This theorem is referenced by: mapdcnvordN 37418 mapdcv 37420 mapdin 37422 mapdlsm 37424 mapdcnvatN 37426 hdmaprnlem3N 37613 hdmaprnlem9N 37620 hdmaprnlem16N 37625

W3C validator