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