lspindpi - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > lspindpi		Structured version Visualization version GIF version

Theorem lspindpi 21237

Description: Partial independence property. (Contributed by NM, 23-Apr-2015.)

**Hypotheses**
Ref	Expression
lspindpi.v	⊢ 𝑉 = (Base‘𝑊)
lspindpi.n	⊢ 𝑁 = (LSpan‘𝑊)
lspindpi.w	⊢ (𝜑 → 𝑊 ∈ LVec)
lspindpi.x	⊢ (𝜑 → 𝑋 ∈ 𝑉)
lspindpi.y	⊢ (𝜑 → 𝑌 ∈ 𝑉)
lspindpi.z	⊢ (𝜑 → 𝑍 ∈ 𝑉)
lspindpi.e	⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍}))

**Assertion**
Ref	Expression
lspindpi	⊢ (𝜑 → ((𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}) ∧ (𝑁‘{𝑋}) ≠ (𝑁‘{𝑍})))

**Proof of Theorem lspindpi**
Step	Hyp	Ref	Expression
1		lspindpi.e	. . 3 ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍}))
2		lspindpi.w	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑊 ∈ LVec)
3		lveclmod 21208	. . . . . . . . . . 11 ⊢ (𝑊 ∈ LVec → 𝑊 ∈ LMod)
4	2, 3	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → 𝑊 ∈ LMod)
5		eqid 2763	. . . . . . . . . . 11 ⊢ (LSubSp‘𝑊) = (LSubSp‘𝑊)
6	5	lsssssubg 21060	. . . . . . . . . 10 ⊢ (𝑊 ∈ LMod → (LSubSp‘𝑊) ⊆ (SubGrp‘𝑊))
7	4, 6	syl 18	. . . . . . . . 9 ⊢ (𝜑 → (LSubSp‘𝑊) ⊆ (SubGrp‘𝑊))
8		lspindpi.y	. . . . . . . . . 10 ⊢ (𝜑 → 𝑌 ∈ 𝑉)
9		lspindpi.v	. . . . . . . . . . 11 ⊢ 𝑉 = (Base‘𝑊)
10		lspindpi.n	. . . . . . . . . . 11 ⊢ 𝑁 = (LSpan‘𝑊)
11	9, 5, 10	lspsncl 21079	. . . . . . . . . 10 ⊢ ((𝑊 ∈ LMod ∧ 𝑌 ∈ 𝑉) → (𝑁‘{𝑌}) ∈ (LSubSp‘𝑊))
12	4, 8, 11	syl2anc 595	. . . . . . . . 9 ⊢ (𝜑 → (𝑁‘{𝑌}) ∈ (LSubSp‘𝑊))
13	7, 12	sseldd 3939	. . . . . . . 8 ⊢ (𝜑 → (𝑁‘{𝑌}) ∈ (SubGrp‘𝑊))
14		lspindpi.z	. . . . . . . . . 10 ⊢ (𝜑 → 𝑍 ∈ 𝑉)
15	9, 5, 10	lspsncl 21079	. . . . . . . . . 10 ⊢ ((𝑊 ∈ LMod ∧ 𝑍 ∈ 𝑉) → (𝑁‘{𝑍}) ∈ (LSubSp‘𝑊))
16	4, 14, 15	syl2anc 595	. . . . . . . . 9 ⊢ (𝜑 → (𝑁‘{𝑍}) ∈ (LSubSp‘𝑊))
17	7, 16	sseldd 3939	. . . . . . . 8 ⊢ (𝜑 → (𝑁‘{𝑍}) ∈ (SubGrp‘𝑊))
18		eqid 2763	. . . . . . . . 9 ⊢ (LSSum‘𝑊) = (LSSum‘𝑊)
19	18	lsmub1 19728	. . . . . . . 8 ⊢ (((𝑁‘{𝑌}) ∈ (SubGrp‘𝑊) ∧ (𝑁‘{𝑍}) ∈ (SubGrp‘𝑊)) → (𝑁‘{𝑌}) ⊆ ((𝑁‘{𝑌})(LSSum‘𝑊)(𝑁‘{𝑍})))
20	13, 17, 19	syl2anc 595	. . . . . . 7 ⊢ (𝜑 → (𝑁‘{𝑌}) ⊆ ((𝑁‘{𝑌})(LSSum‘𝑊)(𝑁‘{𝑍})))
21	9, 10, 18, 4, 8, 14	lsmpr 21191	. . . . . . 7 ⊢ (𝜑 → (𝑁‘{𝑌, 𝑍}) = ((𝑁‘{𝑌})(LSSum‘𝑊)(𝑁‘{𝑍})))
22	20, 21	sseqtrrd 3975	. . . . . 6 ⊢ (𝜑 → (𝑁‘{𝑌}) ⊆ (𝑁‘{𝑌, 𝑍}))
23		sseq1 3963	. . . . . 6 ⊢ ((𝑁‘{𝑋}) = (𝑁‘{𝑌}) → ((𝑁‘{𝑋}) ⊆ (𝑁‘{𝑌, 𝑍}) ↔ (𝑁‘{𝑌}) ⊆ (𝑁‘{𝑌, 𝑍})))
24	22, 23	syl5ibrcom 250	. . . . 5 ⊢ (𝜑 → ((𝑁‘{𝑋}) = (𝑁‘{𝑌}) → (𝑁‘{𝑋}) ⊆ (𝑁‘{𝑌, 𝑍})))
25	9, 5, 10, 4, 8, 14	lspprcl 21080	. . . . . 6 ⊢ (𝜑 → (𝑁‘{𝑌, 𝑍}) ∈ (LSubSp‘𝑊))
26		lspindpi.x	. . . . . 6 ⊢ (𝜑 → 𝑋 ∈ 𝑉)
27	9, 5, 10, 4, 25, 26	ellspsn5b 21097	. . . . 5 ⊢ (𝜑 → (𝑋 ∈ (𝑁‘{𝑌, 𝑍}) ↔ (𝑁‘{𝑋}) ⊆ (𝑁‘{𝑌, 𝑍})))
28	24, 27	sylibrd 262	. . . 4 ⊢ (𝜑 → ((𝑁‘{𝑋}) = (𝑁‘{𝑌}) → 𝑋 ∈ (𝑁‘{𝑌, 𝑍})))
29	28	necon3bd 2972	. . 3 ⊢ (𝜑 → (¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍}) → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})))
30	1, 29	mpd 16	. 2 ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))
31	18	lsmub2 19729	. . . . . . . 8 ⊢ (((𝑁‘{𝑌}) ∈ (SubGrp‘𝑊) ∧ (𝑁‘{𝑍}) ∈ (SubGrp‘𝑊)) → (𝑁‘{𝑍}) ⊆ ((𝑁‘{𝑌})(LSSum‘𝑊)(𝑁‘{𝑍})))
32	13, 17, 31	syl2anc 595	. . . . . . 7 ⊢ (𝜑 → (𝑁‘{𝑍}) ⊆ ((𝑁‘{𝑌})(LSSum‘𝑊)(𝑁‘{𝑍})))
33	32, 21	sseqtrrd 3975	. . . . . 6 ⊢ (𝜑 → (𝑁‘{𝑍}) ⊆ (𝑁‘{𝑌, 𝑍}))
34		sseq1 3963	. . . . . 6 ⊢ ((𝑁‘{𝑋}) = (𝑁‘{𝑍}) → ((𝑁‘{𝑋}) ⊆ (𝑁‘{𝑌, 𝑍}) ↔ (𝑁‘{𝑍}) ⊆ (𝑁‘{𝑌, 𝑍})))
35	33, 34	syl5ibrcom 250	. . . . 5 ⊢ (𝜑 → ((𝑁‘{𝑋}) = (𝑁‘{𝑍}) → (𝑁‘{𝑋}) ⊆ (𝑁‘{𝑌, 𝑍})))
36	35, 27	sylibrd 262	. . . 4 ⊢ (𝜑 → ((𝑁‘{𝑋}) = (𝑁‘{𝑍}) → 𝑋 ∈ (𝑁‘{𝑌, 𝑍})))
37	36	necon3bd 2972	. . 3 ⊢ (𝜑 → (¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍}) → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑍})))
38	1, 37	mpd 16	. 2 ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑍}))
39	30, 38	jca 520	1 ⊢ (𝜑 → ((𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}) ∧ (𝑁‘{𝑋}) ≠ (𝑁‘{𝑍})))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 400 = wceq 1570 ∈ wcel 2143 ≠ wne 2958 ⊆ wss 3906 {csn 4590 {cpr 4592 ‘cfv 6538 (class class class)co 7412 Basecbs 17270 SubGrpcsubg 19187 LSSumclsm 19705 LModclmod 20962 LSubSpclss 21033 LSpanclspn 21073 LVecclvec 21204

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1825 ax-4 1839 ax-5 1940 ax-6 1997 ax-7 2038 ax-8 2145 ax-9 2153 ax-10 2176 ax-11 2192 ax-12 2213 ax-ext 2735 ax-rep 5239 ax-sep 5258 ax-nul 5270 ax-pow 5338 ax-pr 5406 ax-un 7734 ax-cnex 11157 ax-resscn 11158 ax-1cn 11159 ax-icn 11160 ax-addcl 11161 ax-addrcl 11162 ax-mulcl 11163 ax-mulrcl 11164 ax-mulcom 11165 ax-addass 11166 ax-mulass 11167 ax-distr 11168 ax-i2m1 11169 ax-1ne0 11170 ax-1rid 11171 ax-rnegex 11172 ax-rrecex 11173 ax-cnre 11174 ax-pre-lttri 11175 ax-pre-lttrn 11176 ax-pre-ltadd 11177 ax-pre-mulgt0 11178

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1810 df-nf 1814 df-sb 2097 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 3369 df-reu 3370 df-rab 3417 df-v 3457 df-sbc 3746 df-csb 3855 df-dif 3909 df-un 3911 df-in 3913 df-ss 3923 df-pss 3926 df-nul 4288 df-if 4489 df-pw 4565 df-sn 4591 df-pr 4593 df-op 4597 df-uni 4874 df-int 4914 df-iun 4959 df-br 5111 df-opab 5175 df-mpt 5194 df-tr 5220 df-id 5558 df-eprel 5563 df-po 5571 df-so 5572 df-fr 5616 df-we 5618 df-xp 5669 df-rel 5670 df-cnv 5671 df-co 5672 df-dm 5673 df-rn 5674 df-res 5675 df-ima 5676 df-pred 6304 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6494 df-fun 6540 df-fn 6541 df-f 6542 df-f1 6543 df-fo 6544 df-f1o 6545 df-fv 6546 df-riota 7369 df-ov 7415 df-oprab 7416 df-mpo 7417 df-om 7864 df-1st 7987 df-2nd 7988 df-frecs 8279 df-wrecs 8310 df-recs 8359 df-rdg 8398 df-er 8695 df-en 8945 df-dom 8946 df-sdom 8947 df-pnf 11246 df-mnf 11247 df-xr 11248 df-ltxr 11249 df-le 11250 df-sub 11444 df-neg 11445 df-nn 12235 df-2 12304 df-sets 17225 df-slot 17243 df-ndx 17255 df-base 17271 df-ress 17292 df-plusg 17324 df-0g 17495 df-mgm 18699 df-sgrp 18778 df-mnd 18794 df-submnd 18843 df-grp 19004 df-minusg 19005 df-sbg 19006 df-subg 19190 df-cntz 19388 df-lsm 19707 df-cmn 19853 df-abl 19854 df-mgp 20218 df-ur 20265 df-ring 20318 df-lmod 20964 df-lss 21034 df-lsp 21074 df-lvec 21205

This theorem is referenced by: lspindp1 21238 baerlem5amN 42468 baerlem5bmN 42469 baerlem5abmN 42470 mapdindp4 42475 mapdh6bN 42489 mapdh6cN 42490 mapdh6dN 42491 mapdh6eN 42492 mapdh6fN 42493 mapdh6hN 42495 mapdh7eN 42500 mapdh7dN 42502 mapdh7fN 42503 mapdh75fN 42507 mapdh8aa 42528 mapdh8ab 42529 mapdh8ad 42531 mapdh8c 42533 mapdh8d0N 42534 mapdh8d 42535 mapdh8e 42536 mapdh9a 42541 mapdh9aOLDN 42542 hdmap1eq4N 42558 hdmap1l6b 42563 hdmap1l6c 42564 hdmap1l6d 42565 hdmap1l6e 42566 hdmap1l6f 42567 hdmap1l6h 42569 hdmap1eulemOLDN 42575 hdmapval0 42585 hdmapval3lemN 42589 hdmap10lem 42591 hdmap11lem1 42593 hdmap14lem11 42630

W3C validator