Step |
Hyp |
Ref |
Expression |
1 |
|
filnm.b |
⊢ 𝐵 = ( Base ‘ 𝑊 ) |
2 |
|
simpl |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝐵 ∈ Fin ) → 𝑊 ∈ LMod ) |
3 |
|
eqid |
⊢ ( LSubSp ‘ 𝑊 ) = ( LSubSp ‘ 𝑊 ) |
4 |
1 3
|
lssss |
⊢ ( 𝑎 ∈ ( LSubSp ‘ 𝑊 ) → 𝑎 ⊆ 𝐵 ) |
5 |
4
|
adantl |
⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐵 ∈ Fin ) ∧ 𝑎 ∈ ( LSubSp ‘ 𝑊 ) ) → 𝑎 ⊆ 𝐵 ) |
6 |
|
velpw |
⊢ ( 𝑎 ∈ 𝒫 𝐵 ↔ 𝑎 ⊆ 𝐵 ) |
7 |
5 6
|
sylibr |
⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐵 ∈ Fin ) ∧ 𝑎 ∈ ( LSubSp ‘ 𝑊 ) ) → 𝑎 ∈ 𝒫 𝐵 ) |
8 |
|
simplr |
⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐵 ∈ Fin ) ∧ 𝑎 ∈ ( LSubSp ‘ 𝑊 ) ) → 𝐵 ∈ Fin ) |
9 |
|
ssfi |
⊢ ( ( 𝐵 ∈ Fin ∧ 𝑎 ⊆ 𝐵 ) → 𝑎 ∈ Fin ) |
10 |
8 5 9
|
syl2anc |
⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐵 ∈ Fin ) ∧ 𝑎 ∈ ( LSubSp ‘ 𝑊 ) ) → 𝑎 ∈ Fin ) |
11 |
7 10
|
elind |
⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐵 ∈ Fin ) ∧ 𝑎 ∈ ( LSubSp ‘ 𝑊 ) ) → 𝑎 ∈ ( 𝒫 𝐵 ∩ Fin ) ) |
12 |
|
eqid |
⊢ ( LSpan ‘ 𝑊 ) = ( LSpan ‘ 𝑊 ) |
13 |
3 12
|
lspid |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝑎 ∈ ( LSubSp ‘ 𝑊 ) ) → ( ( LSpan ‘ 𝑊 ) ‘ 𝑎 ) = 𝑎 ) |
14 |
13
|
adantlr |
⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐵 ∈ Fin ) ∧ 𝑎 ∈ ( LSubSp ‘ 𝑊 ) ) → ( ( LSpan ‘ 𝑊 ) ‘ 𝑎 ) = 𝑎 ) |
15 |
14
|
eqcomd |
⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐵 ∈ Fin ) ∧ 𝑎 ∈ ( LSubSp ‘ 𝑊 ) ) → 𝑎 = ( ( LSpan ‘ 𝑊 ) ‘ 𝑎 ) ) |
16 |
|
fveq2 |
⊢ ( 𝑏 = 𝑎 → ( ( LSpan ‘ 𝑊 ) ‘ 𝑏 ) = ( ( LSpan ‘ 𝑊 ) ‘ 𝑎 ) ) |
17 |
16
|
rspceeqv |
⊢ ( ( 𝑎 ∈ ( 𝒫 𝐵 ∩ Fin ) ∧ 𝑎 = ( ( LSpan ‘ 𝑊 ) ‘ 𝑎 ) ) → ∃ 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) 𝑎 = ( ( LSpan ‘ 𝑊 ) ‘ 𝑏 ) ) |
18 |
11 15 17
|
syl2anc |
⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐵 ∈ Fin ) ∧ 𝑎 ∈ ( LSubSp ‘ 𝑊 ) ) → ∃ 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) 𝑎 = ( ( LSpan ‘ 𝑊 ) ‘ 𝑏 ) ) |
19 |
18
|
ralrimiva |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝐵 ∈ Fin ) → ∀ 𝑎 ∈ ( LSubSp ‘ 𝑊 ) ∃ 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) 𝑎 = ( ( LSpan ‘ 𝑊 ) ‘ 𝑏 ) ) |
20 |
1 3 12
|
islnm2 |
⊢ ( 𝑊 ∈ LNoeM ↔ ( 𝑊 ∈ LMod ∧ ∀ 𝑎 ∈ ( LSubSp ‘ 𝑊 ) ∃ 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) 𝑎 = ( ( LSpan ‘ 𝑊 ) ‘ 𝑏 ) ) ) |
21 |
2 19 20
|
sylanbrc |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝐵 ∈ Fin ) → 𝑊 ∈ LNoeM ) |