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 42121

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 2737	. . . 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 42042	. . . 4 ⊢ (𝜑 → 𝐶 ∈ LMod)
9		mapdindp.g	. . . . 5 ⊢ (𝜑 → 𝐺 ∈ 𝐷)
10		mapdindp.e	. . . . 5 ⊢ (𝜑 → 𝐸 ∈ 𝐷)
11	2, 3, 4, 8, 9, 10	lspprcl 20962	. . . 4 ⊢ (𝜑 → (𝐽‘{𝐺, 𝐸}) ∈ (LSubSp‘𝐶))
12		mapdindp.f	. . . 4 ⊢ (𝜑 → 𝐹 ∈ 𝐷)
13	2, 3, 4, 8, 11, 12	ellspsn5b 20979	. . 3 ⊢ (𝜑 → (𝐹 ∈ (𝐽‘{𝐺, 𝐸}) ↔ (𝐽‘{𝐹}) ⊆ (𝐽‘{𝐺, 𝐸})))
14		mapdindp.v	. . . . 5 ⊢ 𝑉 = (Base‘𝑈)
15		eqid 2737	. . . . 5 ⊢ (LSubSp‘𝑈) = (LSubSp‘𝑈)
16		mapdindp.n	. . . . 5 ⊢ 𝑁 = (LSpan‘𝑈)
17		mapdindp.u	. . . . . 6 ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)
18	5, 17, 7	dvhlmod 41560	. . . . 5 ⊢ (𝜑 → 𝑈 ∈ LMod)
19		mapdindp.y	. . . . . 6 ⊢ (𝜑 → 𝑌 ∈ 𝑉)
20		mapdindp.z	. . . . . 6 ⊢ (𝜑 → 𝑍 ∈ 𝑉)
21	14, 15, 16, 18, 19, 20	lspprcl 20962	. . . . 5 ⊢ (𝜑 → (𝑁‘{𝑌, 𝑍}) ∈ (LSubSp‘𝑈))
22		mapdindp.x	. . . . 5 ⊢ (𝜑 → 𝑋 ∈ 𝑉)
23	14, 15, 16, 18, 21, 22	ellspsn5b 20979	. . . 4 ⊢ (𝜑 → (𝑋 ∈ (𝑁‘{𝑌, 𝑍}) ↔ (𝑁‘{𝑋}) ⊆ (𝑁‘{𝑌, 𝑍})))
24		mapdindp.m	. . . . 5 ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)
25	14, 15, 16	lspsncl 20961	. . . . . 6 ⊢ ((𝑈 ∈ LMod ∧ 𝑋 ∈ 𝑉) → (𝑁‘{𝑋}) ∈ (LSubSp‘𝑈))
26	18, 22, 25	syl2anc 585	. . . . 5 ⊢ (𝜑 → (𝑁‘{𝑋}) ∈ (LSubSp‘𝑈))
27	5, 17, 15, 24, 7, 26, 21	mapdord 42088	. . . 4 ⊢ (𝜑 → ((𝑀‘(𝑁‘{𝑋})) ⊆ (𝑀‘(𝑁‘{𝑌, 𝑍})) ↔ (𝑁‘{𝑋}) ⊆ (𝑁‘{𝑌, 𝑍})))
28		mapdindp.mx	. . . . 5 ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐹}))
29		eqid 2737	. . . . . . . . 9 ⊢ (LSSum‘𝑈) = (LSSum‘𝑈)
30	14, 16, 29, 18, 19, 20	lsmpr 21074	. . . . . . . 8 ⊢ (𝜑 → (𝑁‘{𝑌, 𝑍}) = ((𝑁‘{𝑌})(LSSum‘𝑈)(𝑁‘{𝑍})))
31	30	fveq2d 6836	. . . . . . 7 ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑌, 𝑍})) = (𝑀‘((𝑁‘{𝑌})(LSSum‘𝑈)(𝑁‘{𝑍}))))
32		eqid 2737	. . . . . . . 8 ⊢ (LSSum‘𝐶) = (LSSum‘𝐶)
33	14, 15, 16	lspsncl 20961	. . . . . . . . 9 ⊢ ((𝑈 ∈ LMod ∧ 𝑌 ∈ 𝑉) → (𝑁‘{𝑌}) ∈ (LSubSp‘𝑈))
34	18, 19, 33	syl2anc 585	. . . . . . . 8 ⊢ (𝜑 → (𝑁‘{𝑌}) ∈ (LSubSp‘𝑈))
35	14, 15, 16	lspsncl 20961	. . . . . . . . 9 ⊢ ((𝑈 ∈ LMod ∧ 𝑍 ∈ 𝑉) → (𝑁‘{𝑍}) ∈ (LSubSp‘𝑈))
36	18, 20, 35	syl2anc 585	. . . . . . . 8 ⊢ (𝜑 → (𝑁‘{𝑍}) ∈ (LSubSp‘𝑈))
37	5, 24, 17, 15, 29, 6, 32, 7, 34, 36	mapdlsm 42114	. . . . . . 7 ⊢ (𝜑 → (𝑀‘((𝑁‘{𝑌})(LSSum‘𝑈)(𝑁‘{𝑍}))) = ((𝑀‘(𝑁‘{𝑌}))(LSSum‘𝐶)(𝑀‘(𝑁‘{𝑍}))))
38		mapdindp.my	. . . . . . . 8 ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑌})) = (𝐽‘{𝐺}))
39		mapdindp.mg	. . . . . . . 8 ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑍})) = (𝐽‘{𝐸}))
40	38, 39	oveq12d 7376	. . . . . . 7 ⊢ (𝜑 → ((𝑀‘(𝑁‘{𝑌}))(LSSum‘𝐶)(𝑀‘(𝑁‘{𝑍}))) = ((𝐽‘{𝐺})(LSSum‘𝐶)(𝐽‘{𝐸})))
41	31, 37, 40	3eqtrd 2776	. . . . . 6 ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑌, 𝑍})) = ((𝐽‘{𝐺})(LSSum‘𝐶)(𝐽‘{𝐸})))
42	2, 4, 32, 8, 9, 10	lsmpr 21074	. . . . . 6 ⊢ (𝜑 → (𝐽‘{𝐺, 𝐸}) = ((𝐽‘{𝐺})(LSSum‘𝐶)(𝐽‘{𝐸})))
43	41, 42	eqtr4d 2775	. . . . 5 ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑌, 𝑍})) = (𝐽‘{𝐺, 𝐸}))
44	28, 43	sseq12d 3956	. . . 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 3890 {csn 4568 {cpr 4570 ‘cfv 6490 (class class class)co 7358 Basecbs 17168 LSSumclsm 19598 LModclmod 20844 LSubSpclss 20915 LSpanclspn 20955 HLchlt 39800 LHypclh 40434 DVecHcdvh 41528 LCDualclcd 42036 mapdcmpd 42074

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 2709 ax-rep 5212 ax-sep 5231 ax-nul 5241 ax-pow 5300 ax-pr 5368 ax-un 7680 ax-cnex 11083 ax-resscn 11084 ax-1cn 11085 ax-icn 11086 ax-addcl 11087 ax-addrcl 11088 ax-mulcl 11089 ax-mulrcl 11090 ax-mulcom 11091 ax-addass 11092 ax-mulass 11093 ax-distr 11094 ax-i2m1 11095 ax-1ne0 11096 ax-1rid 11097 ax-rnegex 11098 ax-rrecex 11099 ax-cnre 11100 ax-pre-lttri 11101 ax-pre-lttrn 11102 ax-pre-ltadd 11103 ax-pre-mulgt0 11104 ax-riotaBAD 39403

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 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3063 df-rmo 3343 df-reu 3344 df-rab 3391 df-v 3432 df-sbc 3730 df-csb 3839 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-pss 3910 df-nul 4275 df-if 4468 df-pw 4544 df-sn 4569 df-pr 4571 df-tp 4573 df-op 4575 df-uni 4852 df-int 4891 df-iun 4936 df-iin 4937 df-br 5087 df-opab 5149 df-mpt 5168 df-tr 5194 df-id 5517 df-eprel 5522 df-po 5530 df-so 5531 df-fr 5575 df-we 5577 df-xp 5628 df-rel 5629 df-cnv 5630 df-co 5631 df-dm 5632 df-rn 5633 df-res 5634 df-ima 5635 df-pred 6257 df-ord 6318 df-on 6319 df-lim 6320 df-suc 6321 df-iota 6446 df-fun 6492 df-fn 6493 df-f 6494 df-f1 6495 df-fo 6496 df-f1o 6497 df-fv 6498 df-riota 7315 df-ov 7361 df-oprab 7362 df-mpo 7363 df-of 7622 df-om 7809 df-1st 7933 df-2nd 7934 df-tpos 8167 df-undef 8214 df-frecs 8222 df-wrecs 8253 df-recs 8302 df-rdg 8340 df-1o 8396 df-2o 8397 df-er 8634 df-map 8766 df-en 8885 df-dom 8886 df-sdom 8887 df-fin 8888 df-pnf 11170 df-mnf 11171 df-xr 11172 df-ltxr 11173 df-le 11174 df-sub 11368 df-neg 11369 df-nn 12164 df-2 12233 df-3 12234 df-4 12235 df-5 12236 df-6 12237 df-n0 12427 df-z 12514 df-uz 12778 df-fz 13451 df-struct 17106 df-sets 17123 df-slot 17141 df-ndx 17153 df-base 17169 df-ress 17190 df-plusg 17222 df-mulr 17223 df-sca 17225 df-vsca 17226 df-0g 17393 df-mre 17537 df-mrc 17538 df-acs 17540 df-proset 18249 df-poset 18268 df-plt 18283 df-lub 18299 df-glb 18300 df-join 18301 df-meet 18302 df-p0 18378 df-p1 18379 df-lat 18387 df-clat 18454 df-mgm 18597 df-sgrp 18676 df-mnd 18692 df-submnd 18741 df-grp 18901 df-minusg 18902 df-sbg 18903 df-subg 19088 df-cntz 19281 df-oppg 19310 df-lsm 19600 df-cmn 19746 df-abl 19747 df-mgp 20111 df-rng 20123 df-ur 20152 df-ring 20205 df-oppr 20306 df-dvdsr 20326 df-unit 20327 df-invr 20357 df-dvr 20370 df-nzr 20479 df-rlreg 20660 df-domn 20661 df-drng 20697 df-lmod 20846 df-lss 20916 df-lsp 20956 df-lvec 21088 df-lsatoms 39426 df-lshyp 39427 df-lcv 39469 df-lfl 39508 df-lkr 39536 df-ldual 39574 df-oposet 39626 df-ol 39628 df-oml 39629 df-covers 39716 df-ats 39717 df-atl 39748 df-cvlat 39772 df-hlat 39801 df-llines 39948 df-lplanes 39949 df-lvols 39950 df-lines 39951 df-psubsp 39953 df-pmap 39954 df-padd 40246 df-lhyp 40438 df-laut 40439 df-ldil 40554 df-ltrn 40555 df-trl 40609 df-tgrp 41193 df-tendo 41205 df-edring 41207 df-dveca 41453 df-disoa 41479 df-dvech 41529 df-dib 41589 df-dic 41623 df-dih 41679 df-doch 41798 df-djh 41845 df-lcdual 42037 df-mapd 42075

This theorem is referenced by: mapdheq4lem 42181 mapdh6lem1N 42183 mapdh6lem2N 42184 hdmap1l6lem1 42257 hdmap1l6lem2 42258

W3C validator