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 21098

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 21069	. . . . . . . . . . 11 ⊢ (𝑊 ∈ LVec → 𝑊 ∈ LMod)
4	2, 3	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝑊 ∈ LMod)
5		eqid 2736	. . . . . . . . . . 11 ⊢ (LSubSp‘𝑊) = (LSubSp‘𝑊)
6	5	lsssssubg 20920	. . . . . . . . . 10 ⊢ (𝑊 ∈ LMod → (LSubSp‘𝑊) ⊆ (SubGrp‘𝑊))
7	4, 6	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (LSubSp‘𝑊) ⊆ (SubGrp‘𝑊))
8		lspindpi.y	. . . . . . . . . 10 ⊢ (𝜑 → 𝑌 ∈ 𝑉)
9		lspindpi.v	. . . . . . . . . . 11 ⊢ 𝑉 = (Base‘𝑊)
10		lspindpi.n	. . . . . . . . . . 11 ⊢ 𝑁 = (LSpan‘𝑊)
11	9, 5, 10	lspsncl 20939	. . . . . . . . . 10 ⊢ ((𝑊 ∈ LMod ∧ 𝑌 ∈ 𝑉) → (𝑁‘{𝑌}) ∈ (LSubSp‘𝑊))
12	4, 8, 11	syl2anc 584	. . . . . . . . 9 ⊢ (𝜑 → (𝑁‘{𝑌}) ∈ (LSubSp‘𝑊))
13	7, 12	sseldd 3964	. . . . . . . 8 ⊢ (𝜑 → (𝑁‘{𝑌}) ∈ (SubGrp‘𝑊))
14		lspindpi.z	. . . . . . . . . 10 ⊢ (𝜑 → 𝑍 ∈ 𝑉)
15	9, 5, 10	lspsncl 20939	. . . . . . . . . 10 ⊢ ((𝑊 ∈ LMod ∧ 𝑍 ∈ 𝑉) → (𝑁‘{𝑍}) ∈ (LSubSp‘𝑊))
16	4, 14, 15	syl2anc 584	. . . . . . . . 9 ⊢ (𝜑 → (𝑁‘{𝑍}) ∈ (LSubSp‘𝑊))
17	7, 16	sseldd 3964	. . . . . . . 8 ⊢ (𝜑 → (𝑁‘{𝑍}) ∈ (SubGrp‘𝑊))
18		eqid 2736	. . . . . . . . 9 ⊢ (LSSum‘𝑊) = (LSSum‘𝑊)
19	18	lsmub1 19643	. . . . . . . 8 ⊢ (((𝑁‘{𝑌}) ∈ (SubGrp‘𝑊) ∧ (𝑁‘{𝑍}) ∈ (SubGrp‘𝑊)) → (𝑁‘{𝑌}) ⊆ ((𝑁‘{𝑌})(LSSum‘𝑊)(𝑁‘{𝑍})))
20	13, 17, 19	syl2anc 584	. . . . . . 7 ⊢ (𝜑 → (𝑁‘{𝑌}) ⊆ ((𝑁‘{𝑌})(LSSum‘𝑊)(𝑁‘{𝑍})))
21	9, 10, 18, 4, 8, 14	lsmpr 21052	. . . . . . 7 ⊢ (𝜑 → (𝑁‘{𝑌, 𝑍}) = ((𝑁‘{𝑌})(LSSum‘𝑊)(𝑁‘{𝑍})))
22	20, 21	sseqtrrd 4001	. . . . . 6 ⊢ (𝜑 → (𝑁‘{𝑌}) ⊆ (𝑁‘{𝑌, 𝑍}))
23		sseq1 3989	. . . . . 6 ⊢ ((𝑁‘{𝑋}) = (𝑁‘{𝑌}) → ((𝑁‘{𝑋}) ⊆ (𝑁‘{𝑌, 𝑍}) ↔ (𝑁‘{𝑌}) ⊆ (𝑁‘{𝑌, 𝑍})))
24	22, 23	syl5ibrcom 247	. . . . 5 ⊢ (𝜑 → ((𝑁‘{𝑋}) = (𝑁‘{𝑌}) → (𝑁‘{𝑋}) ⊆ (𝑁‘{𝑌, 𝑍})))
25	9, 5, 10, 4, 8, 14	lspprcl 20940	. . . . . 6 ⊢ (𝜑 → (𝑁‘{𝑌, 𝑍}) ∈ (LSubSp‘𝑊))
26		lspindpi.x	. . . . . 6 ⊢ (𝜑 → 𝑋 ∈ 𝑉)
27	9, 5, 10, 4, 25, 26	ellspsn5b 20957	. . . . 5 ⊢ (𝜑 → (𝑋 ∈ (𝑁‘{𝑌, 𝑍}) ↔ (𝑁‘{𝑋}) ⊆ (𝑁‘{𝑌, 𝑍})))
28	24, 27	sylibrd 259	. . . 4 ⊢ (𝜑 → ((𝑁‘{𝑋}) = (𝑁‘{𝑌}) → 𝑋 ∈ (𝑁‘{𝑌, 𝑍})))
29	28	necon3bd 2947	. . 3 ⊢ (𝜑 → (¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍}) → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})))
30	1, 29	mpd 15	. 2 ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))
31	18	lsmub2 19644	. . . . . . . 8 ⊢ (((𝑁‘{𝑌}) ∈ (SubGrp‘𝑊) ∧ (𝑁‘{𝑍}) ∈ (SubGrp‘𝑊)) → (𝑁‘{𝑍}) ⊆ ((𝑁‘{𝑌})(LSSum‘𝑊)(𝑁‘{𝑍})))
32	13, 17, 31	syl2anc 584	. . . . . . 7 ⊢ (𝜑 → (𝑁‘{𝑍}) ⊆ ((𝑁‘{𝑌})(LSSum‘𝑊)(𝑁‘{𝑍})))
33	32, 21	sseqtrrd 4001	. . . . . 6 ⊢ (𝜑 → (𝑁‘{𝑍}) ⊆ (𝑁‘{𝑌, 𝑍}))
34		sseq1 3989	. . . . . 6 ⊢ ((𝑁‘{𝑋}) = (𝑁‘{𝑍}) → ((𝑁‘{𝑋}) ⊆ (𝑁‘{𝑌, 𝑍}) ↔ (𝑁‘{𝑍}) ⊆ (𝑁‘{𝑌, 𝑍})))
35	33, 34	syl5ibrcom 247	. . . . 5 ⊢ (𝜑 → ((𝑁‘{𝑋}) = (𝑁‘{𝑍}) → (𝑁‘{𝑋}) ⊆ (𝑁‘{𝑌, 𝑍})))
36	35, 27	sylibrd 259	. . . 4 ⊢ (𝜑 → ((𝑁‘{𝑋}) = (𝑁‘{𝑍}) → 𝑋 ∈ (𝑁‘{𝑌, 𝑍})))
37	36	necon3bd 2947	. . 3 ⊢ (𝜑 → (¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍}) → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑍})))
38	1, 37	mpd 15	. 2 ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑍}))
39	30, 38	jca 511	1 ⊢ (𝜑 → ((𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}) ∧ (𝑁‘{𝑋}) ≠ (𝑁‘{𝑍})))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 395 = wceq 1540 ∈ wcel 2109 ≠ wne 2933 ⊆ wss 3931 {csn 4606 {cpr 4608 ‘cfv 6536 (class class class)co 7410 Basecbs 17233 SubGrpcsubg 19108 LSSumclsm 19620 LModclmod 20822 LSubSpclss 20893 LSpanclspn 20933 LVecclvec 21065

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2708 ax-rep 5254 ax-sep 5271 ax-nul 5281 ax-pow 5340 ax-pr 5407 ax-un 7734 ax-cnex 11190 ax-resscn 11191 ax-1cn 11192 ax-icn 11193 ax-addcl 11194 ax-addrcl 11195 ax-mulcl 11196 ax-mulrcl 11197 ax-mulcom 11198 ax-addass 11199 ax-mulass 11200 ax-distr 11201 ax-i2m1 11202 ax-1ne0 11203 ax-1rid 11204 ax-rnegex 11205 ax-rrecex 11206 ax-cnre 11207 ax-pre-lttri 11208 ax-pre-lttrn 11209 ax-pre-ltadd 11210 ax-pre-mulgt0 11211

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2810 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3062 df-rmo 3364 df-reu 3365 df-rab 3421 df-v 3466 df-sbc 3771 df-csb 3880 df-dif 3934 df-un 3936 df-in 3938 df-ss 3948 df-pss 3951 df-nul 4314 df-if 4506 df-pw 4582 df-sn 4607 df-pr 4609 df-op 4613 df-uni 4889 df-int 4928 df-iun 4974 df-br 5125 df-opab 5187 df-mpt 5207 df-tr 5235 df-id 5553 df-eprel 5558 df-po 5566 df-so 5567 df-fr 5611 df-we 5613 df-xp 5665 df-rel 5666 df-cnv 5667 df-co 5668 df-dm 5669 df-rn 5670 df-res 5671 df-ima 5672 df-pred 6295 df-ord 6360 df-on 6361 df-lim 6362 df-suc 6363 df-iota 6489 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-riota 7367 df-ov 7413 df-oprab 7414 df-mpo 7415 df-om 7867 df-1st 7993 df-2nd 7994 df-frecs 8285 df-wrecs 8316 df-recs 8390 df-rdg 8429 df-er 8724 df-en 8965 df-dom 8966 df-sdom 8967 df-pnf 11276 df-mnf 11277 df-xr 11278 df-ltxr 11279 df-le 11280 df-sub 11473 df-neg 11474 df-nn 12246 df-2 12308 df-sets 17188 df-slot 17206 df-ndx 17218 df-base 17234 df-ress 17257 df-plusg 17289 df-0g 17460 df-mgm 18623 df-sgrp 18702 df-mnd 18718 df-submnd 18767 df-grp 18924 df-minusg 18925 df-sbg 18926 df-subg 19111 df-cntz 19305 df-lsm 19622 df-cmn 19768 df-abl 19769 df-mgp 20106 df-ur 20147 df-ring 20200 df-lmod 20824 df-lss 20894 df-lsp 20934 df-lvec 21066

This theorem is referenced by: lspindp1 21099 baerlem5amN 41740 baerlem5bmN 41741 baerlem5abmN 41742 mapdindp4 41747 mapdh6bN 41761 mapdh6cN 41762 mapdh6dN 41763 mapdh6eN 41764 mapdh6fN 41765 mapdh6hN 41767 mapdh7eN 41772 mapdh7dN 41774 mapdh7fN 41775 mapdh75fN 41779 mapdh8aa 41800 mapdh8ab 41801 mapdh8ad 41803 mapdh8c 41805 mapdh8d0N 41806 mapdh8d 41807 mapdh8e 41808 mapdh9a 41813 mapdh9aOLDN 41814 hdmap1eq4N 41830 hdmap1l6b 41835 hdmap1l6c 41836 hdmap1l6d 41837 hdmap1l6e 41838 hdmap1l6f 41839 hdmap1l6h 41841 hdmap1eulemOLDN 41847 hdmapval0 41857 hdmapval3lemN 41861 hdmap10lem 41863 hdmap11lem1 41865 hdmap14lem11 41902

W3C validator