Proof of Theorem islinds2
Step | Hyp | Ref
| Expression |
1 | | islindf.b |
. . 3
⊢ 𝐵 = (Base‘𝑊) |
2 | 1 | islinds 20655 |
. 2
⊢ (𝑊 ∈ 𝑌 → (𝐹 ∈ (LIndS‘𝑊) ↔ (𝐹 ⊆ 𝐵 ∧ ( I ↾ 𝐹) LIndF 𝑊))) |
3 | 1 | fvexi 6513 |
. . . . . . 7
⊢ 𝐵 ∈ V |
4 | 3 | ssex 5081 |
. . . . . 6
⊢ (𝐹 ⊆ 𝐵 → 𝐹 ∈ V) |
5 | 4 | adantl 474 |
. . . . 5
⊢ ((𝑊 ∈ 𝑌 ∧ 𝐹 ⊆ 𝐵) → 𝐹 ∈ V) |
6 | | resiexg 7434 |
. . . . 5
⊢ (𝐹 ∈ V → ( I ↾
𝐹) ∈
V) |
7 | 5, 6 | syl 17 |
. . . 4
⊢ ((𝑊 ∈ 𝑌 ∧ 𝐹 ⊆ 𝐵) → ( I ↾ 𝐹) ∈ V) |
8 | | islindf.v |
. . . . 5
⊢ · = (
·𝑠 ‘𝑊) |
9 | | islindf.k |
. . . . 5
⊢ 𝐾 = (LSpan‘𝑊) |
10 | | islindf.s |
. . . . 5
⊢ 𝑆 = (Scalar‘𝑊) |
11 | | islindf.n |
. . . . 5
⊢ 𝑁 = (Base‘𝑆) |
12 | | islindf.z |
. . . . 5
⊢ 0 =
(0g‘𝑆) |
13 | 1, 8, 9, 10, 11, 12 | islindf 20658 |
. . . 4
⊢ ((𝑊 ∈ 𝑌 ∧ ( I ↾ 𝐹) ∈ V) → (( I ↾ 𝐹) LIndF 𝑊 ↔ (( I ↾ 𝐹):dom ( I ↾ 𝐹)⟶𝐵 ∧ ∀𝑥 ∈ dom ( I ↾ 𝐹)∀𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · (( I ↾ 𝐹)‘𝑥)) ∈ (𝐾‘(( I ↾ 𝐹) “ (dom ( I ↾ 𝐹) ∖ {𝑥})))))) |
14 | 7, 13 | syldan 582 |
. . 3
⊢ ((𝑊 ∈ 𝑌 ∧ 𝐹 ⊆ 𝐵) → (( I ↾ 𝐹) LIndF 𝑊 ↔ (( I ↾ 𝐹):dom ( I ↾ 𝐹)⟶𝐵 ∧ ∀𝑥 ∈ dom ( I ↾ 𝐹)∀𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · (( I ↾ 𝐹)‘𝑥)) ∈ (𝐾‘(( I ↾ 𝐹) “ (dom ( I ↾ 𝐹) ∖ {𝑥})))))) |
15 | 14 | pm5.32da 571 |
. 2
⊢ (𝑊 ∈ 𝑌 → ((𝐹 ⊆ 𝐵 ∧ ( I ↾ 𝐹) LIndF 𝑊) ↔ (𝐹 ⊆ 𝐵 ∧ (( I ↾ 𝐹):dom ( I ↾ 𝐹)⟶𝐵 ∧ ∀𝑥 ∈ dom ( I ↾ 𝐹)∀𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · (( I ↾ 𝐹)‘𝑥)) ∈ (𝐾‘(( I ↾ 𝐹) “ (dom ( I ↾ 𝐹) ∖ {𝑥}))))))) |
16 | | f1oi 6481 |
. . . . . . . . 9
⊢ ( I
↾ 𝐹):𝐹–1-1-onto→𝐹 |
17 | | f1of 6444 |
. . . . . . . . 9
⊢ (( I
↾ 𝐹):𝐹–1-1-onto→𝐹 → ( I ↾ 𝐹):𝐹⟶𝐹) |
18 | 16, 17 | ax-mp 5 |
. . . . . . . 8
⊢ ( I
↾ 𝐹):𝐹⟶𝐹 |
19 | | dmresi 5763 |
. . . . . . . . 9
⊢ dom ( I
↾ 𝐹) = 𝐹 |
20 | 19 | feq2i 6336 |
. . . . . . . 8
⊢ (( I
↾ 𝐹):dom ( I ↾
𝐹)⟶𝐹 ↔ ( I ↾ 𝐹):𝐹⟶𝐹) |
21 | 18, 20 | mpbir 223 |
. . . . . . 7
⊢ ( I
↾ 𝐹):dom ( I ↾
𝐹)⟶𝐹 |
22 | | fss 6357 |
. . . . . . 7
⊢ ((( I
↾ 𝐹):dom ( I ↾
𝐹)⟶𝐹 ∧ 𝐹 ⊆ 𝐵) → ( I ↾ 𝐹):dom ( I ↾ 𝐹)⟶𝐵) |
23 | 21, 22 | mpan 677 |
. . . . . 6
⊢ (𝐹 ⊆ 𝐵 → ( I ↾ 𝐹):dom ( I ↾ 𝐹)⟶𝐵) |
24 | 23 | biantrurd 525 |
. . . . 5
⊢ (𝐹 ⊆ 𝐵 → (∀𝑥 ∈ 𝐹 ∀𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · 𝑥) ∈ (𝐾‘(𝐹 ∖ {𝑥})) ↔ (( I ↾ 𝐹):dom ( I ↾ 𝐹)⟶𝐵 ∧ ∀𝑥 ∈ 𝐹 ∀𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · 𝑥) ∈ (𝐾‘(𝐹 ∖ {𝑥}))))) |
25 | 19 | raleqi 3353 |
. . . . . . 7
⊢
(∀𝑥 ∈
dom ( I ↾ 𝐹)∀𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · (( I ↾ 𝐹)‘𝑥)) ∈ (𝐾‘(( I ↾ 𝐹) “ (dom ( I ↾ 𝐹) ∖ {𝑥}))) ↔ ∀𝑥 ∈ 𝐹 ∀𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · (( I ↾ 𝐹)‘𝑥)) ∈ (𝐾‘(( I ↾ 𝐹) “ (dom ( I ↾ 𝐹) ∖ {𝑥})))) |
26 | | fvresi 6758 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝐹 → (( I ↾ 𝐹)‘𝑥) = 𝑥) |
27 | 26 | oveq2d 6992 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝐹 → (𝑘 · (( I ↾ 𝐹)‘𝑥)) = (𝑘 · 𝑥)) |
28 | 19 | difeq1i 3985 |
. . . . . . . . . . . . . . 15
⊢ (dom ( I
↾ 𝐹) ∖ {𝑥}) = (𝐹 ∖ {𝑥}) |
29 | 28 | imaeq2i 5768 |
. . . . . . . . . . . . . 14
⊢ (( I
↾ 𝐹) “ (dom ( I
↾ 𝐹) ∖ {𝑥})) = (( I ↾ 𝐹) “ (𝐹 ∖ {𝑥})) |
30 | | difss 3998 |
. . . . . . . . . . . . . . 15
⊢ (𝐹 ∖ {𝑥}) ⊆ 𝐹 |
31 | | resiima 5784 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹 ∖ {𝑥}) ⊆ 𝐹 → (( I ↾ 𝐹) “ (𝐹 ∖ {𝑥})) = (𝐹 ∖ {𝑥})) |
32 | 30, 31 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ (( I
↾ 𝐹) “ (𝐹 ∖ {𝑥})) = (𝐹 ∖ {𝑥}) |
33 | 29, 32 | eqtri 2802 |
. . . . . . . . . . . . 13
⊢ (( I
↾ 𝐹) “ (dom ( I
↾ 𝐹) ∖ {𝑥})) = (𝐹 ∖ {𝑥}) |
34 | 33 | fveq2i 6502 |
. . . . . . . . . . . 12
⊢ (𝐾‘(( I ↾ 𝐹) “ (dom ( I ↾ 𝐹) ∖ {𝑥}))) = (𝐾‘(𝐹 ∖ {𝑥})) |
35 | 34 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝐹 → (𝐾‘(( I ↾ 𝐹) “ (dom ( I ↾ 𝐹) ∖ {𝑥}))) = (𝐾‘(𝐹 ∖ {𝑥}))) |
36 | 27, 35 | eleq12d 2860 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐹 → ((𝑘 · (( I ↾ 𝐹)‘𝑥)) ∈ (𝐾‘(( I ↾ 𝐹) “ (dom ( I ↾ 𝐹) ∖ {𝑥}))) ↔ (𝑘 · 𝑥) ∈ (𝐾‘(𝐹 ∖ {𝑥})))) |
37 | 36 | notbid 310 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐹 → (¬ (𝑘 · (( I ↾ 𝐹)‘𝑥)) ∈ (𝐾‘(( I ↾ 𝐹) “ (dom ( I ↾ 𝐹) ∖ {𝑥}))) ↔ ¬ (𝑘 · 𝑥) ∈ (𝐾‘(𝐹 ∖ {𝑥})))) |
38 | 37 | ralbidv 3147 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐹 → (∀𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · (( I ↾ 𝐹)‘𝑥)) ∈ (𝐾‘(( I ↾ 𝐹) “ (dom ( I ↾ 𝐹) ∖ {𝑥}))) ↔ ∀𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · 𝑥) ∈ (𝐾‘(𝐹 ∖ {𝑥})))) |
39 | 38 | ralbiia 3114 |
. . . . . . 7
⊢
(∀𝑥 ∈
𝐹 ∀𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · (( I ↾ 𝐹)‘𝑥)) ∈ (𝐾‘(( I ↾ 𝐹) “ (dom ( I ↾ 𝐹) ∖ {𝑥}))) ↔ ∀𝑥 ∈ 𝐹 ∀𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · 𝑥) ∈ (𝐾‘(𝐹 ∖ {𝑥}))) |
40 | 25, 39 | bitri 267 |
. . . . . 6
⊢
(∀𝑥 ∈
dom ( I ↾ 𝐹)∀𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · (( I ↾ 𝐹)‘𝑥)) ∈ (𝐾‘(( I ↾ 𝐹) “ (dom ( I ↾ 𝐹) ∖ {𝑥}))) ↔ ∀𝑥 ∈ 𝐹 ∀𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · 𝑥) ∈ (𝐾‘(𝐹 ∖ {𝑥}))) |
41 | 40 | anbi2i 613 |
. . . . 5
⊢ ((( I
↾ 𝐹):dom ( I ↾
𝐹)⟶𝐵 ∧ ∀𝑥 ∈ dom ( I ↾ 𝐹)∀𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · (( I ↾ 𝐹)‘𝑥)) ∈ (𝐾‘(( I ↾ 𝐹) “ (dom ( I ↾ 𝐹) ∖ {𝑥})))) ↔ (( I ↾ 𝐹):dom ( I ↾ 𝐹)⟶𝐵 ∧ ∀𝑥 ∈ 𝐹 ∀𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · 𝑥) ∈ (𝐾‘(𝐹 ∖ {𝑥})))) |
42 | 24, 41 | syl6rbbr 282 |
. . . 4
⊢ (𝐹 ⊆ 𝐵 → ((( I ↾ 𝐹):dom ( I ↾ 𝐹)⟶𝐵 ∧ ∀𝑥 ∈ dom ( I ↾ 𝐹)∀𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · (( I ↾ 𝐹)‘𝑥)) ∈ (𝐾‘(( I ↾ 𝐹) “ (dom ( I ↾ 𝐹) ∖ {𝑥})))) ↔ ∀𝑥 ∈ 𝐹 ∀𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · 𝑥) ∈ (𝐾‘(𝐹 ∖ {𝑥})))) |
43 | 42 | pm5.32i 567 |
. . 3
⊢ ((𝐹 ⊆ 𝐵 ∧ (( I ↾ 𝐹):dom ( I ↾ 𝐹)⟶𝐵 ∧ ∀𝑥 ∈ dom ( I ↾ 𝐹)∀𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · (( I ↾ 𝐹)‘𝑥)) ∈ (𝐾‘(( I ↾ 𝐹) “ (dom ( I ↾ 𝐹) ∖ {𝑥}))))) ↔ (𝐹 ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐹 ∀𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · 𝑥) ∈ (𝐾‘(𝐹 ∖ {𝑥})))) |
44 | 43 | a1i 11 |
. 2
⊢ (𝑊 ∈ 𝑌 → ((𝐹 ⊆ 𝐵 ∧ (( I ↾ 𝐹):dom ( I ↾ 𝐹)⟶𝐵 ∧ ∀𝑥 ∈ dom ( I ↾ 𝐹)∀𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · (( I ↾ 𝐹)‘𝑥)) ∈ (𝐾‘(( I ↾ 𝐹) “ (dom ( I ↾ 𝐹) ∖ {𝑥}))))) ↔ (𝐹 ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐹 ∀𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · 𝑥) ∈ (𝐾‘(𝐹 ∖ {𝑥}))))) |
45 | 2, 15, 44 | 3bitrd 297 |
1
⊢ (𝑊 ∈ 𝑌 → (𝐹 ∈ (LIndS‘𝑊) ↔ (𝐹 ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐹 ∀𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · 𝑥) ∈ (𝐾‘(𝐹 ∖ {𝑥}))))) |