Step | Hyp | Ref
| Expression |
1 | | eqid 2610 |
. . . . 5
⊢
(Base‘𝑊) =
(Base‘𝑊) |
2 | 1 | lindff 19973 |
. . . 4
⊢ ((𝐹 LIndF 𝑊 ∧ 𝑊 ∈ LMod) → 𝐹:dom 𝐹⟶(Base‘𝑊)) |
3 | 2 | ancoms 468 |
. . 3
⊢ ((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊) → 𝐹:dom 𝐹⟶(Base‘𝑊)) |
4 | | frn 5966 |
. . 3
⊢ (𝐹:dom 𝐹⟶(Base‘𝑊) → ran 𝐹 ⊆ (Base‘𝑊)) |
5 | 3, 4 | syl 17 |
. 2
⊢ ((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊) → ran 𝐹 ⊆ (Base‘𝑊)) |
6 | | simpll 786 |
. . . . . . 7
⊢ (((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊) ∧ 𝑦 ∈ dom 𝐹) → 𝑊 ∈ LMod) |
7 | | imassrn 5396 |
. . . . . . . . 9
⊢ (𝐹 “ (dom 𝐹 ∖ {𝑦})) ⊆ ran 𝐹 |
8 | 7, 5 | syl5ss 3579 |
. . . . . . . 8
⊢ ((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊) → (𝐹 “ (dom 𝐹 ∖ {𝑦})) ⊆ (Base‘𝑊)) |
9 | 8 | adantr 480 |
. . . . . . 7
⊢ (((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊) ∧ 𝑦 ∈ dom 𝐹) → (𝐹 “ (dom 𝐹 ∖ {𝑦})) ⊆ (Base‘𝑊)) |
10 | | ffun 5961 |
. . . . . . . . 9
⊢ (𝐹:dom 𝐹⟶(Base‘𝑊) → Fun 𝐹) |
11 | 3, 10 | syl 17 |
. . . . . . . 8
⊢ ((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊) → Fun 𝐹) |
12 | | eldifsn 4260 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (ran 𝐹 ∖ {(𝐹‘𝑦)}) ↔ (𝑥 ∈ ran 𝐹 ∧ 𝑥 ≠ (𝐹‘𝑦))) |
13 | | funfn 5833 |
. . . . . . . . . . . . . 14
⊢ (Fun
𝐹 ↔ 𝐹 Fn dom 𝐹) |
14 | | fvelrnb 6153 |
. . . . . . . . . . . . . 14
⊢ (𝐹 Fn dom 𝐹 → (𝑥 ∈ ran 𝐹 ↔ ∃𝑘 ∈ dom 𝐹(𝐹‘𝑘) = 𝑥)) |
15 | 13, 14 | sylbi 206 |
. . . . . . . . . . . . 13
⊢ (Fun
𝐹 → (𝑥 ∈ ran 𝐹 ↔ ∃𝑘 ∈ dom 𝐹(𝐹‘𝑘) = 𝑥)) |
16 | 15 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((Fun
𝐹 ∧ 𝑦 ∈ dom 𝐹) → (𝑥 ∈ ran 𝐹 ↔ ∃𝑘 ∈ dom 𝐹(𝐹‘𝑘) = 𝑥)) |
17 | | difss 3699 |
. . . . . . . . . . . . . . . . . 18
⊢ (dom
𝐹 ∖ {𝑦}) ⊆ dom 𝐹 |
18 | 17 | jctr 563 |
. . . . . . . . . . . . . . . . 17
⊢ (Fun
𝐹 → (Fun 𝐹 ∧ (dom 𝐹 ∖ {𝑦}) ⊆ dom 𝐹)) |
19 | 18 | ad2antrr 758 |
. . . . . . . . . . . . . . . 16
⊢ (((Fun
𝐹 ∧ 𝑦 ∈ dom 𝐹) ∧ (𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ≠ (𝐹‘𝑦))) → (Fun 𝐹 ∧ (dom 𝐹 ∖ {𝑦}) ⊆ dom 𝐹)) |
20 | | simpl 472 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ≠ (𝐹‘𝑦)) → 𝑘 ∈ dom 𝐹) |
21 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 = 𝑦 → (𝐹‘𝑘) = (𝐹‘𝑦)) |
22 | 21 | necon3i 2814 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐹‘𝑘) ≠ (𝐹‘𝑦) → 𝑘 ≠ 𝑦) |
23 | 22 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ≠ (𝐹‘𝑦)) → 𝑘 ≠ 𝑦) |
24 | | eldifsn 4260 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ (dom 𝐹 ∖ {𝑦}) ↔ (𝑘 ∈ dom 𝐹 ∧ 𝑘 ≠ 𝑦)) |
25 | 20, 23, 24 | sylanbrc 695 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ≠ (𝐹‘𝑦)) → 𝑘 ∈ (dom 𝐹 ∖ {𝑦})) |
26 | 25 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ (((Fun
𝐹 ∧ 𝑦 ∈ dom 𝐹) ∧ (𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ≠ (𝐹‘𝑦))) → 𝑘 ∈ (dom 𝐹 ∖ {𝑦})) |
27 | | funfvima2 6397 |
. . . . . . . . . . . . . . . 16
⊢ ((Fun
𝐹 ∧ (dom 𝐹 ∖ {𝑦}) ⊆ dom 𝐹) → (𝑘 ∈ (dom 𝐹 ∖ {𝑦}) → (𝐹‘𝑘) ∈ (𝐹 “ (dom 𝐹 ∖ {𝑦})))) |
28 | 19, 26, 27 | sylc 63 |
. . . . . . . . . . . . . . 15
⊢ (((Fun
𝐹 ∧ 𝑦 ∈ dom 𝐹) ∧ (𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ≠ (𝐹‘𝑦))) → (𝐹‘𝑘) ∈ (𝐹 “ (dom 𝐹 ∖ {𝑦}))) |
29 | 28 | expr 641 |
. . . . . . . . . . . . . 14
⊢ (((Fun
𝐹 ∧ 𝑦 ∈ dom 𝐹) ∧ 𝑘 ∈ dom 𝐹) → ((𝐹‘𝑘) ≠ (𝐹‘𝑦) → (𝐹‘𝑘) ∈ (𝐹 “ (dom 𝐹 ∖ {𝑦})))) |
30 | | neeq1 2844 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹‘𝑘) = 𝑥 → ((𝐹‘𝑘) ≠ (𝐹‘𝑦) ↔ 𝑥 ≠ (𝐹‘𝑦))) |
31 | | eleq1 2676 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹‘𝑘) = 𝑥 → ((𝐹‘𝑘) ∈ (𝐹 “ (dom 𝐹 ∖ {𝑦})) ↔ 𝑥 ∈ (𝐹 “ (dom 𝐹 ∖ {𝑦})))) |
32 | 30, 31 | imbi12d 333 |
. . . . . . . . . . . . . 14
⊢ ((𝐹‘𝑘) = 𝑥 → (((𝐹‘𝑘) ≠ (𝐹‘𝑦) → (𝐹‘𝑘) ∈ (𝐹 “ (dom 𝐹 ∖ {𝑦}))) ↔ (𝑥 ≠ (𝐹‘𝑦) → 𝑥 ∈ (𝐹 “ (dom 𝐹 ∖ {𝑦}))))) |
33 | 29, 32 | syl5ibcom 234 |
. . . . . . . . . . . . 13
⊢ (((Fun
𝐹 ∧ 𝑦 ∈ dom 𝐹) ∧ 𝑘 ∈ dom 𝐹) → ((𝐹‘𝑘) = 𝑥 → (𝑥 ≠ (𝐹‘𝑦) → 𝑥 ∈ (𝐹 “ (dom 𝐹 ∖ {𝑦}))))) |
34 | 33 | rexlimdva 3013 |
. . . . . . . . . . . 12
⊢ ((Fun
𝐹 ∧ 𝑦 ∈ dom 𝐹) → (∃𝑘 ∈ dom 𝐹(𝐹‘𝑘) = 𝑥 → (𝑥 ≠ (𝐹‘𝑦) → 𝑥 ∈ (𝐹 “ (dom 𝐹 ∖ {𝑦}))))) |
35 | 16, 34 | sylbid 229 |
. . . . . . . . . . 11
⊢ ((Fun
𝐹 ∧ 𝑦 ∈ dom 𝐹) → (𝑥 ∈ ran 𝐹 → (𝑥 ≠ (𝐹‘𝑦) → 𝑥 ∈ (𝐹 “ (dom 𝐹 ∖ {𝑦}))))) |
36 | 35 | impd 446 |
. . . . . . . . . 10
⊢ ((Fun
𝐹 ∧ 𝑦 ∈ dom 𝐹) → ((𝑥 ∈ ran 𝐹 ∧ 𝑥 ≠ (𝐹‘𝑦)) → 𝑥 ∈ (𝐹 “ (dom 𝐹 ∖ {𝑦})))) |
37 | 12, 36 | syl5bi 231 |
. . . . . . . . 9
⊢ ((Fun
𝐹 ∧ 𝑦 ∈ dom 𝐹) → (𝑥 ∈ (ran 𝐹 ∖ {(𝐹‘𝑦)}) → 𝑥 ∈ (𝐹 “ (dom 𝐹 ∖ {𝑦})))) |
38 | 37 | ssrdv 3574 |
. . . . . . . 8
⊢ ((Fun
𝐹 ∧ 𝑦 ∈ dom 𝐹) → (ran 𝐹 ∖ {(𝐹‘𝑦)}) ⊆ (𝐹 “ (dom 𝐹 ∖ {𝑦}))) |
39 | 11, 38 | sylan 487 |
. . . . . . 7
⊢ (((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊) ∧ 𝑦 ∈ dom 𝐹) → (ran 𝐹 ∖ {(𝐹‘𝑦)}) ⊆ (𝐹 “ (dom 𝐹 ∖ {𝑦}))) |
40 | | eqid 2610 |
. . . . . . . 8
⊢
(LSpan‘𝑊) =
(LSpan‘𝑊) |
41 | 1, 40 | lspss 18805 |
. . . . . . 7
⊢ ((𝑊 ∈ LMod ∧ (𝐹 “ (dom 𝐹 ∖ {𝑦})) ⊆ (Base‘𝑊) ∧ (ran 𝐹 ∖ {(𝐹‘𝑦)}) ⊆ (𝐹 “ (dom 𝐹 ∖ {𝑦}))) → ((LSpan‘𝑊)‘(ran 𝐹 ∖ {(𝐹‘𝑦)})) ⊆ ((LSpan‘𝑊)‘(𝐹 “ (dom 𝐹 ∖ {𝑦})))) |
42 | 6, 9, 39, 41 | syl3anc 1318 |
. . . . . 6
⊢ (((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊) ∧ 𝑦 ∈ dom 𝐹) → ((LSpan‘𝑊)‘(ran 𝐹 ∖ {(𝐹‘𝑦)})) ⊆ ((LSpan‘𝑊)‘(𝐹 “ (dom 𝐹 ∖ {𝑦})))) |
43 | 42 | adantrr 749 |
. . . . 5
⊢ (((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊) ∧ (𝑦 ∈ dom 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}))) → ((LSpan‘𝑊)‘(ran 𝐹 ∖ {(𝐹‘𝑦)})) ⊆ ((LSpan‘𝑊)‘(𝐹 “ (dom 𝐹 ∖ {𝑦})))) |
44 | | simplr 788 |
. . . . . 6
⊢ (((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊) ∧ (𝑦 ∈ dom 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}))) → 𝐹 LIndF 𝑊) |
45 | | simprl 790 |
. . . . . 6
⊢ (((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊) ∧ (𝑦 ∈ dom 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}))) → 𝑦 ∈ dom 𝐹) |
46 | | eldifi 3694 |
. . . . . . 7
⊢ (𝑘 ∈
((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}) → 𝑘 ∈ (Base‘(Scalar‘𝑊))) |
47 | 46 | ad2antll 761 |
. . . . . 6
⊢ (((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊) ∧ (𝑦 ∈ dom 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}))) → 𝑘 ∈ (Base‘(Scalar‘𝑊))) |
48 | | eldifsni 4261 |
. . . . . . 7
⊢ (𝑘 ∈
((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}) → 𝑘 ≠
(0g‘(Scalar‘𝑊))) |
49 | 48 | ad2antll 761 |
. . . . . 6
⊢ (((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊) ∧ (𝑦 ∈ dom 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}))) → 𝑘 ≠
(0g‘(Scalar‘𝑊))) |
50 | | eqid 2610 |
. . . . . . 7
⊢ (
·𝑠 ‘𝑊) = ( ·𝑠
‘𝑊) |
51 | | eqid 2610 |
. . . . . . 7
⊢
(Scalar‘𝑊) =
(Scalar‘𝑊) |
52 | | eqid 2610 |
. . . . . . 7
⊢
(0g‘(Scalar‘𝑊)) =
(0g‘(Scalar‘𝑊)) |
53 | | eqid 2610 |
. . . . . . 7
⊢
(Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊)) |
54 | 50, 40, 51, 52, 53 | lindfind 19974 |
. . . . . 6
⊢ (((𝐹 LIndF 𝑊 ∧ 𝑦 ∈ dom 𝐹) ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑘 ≠
(0g‘(Scalar‘𝑊)))) → ¬ (𝑘( ·𝑠
‘𝑊)(𝐹‘𝑦)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (dom 𝐹 ∖ {𝑦})))) |
55 | 44, 45, 47, 49, 54 | syl22anc 1319 |
. . . . 5
⊢ (((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊) ∧ (𝑦 ∈ dom 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}))) → ¬ (𝑘( ·𝑠
‘𝑊)(𝐹‘𝑦)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (dom 𝐹 ∖ {𝑦})))) |
56 | 43, 55 | ssneldd 3571 |
. . . 4
⊢ (((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊) ∧ (𝑦 ∈ dom 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}))) → ¬ (𝑘( ·𝑠
‘𝑊)(𝐹‘𝑦)) ∈ ((LSpan‘𝑊)‘(ran 𝐹 ∖ {(𝐹‘𝑦)}))) |
57 | 56 | ralrimivva 2954 |
. . 3
⊢ ((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊) → ∀𝑦 ∈ dom 𝐹∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}) ¬ (𝑘( ·𝑠
‘𝑊)(𝐹‘𝑦)) ∈ ((LSpan‘𝑊)‘(ran 𝐹 ∖ {(𝐹‘𝑦)}))) |
58 | 11, 13 | sylib 207 |
. . . 4
⊢ ((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊) → 𝐹 Fn dom 𝐹) |
59 | | oveq2 6557 |
. . . . . . . 8
⊢ (𝑥 = (𝐹‘𝑦) → (𝑘( ·𝑠
‘𝑊)𝑥) = (𝑘( ·𝑠
‘𝑊)(𝐹‘𝑦))) |
60 | | sneq 4135 |
. . . . . . . . . 10
⊢ (𝑥 = (𝐹‘𝑦) → {𝑥} = {(𝐹‘𝑦)}) |
61 | 60 | difeq2d 3690 |
. . . . . . . . 9
⊢ (𝑥 = (𝐹‘𝑦) → (ran 𝐹 ∖ {𝑥}) = (ran 𝐹 ∖ {(𝐹‘𝑦)})) |
62 | 61 | fveq2d 6107 |
. . . . . . . 8
⊢ (𝑥 = (𝐹‘𝑦) → ((LSpan‘𝑊)‘(ran 𝐹 ∖ {𝑥})) = ((LSpan‘𝑊)‘(ran 𝐹 ∖ {(𝐹‘𝑦)}))) |
63 | 59, 62 | eleq12d 2682 |
. . . . . . 7
⊢ (𝑥 = (𝐹‘𝑦) → ((𝑘( ·𝑠
‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘(ran 𝐹 ∖ {𝑥})) ↔ (𝑘( ·𝑠
‘𝑊)(𝐹‘𝑦)) ∈ ((LSpan‘𝑊)‘(ran 𝐹 ∖ {(𝐹‘𝑦)})))) |
64 | 63 | notbid 307 |
. . . . . 6
⊢ (𝑥 = (𝐹‘𝑦) → (¬ (𝑘( ·𝑠
‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘(ran 𝐹 ∖ {𝑥})) ↔ ¬ (𝑘( ·𝑠
‘𝑊)(𝐹‘𝑦)) ∈ ((LSpan‘𝑊)‘(ran 𝐹 ∖ {(𝐹‘𝑦)})))) |
65 | 64 | ralbidv 2969 |
. . . . 5
⊢ (𝑥 = (𝐹‘𝑦) → (∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}) ¬ (𝑘( ·𝑠
‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘(ran 𝐹 ∖ {𝑥})) ↔ ∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}) ¬ (𝑘( ·𝑠
‘𝑊)(𝐹‘𝑦)) ∈ ((LSpan‘𝑊)‘(ran 𝐹 ∖ {(𝐹‘𝑦)})))) |
66 | 65 | ralrn 6270 |
. . . 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 246 |
. 2
⊢ ((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊) → ∀𝑥 ∈ ran 𝐹∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}) ¬ (𝑘( ·𝑠
‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘(ran 𝐹 ∖ {𝑥}))) |
69 | 1, 50, 40, 51, 53, 52 | islinds2 19971 |
. . 3
⊢ (𝑊 ∈ LMod → (ran 𝐹 ∈ (LIndS‘𝑊) ↔ (ran 𝐹 ⊆ (Base‘𝑊) ∧ ∀𝑥 ∈ ran 𝐹∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}) ¬ (𝑘( ·𝑠
‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘(ran 𝐹 ∖ {𝑥}))))) |
70 | 69 | adantr 480 |
. 2
⊢ ((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊) → (ran 𝐹 ∈ (LIndS‘𝑊) ↔ (ran 𝐹 ⊆ (Base‘𝑊) ∧ ∀𝑥 ∈ ran 𝐹∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖
{(0g‘(Scalar‘𝑊))}) ¬ (𝑘( ·𝑠
‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘(ran 𝐹 ∖ {𝑥}))))) |
71 | 5, 68, 70 | mpbir2and 959 |
1
⊢ ((𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊) → ran 𝐹 ∈ (LIndS‘𝑊)) |