Theorem lspss 21292

Description: Span preserves subset ordering. (spanss 31983 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 1212	. . . . 5 ⊢ (((𝑊 ∈ LMod ∧ 𝑈 ⊆ 𝑉 ∧ 𝑇 ⊆ 𝑈) ∧ 𝑡 ∈ (LSubSp‘𝑊)) → 𝑇 ⊆ 𝑈)
2		sstr2 3920	. . . . 5 ⊢ (𝑇 ⊆ 𝑈 → (𝑈 ⊆ 𝑡 → 𝑇 ⊆ 𝑡))
3	1, 2	syl 18	. . . 4 ⊢ (((𝑊 ∈ LMod ∧ 𝑈 ⊆ 𝑉 ∧ 𝑇 ⊆ 𝑈) ∧ 𝑡 ∈ (LSubSp‘𝑊)) → (𝑈 ⊆ 𝑡 → 𝑇 ⊆ 𝑡))
4	3	ss2rabdv 4003	. . 3 ⊢ ((𝑊 ∈ LMod ∧ 𝑈 ⊆ 𝑉 ∧ 𝑇 ⊆ 𝑈) → {𝑡 ∈ (LSubSp‘𝑊) ∣ 𝑈 ⊆ 𝑡} ⊆ {𝑡 ∈ (LSubSp‘𝑊) ∣ 𝑇 ⊆ 𝑡})
5		intss 4932	. . 3 ⊢ ({𝑡 ∈ (LSubSp‘𝑊) ∣ 𝑈 ⊆ 𝑡} ⊆ {𝑡 ∈ (LSubSp‘𝑊) ∣ 𝑇 ⊆ 𝑡} → ∩ {𝑡 ∈ (LSubSp‘𝑊) ∣ 𝑇 ⊆ 𝑡} ⊆ ∩ {𝑡 ∈ (LSubSp‘𝑊) ∣ 𝑈 ⊆ 𝑡})
6	4, 5	syl 18	. 2 ⊢ ((𝑊 ∈ LMod ∧ 𝑈 ⊆ 𝑉 ∧ 𝑇 ⊆ 𝑈) → ∩ {𝑡 ∈ (LSubSp‘𝑊) ∣ 𝑇 ⊆ 𝑡} ⊆ ∩ {𝑡 ∈ (LSubSp‘𝑊) ∣ 𝑈 ⊆ 𝑡})
7		simp1 1154	. . 3 ⊢ ((𝑊 ∈ LMod ∧ 𝑈 ⊆ 𝑉 ∧ 𝑇 ⊆ 𝑈) → 𝑊 ∈ LMod)
8		simp3 1156	. . . 4 ⊢ ((𝑊 ∈ LMod ∧ 𝑈 ⊆ 𝑉 ∧ 𝑇 ⊆ 𝑈) → 𝑇 ⊆ 𝑈)
9		simp2 1155	. . . 4 ⊢ ((𝑊 ∈ LMod ∧ 𝑈 ⊆ 𝑉 ∧ 𝑇 ⊆ 𝑈) → 𝑈 ⊆ 𝑉)
10	8, 9	sstrd 3923	. . 3 ⊢ ((𝑊 ∈ LMod ∧ 𝑈 ⊆ 𝑉 ∧ 𝑇 ⊆ 𝑈) → 𝑇 ⊆ 𝑉)
11		lspss.v	. . . 4 ⊢ 𝑉 = (Base‘𝑊)
12		eqid 2763	. . . 4 ⊢ (LSubSp‘𝑊) = (LSubSp‘𝑊)
13		lspss.n	. . . 4 ⊢ 𝑁 = (LSpan‘𝑊)
14	11, 12, 13	lspval 21283	. . 3 ⊢ ((𝑊 ∈ LMod ∧ 𝑇 ⊆ 𝑉) → (𝑁‘𝑇) = ∩ {𝑡 ∈ (LSubSp‘𝑊) ∣ 𝑇 ⊆ 𝑡})
15	7, 10, 14	syl2anc 596	. 2 ⊢ ((𝑊 ∈ LMod ∧ 𝑈 ⊆ 𝑉 ∧ 𝑇 ⊆ 𝑈) → (𝑁‘𝑇) = ∩ {𝑡 ∈ (LSubSp‘𝑊) ∣ 𝑇 ⊆ 𝑡})
16	11, 12, 13	lspval 21283	. . 3 ⊢ ((𝑊 ∈ LMod ∧ 𝑈 ⊆ 𝑉) → (𝑁‘𝑈) = ∩ {𝑡 ∈ (LSubSp‘𝑊) ∣ 𝑈 ⊆ 𝑡})
17	16	3adant3 1150	. 2 ⊢ ((𝑊 ∈ LMod ∧ 𝑈 ⊆ 𝑉 ∧ 𝑇 ⊆ 𝑈) → (𝑁‘𝑈) = ∩ {𝑡 ∈ (LSubSp‘𝑊) ∣ 𝑈 ⊆ 𝑡})
18	6, 15, 17	3sstr4d 3968	1 ⊢ ((𝑊 ∈ LMod ∧ 𝑈 ⊆ 𝑉 ∧ 𝑇 ⊆ 𝑈) → (𝑁‘𝑇) ⊆ (𝑁‘𝑈))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103   = wceq 1570   ∈ wcel 2147  {crab 3416   ⊆ wss 3900  ∩ cint 4910  ‘cfv 6561  Basecbs 17419  LModclmod 21168  LSubSpclss 21239  LSpanclspn 21279

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-rep 5236  ax-sep 5253  ax-nul 5264  ax-pow 5332  ax-pr 5396

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-int 4911  df-iun 4956  df-br 5107  df-opab 5172  df-mpt 5191  df-id 5551  df-xp 5662  df-rel 5663  df-cnv 5664  df-co 5665  df-dm 5666  df-rn 5667  df-res 5668  df-ima 5669  df-iota 6515  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-riota 7403  df-ov 7449  df-0g 17644  df-mgm 18848  df-sgrp 18940  df-mnd 18956  df-grp 19179  df-lmod 21170  df-lss 21240  df-lsp 21280

This theorem is used by:  lspun  21295  lspssp  21296  lspprid1  21305  lbspss  21390  lspsolvlem  21453  lspsolv  21454  lsppratlem3  21460  lbsextlem2  21470  lbsextlem3  21471  lbsextlem4  21472  lindfrn  22160  f1lindf  22161  mxidlprm  34079  idlsrgmulrss1  34127  idlsrgmulrss2  34128  lindsunlem  34339  dimkerim  34342  lindsadd  38741  lssats  40272  lpssat  40273  lssatle  40275  lssat  40276  dvhdimlem  42704  dvh3dim3N  42709  mapdindp2  42981  lspindp5  43030