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 21067

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 21038	. . . . . . . . . . 11 ⊢ (𝑊 ∈ LVec → 𝑊 ∈ LMod)
4	2, 3	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝑊 ∈ LMod)
5		eqid 2731	. . . . . . . . . . 11 ⊢ (LSubSp‘𝑊) = (LSubSp‘𝑊)
6	5	lsssssubg 20889	. . . . . . . . . 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 20908	. . . . . . . . . 10 ⊢ ((𝑊 ∈ LMod ∧ 𝑌 ∈ 𝑉) → (𝑁‘{𝑌}) ∈ (LSubSp‘𝑊))
12	4, 8, 11	syl2anc 584	. . . . . . . . 9 ⊢ (𝜑 → (𝑁‘{𝑌}) ∈ (LSubSp‘𝑊))
13	7, 12	sseldd 3935	. . . . . . . 8 ⊢ (𝜑 → (𝑁‘{𝑌}) ∈ (SubGrp‘𝑊))
14		lspindpi.z	. . . . . . . . . 10 ⊢ (𝜑 → 𝑍 ∈ 𝑉)
15	9, 5, 10	lspsncl 20908	. . . . . . . . . 10 ⊢ ((𝑊 ∈ LMod ∧ 𝑍 ∈ 𝑉) → (𝑁‘{𝑍}) ∈ (LSubSp‘𝑊))
16	4, 14, 15	syl2anc 584	. . . . . . . . 9 ⊢ (𝜑 → (𝑁‘{𝑍}) ∈ (LSubSp‘𝑊))
17	7, 16	sseldd 3935	. . . . . . . 8 ⊢ (𝜑 → (𝑁‘{𝑍}) ∈ (SubGrp‘𝑊))
18		eqid 2731	. . . . . . . . 9 ⊢ (LSSum‘𝑊) = (LSSum‘𝑊)
19	18	lsmub1 19567	. . . . . . . 8 ⊢ (((𝑁‘{𝑌}) ∈ (SubGrp‘𝑊) ∧ (𝑁‘{𝑍}) ∈ (SubGrp‘𝑊)) → (𝑁‘{𝑌}) ⊆ ((𝑁‘{𝑌})(LSSum‘𝑊)(𝑁‘{𝑍})))
20	13, 17, 19	syl2anc 584	. . . . . . 7 ⊢ (𝜑 → (𝑁‘{𝑌}) ⊆ ((𝑁‘{𝑌})(LSSum‘𝑊)(𝑁‘{𝑍})))
21	9, 10, 18, 4, 8, 14	lsmpr 21021	. . . . . . 7 ⊢ (𝜑 → (𝑁‘{𝑌, 𝑍}) = ((𝑁‘{𝑌})(LSSum‘𝑊)(𝑁‘{𝑍})))
22	20, 21	sseqtrrd 3972	. . . . . 6 ⊢ (𝜑 → (𝑁‘{𝑌}) ⊆ (𝑁‘{𝑌, 𝑍}))
23		sseq1 3960	. . . . . 6 ⊢ ((𝑁‘{𝑋}) = (𝑁‘{𝑌}) → ((𝑁‘{𝑋}) ⊆ (𝑁‘{𝑌, 𝑍}) ↔ (𝑁‘{𝑌}) ⊆ (𝑁‘{𝑌, 𝑍})))
24	22, 23	syl5ibrcom 247	. . . . 5 ⊢ (𝜑 → ((𝑁‘{𝑋}) = (𝑁‘{𝑌}) → (𝑁‘{𝑋}) ⊆ (𝑁‘{𝑌, 𝑍})))
25	9, 5, 10, 4, 8, 14	lspprcl 20909	. . . . . 6 ⊢ (𝜑 → (𝑁‘{𝑌, 𝑍}) ∈ (LSubSp‘𝑊))
26		lspindpi.x	. . . . . 6 ⊢ (𝜑 → 𝑋 ∈ 𝑉)
27	9, 5, 10, 4, 25, 26	ellspsn5b 20926	. . . . 5 ⊢ (𝜑 → (𝑋 ∈ (𝑁‘{𝑌, 𝑍}) ↔ (𝑁‘{𝑋}) ⊆ (𝑁‘{𝑌, 𝑍})))
28	24, 27	sylibrd 259	. . . 4 ⊢ (𝜑 → ((𝑁‘{𝑋}) = (𝑁‘{𝑌}) → 𝑋 ∈ (𝑁‘{𝑌, 𝑍})))
29	28	necon3bd 2942	. . 3 ⊢ (𝜑 → (¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍}) → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})))
30	1, 29	mpd 15	. 2 ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))
31	18	lsmub2 19568	. . . . . . . 8 ⊢ (((𝑁‘{𝑌}) ∈ (SubGrp‘𝑊) ∧ (𝑁‘{𝑍}) ∈ (SubGrp‘𝑊)) → (𝑁‘{𝑍}) ⊆ ((𝑁‘{𝑌})(LSSum‘𝑊)(𝑁‘{𝑍})))
32	13, 17, 31	syl2anc 584	. . . . . . 7 ⊢ (𝜑 → (𝑁‘{𝑍}) ⊆ ((𝑁‘{𝑌})(LSSum‘𝑊)(𝑁‘{𝑍})))
33	32, 21	sseqtrrd 3972	. . . . . 6 ⊢ (𝜑 → (𝑁‘{𝑍}) ⊆ (𝑁‘{𝑌, 𝑍}))
34		sseq1 3960	. . . . . 6 ⊢ ((𝑁‘{𝑋}) = (𝑁‘{𝑍}) → ((𝑁‘{𝑋}) ⊆ (𝑁‘{𝑌, 𝑍}) ↔ (𝑁‘{𝑍}) ⊆ (𝑁‘{𝑌, 𝑍})))
35	33, 34	syl5ibrcom 247	. . . . 5 ⊢ (𝜑 → ((𝑁‘{𝑋}) = (𝑁‘{𝑍}) → (𝑁‘{𝑋}) ⊆ (𝑁‘{𝑌, 𝑍})))
36	35, 27	sylibrd 259	. . . 4 ⊢ (𝜑 → ((𝑁‘{𝑋}) = (𝑁‘{𝑍}) → 𝑋 ∈ (𝑁‘{𝑌, 𝑍})))
37	36	necon3bd 2942	. . 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 1541 ∈ wcel 2111 ≠ wne 2928 ⊆ wss 3902 {csn 4576 {cpr 4578 ‘cfv 6481 (class class class)co 7346 Basecbs 17117 SubGrpcsubg 19030 LSSumclsm 19544 LModclmod 20791 LSubSpclss 20862 LSpanclspn 20902 LVecclvec 21034

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2113 ax-9 2121 ax-10 2144 ax-11 2160 ax-12 2180 ax-ext 2703 ax-rep 5217 ax-sep 5234 ax-nul 5244 ax-pow 5303 ax-pr 5370 ax-un 7668 ax-cnex 11059 ax-resscn 11060 ax-1cn 11061 ax-icn 11062 ax-addcl 11063 ax-addrcl 11064 ax-mulcl 11065 ax-mulrcl 11066 ax-mulcom 11067 ax-addass 11068 ax-mulass 11069 ax-distr 11070 ax-i2m1 11071 ax-1ne0 11072 ax-1rid 11073 ax-rnegex 11074 ax-rrecex 11075 ax-cnre 11076 ax-pre-lttri 11077 ax-pre-lttrn 11078 ax-pre-ltadd 11079 ax-pre-mulgt0 11080

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2535 df-eu 2564 df-clab 2710 df-cleq 2723 df-clel 2806 df-nfc 2881 df-ne 2929 df-nel 3033 df-ral 3048 df-rex 3057 df-rmo 3346 df-reu 3347 df-rab 3396 df-v 3438 df-sbc 3742 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-pss 3922 df-nul 4284 df-if 4476 df-pw 4552 df-sn 4577 df-pr 4579 df-op 4583 df-uni 4860 df-int 4898 df-iun 4943 df-br 5092 df-opab 5154 df-mpt 5173 df-tr 5199 df-id 5511 df-eprel 5516 df-po 5524 df-so 5525 df-fr 5569 df-we 5571 df-xp 5622 df-rel 5623 df-cnv 5624 df-co 5625 df-dm 5626 df-rn 5627 df-res 5628 df-ima 5629 df-pred 6248 df-ord 6309 df-on 6310 df-lim 6311 df-suc 6312 df-iota 6437 df-fun 6483 df-fn 6484 df-f 6485 df-f1 6486 df-fo 6487 df-f1o 6488 df-fv 6489 df-riota 7303 df-ov 7349 df-oprab 7350 df-mpo 7351 df-om 7797 df-1st 7921 df-2nd 7922 df-frecs 8211 df-wrecs 8242 df-recs 8291 df-rdg 8329 df-er 8622 df-en 8870 df-dom 8871 df-sdom 8872 df-pnf 11145 df-mnf 11146 df-xr 11147 df-ltxr 11148 df-le 11149 df-sub 11343 df-neg 11344 df-nn 12123 df-2 12185 df-sets 17072 df-slot 17090 df-ndx 17102 df-base 17118 df-ress 17139 df-plusg 17171 df-0g 17342 df-mgm 18545 df-sgrp 18624 df-mnd 18640 df-submnd 18689 df-grp 18846 df-minusg 18847 df-sbg 18848 df-subg 19033 df-cntz 19227 df-lsm 19546 df-cmn 19692 df-abl 19693 df-mgp 20057 df-ur 20098 df-ring 20151 df-lmod 20793 df-lss 20863 df-lsp 20903 df-lvec 21035

This theorem is referenced by: lspindp1 21068 baerlem5amN 41754 baerlem5bmN 41755 baerlem5abmN 41756 mapdindp4 41761 mapdh6bN 41775 mapdh6cN 41776 mapdh6dN 41777 mapdh6eN 41778 mapdh6fN 41779 mapdh6hN 41781 mapdh7eN 41786 mapdh7dN 41788 mapdh7fN 41789 mapdh75fN 41793 mapdh8aa 41814 mapdh8ab 41815 mapdh8ad 41817 mapdh8c 41819 mapdh8d0N 41820 mapdh8d 41821 mapdh8e 41822 mapdh9a 41827 mapdh9aOLDN 41828 hdmap1eq4N 41844 hdmap1l6b 41849 hdmap1l6c 41850 hdmap1l6d 41851 hdmap1l6e 41852 hdmap1l6f 41853 hdmap1l6h 41855 hdmap1eulemOLDN 41861 hdmapval0 41871 hdmapval3lemN 41875 hdmap10lem 41877 hdmap11lem1 41879 hdmap14lem11 41916

W3C validator