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 42822

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 2760	. . . 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 42743	. . . 4 ⊢ (𝜑 → 𝐶 ∈ LMod)
9		mapdindp.g	. . . . 5 ⊢ (𝜑 → 𝐺 ∈ 𝐷)
10		mapdindp.e	. . . . 5 ⊢ (𝜑 → 𝐸 ∈ 𝐷)
11	2, 3, 4, 8, 9, 10	lspprcl 21259	. . . 4 ⊢ (𝜑 → (𝐽‘{𝐺, 𝐸}) ∈ (LSubSp‘𝐶))
12		mapdindp.f	. . . 4 ⊢ (𝜑 → 𝐹 ∈ 𝐷)
13	2, 3, 4, 8, 11, 12	ellspsn5b 21276	. . 3 ⊢ (𝜑 → (𝐹 ∈ (𝐽‘{𝐺, 𝐸}) ↔ (𝐽‘{𝐹}) ⊆ (𝐽‘{𝐺, 𝐸})))
14		mapdindp.v	. . . . 5 ⊢ 𝑉 = (Base‘𝑈)
15		eqid 2760	. . . . 5 ⊢ (LSubSp‘𝑈) = (LSubSp‘𝑈)
16		mapdindp.n	. . . . 5 ⊢ 𝑁 = (LSpan‘𝑈)
17		mapdindp.u	. . . . . 6 ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)
18	5, 17, 7	dvhlmod 42261	. . . . 5 ⊢ (𝜑 → 𝑈 ∈ LMod)
19		mapdindp.y	. . . . . 6 ⊢ (𝜑 → 𝑌 ∈ 𝑉)
20		mapdindp.z	. . . . . 6 ⊢ (𝜑 → 𝑍 ∈ 𝑉)
21	14, 15, 16, 18, 19, 20	lspprcl 21259	. . . . 5 ⊢ (𝜑 → (𝑁‘{𝑌, 𝑍}) ∈ (LSubSp‘𝑈))
22		mapdindp.x	. . . . 5 ⊢ (𝜑 → 𝑋 ∈ 𝑉)
23	14, 15, 16, 18, 21, 22	ellspsn5b 21276	. . . 4 ⊢ (𝜑 → (𝑋 ∈ (𝑁‘{𝑌, 𝑍}) ↔ (𝑁‘{𝑋}) ⊆ (𝑁‘{𝑌, 𝑍})))
24		mapdindp.m	. . . . 5 ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)
25	14, 15, 16	lspsncl 21258	. . . . . 6 ⊢ ((𝑈 ∈ LMod ∧ 𝑋 ∈ 𝑉) → (𝑁‘{𝑋}) ∈ (LSubSp‘𝑈))
26	18, 22, 25	syl2anc 596	. . . . 5 ⊢ (𝜑 → (𝑁‘{𝑋}) ∈ (LSubSp‘𝑈))
27	5, 17, 15, 24, 7, 26, 21	mapdord 42789	. . . 4 ⊢ (𝜑 → ((𝑀‘(𝑁‘{𝑋})) ⊆ (𝑀‘(𝑁‘{𝑌, 𝑍})) ↔ (𝑁‘{𝑋}) ⊆ (𝑁‘{𝑌, 𝑍})))
28		mapdindp.mx	. . . . 5 ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐹}))
29		eqid 2760	. . . . . . . . 9 ⊢ (LSSum‘𝑈) = (LSSum‘𝑈)
30	14, 16, 29, 18, 19, 20	lsmpr 21370	. . . . . . . 8 ⊢ (𝜑 → (𝑁‘{𝑌, 𝑍}) = ((𝑁‘{𝑌})(LSSum‘𝑈)(𝑁‘{𝑍})))
31	30	fveq2d 6890	. . . . . . 7 ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑌, 𝑍})) = (𝑀‘((𝑁‘{𝑌})(LSSum‘𝑈)(𝑁‘{𝑍}))))
32		eqid 2760	. . . . . . . 8 ⊢ (LSSum‘𝐶) = (LSSum‘𝐶)
33	14, 15, 16	lspsncl 21258	. . . . . . . . 9 ⊢ ((𝑈 ∈ LMod ∧ 𝑌 ∈ 𝑉) → (𝑁‘{𝑌}) ∈ (LSubSp‘𝑈))
34	18, 19, 33	syl2anc 596	. . . . . . . 8 ⊢ (𝜑 → (𝑁‘{𝑌}) ∈ (LSubSp‘𝑈))
35	14, 15, 16	lspsncl 21258	. . . . . . . . 9 ⊢ ((𝑈 ∈ LMod ∧ 𝑍 ∈ 𝑉) → (𝑁‘{𝑍}) ∈ (LSubSp‘𝑈))
36	18, 20, 35	syl2anc 596	. . . . . . . 8 ⊢ (𝜑 → (𝑁‘{𝑍}) ∈ (LSubSp‘𝑈))
37	5, 24, 17, 15, 29, 6, 32, 7, 34, 36	mapdlsm 42815	. . . . . . 7 ⊢ (𝜑 → (𝑀‘((𝑁‘{𝑌})(LSSum‘𝑈)(𝑁‘{𝑍}))) = ((𝑀‘(𝑁‘{𝑌}))(LSSum‘𝐶)(𝑀‘(𝑁‘{𝑍}))))
38		mapdindp.my	. . . . . . . 8 ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑌})) = (𝐽‘{𝐺}))
39		mapdindp.mg	. . . . . . . 8 ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑍})) = (𝐽‘{𝐸}))
40	38, 39	oveq12d 7439	. . . . . . 7 ⊢ (𝜑 → ((𝑀‘(𝑁‘{𝑌}))(LSSum‘𝐶)(𝑀‘(𝑁‘{𝑍}))) = ((𝐽‘{𝐺})(LSSum‘𝐶)(𝐽‘{𝐸})))
41	31, 37, 40	3eqtrd 2799	. . . . . 6 ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑌, 𝑍})) = ((𝐽‘{𝐺})(LSSum‘𝐶)(𝐽‘{𝐸})))
42	2, 4, 32, 8, 9, 10	lsmpr 21370	. . . . . 6 ⊢ (𝜑 → (𝐽‘{𝐺, 𝐸}) = ((𝐽‘{𝐺})(LSSum‘𝐶)(𝐽‘{𝐸})))
43	41, 42	eqtr4d 2798	. . . . 5 ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑌, 𝑍})) = (𝐽‘{𝐺, 𝐸}))
44	28, 43	sseq12d 3941	. . . 4 ⊢ (𝜑 → ((𝑀‘(𝑁‘{𝑋})) ⊆ (𝑀‘(𝑁‘{𝑌, 𝑍})) ↔ (𝐽‘{𝐹}) ⊆ (𝐽‘{𝐺, 𝐸})))
45	23, 27, 44	3bitr2rd 311	. . 3 ⊢ (𝜑 → ((𝐽‘{𝐹}) ⊆ (𝐽‘{𝐺, 𝐸}) ↔ 𝑋 ∈ (𝑁‘{𝑌, 𝑍})))
46	13, 45	bitrd 282	. 2 ⊢ (𝜑 → (𝐹 ∈ (𝐽‘{𝐺, 𝐸}) ↔ 𝑋 ∈ (𝑁‘{𝑌, 𝑍})))
47	1, 46	mtbird 328	1 ⊢ (𝜑 → ¬ 𝐹 ∈ (𝐽‘{𝐺, 𝐸}))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ∧ wa 401 = wceq 1569 ∈ wcel 2144 ⊆ wss 3895 {csn 4584 {cpr 4586 ‘cfv 6539 (class class class)co 7421 Basecbs 17393 LSSumclsm 19854 LModclmod 21141 LSubSpclss 21212 LSpanclspn 21252 HLchlt 40501 LHypclh 41135 DVecHcdvh 42229 LCDualclcd 42737 mapdcmpd 42775

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2212 ax-ext 2732 ax-rep 5231 ax-sep 5248 ax-nul 5259 ax-pow 5326 ax-pr 5390 ax-un 7752 ax-cnex 11260 ax-resscn 11261 ax-1cn 11262 ax-icn 11263 ax-addcl 11264 ax-addrcl 11265 ax-mulcl 11266 ax-mulrcl 11267 ax-mulcom 11268 ax-addass 11269 ax-mulass 11270 ax-distr 11271 ax-i2m1 11272 ax-1ne0 11273 ax-1rid 11274 ax-rnegex 11275 ax-rrecex 11276 ax-cnre 11277 ax-pre-lttri 11278 ax-pre-lttrn 11279 ax-pre-ltadd 11280 ax-pre-mulgt0 11281 ax-riotaBAD 40104

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2099 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3739 df-csb 3847 df-ss 3896 df-pss 4014 df-dif 4047 df-in 4091 df-un 4151 df-nul 4279 df-if 4482 df-pw 4558 df-sn 4585 df-pr 4587 df-tp 4589 df-op 4835 df-uni 4867 df-int 4907 df-iun 4952 df-iin 4953 df-br 5103 df-opab 5167 df-mpt 5186 df-tr 5212 df-id 5545 df-eprel 5550 df-po 5558 df-so 5559 df-fr 5603 df-we 5605 df-xp 5656 df-rel 5657 df-cnv 5658 df-co 5659 df-dm 5660 df-rn 5661 df-res 5662 df-ima 5663 df-pred 6304 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6494 df-fun 6541 df-fn 6542 df-f 6543 df-f1 6544 df-fo 6545 df-f1o 6546 df-fv 6547 df-riota 7378 df-ov 7424 df-oprab 7425 df-mpo 7426 df-of 7694 df-om 7879 df-1st 8002 df-2nd 8003 df-tpos 8247 df-undef 8294 df-frecs 8303 df-wrecs 8334 df-recs 8383 df-rdg 8422 df-1o 8480 df-2o 8481 df-er 8721 df-map 8853 df-en 8978 df-dom 8979 df-sdom 8980 df-fin 8981 df-pnf 11349 df-mnf 11350 df-xr 11351 df-ltxr 11352 df-le 11353 df-sub 11547 df-neg 11548 df-nn 12340 df-2 12409 df-3 12410 df-4 12411 df-5 12412 df-6 12413 df-n0 12611 df-z 12698 df-uz 12970 df-fz 13644 df-struct 17331 df-sets 17348 df-slot 17366 df-ndx 17378 df-base 17394 df-ress 17415 df-plusg 17447 df-mulr 17448 df-sca 17450 df-vsca 17451 df-0g 17618 df-mre 17762 df-mrc 17763 df-acs 17765 df-proset 18474 df-poset 18493 df-plt 18508 df-lub 18524 df-glb 18525 df-join 18526 df-meet 18527 df-p0 18603 df-p1 18604 df-lat 18612 df-clat 18679 df-mgm 18822 df-sgrp 18914 df-mnd 18930 df-submnd 18985 df-grp 19153 df-minusg 19154 df-sbg 19155 df-subg 19339 df-cntz 19537 df-oppg 19566 df-lsm 19856 df-cmn 20002 df-abl 20003 df-mgp 20367 df-rng 20381 df-ur 20414 df-ring 20467 df-oppr 20573 df-dvdsr 20593 df-unit 20594 df-invr 20624 df-dvr 20637 df-nzr 20769 df-rlreg 20952 df-domn 20953 df-drng 20988 df-lmod 21143 df-lss 21213 df-lsp 21253 df-lvec 21384 df-lsatoms 40127 df-lshyp 40128 df-lcv 40170 df-lfl 40209 df-lkr 40237 df-ldual 40275 df-oposet 40327 df-ol 40329 df-oml 40330 df-covers 40417 df-ats 40418 df-atl 40449 df-cvlat 40473 df-hlat 40502 df-llines 40649 df-lplanes 40650 df-lvols 40651 df-lines 40652 df-psubsp 40654 df-pmap 40655 df-padd 40947 df-lhyp 41139 df-laut 41140 df-ldil 41255 df-ltrn 41256 df-trl 41310 df-tgrp 41894 df-tendo 41906 df-edring 41908 df-dveca 42154 df-disoa 42180 df-dvech 42230 df-dib 42290 df-dic 42324 df-dih 42380 df-doch 42499 df-djh 42546 df-lcdual 42738 df-mapd 42776

This theorem is used by: mapdheq4lem 42882 mapdh6lem1N 42884 mapdh6lem2N 42885 hdmap1l6lem1 42958 hdmap1l6lem2 42959

W3C validator