Proof of Theorem islinds2
Step | Hyp | Ref
| Expression |
1 | | islindf.b |
. . 3
⊢ 𝐵 = (Base‘𝑊) |
2 | 1 | islinds 19967 |
. 2
⊢ (𝑊 ∈ 𝑌 → (𝐹 ∈ (LIndS‘𝑊) ↔ (𝐹 ⊆ 𝐵 ∧ ( I ↾ 𝐹) LIndF 𝑊))) |
3 | | fvex 6113 |
. . . . . . . 8
⊢
(Base‘𝑊)
∈ V |
4 | 1, 3 | eqeltri 2684 |
. . . . . . 7
⊢ 𝐵 ∈ V |
5 | 4 | ssex 4730 |
. . . . . 6
⊢ (𝐹 ⊆ 𝐵 → 𝐹 ∈ V) |
6 | 5 | adantl 481 |
. . . . 5
⊢ ((𝑊 ∈ 𝑌 ∧ 𝐹 ⊆ 𝐵) → 𝐹 ∈ V) |
7 | | resiexg 6994 |
. . . . 5
⊢ (𝐹 ∈ V → ( I ↾
𝐹) ∈
V) |
8 | 6, 7 | syl 17 |
. . . 4
⊢ ((𝑊 ∈ 𝑌 ∧ 𝐹 ⊆ 𝐵) → ( I ↾ 𝐹) ∈ V) |
9 | | islindf.v |
. . . . 5
⊢ · = (
·𝑠 ‘𝑊) |
10 | | islindf.k |
. . . . 5
⊢ 𝐾 = (LSpan‘𝑊) |
11 | | islindf.s |
. . . . 5
⊢ 𝑆 = (Scalar‘𝑊) |
12 | | islindf.n |
. . . . 5
⊢ 𝑁 = (Base‘𝑆) |
13 | | islindf.z |
. . . . 5
⊢ 0 =
(0g‘𝑆) |
14 | 1, 9, 10, 11, 12, 13 | islindf 19970 |
. . . 4
⊢ ((𝑊 ∈ 𝑌 ∧ ( I ↾ 𝐹) ∈ V) → (( I ↾ 𝐹) LIndF 𝑊 ↔ (( I ↾ 𝐹):dom ( I ↾ 𝐹)⟶𝐵 ∧ ∀𝑥 ∈ dom ( I ↾ 𝐹)∀𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · (( I ↾ 𝐹)‘𝑥)) ∈ (𝐾‘(( I ↾ 𝐹) “ (dom ( I ↾ 𝐹) ∖ {𝑥})))))) |
15 | 8, 14 | syldan 486 |
. . 3
⊢ ((𝑊 ∈ 𝑌 ∧ 𝐹 ⊆ 𝐵) → (( I ↾ 𝐹) LIndF 𝑊 ↔ (( I ↾ 𝐹):dom ( I ↾ 𝐹)⟶𝐵 ∧ ∀𝑥 ∈ dom ( I ↾ 𝐹)∀𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · (( I ↾ 𝐹)‘𝑥)) ∈ (𝐾‘(( I ↾ 𝐹) “ (dom ( I ↾ 𝐹) ∖ {𝑥})))))) |
16 | 15 | pm5.32da 671 |
. 2
⊢ (𝑊 ∈ 𝑌 → ((𝐹 ⊆ 𝐵 ∧ ( I ↾ 𝐹) LIndF 𝑊) ↔ (𝐹 ⊆ 𝐵 ∧ (( I ↾ 𝐹):dom ( I ↾ 𝐹)⟶𝐵 ∧ ∀𝑥 ∈ dom ( I ↾ 𝐹)∀𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · (( I ↾ 𝐹)‘𝑥)) ∈ (𝐾‘(( I ↾ 𝐹) “ (dom ( I ↾ 𝐹) ∖ {𝑥}))))))) |
17 | | f1oi 6086 |
. . . . . . . . 9
⊢ ( I
↾ 𝐹):𝐹–1-1-onto→𝐹 |
18 | | f1of 6050 |
. . . . . . . . 9
⊢ (( I
↾ 𝐹):𝐹–1-1-onto→𝐹 → ( I ↾ 𝐹):𝐹⟶𝐹) |
19 | 17, 18 | ax-mp 5 |
. . . . . . . 8
⊢ ( I
↾ 𝐹):𝐹⟶𝐹 |
20 | | dmresi 5376 |
. . . . . . . . 9
⊢ dom ( I
↾ 𝐹) = 𝐹 |
21 | 20 | feq2i 5950 |
. . . . . . . 8
⊢ (( I
↾ 𝐹):dom ( I ↾
𝐹)⟶𝐹 ↔ ( I ↾ 𝐹):𝐹⟶𝐹) |
22 | 19, 21 | mpbir 220 |
. . . . . . 7
⊢ ( I
↾ 𝐹):dom ( I ↾
𝐹)⟶𝐹 |
23 | | fss 5969 |
. . . . . . 7
⊢ ((( I
↾ 𝐹):dom ( I ↾
𝐹)⟶𝐹 ∧ 𝐹 ⊆ 𝐵) → ( I ↾ 𝐹):dom ( I ↾ 𝐹)⟶𝐵) |
24 | 22, 23 | mpan 702 |
. . . . . 6
⊢ (𝐹 ⊆ 𝐵 → ( I ↾ 𝐹):dom ( I ↾ 𝐹)⟶𝐵) |
25 | 24 | biantrurd 528 |
. . . . 5
⊢ (𝐹 ⊆ 𝐵 → (∀𝑥 ∈ 𝐹 ∀𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · 𝑥) ∈ (𝐾‘(𝐹 ∖ {𝑥})) ↔ (( I ↾ 𝐹):dom ( I ↾ 𝐹)⟶𝐵 ∧ ∀𝑥 ∈ 𝐹 ∀𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · 𝑥) ∈ (𝐾‘(𝐹 ∖ {𝑥}))))) |
26 | 20 | raleqi 3119 |
. . . . . . 7
⊢
(∀𝑥 ∈
dom ( I ↾ 𝐹)∀𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · (( I ↾ 𝐹)‘𝑥)) ∈ (𝐾‘(( I ↾ 𝐹) “ (dom ( I ↾ 𝐹) ∖ {𝑥}))) ↔ ∀𝑥 ∈ 𝐹 ∀𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · (( I ↾ 𝐹)‘𝑥)) ∈ (𝐾‘(( I ↾ 𝐹) “ (dom ( I ↾ 𝐹) ∖ {𝑥})))) |
27 | | fvresi 6344 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝐹 → (( I ↾ 𝐹)‘𝑥) = 𝑥) |
28 | 27 | oveq2d 6565 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝐹 → (𝑘 · (( I ↾ 𝐹)‘𝑥)) = (𝑘 · 𝑥)) |
29 | 20 | difeq1i 3686 |
. . . . . . . . . . . . . . 15
⊢ (dom ( I
↾ 𝐹) ∖ {𝑥}) = (𝐹 ∖ {𝑥}) |
30 | 29 | imaeq2i 5383 |
. . . . . . . . . . . . . 14
⊢ (( I
↾ 𝐹) “ (dom ( I
↾ 𝐹) ∖ {𝑥})) = (( I ↾ 𝐹) “ (𝐹 ∖ {𝑥})) |
31 | | difss 3699 |
. . . . . . . . . . . . . . 15
⊢ (𝐹 ∖ {𝑥}) ⊆ 𝐹 |
32 | | resiima 5399 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹 ∖ {𝑥}) ⊆ 𝐹 → (( I ↾ 𝐹) “ (𝐹 ∖ {𝑥})) = (𝐹 ∖ {𝑥})) |
33 | 31, 32 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ (( I
↾ 𝐹) “ (𝐹 ∖ {𝑥})) = (𝐹 ∖ {𝑥}) |
34 | 30, 33 | eqtri 2632 |
. . . . . . . . . . . . 13
⊢ (( I
↾ 𝐹) “ (dom ( I
↾ 𝐹) ∖ {𝑥})) = (𝐹 ∖ {𝑥}) |
35 | 34 | fveq2i 6106 |
. . . . . . . . . . . 12
⊢ (𝐾‘(( I ↾ 𝐹) “ (dom ( I ↾ 𝐹) ∖ {𝑥}))) = (𝐾‘(𝐹 ∖ {𝑥})) |
36 | 35 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝐹 → (𝐾‘(( I ↾ 𝐹) “ (dom ( I ↾ 𝐹) ∖ {𝑥}))) = (𝐾‘(𝐹 ∖ {𝑥}))) |
37 | 28, 36 | eleq12d 2682 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐹 → ((𝑘 · (( I ↾ 𝐹)‘𝑥)) ∈ (𝐾‘(( I ↾ 𝐹) “ (dom ( I ↾ 𝐹) ∖ {𝑥}))) ↔ (𝑘 · 𝑥) ∈ (𝐾‘(𝐹 ∖ {𝑥})))) |
38 | 37 | notbid 307 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐹 → (¬ (𝑘 · (( I ↾ 𝐹)‘𝑥)) ∈ (𝐾‘(( I ↾ 𝐹) “ (dom ( I ↾ 𝐹) ∖ {𝑥}))) ↔ ¬ (𝑘 · 𝑥) ∈ (𝐾‘(𝐹 ∖ {𝑥})))) |
39 | 38 | ralbidv 2969 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐹 → (∀𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · (( I ↾ 𝐹)‘𝑥)) ∈ (𝐾‘(( I ↾ 𝐹) “ (dom ( I ↾ 𝐹) ∖ {𝑥}))) ↔ ∀𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · 𝑥) ∈ (𝐾‘(𝐹 ∖ {𝑥})))) |
40 | 39 | ralbiia 2962 |
. . . . . . 7
⊢
(∀𝑥 ∈
𝐹 ∀𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · (( I ↾ 𝐹)‘𝑥)) ∈ (𝐾‘(( I ↾ 𝐹) “ (dom ( I ↾ 𝐹) ∖ {𝑥}))) ↔ ∀𝑥 ∈ 𝐹 ∀𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · 𝑥) ∈ (𝐾‘(𝐹 ∖ {𝑥}))) |
41 | 26, 40 | bitri 263 |
. . . . . 6
⊢
(∀𝑥 ∈
dom ( I ↾ 𝐹)∀𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · (( I ↾ 𝐹)‘𝑥)) ∈ (𝐾‘(( I ↾ 𝐹) “ (dom ( I ↾ 𝐹) ∖ {𝑥}))) ↔ ∀𝑥 ∈ 𝐹 ∀𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · 𝑥) ∈ (𝐾‘(𝐹 ∖ {𝑥}))) |
42 | 41 | anbi2i 726 |
. . . . 5
⊢ ((( I
↾ 𝐹):dom ( I ↾
𝐹)⟶𝐵 ∧ ∀𝑥 ∈ dom ( I ↾ 𝐹)∀𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · (( I ↾ 𝐹)‘𝑥)) ∈ (𝐾‘(( I ↾ 𝐹) “ (dom ( I ↾ 𝐹) ∖ {𝑥})))) ↔ (( I ↾ 𝐹):dom ( I ↾ 𝐹)⟶𝐵 ∧ ∀𝑥 ∈ 𝐹 ∀𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · 𝑥) ∈ (𝐾‘(𝐹 ∖ {𝑥})))) |
43 | 25, 42 | syl6rbbr 278 |
. . . 4
⊢ (𝐹 ⊆ 𝐵 → ((( I ↾ 𝐹):dom ( I ↾ 𝐹)⟶𝐵 ∧ ∀𝑥 ∈ dom ( I ↾ 𝐹)∀𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · (( I ↾ 𝐹)‘𝑥)) ∈ (𝐾‘(( I ↾ 𝐹) “ (dom ( I ↾ 𝐹) ∖ {𝑥})))) ↔ ∀𝑥 ∈ 𝐹 ∀𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · 𝑥) ∈ (𝐾‘(𝐹 ∖ {𝑥})))) |
44 | 43 | pm5.32i 667 |
. . 3
⊢ ((𝐹 ⊆ 𝐵 ∧ (( I ↾ 𝐹):dom ( I ↾ 𝐹)⟶𝐵 ∧ ∀𝑥 ∈ dom ( I ↾ 𝐹)∀𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · (( I ↾ 𝐹)‘𝑥)) ∈ (𝐾‘(( I ↾ 𝐹) “ (dom ( I ↾ 𝐹) ∖ {𝑥}))))) ↔ (𝐹 ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐹 ∀𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · 𝑥) ∈ (𝐾‘(𝐹 ∖ {𝑥})))) |
45 | 44 | a1i 11 |
. 2
⊢ (𝑊 ∈ 𝑌 → ((𝐹 ⊆ 𝐵 ∧ (( I ↾ 𝐹):dom ( I ↾ 𝐹)⟶𝐵 ∧ ∀𝑥 ∈ dom ( I ↾ 𝐹)∀𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · (( I ↾ 𝐹)‘𝑥)) ∈ (𝐾‘(( I ↾ 𝐹) “ (dom ( I ↾ 𝐹) ∖ {𝑥}))))) ↔ (𝐹 ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐹 ∀𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · 𝑥) ∈ (𝐾‘(𝐹 ∖ {𝑥}))))) |
46 | 2, 16, 45 | 3bitrd 293 |
1
⊢ (𝑊 ∈ 𝑌 → (𝐹 ∈ (LIndS‘𝑊) ↔ (𝐹 ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐹 ∀𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · 𝑥) ∈ (𝐾‘(𝐹 ∖ {𝑥}))))) |