mapdsn - Mathbox for Norm Megill

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

Theorem mapdsn 41584

Description: Value of the map defined by df-mapd 41568 at the span of a singleton. (Contributed by NM, 16-Feb-2015.)

**Hypotheses**
Ref	Expression
mapdsn.h	⊢ 𝐻 = (LHyp‘𝐾)
mapdsn.o	⊢ 𝑂 = ((ocH‘𝐾)‘𝑊)
mapdsn.m	⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)
mapdsn.u	⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)
mapdsn.v	⊢ 𝑉 = (Base‘𝑈)
mapdsn.n	⊢ 𝑁 = (LSpan‘𝑈)
mapdsn.f	⊢ 𝐹 = (LFnl‘𝑈)
mapdsn.l	⊢ 𝐿 = (LKer‘𝑈)
mapdsn.k	⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
mapdsn.x	⊢ (𝜑 → 𝑋 ∈ 𝑉)

**Assertion**
Ref	Expression
mapdsn	⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = {𝑓 ∈ 𝐹 ∣ (𝑂‘{𝑋}) ⊆ (𝐿‘𝑓)})

Distinct variable groups: 𝑓,𝐹 𝑓,𝐾 𝑓,𝑁 𝑓,𝑊 𝑓,𝑋 𝜑,𝑓 Allowed substitution hints: 𝑈(𝑓) 𝐻(𝑓) 𝐿(𝑓) 𝑀(𝑓) 𝑂(𝑓) 𝑉(𝑓)

**Proof of Theorem mapdsn**
Step	Hyp	Ref	Expression
1		mapdsn.h	. . 3 ⊢ 𝐻 = (LHyp‘𝐾)
2		mapdsn.u	. . 3 ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)
3		eqid 2734	. . 3 ⊢ (LSubSp‘𝑈) = (LSubSp‘𝑈)
4		mapdsn.f	. . 3 ⊢ 𝐹 = (LFnl‘𝑈)
5		mapdsn.l	. . 3 ⊢ 𝐿 = (LKer‘𝑈)
6		mapdsn.o	. . 3 ⊢ 𝑂 = ((ocH‘𝐾)‘𝑊)
7		mapdsn.m	. . 3 ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)
8		mapdsn.k	. . 3 ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
9	1, 2, 8	dvhlmod 41053	. . . 4 ⊢ (𝜑 → 𝑈 ∈ LMod)
10		mapdsn.x	. . . 4 ⊢ (𝜑 → 𝑋 ∈ 𝑉)
11		mapdsn.v	. . . . 5 ⊢ 𝑉 = (Base‘𝑈)
12		mapdsn.n	. . . . 5 ⊢ 𝑁 = (LSpan‘𝑈)
13	11, 3, 12	lspsncl 20948	. . . 4 ⊢ ((𝑈 ∈ LMod ∧ 𝑋 ∈ 𝑉) → (𝑁‘{𝑋}) ∈ (LSubSp‘𝑈))
14	9, 10, 13	syl2anc 584	. . 3 ⊢ (𝜑 → (𝑁‘{𝑋}) ∈ (LSubSp‘𝑈))
15	1, 2, 3, 4, 5, 6, 7, 8, 14	mapdval 41571	. 2 ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = {𝑓 ∈ 𝐹 ∣ ((𝑂‘(𝑂‘(𝐿‘𝑓))) = (𝐿‘𝑓) ∧ (𝑂‘(𝐿‘𝑓)) ⊆ (𝑁‘{𝑋}))})
16	8	ad2antrr 726	. . . . . 6 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐹) ∧ ((𝑂‘(𝑂‘(𝐿‘𝑓))) = (𝐿‘𝑓) ∧ (𝑂‘(𝐿‘𝑓)) ⊆ (𝑁‘{𝑋}))) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
17	10	snssd 4791	. . . . . . . 8 ⊢ (𝜑 → {𝑋} ⊆ 𝑉)
18	11, 12	lspssv 20954	. . . . . . . 8 ⊢ ((𝑈 ∈ LMod ∧ {𝑋} ⊆ 𝑉) → (𝑁‘{𝑋}) ⊆ 𝑉)
19	9, 17, 18	syl2anc 584	. . . . . . 7 ⊢ (𝜑 → (𝑁‘{𝑋}) ⊆ 𝑉)
20	19	ad2antrr 726	. . . . . 6 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐹) ∧ ((𝑂‘(𝑂‘(𝐿‘𝑓))) = (𝐿‘𝑓) ∧ (𝑂‘(𝐿‘𝑓)) ⊆ (𝑁‘{𝑋}))) → (𝑁‘{𝑋}) ⊆ 𝑉)
21		simprr 772	. . . . . 6 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐹) ∧ ((𝑂‘(𝑂‘(𝐿‘𝑓))) = (𝐿‘𝑓) ∧ (𝑂‘(𝐿‘𝑓)) ⊆ (𝑁‘{𝑋}))) → (𝑂‘(𝐿‘𝑓)) ⊆ (𝑁‘{𝑋}))
22	1, 2, 11, 6	dochss 41308	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑁‘{𝑋}) ⊆ 𝑉 ∧ (𝑂‘(𝐿‘𝑓)) ⊆ (𝑁‘{𝑋})) → (𝑂‘(𝑁‘{𝑋})) ⊆ (𝑂‘(𝑂‘(𝐿‘𝑓))))
23	16, 20, 21, 22	syl3anc 1372	. . . . 5 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐹) ∧ ((𝑂‘(𝑂‘(𝐿‘𝑓))) = (𝐿‘𝑓) ∧ (𝑂‘(𝐿‘𝑓)) ⊆ (𝑁‘{𝑋}))) → (𝑂‘(𝑁‘{𝑋})) ⊆ (𝑂‘(𝑂‘(𝐿‘𝑓))))
24	1, 2, 6, 11, 12, 8, 17	dochocsp 41322	. . . . . 6 ⊢ (𝜑 → (𝑂‘(𝑁‘{𝑋})) = (𝑂‘{𝑋}))
25	24	ad2antrr 726	. . . . 5 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐹) ∧ ((𝑂‘(𝑂‘(𝐿‘𝑓))) = (𝐿‘𝑓) ∧ (𝑂‘(𝐿‘𝑓)) ⊆ (𝑁‘{𝑋}))) → (𝑂‘(𝑁‘{𝑋})) = (𝑂‘{𝑋}))
26		simprl 770	. . . . 5 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐹) ∧ ((𝑂‘(𝑂‘(𝐿‘𝑓))) = (𝐿‘𝑓) ∧ (𝑂‘(𝐿‘𝑓)) ⊆ (𝑁‘{𝑋}))) → (𝑂‘(𝑂‘(𝐿‘𝑓))) = (𝐿‘𝑓))
27	23, 25, 26	3sstr3d 4020	. . . 4 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐹) ∧ ((𝑂‘(𝑂‘(𝐿‘𝑓))) = (𝐿‘𝑓) ∧ (𝑂‘(𝐿‘𝑓)) ⊆ (𝑁‘{𝑋}))) → (𝑂‘{𝑋}) ⊆ (𝐿‘𝑓))
28	8	ad2antrr 726	. . . . . 6 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐹) ∧ (𝑂‘{𝑋}) ⊆ (𝐿‘𝑓)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
29		simplr 768	. . . . . 6 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐹) ∧ (𝑂‘{𝑋}) ⊆ (𝐿‘𝑓)) → 𝑓 ∈ 𝐹)
30	10	ad2antrr 726	. . . . . 6 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐹) ∧ (𝑂‘{𝑋}) ⊆ (𝐿‘𝑓)) → 𝑋 ∈ 𝑉)
31		simpr 484	. . . . . 6 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐹) ∧ (𝑂‘{𝑋}) ⊆ (𝐿‘𝑓)) → (𝑂‘{𝑋}) ⊆ (𝐿‘𝑓))
32	1, 6, 2, 11, 4, 5, 28, 29, 30, 31	lcfl9a 41448	. . . . 5 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐹) ∧ (𝑂‘{𝑋}) ⊆ (𝐿‘𝑓)) → (𝑂‘(𝑂‘(𝐿‘𝑓))) = (𝐿‘𝑓))
33	9	ad2antrr 726	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐹) ∧ (𝑂‘{𝑋}) ⊆ (𝐿‘𝑓)) → 𝑈 ∈ LMod)
34	11, 4, 5, 33, 29	lkrssv 39038	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐹) ∧ (𝑂‘{𝑋}) ⊆ (𝐿‘𝑓)) → (𝐿‘𝑓) ⊆ 𝑉)
35	1, 2, 11, 6	dochss 41308	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐿‘𝑓) ⊆ 𝑉 ∧ (𝑂‘{𝑋}) ⊆ (𝐿‘𝑓)) → (𝑂‘(𝐿‘𝑓)) ⊆ (𝑂‘(𝑂‘{𝑋})))
36	28, 34, 31, 35	syl3anc 1372	. . . . . 6 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐹) ∧ (𝑂‘{𝑋}) ⊆ (𝐿‘𝑓)) → (𝑂‘(𝐿‘𝑓)) ⊆ (𝑂‘(𝑂‘{𝑋})))
37	1, 2, 6, 11, 12, 8, 10	dochocsn 41324	. . . . . . 7 ⊢ (𝜑 → (𝑂‘(𝑂‘{𝑋})) = (𝑁‘{𝑋}))
38	37	ad2antrr 726	. . . . . 6 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐹) ∧ (𝑂‘{𝑋}) ⊆ (𝐿‘𝑓)) → (𝑂‘(𝑂‘{𝑋})) = (𝑁‘{𝑋}))
39	36, 38	sseqtrd 4002	. . . . 5 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐹) ∧ (𝑂‘{𝑋}) ⊆ (𝐿‘𝑓)) → (𝑂‘(𝐿‘𝑓)) ⊆ (𝑁‘{𝑋}))
40	32, 39	jca 511	. . . 4 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐹) ∧ (𝑂‘{𝑋}) ⊆ (𝐿‘𝑓)) → ((𝑂‘(𝑂‘(𝐿‘𝑓))) = (𝐿‘𝑓) ∧ (𝑂‘(𝐿‘𝑓)) ⊆ (𝑁‘{𝑋})))
41	27, 40	impbida 800	. . 3 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐹) → (((𝑂‘(𝑂‘(𝐿‘𝑓))) = (𝐿‘𝑓) ∧ (𝑂‘(𝐿‘𝑓)) ⊆ (𝑁‘{𝑋})) ↔ (𝑂‘{𝑋}) ⊆ (𝐿‘𝑓)))
42	41	rabbidva 3427	. 2 ⊢ (𝜑 → {𝑓 ∈ 𝐹 ∣ ((𝑂‘(𝑂‘(𝐿‘𝑓))) = (𝐿‘𝑓) ∧ (𝑂‘(𝐿‘𝑓)) ⊆ (𝑁‘{𝑋}))} = {𝑓 ∈ 𝐹 ∣ (𝑂‘{𝑋}) ⊆ (𝐿‘𝑓)})
43	15, 42	eqtrd 2769	1 ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = {𝑓 ∈ 𝐹 ∣ (𝑂‘{𝑋}) ⊆ (𝐿‘𝑓)})

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 = wceq 1539 ∈ wcel 2107 {crab 3420 ⊆ wss 3933 {csn 4608 ‘cfv 6542 Basecbs 17230 LModclmod 20831 LSubSpclss 20902 LSpanclspn 20942 LFnlclfn 38999 LKerclk 39027 HLchlt 39292 LHypclh 39927 DVecHcdvh 41021 ocHcoch 41290 mapdcmpd 41567

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-10 2140 ax-11 2156 ax-12 2176 ax-ext 2706 ax-rep 5261 ax-sep 5278 ax-nul 5288 ax-pow 5347 ax-pr 5414 ax-un 7738 ax-cnex 11194 ax-resscn 11195 ax-1cn 11196 ax-icn 11197 ax-addcl 11198 ax-addrcl 11199 ax-mulcl 11200 ax-mulrcl 11201 ax-mulcom 11202 ax-addass 11203 ax-mulass 11204 ax-distr 11205 ax-i2m1 11206 ax-1ne0 11207 ax-1rid 11208 ax-rnegex 11209 ax-rrecex 11210 ax-cnre 11211 ax-pre-lttri 11212 ax-pre-lttrn 11213 ax-pre-ltadd 11214 ax-pre-mulgt0 11215 ax-riotaBAD 38895

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1779 df-nf 1783 df-sb 2064 df-mo 2538 df-eu 2567 df-clab 2713 df-cleq 2726 df-clel 2808 df-nfc 2884 df-ne 2932 df-nel 3036 df-ral 3051 df-rex 3060 df-rmo 3364 df-reu 3365 df-rab 3421 df-v 3466 df-sbc 3773 df-csb 3882 df-dif 3936 df-un 3938 df-in 3940 df-ss 3950 df-pss 3953 df-nul 4316 df-if 4508 df-pw 4584 df-sn 4609 df-pr 4611 df-tp 4613 df-op 4615 df-uni 4890 df-int 4929 df-iun 4975 df-iin 4976 df-br 5126 df-opab 5188 df-mpt 5208 df-tr 5242 df-id 5560 df-eprel 5566 df-po 5574 df-so 5575 df-fr 5619 df-we 5621 df-xp 5673 df-rel 5674 df-cnv 5675 df-co 5676 df-dm 5677 df-rn 5678 df-res 5679 df-ima 5680 df-pred 6303 df-ord 6368 df-on 6369 df-lim 6370 df-suc 6371 df-iota 6495 df-fun 6544 df-fn 6545 df-f 6546 df-f1 6547 df-fo 6548 df-f1o 6549 df-fv 6550 df-riota 7371 df-ov 7417 df-oprab 7418 df-mpo 7419 df-om 7871 df-1st 7997 df-2nd 7998 df-tpos 8234 df-undef 8281 df-frecs 8289 df-wrecs 8320 df-recs 8394 df-rdg 8433 df-1o 8489 df-er 8728 df-map 8851 df-en 8969 df-dom 8970 df-sdom 8971 df-fin 8972 df-pnf 11280 df-mnf 11281 df-xr 11282 df-ltxr 11283 df-le 11284 df-sub 11477 df-neg 11478 df-nn 12250 df-2 12312 df-3 12313 df-4 12314 df-5 12315 df-6 12316 df-n0 12511 df-z 12598 df-uz 12862 df-fz 13531 df-struct 17167 df-sets 17184 df-slot 17202 df-ndx 17214 df-base 17231 df-ress 17257 df-plusg 17290 df-mulr 17291 df-sca 17293 df-vsca 17294 df-0g 17462 df-proset 18315 df-poset 18334 df-plt 18349 df-lub 18365 df-glb 18366 df-join 18367 df-meet 18368 df-p0 18444 df-p1 18445 df-lat 18451 df-clat 18518 df-mgm 18627 df-sgrp 18706 df-mnd 18722 df-submnd 18771 df-grp 18928 df-minusg 18929 df-sbg 18930 df-subg 19115 df-cntz 19309 df-lsm 19627 df-cmn 19773 df-abl 19774 df-mgp 20111 df-rng 20123 df-ur 20152 df-ring 20205 df-oppr 20307 df-dvdsr 20330 df-unit 20331 df-invr 20361 df-dvr 20374 df-drng 20704 df-lmod 20833 df-lss 20903 df-lsp 20943 df-lvec 21075 df-lsatoms 38918 df-lshyp 38919 df-lfl 39000 df-lkr 39028 df-oposet 39118 df-ol 39120 df-oml 39121 df-covers 39208 df-ats 39209 df-atl 39240 df-cvlat 39264 df-hlat 39293 df-llines 39441 df-lplanes 39442 df-lvols 39443 df-lines 39444 df-psubsp 39446 df-pmap 39447 df-padd 39739 df-lhyp 39931 df-laut 39932 df-ldil 40047 df-ltrn 40048 df-trl 40102 df-tgrp 40686 df-tendo 40698 df-edring 40700 df-dveca 40946 df-disoa 40972 df-dvech 41022 df-dib 41082 df-dic 41116 df-dih 41172 df-doch 41291 df-djh 41338 df-mapd 41568

This theorem is referenced by: mapdsn2 41585 hdmaplkr 41856

W3C validator