Theorem lspss 20329

Description: Span preserves subset ordering. (spanss 29846 analog.) (Contributed by NM, 11-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.)

Hypotheses

Ref	Expression
lspss.v	⊢ 𝑉 = (Base‘𝑊)
lspss.n	⊢ 𝑁 = (LSpan‘𝑊)

Assertion

Ref	Expression
lspss	⊢ ((𝑊 ∈ LMod ∧ 𝑈 ⊆ 𝑉 ∧ 𝑇 ⊆ 𝑈) → (𝑁‘𝑇) ⊆ (𝑁‘𝑈))

Proof of Theorem lspss

Dummy variable 𝑡 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		simpl3 1192	. . . . 5 ⊢ (((𝑊 ∈ LMod ∧ 𝑈 ⊆ 𝑉 ∧ 𝑇 ⊆ 𝑈) ∧ 𝑡 ∈ (LSubSp‘𝑊)) → 𝑇 ⊆ 𝑈)
2		sstr2 3938	. . . . 5 ⊢ (𝑇 ⊆ 𝑈 → (𝑈 ⊆ 𝑡 → 𝑇 ⊆ 𝑡))
3	1, 2	syl 17	. . . 4 ⊢ (((𝑊 ∈ LMod ∧ 𝑈 ⊆ 𝑉 ∧ 𝑇 ⊆ 𝑈) ∧ 𝑡 ∈ (LSubSp‘𝑊)) → (𝑈 ⊆ 𝑡 → 𝑇 ⊆ 𝑡))
4	3	ss2rabdv 4020	. . 3 ⊢ ((𝑊 ∈ LMod ∧ 𝑈 ⊆ 𝑉 ∧ 𝑇 ⊆ 𝑈) → {𝑡 ∈ (LSubSp‘𝑊) ∣ 𝑈 ⊆ 𝑡} ⊆ {𝑡 ∈ (LSubSp‘𝑊) ∣ 𝑇 ⊆ 𝑡})
5		intss 4913	. . 3 ⊢ ({𝑡 ∈ (LSubSp‘𝑊) ∣ 𝑈 ⊆ 𝑡} ⊆ {𝑡 ∈ (LSubSp‘𝑊) ∣ 𝑇 ⊆ 𝑡} → ∩ {𝑡 ∈ (LSubSp‘𝑊) ∣ 𝑇 ⊆ 𝑡} ⊆ ∩ {𝑡 ∈ (LSubSp‘𝑊) ∣ 𝑈 ⊆ 𝑡})
6	4, 5	syl 17	. 2 ⊢ ((𝑊 ∈ LMod ∧ 𝑈 ⊆ 𝑉 ∧ 𝑇 ⊆ 𝑈) → ∩ {𝑡 ∈ (LSubSp‘𝑊) ∣ 𝑇 ⊆ 𝑡} ⊆ ∩ {𝑡 ∈ (LSubSp‘𝑊) ∣ 𝑈 ⊆ 𝑡})
7		simp1 1135	. . 3 ⊢ ((𝑊 ∈ LMod ∧ 𝑈 ⊆ 𝑉 ∧ 𝑇 ⊆ 𝑈) → 𝑊 ∈ LMod)
8		simp3 1137	. . . 4 ⊢ ((𝑊 ∈ LMod ∧ 𝑈 ⊆ 𝑉 ∧ 𝑇 ⊆ 𝑈) → 𝑇 ⊆ 𝑈)
9		simp2 1136	. . . 4 ⊢ ((𝑊 ∈ LMod ∧ 𝑈 ⊆ 𝑉 ∧ 𝑇 ⊆ 𝑈) → 𝑈 ⊆ 𝑉)
10	8, 9	sstrd 3941	. . 3 ⊢ ((𝑊 ∈ LMod ∧ 𝑈 ⊆ 𝑉 ∧ 𝑇 ⊆ 𝑈) → 𝑇 ⊆ 𝑉)
11		lspss.v	. . . 4 ⊢ 𝑉 = (Base‘𝑊)
12		eqid 2737	. . . 4 ⊢ (LSubSp‘𝑊) = (LSubSp‘𝑊)
13		lspss.n	. . . 4 ⊢ 𝑁 = (LSpan‘𝑊)
14	11, 12, 13	lspval 20320	. . 3 ⊢ ((𝑊 ∈ LMod ∧ 𝑇 ⊆ 𝑉) → (𝑁‘𝑇) = ∩ {𝑡 ∈ (LSubSp‘𝑊) ∣ 𝑇 ⊆ 𝑡})
15	7, 10, 14	syl2anc 584	. 2 ⊢ ((𝑊 ∈ LMod ∧ 𝑈 ⊆ 𝑉 ∧ 𝑇 ⊆ 𝑈) → (𝑁‘𝑇) = ∩ {𝑡 ∈ (LSubSp‘𝑊) ∣ 𝑇 ⊆ 𝑡})
16	11, 12, 13	lspval 20320	. . 3 ⊢ ((𝑊 ∈ LMod ∧ 𝑈 ⊆ 𝑉) → (𝑁‘𝑈) = ∩ {𝑡 ∈ (LSubSp‘𝑊) ∣ 𝑈 ⊆ 𝑡})
17	16	3adant3 1131	. 2 ⊢ ((𝑊 ∈ LMod ∧ 𝑈 ⊆ 𝑉 ∧ 𝑇 ⊆ 𝑈) → (𝑁‘𝑈) = ∩ {𝑡 ∈ (LSubSp‘𝑊) ∣ 𝑈 ⊆ 𝑡})
18	6, 15, 17	3sstr4d 3978	1 ⊢ ((𝑊 ∈ LMod ∧ 𝑈 ⊆ 𝑉 ∧ 𝑇 ⊆ 𝑈) → (𝑁‘𝑇) ⊆ (𝑁‘𝑈))

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1086   = wceq 1540   ∈ wcel 2105  {crab 3404   ⊆ wss 3897  ∩ cint 4892  ‘cfv 6466  Basecbs 16989  LModclmod 20206  LSubSpclss 20276  LSpanclspn 20316

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2708  ax-rep 5224  ax-sep 5238  ax-nul 5245  ax-pow 5303  ax-pr 5367

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-ral 3063  df-rex 3072  df-rmo 3350  df-reu 3351  df-rab 3405  df-v 3443  df-sbc 3727  df-csb 3843  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4268  df-if 4472  df-pw 4547  df-sn 4572  df-pr 4574  df-op 4578  df-uni 4851  df-int 4893  df-iun 4939  df-br 5088  df-opab 5150  df-mpt 5171  df-id 5507  df-xp 5614  df-rel 5615  df-cnv 5616  df-co 5617  df-dm 5618  df-rn 5619  df-res 5620  df-ima 5621  df-iota 6418  df-fun 6468  df-fn 6469  df-f 6470  df-f1 6471  df-fo 6472  df-f1o 6473  df-fv 6474  df-riota 7274  df-ov 7320  df-0g 17229  df-mgm 18403  df-sgrp 18452  df-mnd 18463  df-grp 18656  df-lmod 20208  df-lss 20277  df-lsp 20317

This theorem is referenced by:  lspun  20332  lspssp  20333  lspprid1  20342  lbspss  20427  lspsolvlem  20487  lspsolv  20488  lsppratlem3  20494  lbsextlem2  20504  lbsextlem3  20505  lbsextlem4  20506  lindfrn  21111  f1lindf  21112  mxidlprm  31779  idlsrgmulrss1  31795  idlsrgmulrss2  31796  lindsunlem  31845  dimkerim  31848  lindsadd  35842  lssats  37246  lpssat  37247  lssatle  37249  lssat  37250  dvhdimlem  39679  dvh3dim3N  39684  mapdindp2  39956  lspindp5  40005