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 42522

Description: Value of the map defined by df-mapd 42506 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 2762	. . 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 41991	. . . 4 ⊢ (𝜑 → 𝑈 ∈ LMod)
10		mapdsn.x	. . . 4 ⊢ (𝜑 → 𝑋 ∈ 𝑉)
11		mapdsn.v	. . . . 5 ⊢ 𝑉 = (Base‘𝑈)
12		mapdsn.n	. . . . 5 ⊢ 𝑁 = (LSpan‘𝑈)
13	11, 3, 12	lspsncl 21167	. . . 4 ⊢ ((𝑈 ∈ LMod ∧ 𝑋 ∈ 𝑉) → (𝑁‘{𝑋}) ∈ (LSubSp‘𝑈))
14	9, 10, 13	syl2anc 596	. . 3 ⊢ (𝜑 → (𝑁‘{𝑋}) ∈ (LSubSp‘𝑈))
15	1, 2, 3, 4, 5, 6, 7, 8, 14	mapdval 42509	. 2 ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = {𝑓 ∈ 𝐹 ∣ ((𝑂‘(𝑂‘(𝐿‘𝑓))) = (𝐿‘𝑓) ∧ (𝑂‘(𝐿‘𝑓)) ⊆ (𝑁‘{𝑋}))})
16	8	ad2antrr 739	. . . . . 6 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐹) ∧ ((𝑂‘(𝑂‘(𝐿‘𝑓))) = (𝐿‘𝑓) ∧ (𝑂‘(𝐿‘𝑓)) ⊆ (𝑁‘{𝑋}))) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
17	10	snssd 4750	. . . . . . . 8 ⊢ (𝜑 → {𝑋} ⊆ 𝑉)
18	11, 12	lspssv 21173	. . . . . . . 8 ⊢ ((𝑈 ∈ LMod ∧ {𝑋} ⊆ 𝑉) → (𝑁‘{𝑋}) ⊆ 𝑉)
19	9, 17, 18	syl2anc 596	. . . . . . 7 ⊢ (𝜑 → (𝑁‘{𝑋}) ⊆ 𝑉)
20	19	ad2antrr 739	. . . . . 6 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐹) ∧ ((𝑂‘(𝑂‘(𝐿‘𝑓))) = (𝐿‘𝑓) ∧ (𝑂‘(𝐿‘𝑓)) ⊆ (𝑁‘{𝑋}))) → (𝑁‘{𝑋}) ⊆ 𝑉)
21		simprr 785	. . . . . 6 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐹) ∧ ((𝑂‘(𝑂‘(𝐿‘𝑓))) = (𝐿‘𝑓) ∧ (𝑂‘(𝐿‘𝑓)) ⊆ (𝑁‘{𝑋}))) → (𝑂‘(𝐿‘𝑓)) ⊆ (𝑁‘{𝑋}))
22	1, 2, 11, 6	dochss 42246	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑁‘{𝑋}) ⊆ 𝑉 ∧ (𝑂‘(𝐿‘𝑓)) ⊆ (𝑁‘{𝑋})) → (𝑂‘(𝑁‘{𝑋})) ⊆ (𝑂‘(𝑂‘(𝐿‘𝑓))))
23	16, 20, 21, 22	syl3anc 1398	. . . . 5 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐹) ∧ ((𝑂‘(𝑂‘(𝐿‘𝑓))) = (𝐿‘𝑓) ∧ (𝑂‘(𝐿‘𝑓)) ⊆ (𝑁‘{𝑋}))) → (𝑂‘(𝑁‘{𝑋})) ⊆ (𝑂‘(𝑂‘(𝐿‘𝑓))))
24	1, 2, 6, 11, 12, 8, 17	dochocsp 42260	. . . . . 6 ⊢ (𝜑 → (𝑂‘(𝑁‘{𝑋})) = (𝑂‘{𝑋}))
25	24	ad2antrr 739	. . . . 5 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐹) ∧ ((𝑂‘(𝑂‘(𝐿‘𝑓))) = (𝐿‘𝑓) ∧ (𝑂‘(𝐿‘𝑓)) ⊆ (𝑁‘{𝑋}))) → (𝑂‘(𝑁‘{𝑋})) = (𝑂‘{𝑋}))
26		simprl 783	. . . . 5 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐹) ∧ ((𝑂‘(𝑂‘(𝐿‘𝑓))) = (𝐿‘𝑓) ∧ (𝑂‘(𝐿‘𝑓)) ⊆ (𝑁‘{𝑋}))) → (𝑂‘(𝑂‘(𝐿‘𝑓))) = (𝐿‘𝑓))
27	23, 25, 26	3sstr3d 3988	. . . 4 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐹) ∧ ((𝑂‘(𝑂‘(𝐿‘𝑓))) = (𝐿‘𝑓) ∧ (𝑂‘(𝐿‘𝑓)) ⊆ (𝑁‘{𝑋}))) → (𝑂‘{𝑋}) ⊆ (𝐿‘𝑓))
28	8	ad2antrr 739	. . . . . 6 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐹) ∧ (𝑂‘{𝑋}) ⊆ (𝐿‘𝑓)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
29		simplr 781	. . . . . 6 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐹) ∧ (𝑂‘{𝑋}) ⊆ (𝐿‘𝑓)) → 𝑓 ∈ 𝐹)
30	10	ad2antrr 739	. . . . . 6 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐹) ∧ (𝑂‘{𝑋}) ⊆ (𝐿‘𝑓)) → 𝑋 ∈ 𝑉)
31		simpr 490	. . . . . 6 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐹) ∧ (𝑂‘{𝑋}) ⊆ (𝐿‘𝑓)) → (𝑂‘{𝑋}) ⊆ (𝐿‘𝑓))
32	1, 6, 2, 11, 4, 5, 28, 29, 30, 31	lcfl9a 42386	. . . . 5 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐹) ∧ (𝑂‘{𝑋}) ⊆ (𝐿‘𝑓)) → (𝑂‘(𝑂‘(𝐿‘𝑓))) = (𝐿‘𝑓))
33	9	ad2antrr 739	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐹) ∧ (𝑂‘{𝑋}) ⊆ (𝐿‘𝑓)) → 𝑈 ∈ LMod)
34	11, 4, 5, 33, 29	lkrssv 39977	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐹) ∧ (𝑂‘{𝑋}) ⊆ (𝐿‘𝑓)) → (𝐿‘𝑓) ⊆ 𝑉)
35	1, 2, 11, 6	dochss 42246	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐿‘𝑓) ⊆ 𝑉 ∧ (𝑂‘{𝑋}) ⊆ (𝐿‘𝑓)) → (𝑂‘(𝐿‘𝑓)) ⊆ (𝑂‘(𝑂‘{𝑋})))
36	28, 34, 31, 35	syl3anc 1398	. . . . . 6 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐹) ∧ (𝑂‘{𝑋}) ⊆ (𝐿‘𝑓)) → (𝑂‘(𝐿‘𝑓)) ⊆ (𝑂‘(𝑂‘{𝑋})))
37	1, 2, 6, 11, 12, 8, 10	dochocsn 42262	. . . . . . 7 ⊢ (𝜑 → (𝑂‘(𝑂‘{𝑋})) = (𝑁‘{𝑋}))
38	37	ad2antrr 739	. . . . . 6 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐹) ∧ (𝑂‘{𝑋}) ⊆ (𝐿‘𝑓)) → (𝑂‘(𝑂‘{𝑋})) = (𝑁‘{𝑋}))
39	36, 38	sseqtrd 3970	. . . . 5 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐹) ∧ (𝑂‘{𝑋}) ⊆ (𝐿‘𝑓)) → (𝑂‘(𝐿‘𝑓)) ⊆ (𝑁‘{𝑋}))
40	32, 39	jca 521	. . . 4 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐹) ∧ (𝑂‘{𝑋}) ⊆ (𝐿‘𝑓)) → ((𝑂‘(𝑂‘(𝐿‘𝑓))) = (𝐿‘𝑓) ∧ (𝑂‘(𝐿‘𝑓)) ⊆ (𝑁‘{𝑋})))
41	27, 40	impbida 813	. . 3 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐹) → (((𝑂‘(𝑂‘(𝐿‘𝑓))) = (𝐿‘𝑓) ∧ (𝑂‘(𝐿‘𝑓)) ⊆ (𝑁‘{𝑋})) ↔ (𝑂‘{𝑋}) ⊆ (𝐿‘𝑓)))
42	41	rabbidva 3420	. 2 ⊢ (𝜑 → {𝑓 ∈ 𝐹 ∣ ((𝑂‘(𝑂‘(𝐿‘𝑓))) = (𝐿‘𝑓) ∧ (𝑂‘(𝐿‘𝑓)) ⊆ (𝑁‘{𝑋}))} = {𝑓 ∈ 𝐹 ∣ (𝑂‘{𝑋}) ⊆ (𝐿‘𝑓)})
43	15, 42	eqtrd 2797	1 ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = {𝑓 ∈ 𝐹 ∣ (𝑂‘{𝑋}) ⊆ (𝐿‘𝑓)})

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ∧ wa 401 = wceq 1570 ∈ wcel 2145 {crab 3414 ⊆ wss 3902 {csn 4587 ‘cfv 6537 Basecbs 17307 LModclmod 21050 LSubSpclss 21121 LSpanclspn 21161 LFnlclfn 39938 LKerclk 39966 HLchlt 40231 LHypclh 40865 DVecHcdvh 41959 ocHcoch 42228 mapdcmpd 42505

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2215 ax-ext 2734 ax-rep 5236 ax-sep 5255 ax-nul 5267 ax-pow 5334 ax-pr 5402 ax-un 7740 ax-cnex 11184 ax-resscn 11185 ax-1cn 11186 ax-icn 11187 ax-addcl 11188 ax-addrcl 11189 ax-mulcl 11190 ax-mulrcl 11191 ax-mulcom 11192 ax-addass 11193 ax-mulass 11194 ax-distr 11195 ax-i2m1 11196 ax-1ne0 11197 ax-1rid 11198 ax-rnegex 11199 ax-rrecex 11200 ax-cnre 11201 ax-pre-lttri 11202 ax-pre-lttrn 11203 ax-pre-ltadd 11204 ax-pre-mulgt0 11205 ax-riotaBAD 39834

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2566 df-eu 2596 df-clab 2741 df-cleq 2754 df-clel 2837 df-nfc 2911 df-ne 2958 df-nel 3064 df-ral 3079 df-rex 3089 df-rmo 3367 df-reu 3368 df-rab 3415 df-v 3455 df-sbc 3743 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-pss 3922 df-nul 4283 df-if 4486 df-pw 4562 df-sn 4588 df-pr 4590 df-tp 4592 df-op 4594 df-uni 4871 df-int 4911 df-iun 4956 df-iin 4957 df-br 5108 df-opab 5172 df-mpt 5191 df-tr 5217 df-id 5554 df-eprel 5559 df-po 5567 df-so 5568 df-fr 5612 df-we 5614 df-xp 5665 df-rel 5666 df-cnv 5667 df-co 5668 df-dm 5669 df-rn 5670 df-res 5671 df-ima 5672 df-pred 6303 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-riota 7374 df-ov 7420 df-oprab 7421 df-mpo 7422 df-om 7867 df-1st 7990 df-2nd 7991 df-tpos 8228 df-undef 8275 df-frecs 8284 df-wrecs 8315 df-recs 8364 df-rdg 8403 df-1o 8459 df-er 8700 df-map 8832 df-en 8957 df-dom 8958 df-sdom 8959 df-fin 8960 df-pnf 11273 df-mnf 11274 df-xr 11275 df-ltxr 11276 df-le 11277 df-sub 11471 df-neg 11472 df-nn 12262 df-2 12331 df-3 12332 df-4 12333 df-5 12334 df-6 12335 df-n0 12533 df-z 12620 df-uz 12892 df-fz 13566 df-struct 17245 df-sets 17262 df-slot 17280 df-ndx 17292 df-base 17308 df-ress 17329 df-plusg 17361 df-mulr 17362 df-sca 17364 df-vsca 17365 df-0g 17532 df-proset 18388 df-poset 18407 df-plt 18422 df-lub 18438 df-glb 18439 df-join 18440 df-meet 18441 df-p0 18517 df-p1 18518 df-lat 18526 df-clat 18593 df-mgm 18736 df-sgrp 18827 df-mnd 18843 df-submnd 18898 df-grp 19066 df-minusg 19067 df-sbg 19068 df-subg 19252 df-cntz 19450 df-lsm 19769 df-cmn 19915 df-abl 19916 df-mgp 20280 df-rng 20294 df-ur 20327 df-ring 20380 df-oppr 20484 df-dvdsr 20504 df-unit 20505 df-invr 20535 df-dvr 20548 df-drng 20898 df-lmod 21052 df-lss 21122 df-lsp 21162 df-lvec 21293 df-lsatoms 39857 df-lshyp 39858 df-lfl 39939 df-lkr 39967 df-oposet 40057 df-ol 40059 df-oml 40060 df-covers 40147 df-ats 40148 df-atl 40179 df-cvlat 40203 df-hlat 40232 df-llines 40379 df-lplanes 40380 df-lvols 40381 df-lines 40382 df-psubsp 40384 df-pmap 40385 df-padd 40677 df-lhyp 40869 df-laut 40870 df-ldil 40985 df-ltrn 40986 df-trl 41040 df-tgrp 41624 df-tendo 41636 df-edring 41638 df-dveca 41884 df-disoa 41910 df-dvech 41960 df-dib 42020 df-dic 42054 df-dih 42110 df-doch 42229 df-djh 42276 df-mapd 42506

This theorem is used by: mapdsn2 42523 hdmaplkr 42794

W3C validator