Proof of Theorem islinds2
| Step | Hyp | Ref
| Expression |
| 1 | | islindf.b |
. . 3
⊢ 𝐵 = (Base‘𝑊) |
| 2 | 1 | islinds 21829 |
. 2
⊢ (𝑊 ∈ 𝑌 → (𝐹 ∈ (LIndS‘𝑊) ↔ (𝐹 ⊆ 𝐵 ∧ ( I ↾ 𝐹) LIndF 𝑊))) |
| 3 | 1 | fvexi 6920 |
. . . . . . 7
⊢ 𝐵 ∈ V |
| 4 | 3 | ssex 5321 |
. . . . . 6
⊢ (𝐹 ⊆ 𝐵 → 𝐹 ∈ V) |
| 5 | 4 | adantl 481 |
. . . . 5
⊢ ((𝑊 ∈ 𝑌 ∧ 𝐹 ⊆ 𝐵) → 𝐹 ∈ V) |
| 6 | | resiexg 7934 |
. . . . 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 21832 |
. . . 4
⊢ ((𝑊 ∈ 𝑌 ∧ ( I ↾ 𝐹) ∈ V) → (( I ↾ 𝐹) LIndF 𝑊 ↔ (( I ↾ 𝐹):dom ( I ↾ 𝐹)⟶𝐵 ∧ ∀𝑥 ∈ dom ( I ↾ 𝐹)∀𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · (( I ↾ 𝐹)‘𝑥)) ∈ (𝐾‘(( I ↾ 𝐹) “ (dom ( I ↾ 𝐹) ∖ {𝑥})))))) |
| 14 | 7, 13 | syldan 591 |
. . 3
⊢ ((𝑊 ∈ 𝑌 ∧ 𝐹 ⊆ 𝐵) → (( I ↾ 𝐹) LIndF 𝑊 ↔ (( I ↾ 𝐹):dom ( I ↾ 𝐹)⟶𝐵 ∧ ∀𝑥 ∈ dom ( I ↾ 𝐹)∀𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · (( I ↾ 𝐹)‘𝑥)) ∈ (𝐾‘(( I ↾ 𝐹) “ (dom ( I ↾ 𝐹) ∖ {𝑥})))))) |
| 15 | 14 | pm5.32da 579 |
. 2
⊢ (𝑊 ∈ 𝑌 → ((𝐹 ⊆ 𝐵 ∧ ( I ↾ 𝐹) LIndF 𝑊) ↔ (𝐹 ⊆ 𝐵 ∧ (( I ↾ 𝐹):dom ( I ↾ 𝐹)⟶𝐵 ∧ ∀𝑥 ∈ dom ( I ↾ 𝐹)∀𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · (( I ↾ 𝐹)‘𝑥)) ∈ (𝐾‘(( I ↾ 𝐹) “ (dom ( I ↾ 𝐹) ∖ {𝑥}))))))) |
| 16 | | dmresi 6070 |
. . . . . . . 8
⊢ dom ( I
↾ 𝐹) = 𝐹 |
| 17 | 16 | raleqi 3324 |
. . . . . . 7
⊢
(∀𝑥 ∈
dom ( I ↾ 𝐹)∀𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · (( I ↾ 𝐹)‘𝑥)) ∈ (𝐾‘(( I ↾ 𝐹) “ (dom ( I ↾ 𝐹) ∖ {𝑥}))) ↔ ∀𝑥 ∈ 𝐹 ∀𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · (( I ↾ 𝐹)‘𝑥)) ∈ (𝐾‘(( I ↾ 𝐹) “ (dom ( I ↾ 𝐹) ∖ {𝑥})))) |
| 18 | | fvresi 7193 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝐹 → (( I ↾ 𝐹)‘𝑥) = 𝑥) |
| 19 | 18 | oveq2d 7447 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝐹 → (𝑘 · (( I ↾ 𝐹)‘𝑥)) = (𝑘 · 𝑥)) |
| 20 | 16 | difeq1i 4122 |
. . . . . . . . . . . . . . 15
⊢ (dom ( I
↾ 𝐹) ∖ {𝑥}) = (𝐹 ∖ {𝑥}) |
| 21 | 20 | imaeq2i 6076 |
. . . . . . . . . . . . . 14
⊢ (( I
↾ 𝐹) “ (dom ( I
↾ 𝐹) ∖ {𝑥})) = (( I ↾ 𝐹) “ (𝐹 ∖ {𝑥})) |
| 22 | | difss 4136 |
. . . . . . . . . . . . . . 15
⊢ (𝐹 ∖ {𝑥}) ⊆ 𝐹 |
| 23 | | resiima 6094 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹 ∖ {𝑥}) ⊆ 𝐹 → (( I ↾ 𝐹) “ (𝐹 ∖ {𝑥})) = (𝐹 ∖ {𝑥})) |
| 24 | 22, 23 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ (( I
↾ 𝐹) “ (𝐹 ∖ {𝑥})) = (𝐹 ∖ {𝑥}) |
| 25 | 21, 24 | eqtri 2765 |
. . . . . . . . . . . . 13
⊢ (( I
↾ 𝐹) “ (dom ( I
↾ 𝐹) ∖ {𝑥})) = (𝐹 ∖ {𝑥}) |
| 26 | 25 | fveq2i 6909 |
. . . . . . . . . . . 12
⊢ (𝐾‘(( I ↾ 𝐹) “ (dom ( I ↾ 𝐹) ∖ {𝑥}))) = (𝐾‘(𝐹 ∖ {𝑥})) |
| 27 | 26 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝐹 → (𝐾‘(( I ↾ 𝐹) “ (dom ( I ↾ 𝐹) ∖ {𝑥}))) = (𝐾‘(𝐹 ∖ {𝑥}))) |
| 28 | 19, 27 | eleq12d 2835 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐹 → ((𝑘 · (( I ↾ 𝐹)‘𝑥)) ∈ (𝐾‘(( I ↾ 𝐹) “ (dom ( I ↾ 𝐹) ∖ {𝑥}))) ↔ (𝑘 · 𝑥) ∈ (𝐾‘(𝐹 ∖ {𝑥})))) |
| 29 | 28 | notbid 318 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐹 → (¬ (𝑘 · (( I ↾ 𝐹)‘𝑥)) ∈ (𝐾‘(( I ↾ 𝐹) “ (dom ( I ↾ 𝐹) ∖ {𝑥}))) ↔ ¬ (𝑘 · 𝑥) ∈ (𝐾‘(𝐹 ∖ {𝑥})))) |
| 30 | 29 | ralbidv 3178 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐹 → (∀𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · (( I ↾ 𝐹)‘𝑥)) ∈ (𝐾‘(( I ↾ 𝐹) “ (dom ( I ↾ 𝐹) ∖ {𝑥}))) ↔ ∀𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · 𝑥) ∈ (𝐾‘(𝐹 ∖ {𝑥})))) |
| 31 | 30 | ralbiia 3091 |
. . . . . . 7
⊢
(∀𝑥 ∈
𝐹 ∀𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · (( I ↾ 𝐹)‘𝑥)) ∈ (𝐾‘(( I ↾ 𝐹) “ (dom ( I ↾ 𝐹) ∖ {𝑥}))) ↔ ∀𝑥 ∈ 𝐹 ∀𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · 𝑥) ∈ (𝐾‘(𝐹 ∖ {𝑥}))) |
| 32 | 17, 31 | bitri 275 |
. . . . . 6
⊢
(∀𝑥 ∈
dom ( I ↾ 𝐹)∀𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · (( I ↾ 𝐹)‘𝑥)) ∈ (𝐾‘(( I ↾ 𝐹) “ (dom ( I ↾ 𝐹) ∖ {𝑥}))) ↔ ∀𝑥 ∈ 𝐹 ∀𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · 𝑥) ∈ (𝐾‘(𝐹 ∖ {𝑥}))) |
| 33 | 32 | anbi2i 623 |
. . . . 5
⊢ ((( I
↾ 𝐹):dom ( I ↾
𝐹)⟶𝐵 ∧ ∀𝑥 ∈ dom ( I ↾ 𝐹)∀𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · (( I ↾ 𝐹)‘𝑥)) ∈ (𝐾‘(( I ↾ 𝐹) “ (dom ( I ↾ 𝐹) ∖ {𝑥})))) ↔ (( I ↾ 𝐹):dom ( I ↾ 𝐹)⟶𝐵 ∧ ∀𝑥 ∈ 𝐹 ∀𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · 𝑥) ∈ (𝐾‘(𝐹 ∖ {𝑥})))) |
| 34 | | f1oi 6886 |
. . . . . . . . 9
⊢ ( I
↾ 𝐹):𝐹–1-1-onto→𝐹 |
| 35 | | f1of 6848 |
. . . . . . . . 9
⊢ (( I
↾ 𝐹):𝐹–1-1-onto→𝐹 → ( I ↾ 𝐹):𝐹⟶𝐹) |
| 36 | 34, 35 | ax-mp 5 |
. . . . . . . 8
⊢ ( I
↾ 𝐹):𝐹⟶𝐹 |
| 37 | 16 | feq2i 6728 |
. . . . . . . 8
⊢ (( I
↾ 𝐹):dom ( I ↾
𝐹)⟶𝐹 ↔ ( I ↾ 𝐹):𝐹⟶𝐹) |
| 38 | 36, 37 | mpbir 231 |
. . . . . . 7
⊢ ( I
↾ 𝐹):dom ( I ↾
𝐹)⟶𝐹 |
| 39 | | fss 6752 |
. . . . . . 7
⊢ ((( I
↾ 𝐹):dom ( I ↾
𝐹)⟶𝐹 ∧ 𝐹 ⊆ 𝐵) → ( I ↾ 𝐹):dom ( I ↾ 𝐹)⟶𝐵) |
| 40 | 38, 39 | mpan 690 |
. . . . . 6
⊢ (𝐹 ⊆ 𝐵 → ( I ↾ 𝐹):dom ( I ↾ 𝐹)⟶𝐵) |
| 41 | 40 | biantrurd 532 |
. . . . 5
⊢ (𝐹 ⊆ 𝐵 → (∀𝑥 ∈ 𝐹 ∀𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · 𝑥) ∈ (𝐾‘(𝐹 ∖ {𝑥})) ↔ (( I ↾ 𝐹):dom ( I ↾ 𝐹)⟶𝐵 ∧ ∀𝑥 ∈ 𝐹 ∀𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · 𝑥) ∈ (𝐾‘(𝐹 ∖ {𝑥}))))) |
| 42 | 33, 41 | bitr4id 290 |
. . . 4
⊢ (𝐹 ⊆ 𝐵 → ((( I ↾ 𝐹):dom ( I ↾ 𝐹)⟶𝐵 ∧ ∀𝑥 ∈ dom ( I ↾ 𝐹)∀𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · (( I ↾ 𝐹)‘𝑥)) ∈ (𝐾‘(( I ↾ 𝐹) “ (dom ( I ↾ 𝐹) ∖ {𝑥})))) ↔ ∀𝑥 ∈ 𝐹 ∀𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · 𝑥) ∈ (𝐾‘(𝐹 ∖ {𝑥})))) |
| 43 | 42 | pm5.32i 574 |
. . 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 305 |
1
⊢ (𝑊 ∈ 𝑌 → (𝐹 ∈ (LIndS‘𝑊) ↔ (𝐹 ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐹 ∀𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · 𝑥) ∈ (𝐾‘(𝐹 ∖ {𝑥}))))) |