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 42117

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 2736	. . . 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 42038	. . . 4 ⊢ (𝜑 → 𝐶 ∈ LMod)
9		mapdindp.g	. . . . 5 ⊢ (𝜑 → 𝐺 ∈ 𝐷)
10		mapdindp.e	. . . . 5 ⊢ (𝜑 → 𝐸 ∈ 𝐷)
11	2, 3, 4, 8, 9, 10	lspprcl 20973	. . . 4 ⊢ (𝜑 → (𝐽‘{𝐺, 𝐸}) ∈ (LSubSp‘𝐶))
12		mapdindp.f	. . . 4 ⊢ (𝜑 → 𝐹 ∈ 𝐷)
13	2, 3, 4, 8, 11, 12	ellspsn5b 20990	. . 3 ⊢ (𝜑 → (𝐹 ∈ (𝐽‘{𝐺, 𝐸}) ↔ (𝐽‘{𝐹}) ⊆ (𝐽‘{𝐺, 𝐸})))
14		mapdindp.v	. . . . 5 ⊢ 𝑉 = (Base‘𝑈)
15		eqid 2736	. . . . 5 ⊢ (LSubSp‘𝑈) = (LSubSp‘𝑈)
16		mapdindp.n	. . . . 5 ⊢ 𝑁 = (LSpan‘𝑈)
17		mapdindp.u	. . . . . 6 ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)
18	5, 17, 7	dvhlmod 41556	. . . . 5 ⊢ (𝜑 → 𝑈 ∈ LMod)
19		mapdindp.y	. . . . . 6 ⊢ (𝜑 → 𝑌 ∈ 𝑉)
20		mapdindp.z	. . . . . 6 ⊢ (𝜑 → 𝑍 ∈ 𝑉)
21	14, 15, 16, 18, 19, 20	lspprcl 20973	. . . . 5 ⊢ (𝜑 → (𝑁‘{𝑌, 𝑍}) ∈ (LSubSp‘𝑈))
22		mapdindp.x	. . . . 5 ⊢ (𝜑 → 𝑋 ∈ 𝑉)
23	14, 15, 16, 18, 21, 22	ellspsn5b 20990	. . . 4 ⊢ (𝜑 → (𝑋 ∈ (𝑁‘{𝑌, 𝑍}) ↔ (𝑁‘{𝑋}) ⊆ (𝑁‘{𝑌, 𝑍})))
24		mapdindp.m	. . . . 5 ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)
25	14, 15, 16	lspsncl 20972	. . . . . 6 ⊢ ((𝑈 ∈ LMod ∧ 𝑋 ∈ 𝑉) → (𝑁‘{𝑋}) ∈ (LSubSp‘𝑈))
26	18, 22, 25	syl2anc 585	. . . . 5 ⊢ (𝜑 → (𝑁‘{𝑋}) ∈ (LSubSp‘𝑈))
27	5, 17, 15, 24, 7, 26, 21	mapdord 42084	. . . 4 ⊢ (𝜑 → ((𝑀‘(𝑁‘{𝑋})) ⊆ (𝑀‘(𝑁‘{𝑌, 𝑍})) ↔ (𝑁‘{𝑋}) ⊆ (𝑁‘{𝑌, 𝑍})))
28		mapdindp.mx	. . . . 5 ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐹}))
29		eqid 2736	. . . . . . . . 9 ⊢ (LSSum‘𝑈) = (LSSum‘𝑈)
30	14, 16, 29, 18, 19, 20	lsmpr 21084	. . . . . . . 8 ⊢ (𝜑 → (𝑁‘{𝑌, 𝑍}) = ((𝑁‘{𝑌})(LSSum‘𝑈)(𝑁‘{𝑍})))
31	30	fveq2d 6844	. . . . . . 7 ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑌, 𝑍})) = (𝑀‘((𝑁‘{𝑌})(LSSum‘𝑈)(𝑁‘{𝑍}))))
32		eqid 2736	. . . . . . . 8 ⊢ (LSSum‘𝐶) = (LSSum‘𝐶)
33	14, 15, 16	lspsncl 20972	. . . . . . . . 9 ⊢ ((𝑈 ∈ LMod ∧ 𝑌 ∈ 𝑉) → (𝑁‘{𝑌}) ∈ (LSubSp‘𝑈))
34	18, 19, 33	syl2anc 585	. . . . . . . 8 ⊢ (𝜑 → (𝑁‘{𝑌}) ∈ (LSubSp‘𝑈))
35	14, 15, 16	lspsncl 20972	. . . . . . . . 9 ⊢ ((𝑈 ∈ LMod ∧ 𝑍 ∈ 𝑉) → (𝑁‘{𝑍}) ∈ (LSubSp‘𝑈))
36	18, 20, 35	syl2anc 585	. . . . . . . 8 ⊢ (𝜑 → (𝑁‘{𝑍}) ∈ (LSubSp‘𝑈))
37	5, 24, 17, 15, 29, 6, 32, 7, 34, 36	mapdlsm 42110	. . . . . . 7 ⊢ (𝜑 → (𝑀‘((𝑁‘{𝑌})(LSSum‘𝑈)(𝑁‘{𝑍}))) = ((𝑀‘(𝑁‘{𝑌}))(LSSum‘𝐶)(𝑀‘(𝑁‘{𝑍}))))
38		mapdindp.my	. . . . . . . 8 ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑌})) = (𝐽‘{𝐺}))
39		mapdindp.mg	. . . . . . . 8 ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑍})) = (𝐽‘{𝐸}))
40	38, 39	oveq12d 7385	. . . . . . 7 ⊢ (𝜑 → ((𝑀‘(𝑁‘{𝑌}))(LSSum‘𝐶)(𝑀‘(𝑁‘{𝑍}))) = ((𝐽‘{𝐺})(LSSum‘𝐶)(𝐽‘{𝐸})))
41	31, 37, 40	3eqtrd 2775	. . . . . 6 ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑌, 𝑍})) = ((𝐽‘{𝐺})(LSSum‘𝐶)(𝐽‘{𝐸})))
42	2, 4, 32, 8, 9, 10	lsmpr 21084	. . . . . 6 ⊢ (𝜑 → (𝐽‘{𝐺, 𝐸}) = ((𝐽‘{𝐺})(LSSum‘𝐶)(𝐽‘{𝐸})))
43	41, 42	eqtr4d 2774	. . . . 5 ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑌, 𝑍})) = (𝐽‘{𝐺, 𝐸}))
44	28, 43	sseq12d 3955	. . . 4 ⊢ (𝜑 → ((𝑀‘(𝑁‘{𝑋})) ⊆ (𝑀‘(𝑁‘{𝑌, 𝑍})) ↔ (𝐽‘{𝐹}) ⊆ (𝐽‘{𝐺, 𝐸})))
45	23, 27, 44	3bitr2rd 308	. . 3 ⊢ (𝜑 → ((𝐽‘{𝐹}) ⊆ (𝐽‘{𝐺, 𝐸}) ↔ 𝑋 ∈ (𝑁‘{𝑌, 𝑍})))
46	13, 45	bitrd 279	. 2 ⊢ (𝜑 → (𝐹 ∈ (𝐽‘{𝐺, 𝐸}) ↔ 𝑋 ∈ (𝑁‘{𝑌, 𝑍})))
47	1, 46	mtbird 325	1 ⊢ (𝜑 → ¬ 𝐹 ∈ (𝐽‘{𝐺, 𝐸}))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 395 = wceq 1542 ∈ wcel 2114 ⊆ wss 3889 {csn 4567 {cpr 4569 ‘cfv 6498 (class class class)co 7367 Basecbs 17179 LSSumclsm 19609 LModclmod 20855 LSubSpclss 20926 LSpanclspn 20966 HLchlt 39796 LHypclh 40430 DVecHcdvh 41524 LCDualclcd 42032 mapdcmpd 42070

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 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2708 ax-rep 5212 ax-sep 5231 ax-nul 5241 ax-pow 5307 ax-pr 5375 ax-un 7689 ax-cnex 11094 ax-resscn 11095 ax-1cn 11096 ax-icn 11097 ax-addcl 11098 ax-addrcl 11099 ax-mulcl 11100 ax-mulrcl 11101 ax-mulcom 11102 ax-addass 11103 ax-mulass 11104 ax-distr 11105 ax-i2m1 11106 ax-1ne0 11107 ax-1rid 11108 ax-rnegex 11109 ax-rrecex 11110 ax-cnre 11111 ax-pre-lttri 11112 ax-pre-lttrn 11113 ax-pre-ltadd 11114 ax-pre-mulgt0 11115 ax-riotaBAD 39399

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2539 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2811 df-nfc 2885 df-ne 2933 df-nel 3037 df-ral 3052 df-rex 3062 df-rmo 3342 df-reu 3343 df-rab 3390 df-v 3431 df-sbc 3729 df-csb 3838 df-dif 3892 df-un 3894 df-in 3896 df-ss 3906 df-pss 3909 df-nul 4274 df-if 4467 df-pw 4543 df-sn 4568 df-pr 4570 df-tp 4572 df-op 4574 df-uni 4851 df-int 4890 df-iun 4935 df-iin 4936 df-br 5086 df-opab 5148 df-mpt 5167 df-tr 5193 df-id 5526 df-eprel 5531 df-po 5539 df-so 5540 df-fr 5584 df-we 5586 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-res 5643 df-ima 5644 df-pred 6265 df-ord 6326 df-on 6327 df-lim 6328 df-suc 6329 df-iota 6454 df-fun 6500 df-fn 6501 df-f 6502 df-f1 6503 df-fo 6504 df-f1o 6505 df-fv 6506 df-riota 7324 df-ov 7370 df-oprab 7371 df-mpo 7372 df-of 7631 df-om 7818 df-1st 7942 df-2nd 7943 df-tpos 8176 df-undef 8223 df-frecs 8231 df-wrecs 8262 df-recs 8311 df-rdg 8349 df-1o 8405 df-2o 8406 df-er 8643 df-map 8775 df-en 8894 df-dom 8895 df-sdom 8896 df-fin 8897 df-pnf 11181 df-mnf 11182 df-xr 11183 df-ltxr 11184 df-le 11185 df-sub 11379 df-neg 11380 df-nn 12175 df-2 12244 df-3 12245 df-4 12246 df-5 12247 df-6 12248 df-n0 12438 df-z 12525 df-uz 12789 df-fz 13462 df-struct 17117 df-sets 17134 df-slot 17152 df-ndx 17164 df-base 17180 df-ress 17201 df-plusg 17233 df-mulr 17234 df-sca 17236 df-vsca 17237 df-0g 17404 df-mre 17548 df-mrc 17549 df-acs 17551 df-proset 18260 df-poset 18279 df-plt 18294 df-lub 18310 df-glb 18311 df-join 18312 df-meet 18313 df-p0 18389 df-p1 18390 df-lat 18398 df-clat 18465 df-mgm 18608 df-sgrp 18687 df-mnd 18703 df-submnd 18752 df-grp 18912 df-minusg 18913 df-sbg 18914 df-subg 19099 df-cntz 19292 df-oppg 19321 df-lsm 19611 df-cmn 19757 df-abl 19758 df-mgp 20122 df-rng 20134 df-ur 20163 df-ring 20216 df-oppr 20317 df-dvdsr 20337 df-unit 20338 df-invr 20368 df-dvr 20381 df-nzr 20490 df-rlreg 20671 df-domn 20672 df-drng 20708 df-lmod 20857 df-lss 20927 df-lsp 20967 df-lvec 21098 df-lsatoms 39422 df-lshyp 39423 df-lcv 39465 df-lfl 39504 df-lkr 39532 df-ldual 39570 df-oposet 39622 df-ol 39624 df-oml 39625 df-covers 39712 df-ats 39713 df-atl 39744 df-cvlat 39768 df-hlat 39797 df-llines 39944 df-lplanes 39945 df-lvols 39946 df-lines 39947 df-psubsp 39949 df-pmap 39950 df-padd 40242 df-lhyp 40434 df-laut 40435 df-ldil 40550 df-ltrn 40551 df-trl 40605 df-tgrp 41189 df-tendo 41201 df-edring 41203 df-dveca 41449 df-disoa 41475 df-dvech 41525 df-dib 41585 df-dic 41619 df-dih 41675 df-doch 41794 df-djh 41841 df-lcdual 42033 df-mapd 42071

This theorem is referenced by: mapdheq4lem 42177 mapdh6lem1N 42179 mapdh6lem2N 42180 hdmap1l6lem1 42253 hdmap1l6lem2 42254

W3C validator