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 21293

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 21264	. . . . . . . . . . 11 ⊢ (𝑊 ∈ LVec → 𝑊 ∈ LMod)
4	2, 3	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → 𝑊 ∈ LMod)
5		eqid 2766	. . . . . . . . . . 11 ⊢ (LSubSp‘𝑊) = (LSubSp‘𝑊)
6	5	lsssssubg 21116	. . . . . . . . . 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 21135	. . . . . . . . . 10 ⊢ ((𝑊 ∈ LMod ∧ 𝑌 ∈ 𝑉) → (𝑁‘{𝑌}) ∈ (LSubSp‘𝑊))
12	4, 8, 11	syl2anc 596	. . . . . . . . 9 ⊢ (𝜑 → (𝑁‘{𝑌}) ∈ (LSubSp‘𝑊))
13	7, 12	sseldd 3941	. . . . . . . 8 ⊢ (𝜑 → (𝑁‘{𝑌}) ∈ (SubGrp‘𝑊))
14		lspindpi.z	. . . . . . . . . 10 ⊢ (𝜑 → 𝑍 ∈ 𝑉)
15	9, 5, 10	lspsncl 21135	. . . . . . . . . 10 ⊢ ((𝑊 ∈ LMod ∧ 𝑍 ∈ 𝑉) → (𝑁‘{𝑍}) ∈ (LSubSp‘𝑊))
16	4, 14, 15	syl2anc 596	. . . . . . . . 9 ⊢ (𝜑 → (𝑁‘{𝑍}) ∈ (LSubSp‘𝑊))
17	7, 16	sseldd 3941	. . . . . . . 8 ⊢ (𝜑 → (𝑁‘{𝑍}) ∈ (SubGrp‘𝑊))
18		eqid 2766	. . . . . . . . 9 ⊢ (LSSum‘𝑊) = (LSSum‘𝑊)
19	18	lsmub1 19758	. . . . . . . 8 ⊢ (((𝑁‘{𝑌}) ∈ (SubGrp‘𝑊) ∧ (𝑁‘{𝑍}) ∈ (SubGrp‘𝑊)) → (𝑁‘{𝑌}) ⊆ ((𝑁‘{𝑌})(LSSum‘𝑊)(𝑁‘{𝑍})))
20	13, 17, 19	syl2anc 596	. . . . . . 7 ⊢ (𝜑 → (𝑁‘{𝑌}) ⊆ ((𝑁‘{𝑌})(LSSum‘𝑊)(𝑁‘{𝑍})))
21	9, 10, 18, 4, 8, 14	lsmpr 21247	. . . . . . 7 ⊢ (𝜑 → (𝑁‘{𝑌, 𝑍}) = ((𝑁‘{𝑌})(LSSum‘𝑊)(𝑁‘{𝑍})))
22	20, 21	sseqtrrd 3977	. . . . . 6 ⊢ (𝜑 → (𝑁‘{𝑌}) ⊆ (𝑁‘{𝑌, 𝑍}))
23		sseq1 3965	. . . . . 6 ⊢ ((𝑁‘{𝑋}) = (𝑁‘{𝑌}) → ((𝑁‘{𝑋}) ⊆ (𝑁‘{𝑌, 𝑍}) ↔ (𝑁‘{𝑌}) ⊆ (𝑁‘{𝑌, 𝑍})))
24	22, 23	syl5ibrcom 250	. . . . 5 ⊢ (𝜑 → ((𝑁‘{𝑋}) = (𝑁‘{𝑌}) → (𝑁‘{𝑋}) ⊆ (𝑁‘{𝑌, 𝑍})))
25	9, 5, 10, 4, 8, 14	lspprcl 21136	. . . . . 6 ⊢ (𝜑 → (𝑁‘{𝑌, 𝑍}) ∈ (LSubSp‘𝑊))
26		lspindpi.x	. . . . . 6 ⊢ (𝜑 → 𝑋 ∈ 𝑉)
27	9, 5, 10, 4, 25, 26	ellspsn5b 21153	. . . . 5 ⊢ (𝜑 → (𝑋 ∈ (𝑁‘{𝑌, 𝑍}) ↔ (𝑁‘{𝑋}) ⊆ (𝑁‘{𝑌, 𝑍})))
28	24, 27	sylibrd 262	. . . 4 ⊢ (𝜑 → ((𝑁‘{𝑋}) = (𝑁‘{𝑌}) → 𝑋 ∈ (𝑁‘{𝑌, 𝑍})))
29	28	necon3bd 2975	. . 3 ⊢ (𝜑 → (¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍}) → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})))
30	1, 29	mpd 16	. 2 ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))
31	18	lsmub2 19759	. . . . . . . 8 ⊢ (((𝑁‘{𝑌}) ∈ (SubGrp‘𝑊) ∧ (𝑁‘{𝑍}) ∈ (SubGrp‘𝑊)) → (𝑁‘{𝑍}) ⊆ ((𝑁‘{𝑌})(LSSum‘𝑊)(𝑁‘{𝑍})))
32	13, 17, 31	syl2anc 596	. . . . . . 7 ⊢ (𝜑 → (𝑁‘{𝑍}) ⊆ ((𝑁‘{𝑌})(LSSum‘𝑊)(𝑁‘{𝑍})))
33	32, 21	sseqtrrd 3977	. . . . . 6 ⊢ (𝜑 → (𝑁‘{𝑍}) ⊆ (𝑁‘{𝑌, 𝑍}))
34		sseq1 3965	. . . . . 6 ⊢ ((𝑁‘{𝑋}) = (𝑁‘{𝑍}) → ((𝑁‘{𝑋}) ⊆ (𝑁‘{𝑌, 𝑍}) ↔ (𝑁‘{𝑍}) ⊆ (𝑁‘{𝑌, 𝑍})))
35	33, 34	syl5ibrcom 250	. . . . 5 ⊢ (𝜑 → ((𝑁‘{𝑋}) = (𝑁‘{𝑍}) → (𝑁‘{𝑋}) ⊆ (𝑁‘{𝑌, 𝑍})))
36	35, 27	sylibrd 262	. . . 4 ⊢ (𝜑 → ((𝑁‘{𝑋}) = (𝑁‘{𝑍}) → 𝑋 ∈ (𝑁‘{𝑌, 𝑍})))
37	36	necon3bd 2975	. . 3 ⊢ (𝜑 → (¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍}) → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑍})))
38	1, 37	mpd 16	. 2 ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑍}))
39	30, 38	jca 521	1 ⊢ (𝜑 → ((𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}) ∧ (𝑁‘{𝑋}) ≠ (𝑁‘{𝑍})))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ∧ wa 401 = wceq 1570 ∈ wcel 2146 ≠ wne 2961 ⊆ wss 3908 {csn 4594 {cpr 4596 ‘cfv 6543 (class class class)co 7423 Basecbs 17294 SubGrpcsubg 19217 LSSumclsm 19735 LModclmod 21018 LSubSpclss 21089 LSpanclspn 21129 LVecclvec 21260

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2148 ax-9 2156 ax-10 2179 ax-11 2195 ax-12 2216 ax-ext 2738 ax-rep 5243 ax-sep 5262 ax-nul 5274 ax-pow 5341 ax-pr 5409 ax-un 7745 ax-cnex 11174 ax-resscn 11175 ax-1cn 11176 ax-icn 11177 ax-addcl 11178 ax-addrcl 11179 ax-mulcl 11180 ax-mulrcl 11181 ax-mulcom 11182 ax-addass 11183 ax-mulass 11184 ax-distr 11185 ax-i2m1 11186 ax-1ne0 11187 ax-1rid 11188 ax-rnegex 11189 ax-rrecex 11190 ax-cnre 11191 ax-pre-lttri 11192 ax-pre-lttrn 11193 ax-pre-ltadd 11194 ax-pre-mulgt0 11195

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2570 df-eu 2600 df-clab 2745 df-cleq 2758 df-clel 2841 df-nfc 2915 df-ne 2962 df-nel 3068 df-ral 3083 df-rex 3093 df-rmo 3372 df-reu 3373 df-rab 3420 df-v 3460 df-sbc 3748 df-csb 3857 df-dif 3911 df-un 3913 df-in 3915 df-ss 3925 df-pss 3928 df-nul 4290 df-if 4493 df-pw 4569 df-sn 4595 df-pr 4597 df-op 4601 df-uni 4878 df-int 4918 df-iun 4963 df-br 5115 df-opab 5179 df-mpt 5198 df-tr 5224 df-id 5561 df-eprel 5566 df-po 5574 df-so 5575 df-fr 5619 df-we 5621 df-xp 5672 df-rel 5673 df-cnv 5674 df-co 5675 df-dm 5676 df-rn 5677 df-res 5678 df-ima 5679 df-pred 6309 df-ord 6370 df-on 6371 df-lim 6372 df-suc 6373 df-iota 6499 df-fun 6545 df-fn 6546 df-f 6547 df-f1 6548 df-fo 6549 df-f1o 6550 df-fv 6551 df-riota 7380 df-ov 7426 df-oprab 7427 df-mpo 7428 df-om 7872 df-1st 7995 df-2nd 7996 df-frecs 8287 df-wrecs 8318 df-recs 8367 df-rdg 8406 df-er 8703 df-en 8953 df-dom 8954 df-sdom 8955 df-pnf 11263 df-mnf 11264 df-xr 11265 df-ltxr 11266 df-le 11267 df-sub 11461 df-neg 11462 df-nn 12252 df-2 12321 df-sets 17249 df-slot 17267 df-ndx 17279 df-base 17295 df-ress 17316 df-plusg 17348 df-0g 17519 df-mgm 18723 df-sgrp 18806 df-mnd 18822 df-submnd 18873 df-grp 19034 df-minusg 19035 df-sbg 19036 df-subg 19220 df-cntz 19418 df-lsm 19737 df-cmn 19883 df-abl 19884 df-mgp 20248 df-ur 20295 df-ring 20348 df-lmod 21020 df-lss 21090 df-lsp 21130 df-lvec 21261

This theorem is used by: lspindp1 21294 baerlem5amN 42531 baerlem5bmN 42532 baerlem5abmN 42533 mapdindp4 42538 mapdh6bN 42552 mapdh6cN 42553 mapdh6dN 42554 mapdh6eN 42555 mapdh6fN 42556 mapdh6hN 42558 mapdh7eN 42563 mapdh7dN 42565 mapdh7fN 42566 mapdh75fN 42570 mapdh8aa 42591 mapdh8ab 42592 mapdh8ad 42594 mapdh8c 42596 mapdh8d0N 42597 mapdh8d 42598 mapdh8e 42599 mapdh9a 42604 mapdh9aOLDN 42605 hdmap1eq4N 42621 hdmap1l6b 42626 hdmap1l6c 42627 hdmap1l6d 42628 hdmap1l6e 42629 hdmap1l6f 42630 hdmap1l6h 42632 hdmap1eulemOLDN 42638 hdmapval0 42648 hdmapval3lemN 42652 hdmap10lem 42654 hdmap11lem1 42656 hdmap14lem11 42693

W3C validator