mapdindp2 - Mathbox for Norm Megill

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

Theorem mapdindp2 42918

Description: Vector independence lemma. (Contributed by NM, 1-May-2015.)

**Hypotheses**
Ref	Expression
mapdindp1.v	⊢ 𝑉 = (Base‘𝑊)
mapdindp1.p	⊢ + = (+_g‘𝑊)
mapdindp1.o	⊢ 0 = (0_g‘𝑊)
mapdindp1.n	⊢ 𝑁 = (LSpan‘𝑊)
mapdindp1.w	⊢ (𝜑 → 𝑊 ∈ LVec)
mapdindp1.x	⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))
mapdindp1.y	⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))
mapdindp1.z	⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 }))
mapdindp1.W	⊢ (𝜑 → 𝑤 ∈ (𝑉 ∖ { 0 }))
mapdindp1.e	⊢ (𝜑 → (𝑁‘{𝑌}) = (𝑁‘{𝑍}))
mapdindp1.ne	⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))
mapdindp1.f	⊢ (𝜑 → ¬ 𝑤 ∈ (𝑁‘{𝑋, 𝑌}))

**Assertion**
Ref	Expression
mapdindp2	⊢ (𝜑 → ¬ 𝑤 ∈ (𝑁‘{𝑋, (𝑌 + 𝑍)}))

**Proof of Theorem mapdindp2**
Step	Hyp	Ref	Expression
1		preq2 4694	. . . . . 6 ⊢ ((𝑌 + 𝑍) = 0 → {𝑋, (𝑌 + 𝑍)} = {𝑋, 0 })
2	1	fveq2d 6897	. . . . 5 ⊢ ((𝑌 + 𝑍) = 0 → (𝑁‘{𝑋, (𝑌 + 𝑍)}) = (𝑁‘{𝑋, 0 }))
3		mapdindp1.v	. . . . . 6 ⊢ 𝑉 = (Base‘𝑊)
4		mapdindp1.o	. . . . . 6 ⊢ 0 = (0_g‘𝑊)
5		mapdindp1.n	. . . . . 6 ⊢ 𝑁 = (LSpan‘𝑊)
6		mapdindp1.w	. . . . . . 7 ⊢ (𝜑 → 𝑊 ∈ LVec)
7		lveclmod 21393	. . . . . . 7 ⊢ (𝑊 ∈ LVec → 𝑊 ∈ LMod)
8	6, 7	syl 18	. . . . . 6 ⊢ (𝜑 → 𝑊 ∈ LMod)
9		mapdindp1.x	. . . . . . 7 ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))
10	9	eldifad 4053	. . . . . 6 ⊢ (𝜑 → 𝑋 ∈ 𝑉)
11	3, 4, 5, 8, 10	lsppr0 21379	. . . . 5 ⊢ (𝜑 → (𝑁‘{𝑋, 0 }) = (𝑁‘{𝑋}))
12	2, 11	sylan9eqr 2820	. . . 4 ⊢ ((𝜑 ∧ (𝑌 + 𝑍) = 0 ) → (𝑁‘{𝑋, (𝑌 + 𝑍)}) = (𝑁‘{𝑋}))
13		mapdindp1.y	. . . . . . . 8 ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))
14	13	eldifad 4053	. . . . . . 7 ⊢ (𝜑 → 𝑌 ∈ 𝑉)
15		prssi 4779	. . . . . . 7 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → {𝑋, 𝑌} ⊆ 𝑉)
16	10, 14, 15	syl2anc 596	. . . . . 6 ⊢ (𝜑 → {𝑋, 𝑌} ⊆ 𝑉)
17		snsspr1 4772	. . . . . . 7 ⊢ {𝑋} ⊆ {𝑋, 𝑌}
18	17	a1i 11	. . . . . 6 ⊢ (𝜑 → {𝑋} ⊆ {𝑋, 𝑌})
19	3, 5	lspss 21271	. . . . . 6 ⊢ ((𝑊 ∈ LMod ∧ {𝑋, 𝑌} ⊆ 𝑉 ∧ {𝑋} ⊆ {𝑋, 𝑌}) → (𝑁‘{𝑋}) ⊆ (𝑁‘{𝑋, 𝑌}))
20	8, 16, 18, 19	syl3anc 1398	. . . . 5 ⊢ (𝜑 → (𝑁‘{𝑋}) ⊆ (𝑁‘{𝑋, 𝑌}))
21	20	adantr 486	. . . 4 ⊢ ((𝜑 ∧ (𝑌 + 𝑍) = 0 ) → (𝑁‘{𝑋}) ⊆ (𝑁‘{𝑋, 𝑌}))
22	12, 21	eqsstrd 3946	. . 3 ⊢ ((𝜑 ∧ (𝑌 + 𝑍) = 0 ) → (𝑁‘{𝑋, (𝑌 + 𝑍)}) ⊆ (𝑁‘{𝑋, 𝑌}))
23		mapdindp1.f	. . . 4 ⊢ (𝜑 → ¬ 𝑤 ∈ (𝑁‘{𝑋, 𝑌}))
24	23	adantr 486	. . 3 ⊢ ((𝜑 ∧ (𝑌 + 𝑍) = 0 ) → ¬ 𝑤 ∈ (𝑁‘{𝑋, 𝑌}))
25	22, 24	ssneldd 3915	. 2 ⊢ ((𝜑 ∧ (𝑌 + 𝑍) = 0 ) → ¬ 𝑤 ∈ (𝑁‘{𝑋, (𝑌 + 𝑍)}))
26	23	adantr 486	. . 3 ⊢ ((𝜑 ∧ (𝑌 + 𝑍) ≠ 0 ) → ¬ 𝑤 ∈ (𝑁‘{𝑋, 𝑌}))
27		mapdindp1.p	. . . . . 6 ⊢ + = (+_g‘𝑊)
28	6	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ (𝑌 + 𝑍) ≠ 0 ) → 𝑊 ∈ LVec)
29	9	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ (𝑌 + 𝑍) ≠ 0 ) → 𝑋 ∈ (𝑉 ∖ { 0 }))
30	13	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ (𝑌 + 𝑍) ≠ 0 ) → 𝑌 ∈ (𝑉 ∖ { 0 }))
31		mapdindp1.z	. . . . . . 7 ⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 }))
32	31	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ (𝑌 + 𝑍) ≠ 0 ) → 𝑍 ∈ (𝑉 ∖ { 0 }))
33		mapdindp1.W	. . . . . . 7 ⊢ (𝜑 → 𝑤 ∈ (𝑉 ∖ { 0 }))
34	33	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ (𝑌 + 𝑍) ≠ 0 ) → 𝑤 ∈ (𝑉 ∖ { 0 }))
35		mapdindp1.e	. . . . . . 7 ⊢ (𝜑 → (𝑁‘{𝑌}) = (𝑁‘{𝑍}))
36	35	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ (𝑌 + 𝑍) ≠ 0 ) → (𝑁‘{𝑌}) = (𝑁‘{𝑍}))
37		mapdindp1.ne	. . . . . . 7 ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))
38	37	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ (𝑌 + 𝑍) ≠ 0 ) → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))
39		simpr 490	. . . . . 6 ⊢ ((𝜑 ∧ (𝑌 + 𝑍) ≠ 0 ) → (𝑌 + 𝑍) ≠ 0 )
40	3, 27, 4, 5, 28, 29, 30, 32, 34, 36, 38, 26, 39	mapdindp0 42916	. . . . 5 ⊢ ((𝜑 ∧ (𝑌 + 𝑍) ≠ 0 ) → (𝑁‘{(𝑌 + 𝑍)}) = (𝑁‘{𝑌}))
41	40	oveq2d 7443	. . . 4 ⊢ ((𝜑 ∧ (𝑌 + 𝑍) ≠ 0 ) → ((𝑁‘{𝑋})(LSSum‘𝑊)(𝑁‘{(𝑌 + 𝑍)})) = ((𝑁‘{𝑋})(LSSum‘𝑊)(𝑁‘{𝑌})))
42		eqid 2763	. . . . . 6 ⊢ (LSSum‘𝑊) = (LSSum‘𝑊)
43	31	eldifad 4053	. . . . . . 7 ⊢ (𝜑 → 𝑍 ∈ 𝑉)
44	3, 27	lmodvacl 21162	. . . . . . 7 ⊢ ((𝑊 ∈ LMod ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑉) → (𝑌 + 𝑍) ∈ 𝑉)
45	8, 14, 43, 44	syl3anc 1398	. . . . . 6 ⊢ (𝜑 → (𝑌 + 𝑍) ∈ 𝑉)
46	3, 5, 42, 8, 10, 45	lsmpr 21376	. . . . 5 ⊢ (𝜑 → (𝑁‘{𝑋, (𝑌 + 𝑍)}) = ((𝑁‘{𝑋})(LSSum‘𝑊)(𝑁‘{(𝑌 + 𝑍)})))
47	46	adantr 486	. . . 4 ⊢ ((𝜑 ∧ (𝑌 + 𝑍) ≠ 0 ) → (𝑁‘{𝑋, (𝑌 + 𝑍)}) = ((𝑁‘{𝑋})(LSSum‘𝑊)(𝑁‘{(𝑌 + 𝑍)})))
48	3, 5, 42, 8, 10, 14	lsmpr 21376	. . . . 5 ⊢ (𝜑 → (𝑁‘{𝑋, 𝑌}) = ((𝑁‘{𝑋})(LSSum‘𝑊)(𝑁‘{𝑌})))
49	48	adantr 486	. . . 4 ⊢ ((𝜑 ∧ (𝑌 + 𝑍) ≠ 0 ) → (𝑁‘{𝑋, 𝑌}) = ((𝑁‘{𝑋})(LSSum‘𝑊)(𝑁‘{𝑌})))
50	41, 47, 49	3eqtr4d 2808	. . 3 ⊢ ((𝜑 ∧ (𝑌 + 𝑍) ≠ 0 ) → (𝑁‘{𝑋, (𝑌 + 𝑍)}) = (𝑁‘{𝑋, 𝑌}))
51	26, 50	neleqtrrd 2886	. 2 ⊢ ((𝜑 ∧ (𝑌 + 𝑍) ≠ 0 ) → ¬ 𝑤 ∈ (𝑁‘{𝑋, (𝑌 + 𝑍)}))
52	25, 51	pm2.61dane 3045	1 ⊢ (𝜑 → ¬ 𝑤 ∈ (𝑁‘{𝑋, (𝑌 + 𝑍)}))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ∧ wa 401 = wceq 1569 ∈ wcel 2146 ≠ wne 2958 ⊆ wss 3899 ∖ cdif 4047 {csn 4587 {cpr 4589 ‘cfv 6546 (class class class)co 7427 Basecbs 17399 +_gcplusg 17440 0_gc0g 17622 LSSumclsm 19860 LModclmod 21147 LSpanclspn 21258 LVecclvec 21389

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 1944 ax-6 2001 ax-7 2042 ax-8 2148 ax-9 2156 ax-10 2179 ax-11 2196 ax-12 2215 ax-ext 2735 ax-rep 5234 ax-sep 5251 ax-nul 5262 ax-pow 5330 ax-pr 5394 ax-un 7758 ax-cnex 11266 ax-resscn 11267 ax-1cn 11268 ax-icn 11269 ax-addcl 11270 ax-addrcl 11271 ax-mulcl 11272 ax-mulrcl 11273 ax-mulcom 11274 ax-addass 11275 ax-mulass 11276 ax-distr 11277 ax-i2m1 11278 ax-1ne0 11279 ax-1rid 11280 ax-rnegex 11281 ax-rrecex 11282 ax-cnre 11283 ax-pre-lttri 11284 ax-pre-lttrn 11285 ax-pre-ltadd 11286 ax-pre-mulgt0 11287

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 2101 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2838 df-nfc 2912 df-ne 2959 df-nel 3065 df-ral 3080 df-rex 3090 df-rmo 3368 df-reu 3369 df-rab 3416 df-v 3455 df-sbc 3742 df-csb 3851 df-ss 3900 df-pss 4016 df-dif 4049 df-in 4093 df-un 4153 df-nul 4281 df-if 4485 df-pw 4561 df-sn 4588 df-pr 4590 df-op 4838 df-uni 4870 df-int 4910 df-iun 4955 df-br 5106 df-opab 5170 df-mpt 5189 df-tr 5215 df-id 5549 df-eprel 5554 df-po 5562 df-so 5563 df-fr 5607 df-we 5609 df-xp 5660 df-rel 5661 df-cnv 5662 df-co 5663 df-dm 5664 df-rn 5665 df-res 5666 df-ima 5667 df-pred 6310 df-ord 6371 df-on 6372 df-lim 6373 df-suc 6374 df-iota 6500 df-fun 6548 df-fn 6549 df-f 6550 df-f1 6551 df-fo 6552 df-f1o 6553 df-fv 6554 df-riota 7384 df-ov 7430 df-oprab 7431 df-mpo 7432 df-om 7885 df-1st 8008 df-2nd 8009 df-tpos 8254 df-frecs 8310 df-wrecs 8341 df-recs 8390 df-rdg 8429 df-er 8728 df-en 8985 df-dom 8986 df-sdom 8987 df-pnf 11355 df-mnf 11356 df-xr 11357 df-ltxr 11358 df-le 11359 df-sub 11553 df-neg 11554 df-nn 12346 df-2 12415 df-3 12416 df-sets 17354 df-slot 17372 df-ndx 17384 df-base 17400 df-ress 17421 df-plusg 17453 df-mulr 17454 df-0g 17624 df-mgm 18828 df-sgrp 18920 df-mnd 18936 df-submnd 18991 df-grp 19159 df-minusg 19160 df-sbg 19161 df-subg 19345 df-cntz 19543 df-lsm 19862 df-cmn 20008 df-abl 20009 df-mgp 20373 df-rng 20387 df-ur 20420 df-ring 20473 df-oppr 20579 df-dvdsr 20599 df-unit 20600 df-invr 20630 df-drng 20994 df-lmod 21149 df-lss 21219 df-lsp 21259 df-lvec 21390

This theorem is used by: mapdh6dN 42936 hdmap1l6d 43010

W3C validator