Step | Hyp | Ref
| Expression |
1 | | eqid 2622 |
. . . . 5
⊢
(Base‘𝑊) =
(Base‘𝑊) |
2 | 1 | lindff 20154 |
. . . 4
⊢ ((𝐹 LIndF 𝑊 ∧ 𝑊 ∈ LMod) → 𝐹:dom 𝐹⟶(Base‘𝑊)) |
3 | 2 | ancoms 469 |
. . 3
⊢ ((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊) → 𝐹:dom 𝐹⟶(Base‘𝑊)) |
4 | | frn 6053 |
. . 3
⊢ (𝐹:dom 𝐹⟶(Base‘𝑊) → ran 𝐹 ⊆ (Base‘𝑊)) |
5 | 3, 4 | syl 17 |
. 2
⊢ ((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊) → ran 𝐹 ⊆ (Base‘𝑊)) |
6 | | simpll 790 |
. . . . . . 7
⊢ (((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊) ∧ 𝑦 ∈ dom 𝐹) → 𝑊 ∈ LMod) |
7 | | imassrn 5477 |
. . . . . . . . 9
⊢ (𝐹 “ (dom 𝐹 ∖ {𝑦})) ⊆ ran 𝐹 |
8 | 7, 5 | syl5ss 3614 |
. . . . . . . 8
⊢ ((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊) → (𝐹 “ (dom 𝐹 ∖ {𝑦})) ⊆ (Base‘𝑊)) |
9 | 8 | adantr 481 |
. . . . . . 7
⊢ (((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊) ∧ 𝑦 ∈ dom 𝐹) → (𝐹 “ (dom 𝐹 ∖ {𝑦})) ⊆ (Base‘𝑊)) |
10 | | ffun 6048 |
. . . . . . . . 9
⊢ (𝐹:dom 𝐹⟶(Base‘𝑊) → Fun 𝐹) |
11 | 3, 10 | syl 17 |
. . . . . . . 8
⊢ ((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊) → Fun 𝐹) |
12 | | eldifsn 4317 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (ran 𝐹 ∖ {(𝐹‘𝑦)}) ↔ (𝑥 ∈ ran 𝐹 ∧ 𝑥 ≠ (𝐹‘𝑦))) |
13 | | funfn 5918 |
. . . . . . . . . . . . . 14
⊢ (Fun
𝐹 ↔ 𝐹 Fn dom 𝐹) |
14 | | fvelrnb 6243 |
. . . . . . . . . . . . . 14
⊢ (𝐹 Fn dom 𝐹 → (𝑥 ∈ ran 𝐹 ↔ ∃𝑘 ∈ dom 𝐹(𝐹‘𝑘) = 𝑥)) |
15 | 13, 14 | sylbi 207 |
. . . . . . . . . . . . 13
⊢ (Fun
𝐹 → (𝑥 ∈ ran 𝐹 ↔ ∃𝑘 ∈ dom 𝐹(𝐹‘𝑘) = 𝑥)) |
16 | 15 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((Fun
𝐹 ∧ 𝑦 ∈ dom 𝐹) → (𝑥 ∈ ran 𝐹 ↔ ∃𝑘 ∈ dom 𝐹(𝐹‘𝑘) = 𝑥)) |
17 | | difss 3737 |
. . . . . . . . . . . . . . . . . 18
⊢ (dom
𝐹 ∖ {𝑦}) ⊆ dom 𝐹 |
18 | 17 | jctr 565 |
. . . . . . . . . . . . . . . . 17
⊢ (Fun
𝐹 → (Fun 𝐹 ∧ (dom 𝐹 ∖ {𝑦}) ⊆ dom 𝐹)) |
19 | 18 | ad2antrr 762 |
. . . . . . . . . . . . . . . 16
⊢ (((Fun
𝐹 ∧ 𝑦 ∈ dom 𝐹) ∧ (𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ≠ (𝐹‘𝑦))) → (Fun 𝐹 ∧ (dom 𝐹 ∖ {𝑦}) ⊆ dom 𝐹)) |
20 | | simpl 473 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ≠ (𝐹‘𝑦)) → 𝑘 ∈ dom 𝐹) |
21 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 = 𝑦 → (𝐹‘𝑘) = (𝐹‘𝑦)) |
22 | 21 | necon3i 2826 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐹‘𝑘) ≠ (𝐹‘𝑦) → 𝑘 ≠ 𝑦) |
23 | 22 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ≠ (𝐹‘𝑦)) → 𝑘 ≠ 𝑦) |
24 | | eldifsn 4317 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ (dom 𝐹 ∖ {𝑦}) ↔ (𝑘 ∈ dom 𝐹 ∧ 𝑘 ≠ 𝑦)) |
25 | 20, 23, 24 | sylanbrc 698 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ≠ (𝐹‘𝑦)) → 𝑘 ∈ (dom 𝐹 ∖ {𝑦})) |
26 | 25 | adantl 482 |
. . . . . . . . . . . . . . . 16
⊢ (((Fun
𝐹 ∧ 𝑦 ∈ dom 𝐹) ∧ (𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ≠ (𝐹‘𝑦))) → 𝑘 ∈ (dom 𝐹 ∖ {𝑦})) |
27 | | funfvima2 6493 |
. . . . . . . . . . . . . . . 16
⊢ ((Fun
𝐹 ∧ (dom 𝐹 ∖ {𝑦}) ⊆ dom 𝐹) → (𝑘 ∈ (dom 𝐹 ∖ {𝑦}) → (𝐹‘𝑘) ∈ (𝐹 “ (dom 𝐹 ∖ {𝑦})))) |
28 | 19, 26, 27 | sylc 65 |
. . . . . . . . . . . . . . 15
⊢ (((Fun
𝐹 ∧ 𝑦 ∈ dom 𝐹) ∧ (𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ≠ (𝐹‘𝑦))) → (𝐹‘𝑘) ∈ (𝐹 “ (dom 𝐹 ∖ {𝑦}))) |
29 | 28 | expr 643 |
. . . . . . . . . . . . . 14
⊢ (((Fun
𝐹 ∧ 𝑦 ∈ dom 𝐹) ∧ 𝑘 ∈ dom 𝐹) → ((𝐹‘𝑘) ≠ (𝐹‘𝑦) → (𝐹‘𝑘) ∈ (𝐹 “ (dom 𝐹 ∖ {𝑦})))) |
30 | | neeq1 2856 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹‘𝑘) = 𝑥 → ((𝐹‘𝑘) ≠ (𝐹‘𝑦) ↔ 𝑥 ≠ (𝐹‘𝑦))) |
31 | | eleq1 2689 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹‘𝑘) = 𝑥 → ((𝐹‘𝑘) ∈ (𝐹 “ (dom 𝐹 ∖ {𝑦})) ↔ 𝑥 ∈ (𝐹 “ (dom 𝐹 ∖ {𝑦})))) |
32 | 30, 31 | imbi12d 334 |
. . . . . . . . . . . . . 14
⊢ ((𝐹‘𝑘) = 𝑥 → (((𝐹‘𝑘) ≠ (𝐹‘𝑦) → (𝐹‘𝑘) ∈ (𝐹 “ (dom 𝐹 ∖ {𝑦}))) ↔ (𝑥 ≠ (𝐹‘𝑦) → 𝑥 ∈ (𝐹 “ (dom 𝐹 ∖ {𝑦}))))) |
33 | 29, 32 | syl5ibcom 235 |
. . . . . . . . . . . . 13
⊢ (((Fun
𝐹 ∧ 𝑦 ∈ dom 𝐹) ∧ 𝑘 ∈ dom 𝐹) → ((𝐹‘𝑘) = 𝑥 → (𝑥 ≠ (𝐹‘𝑦) → 𝑥 ∈ (𝐹 “ (dom 𝐹 ∖ {𝑦}))))) |
34 | 33 | rexlimdva 3031 |
. . . . . . . . . . . 12
⊢ ((Fun
𝐹 ∧ 𝑦 ∈ dom 𝐹) → (∃𝑘 ∈ dom 𝐹(𝐹‘𝑘) = 𝑥 → (𝑥 ≠ (𝐹‘𝑦) → 𝑥 ∈ (𝐹 “ (dom 𝐹 ∖ {𝑦}))))) |
35 | 16, 34 | sylbid 230 |
. . . . . . . . . . 11
⊢ ((Fun
𝐹 ∧ 𝑦 ∈ dom 𝐹) → (𝑥 ∈ ran 𝐹 → (𝑥 ≠ (𝐹‘𝑦) → 𝑥 ∈ (𝐹 “ (dom 𝐹 ∖ {𝑦}))))) |
36 | 35 | impd 447 |
. . . . . . . . . 10
⊢ ((Fun
𝐹 ∧ 𝑦 ∈ dom 𝐹) → ((𝑥 ∈ ran 𝐹 ∧ 𝑥 ≠ (𝐹‘𝑦)) → 𝑥 ∈ (𝐹 “ (dom 𝐹 ∖ {𝑦})))) |
37 | 12, 36 | syl5bi 232 |
. . . . . . . . 9
⊢ ((Fun
𝐹 ∧ 𝑦 ∈ dom 𝐹) → (𝑥 ∈ (ran 𝐹 ∖ {(𝐹‘𝑦)}) → 𝑥 ∈ (𝐹 “ (dom 𝐹 ∖ {𝑦})))) |
38 | 37 | ssrdv 3609 |
. . . . . . . 8
⊢ ((Fun
𝐹 ∧ 𝑦 ∈ dom 𝐹) → (ran 𝐹 ∖ {(𝐹‘𝑦)}) ⊆ (𝐹 “ (dom 𝐹 ∖ {𝑦}))) |
39 | 11, 38 | sylan 488 |
. . . . . . 7
⊢ (((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊) ∧ 𝑦 ∈ dom 𝐹) → (ran 𝐹 ∖ {(𝐹‘𝑦)}) ⊆ (𝐹 “ (dom 𝐹 ∖ {𝑦}))) |
40 | | eqid 2622 |
. . . . . . . 8
⊢
(LSpan‘𝑊) =
(LSpan‘𝑊) |
41 | 1, 40 | lspss 18984 |
. . . . . . 7
⊢ ((𝑊 ∈ LMod ∧ (𝐹 “ (dom 𝐹 ∖ {𝑦})) ⊆ (Base‘𝑊) ∧ (ran 𝐹 ∖ {(𝐹‘𝑦)}) ⊆ (𝐹 “ (dom 𝐹 ∖ {𝑦}))) → ((LSpan‘𝑊)‘(ran 𝐹 ∖ {(𝐹‘𝑦)})) ⊆ ((LSpan‘𝑊)‘(𝐹 “ (dom 𝐹 ∖ {𝑦})))) |
42 | 6, 9, 39, 41 | syl3anc 1326 |
. . . . . 6
⊢ (((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊) ∧ 𝑦 ∈ dom 𝐹) → ((LSpan‘𝑊)‘(ran 𝐹 ∖ {(𝐹‘𝑦)})) ⊆ ((LSpan‘𝑊)‘(𝐹 “ (dom 𝐹 ∖ {𝑦})))) |
43 | 42 | adantrr 753 |
. . . . 5
⊢ (((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊) ∧ (𝑦 ∈ dom 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}))) → ((LSpan‘𝑊)‘(ran 𝐹 ∖ {(𝐹‘𝑦)})) ⊆ ((LSpan‘𝑊)‘(𝐹 “ (dom 𝐹 ∖ {𝑦})))) |
44 | | simplr 792 |
. . . . . 6
⊢ (((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊) ∧ (𝑦 ∈ dom 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}))) → 𝐹 LIndF 𝑊) |
45 | | simprl 794 |
. . . . . 6
⊢ (((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊) ∧ (𝑦 ∈ dom 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}))) → 𝑦 ∈ dom 𝐹) |
46 | | eldifi 3732 |
. . . . . . 7
⊢ (𝑘 ∈
((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}) → 𝑘 ∈ (Base‘(Scalar‘𝑊))) |
47 | 46 | ad2antll 765 |
. . . . . 6
⊢ (((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊) ∧ (𝑦 ∈ dom 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}))) → 𝑘 ∈ (Base‘(Scalar‘𝑊))) |
48 | | eldifsni 4320 |
. . . . . . 7
⊢ (𝑘 ∈
((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}) → 𝑘 ≠
(0g‘(Scalar‘𝑊))) |
49 | 48 | ad2antll 765 |
. . . . . 6
⊢ (((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊) ∧ (𝑦 ∈ dom 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}))) → 𝑘 ≠
(0g‘(Scalar‘𝑊))) |
50 | | eqid 2622 |
. . . . . . 7
⊢ (
·𝑠 ‘𝑊) = ( ·𝑠
‘𝑊) |
51 | | eqid 2622 |
. . . . . . 7
⊢
(Scalar‘𝑊) =
(Scalar‘𝑊) |
52 | | eqid 2622 |
. . . . . . 7
⊢
(0g‘(Scalar‘𝑊)) =
(0g‘(Scalar‘𝑊)) |
53 | | eqid 2622 |
. . . . . . 7
⊢
(Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊)) |
54 | 50, 40, 51, 52, 53 | lindfind 20155 |
. . . . . 6
⊢ (((𝐹 LIndF 𝑊 ∧ 𝑦 ∈ dom 𝐹) ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑘 ≠
(0g‘(Scalar‘𝑊)))) → ¬ (𝑘( ·𝑠
‘𝑊)(𝐹‘𝑦)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (dom 𝐹 ∖ {𝑦})))) |
55 | 44, 45, 47, 49, 54 | syl22anc 1327 |
. . . . 5
⊢ (((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊) ∧ (𝑦 ∈ dom 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}))) → ¬ (𝑘( ·𝑠
‘𝑊)(𝐹‘𝑦)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (dom 𝐹 ∖ {𝑦})))) |
56 | 43, 55 | ssneldd 3606 |
. . . 4
⊢ (((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊) ∧ (𝑦 ∈ dom 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}))) → ¬ (𝑘( ·𝑠
‘𝑊)(𝐹‘𝑦)) ∈ ((LSpan‘𝑊)‘(ran 𝐹 ∖ {(𝐹‘𝑦)}))) |
57 | 56 | ralrimivva 2971 |
. . 3
⊢ ((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊) → ∀𝑦 ∈ dom 𝐹∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}) ¬ (𝑘( ·𝑠
‘𝑊)(𝐹‘𝑦)) ∈ ((LSpan‘𝑊)‘(ran 𝐹 ∖ {(𝐹‘𝑦)}))) |
58 | 11, 13 | sylib 208 |
. . . 4
⊢ ((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊) → 𝐹 Fn dom 𝐹) |
59 | | oveq2 6658 |
. . . . . . . 8
⊢ (𝑥 = (𝐹‘𝑦) → (𝑘( ·𝑠
‘𝑊)𝑥) = (𝑘( ·𝑠
‘𝑊)(𝐹‘𝑦))) |
60 | | sneq 4187 |
. . . . . . . . . 10
⊢ (𝑥 = (𝐹‘𝑦) → {𝑥} = {(𝐹‘𝑦)}) |
61 | 60 | difeq2d 3728 |
. . . . . . . . 9
⊢ (𝑥 = (𝐹‘𝑦) → (ran 𝐹 ∖ {𝑥}) = (ran 𝐹 ∖ {(𝐹‘𝑦)})) |
62 | 61 | fveq2d 6195 |
. . . . . . . 8
⊢ (𝑥 = (𝐹‘𝑦) → ((LSpan‘𝑊)‘(ran 𝐹 ∖ {𝑥})) = ((LSpan‘𝑊)‘(ran 𝐹 ∖ {(𝐹‘𝑦)}))) |
63 | 59, 62 | eleq12d 2695 |
. . . . . . 7
⊢ (𝑥 = (𝐹‘𝑦) → ((𝑘( ·𝑠
‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘(ran 𝐹 ∖ {𝑥})) ↔ (𝑘( ·𝑠
‘𝑊)(𝐹‘𝑦)) ∈ ((LSpan‘𝑊)‘(ran 𝐹 ∖ {(𝐹‘𝑦)})))) |
64 | 63 | notbid 308 |
. . . . . 6
⊢ (𝑥 = (𝐹‘𝑦) → (¬ (𝑘( ·𝑠
‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘(ran 𝐹 ∖ {𝑥})) ↔ ¬ (𝑘( ·𝑠
‘𝑊)(𝐹‘𝑦)) ∈ ((LSpan‘𝑊)‘(ran 𝐹 ∖ {(𝐹‘𝑦)})))) |
65 | 64 | ralbidv 2986 |
. . . . 5
⊢ (𝑥 = (𝐹‘𝑦) → (∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}) ¬ (𝑘( ·𝑠
‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘(ran 𝐹 ∖ {𝑥})) ↔ ∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}) ¬ (𝑘( ·𝑠
‘𝑊)(𝐹‘𝑦)) ∈ ((LSpan‘𝑊)‘(ran 𝐹 ∖ {(𝐹‘𝑦)})))) |
66 | 65 | ralrn 6362 |
. . . 4
⊢ (𝐹 Fn dom 𝐹 → (∀𝑥 ∈ ran 𝐹∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}) ¬ (𝑘( ·𝑠
‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘(ran 𝐹 ∖ {𝑥})) ↔ ∀𝑦 ∈ dom 𝐹∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}) ¬ (𝑘( ·𝑠
‘𝑊)(𝐹‘𝑦)) ∈ ((LSpan‘𝑊)‘(ran 𝐹 ∖ {(𝐹‘𝑦)})))) |
67 | 58, 66 | syl 17 |
. . 3
⊢ ((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊) → (∀𝑥 ∈ ran 𝐹∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}) ¬ (𝑘( ·𝑠
‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘(ran 𝐹 ∖ {𝑥})) ↔ ∀𝑦 ∈ dom 𝐹∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}) ¬ (𝑘( ·𝑠
‘𝑊)(𝐹‘𝑦)) ∈ ((LSpan‘𝑊)‘(ran 𝐹 ∖ {(𝐹‘𝑦)})))) |
68 | 57, 67 | mpbird 247 |
. 2
⊢ ((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊) → ∀𝑥 ∈ ran 𝐹∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}) ¬ (𝑘( ·𝑠
‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘(ran 𝐹 ∖ {𝑥}))) |
69 | 1, 50, 40, 51, 53, 52 | islinds2 20152 |
. . 3
⊢ (𝑊 ∈ LMod → (ran 𝐹 ∈ (LIndS‘𝑊) ↔ (ran 𝐹 ⊆ (Base‘𝑊) ∧ ∀𝑥 ∈ ran 𝐹∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}) ¬ (𝑘( ·𝑠
‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘(ran 𝐹 ∖ {𝑥}))))) |
70 | 69 | adantr 481 |
. 2
⊢ ((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊) → (ran 𝐹 ∈ (LIndS‘𝑊) ↔ (ran 𝐹 ⊆ (Base‘𝑊) ∧ ∀𝑥 ∈ ran 𝐹∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}) ¬ (𝑘( ·𝑠
‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘(ran 𝐹 ∖ {𝑥}))))) |
71 | 5, 68, 70 | mpbir2and 957 |
1
⊢ ((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊) → ran 𝐹 ∈ (LIndS‘𝑊)) |