mapdindp - Mathbox for Norm Megill

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

Theorem mapdindp 38288

Description: Transfer (part of) vector independence condition from domain to range of projectivity mapd. (Contributed by NM, 11-Apr-2015.)

**Hypotheses**
Ref	Expression
mapdindp.h	⊢ 𝐻 = (LHyp‘𝐾)
mapdindp.m	⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)
mapdindp.u	⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)
mapdindp.v	⊢ 𝑉 = (Base‘𝑈)
mapdindp.n	⊢ 𝑁 = (LSpan‘𝑈)
mapdindp.c	⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)
mapdindp.d	⊢ 𝐷 = (Base‘𝐶)
mapdindp.j	⊢ 𝐽 = (LSpan‘𝐶)
mapdindp.k	⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
mapdindp.f	⊢ (𝜑 → 𝐹 ∈ 𝐷)
mapdindp.mx	⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐹}))
mapdindp.x	⊢ (𝜑 → 𝑋 ∈ 𝑉)
mapdindp.y	⊢ (𝜑 → 𝑌 ∈ 𝑉)
mapdindp.g	⊢ (𝜑 → 𝐺 ∈ 𝐷)
mapdindp.my	⊢ (𝜑 → (𝑀‘(𝑁‘{𝑌})) = (𝐽‘{𝐺}))
mapdindp.z	⊢ (𝜑 → 𝑍 ∈ 𝑉)
mapdindp.e	⊢ (𝜑 → 𝐸 ∈ 𝐷)
mapdindp.mg	⊢ (𝜑 → (𝑀‘(𝑁‘{𝑍})) = (𝐽‘{𝐸}))
mapdindp.xn	⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍}))

**Assertion**
Ref	Expression
mapdindp	⊢ (𝜑 → ¬ 𝐹 ∈ (𝐽‘{𝐺, 𝐸}))

**Proof of Theorem mapdindp**
Step	Hyp	Ref	Expression
1		mapdindp.xn	. 2 ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍}))
2		mapdindp.d	. . . 4 ⊢ 𝐷 = (Base‘𝐶)
3		eqid 2793	. . . 4 ⊢ (LSubSp‘𝐶) = (LSubSp‘𝐶)
4		mapdindp.j	. . . 4 ⊢ 𝐽 = (LSpan‘𝐶)
5		mapdindp.h	. . . . 5 ⊢ 𝐻 = (LHyp‘𝐾)
6		mapdindp.c	. . . . 5 ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)
7		mapdindp.k	. . . . 5 ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
8	5, 6, 7	lcdlmod 38209	. . . 4 ⊢ (𝜑 → 𝐶 ∈ LMod)
9		mapdindp.g	. . . . 5 ⊢ (𝜑 → 𝐺 ∈ 𝐷)
10		mapdindp.e	. . . . 5 ⊢ (𝜑 → 𝐸 ∈ 𝐷)
11	2, 3, 4, 8, 9, 10	lspprcl 19428	. . . 4 ⊢ (𝜑 → (𝐽‘{𝐺, 𝐸}) ∈ (LSubSp‘𝐶))
12		mapdindp.f	. . . 4 ⊢ (𝜑 → 𝐹 ∈ 𝐷)
13	2, 3, 4, 8, 11, 12	lspsnel5 19445	. . 3 ⊢ (𝜑 → (𝐹 ∈ (𝐽‘{𝐺, 𝐸}) ↔ (𝐽‘{𝐹}) ⊆ (𝐽‘{𝐺, 𝐸})))
14		mapdindp.v	. . . . 5 ⊢ 𝑉 = (Base‘𝑈)
15		eqid 2793	. . . . 5 ⊢ (LSubSp‘𝑈) = (LSubSp‘𝑈)
16		mapdindp.n	. . . . 5 ⊢ 𝑁 = (LSpan‘𝑈)
17		mapdindp.u	. . . . . 6 ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)
18	5, 17, 7	dvhlmod 37727	. . . . 5 ⊢ (𝜑 → 𝑈 ∈ LMod)
19		mapdindp.y	. . . . . 6 ⊢ (𝜑 → 𝑌 ∈ 𝑉)
20		mapdindp.z	. . . . . 6 ⊢ (𝜑 → 𝑍 ∈ 𝑉)
21	14, 15, 16, 18, 19, 20	lspprcl 19428	. . . . 5 ⊢ (𝜑 → (𝑁‘{𝑌, 𝑍}) ∈ (LSubSp‘𝑈))
22		mapdindp.x	. . . . 5 ⊢ (𝜑 → 𝑋 ∈ 𝑉)
23	14, 15, 16, 18, 21, 22	lspsnel5 19445	. . . 4 ⊢ (𝜑 → (𝑋 ∈ (𝑁‘{𝑌, 𝑍}) ↔ (𝑁‘{𝑋}) ⊆ (𝑁‘{𝑌, 𝑍})))
24		mapdindp.m	. . . . 5 ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)
25	14, 15, 16	lspsncl 19427	. . . . . 6 ⊢ ((𝑈 ∈ LMod ∧ 𝑋 ∈ 𝑉) → (𝑁‘{𝑋}) ∈ (LSubSp‘𝑈))
26	18, 22, 25	syl2anc 584	. . . . 5 ⊢ (𝜑 → (𝑁‘{𝑋}) ∈ (LSubSp‘𝑈))
27	5, 17, 15, 24, 7, 26, 21	mapdord 38255	. . . 4 ⊢ (𝜑 → ((𝑀‘(𝑁‘{𝑋})) ⊆ (𝑀‘(𝑁‘{𝑌, 𝑍})) ↔ (𝑁‘{𝑋}) ⊆ (𝑁‘{𝑌, 𝑍})))
28		mapdindp.mx	. . . . 5 ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐹}))
29		eqid 2793	. . . . . . . . 9 ⊢ (LSSum‘𝑈) = (LSSum‘𝑈)
30	14, 16, 29, 18, 19, 20	lsmpr 19539	. . . . . . . 8 ⊢ (𝜑 → (𝑁‘{𝑌, 𝑍}) = ((𝑁‘{𝑌})(LSSum‘𝑈)(𝑁‘{𝑍})))
31	30	fveq2d 6534	. . . . . . 7 ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑌, 𝑍})) = (𝑀‘((𝑁‘{𝑌})(LSSum‘𝑈)(𝑁‘{𝑍}))))
32		eqid 2793	. . . . . . . 8 ⊢ (LSSum‘𝐶) = (LSSum‘𝐶)
33	14, 15, 16	lspsncl 19427	. . . . . . . . 9 ⊢ ((𝑈 ∈ LMod ∧ 𝑌 ∈ 𝑉) → (𝑁‘{𝑌}) ∈ (LSubSp‘𝑈))
34	18, 19, 33	syl2anc 584	. . . . . . . 8 ⊢ (𝜑 → (𝑁‘{𝑌}) ∈ (LSubSp‘𝑈))
35	14, 15, 16	lspsncl 19427	. . . . . . . . 9 ⊢ ((𝑈 ∈ LMod ∧ 𝑍 ∈ 𝑉) → (𝑁‘{𝑍}) ∈ (LSubSp‘𝑈))
36	18, 20, 35	syl2anc 584	. . . . . . . 8 ⊢ (𝜑 → (𝑁‘{𝑍}) ∈ (LSubSp‘𝑈))
37	5, 24, 17, 15, 29, 6, 32, 7, 34, 36	mapdlsm 38281	. . . . . . 7 ⊢ (𝜑 → (𝑀‘((𝑁‘{𝑌})(LSSum‘𝑈)(𝑁‘{𝑍}))) = ((𝑀‘(𝑁‘{𝑌}))(LSSum‘𝐶)(𝑀‘(𝑁‘{𝑍}))))
38		mapdindp.my	. . . . . . . 8 ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑌})) = (𝐽‘{𝐺}))
39		mapdindp.mg	. . . . . . . 8 ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑍})) = (𝐽‘{𝐸}))
40	38, 39	oveq12d 7025	. . . . . . 7 ⊢ (𝜑 → ((𝑀‘(𝑁‘{𝑌}))(LSSum‘𝐶)(𝑀‘(𝑁‘{𝑍}))) = ((𝐽‘{𝐺})(LSSum‘𝐶)(𝐽‘{𝐸})))
41	31, 37, 40	3eqtrd 2833	. . . . . 6 ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑌, 𝑍})) = ((𝐽‘{𝐺})(LSSum‘𝐶)(𝐽‘{𝐸})))
42	2, 4, 32, 8, 9, 10	lsmpr 19539	. . . . . 6 ⊢ (𝜑 → (𝐽‘{𝐺, 𝐸}) = ((𝐽‘{𝐺})(LSSum‘𝐶)(𝐽‘{𝐸})))
43	41, 42	eqtr4d 2832	. . . . 5 ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑌, 𝑍})) = (𝐽‘{𝐺, 𝐸}))
44	28, 43	sseq12d 3916	. . . 4 ⊢ (𝜑 → ((𝑀‘(𝑁‘{𝑋})) ⊆ (𝑀‘(𝑁‘{𝑌, 𝑍})) ↔ (𝐽‘{𝐹}) ⊆ (𝐽‘{𝐺, 𝐸})))
45	23, 27, 44	3bitr2rd 309	. . 3 ⊢ (𝜑 → ((𝐽‘{𝐹}) ⊆ (𝐽‘{𝐺, 𝐸}) ↔ 𝑋 ∈ (𝑁‘{𝑌, 𝑍})))
46	13, 45	bitrd 280	. 2 ⊢ (𝜑 → (𝐹 ∈ (𝐽‘{𝐺, 𝐸}) ↔ 𝑋 ∈ (𝑁‘{𝑌, 𝑍})))
47	1, 46	mtbird 326	1 ⊢ (𝜑 → ¬ 𝐹 ∈ (𝐽‘{𝐺, 𝐸}))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 396 = wceq 1520 ∈ wcel 2079 ⊆ wss 3854 {csn 4466 {cpr 4468 ‘cfv 6217 (class class class)co 7007 Basecbs 16300 LSSumclsm 18477 LModclmod 19312 LSubSpclss 19381 LSpanclspn 19421 HLchlt 35967 LHypclh 36601 DVecHcdvh 37695 LCDualclcd 38203 mapdcmpd 38241

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1775 ax-4 1789 ax-5 1886 ax-6 1945 ax-7 1990 ax-8 2081 ax-9 2089 ax-10 2110 ax-11 2124 ax-12 2139 ax-13 2342 ax-ext 2767 ax-rep 5075 ax-sep 5088 ax-nul 5095 ax-pow 5150 ax-pr 5214 ax-un 7310 ax-cnex 10428 ax-resscn 10429 ax-1cn 10430 ax-icn 10431 ax-addcl 10432 ax-addrcl 10433 ax-mulcl 10434 ax-mulrcl 10435 ax-mulcom 10436 ax-addass 10437 ax-mulass 10438 ax-distr 10439 ax-i2m1 10440 ax-1ne0 10441 ax-1rid 10442 ax-rnegex 10443 ax-rrecex 10444 ax-cnre 10445 ax-pre-lttri 10446 ax-pre-lttrn 10447 ax-pre-ltadd 10448 ax-pre-mulgt0 10449 ax-riotaBAD 35570

This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3or 1079 df-3an 1080 df-tru 1523 df-fal 1533 df-ex 1760 df-nf 1764 df-sb 2041 df-mo 2574 df-eu 2610 df-clab 2774 df-cleq 2786 df-clel 2861 df-nfc 2933 df-ne 2983 df-nel 3089 df-ral 3108 df-rex 3109 df-reu 3110 df-rmo 3111 df-rab 3112 df-v 3434 df-sbc 3702 df-csb 3807 df-dif 3857 df-un 3859 df-in 3861 df-ss 3869 df-pss 3871 df-nul 4207 df-if 4376 df-pw 4449 df-sn 4467 df-pr 4469 df-tp 4471 df-op 4473 df-uni 4740 df-int 4777 df-iun 4821 df-iin 4822 df-br 4957 df-opab 5019 df-mpt 5036 df-tr 5058 df-id 5340 df-eprel 5345 df-po 5354 df-so 5355 df-fr 5394 df-we 5396 df-xp 5441 df-rel 5442 df-cnv 5443 df-co 5444 df-dm 5445 df-rn 5446 df-res 5447 df-ima 5448 df-pred 6015 df-ord 6061 df-on 6062 df-lim 6063 df-suc 6064 df-iota 6181 df-fun 6219 df-fn 6220 df-f 6221 df-f1 6222 df-fo 6223 df-f1o 6224 df-fv 6225 df-riota 6968 df-ov 7010 df-oprab 7011 df-mpo 7012 df-of 7258 df-om 7428 df-1st 7536 df-2nd 7537 df-tpos 7734 df-undef 7781 df-wrecs 7789 df-recs 7851 df-rdg 7889 df-1o 7944 df-oadd 7948 df-er 8130 df-map 8249 df-en 8348 df-dom 8349 df-sdom 8350 df-fin 8351 df-pnf 10512 df-mnf 10513 df-xr 10514 df-ltxr 10515 df-le 10516 df-sub 10708 df-neg 10709 df-nn 11476 df-2 11537 df-3 11538 df-4 11539 df-5 11540 df-6 11541 df-n0 11735 df-z 11819 df-uz 12083 df-fz 12732 df-struct 16302 df-ndx 16303 df-slot 16304 df-base 16306 df-sets 16307 df-ress 16308 df-plusg 16395 df-mulr 16396 df-sca 16398 df-vsca 16399 df-0g 16532 df-mre 16674 df-mrc 16675 df-acs 16677 df-proset 17355 df-poset 17373 df-plt 17385 df-lub 17401 df-glb 17402 df-join 17403 df-meet 17404 df-p0 17466 df-p1 17467 df-lat 17473 df-clat 17535 df-mgm 17669 df-sgrp 17711 df-mnd 17722 df-submnd 17763 df-grp 17852 df-minusg 17853 df-sbg 17854 df-subg 18018 df-cntz 18176 df-oppg 18203 df-lsm 18479 df-cmn 18623 df-abl 18624 df-mgp 18918 df-ur 18930 df-ring 18977 df-oppr 19051 df-dvdsr 19069 df-unit 19070 df-invr 19100 df-dvr 19111 df-drng 19182 df-lmod 19314 df-lss 19382 df-lsp 19422 df-lvec 19553 df-lsatoms 35593 df-lshyp 35594 df-lcv 35636 df-lfl 35675 df-lkr 35703 df-ldual 35741 df-oposet 35793 df-ol 35795 df-oml 35796 df-covers 35883 df-ats 35884 df-atl 35915 df-cvlat 35939 df-hlat 35968 df-llines 36115 df-lplanes 36116 df-lvols 36117 df-lines 36118 df-psubsp 36120 df-pmap 36121 df-padd 36413 df-lhyp 36605 df-laut 36606 df-ldil 36721 df-ltrn 36722 df-trl 36776 df-tgrp 37360 df-tendo 37372 df-edring 37374 df-dveca 37620 df-disoa 37646 df-dvech 37696 df-dib 37756 df-dic 37790 df-dih 37846 df-doch 37965 df-djh 38012 df-lcdual 38204 df-mapd 38242

This theorem is referenced by: mapdheq4lem 38348 mapdh6lem1N 38350 mapdh6lem2N 38351 hdmap1l6lem1 38424 hdmap1l6lem2 38425

W3C validator