| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | simplr 769 | . 2
⊢ (((𝐹 LIndF 𝑊 ∧ 𝐸 ∈ dom 𝐹) ∧ (𝐴 ∈ 𝐾 ∧ 𝐴 ≠ 0 )) → 𝐸 ∈ dom 𝐹) | 
| 2 |  | eldifsn 4786 | . . . 4
⊢ (𝐴 ∈ (𝐾 ∖ { 0 }) ↔ (𝐴 ∈ 𝐾 ∧ 𝐴 ≠ 0 )) | 
| 3 | 2 | biimpri 228 | . . 3
⊢ ((𝐴 ∈ 𝐾 ∧ 𝐴 ≠ 0 ) → 𝐴 ∈ (𝐾 ∖ { 0 })) | 
| 4 | 3 | adantl 481 | . 2
⊢ (((𝐹 LIndF 𝑊 ∧ 𝐸 ∈ dom 𝐹) ∧ (𝐴 ∈ 𝐾 ∧ 𝐴 ≠ 0 )) → 𝐴 ∈ (𝐾 ∖ { 0 })) | 
| 5 |  | simpll 767 | . . . 4
⊢ (((𝐹 LIndF 𝑊 ∧ 𝐸 ∈ dom 𝐹) ∧ (𝐴 ∈ 𝐾 ∧ 𝐴 ≠ 0 )) → 𝐹 LIndF 𝑊) | 
| 6 |  | lindfind.l | . . . . . . 7
⊢ 𝐿 = (Scalar‘𝑊) | 
| 7 |  | lindfind.k | . . . . . . 7
⊢ 𝐾 = (Base‘𝐿) | 
| 8 | 6, 7 | elbasfv 17253 | . . . . . 6
⊢ (𝐴 ∈ 𝐾 → 𝑊 ∈ V) | 
| 9 | 8 | ad2antrl 728 | . . . . 5
⊢ (((𝐹 LIndF 𝑊 ∧ 𝐸 ∈ dom 𝐹) ∧ (𝐴 ∈ 𝐾 ∧ 𝐴 ≠ 0 )) → 𝑊 ∈ V) | 
| 10 |  | rellindf 21828 | . . . . . . 7
⊢ Rel
LIndF | 
| 11 | 10 | brrelex1i 5741 | . . . . . 6
⊢ (𝐹 LIndF 𝑊 → 𝐹 ∈ V) | 
| 12 | 11 | ad2antrr 726 | . . . . 5
⊢ (((𝐹 LIndF 𝑊 ∧ 𝐸 ∈ dom 𝐹) ∧ (𝐴 ∈ 𝐾 ∧ 𝐴 ≠ 0 )) → 𝐹 ∈ V) | 
| 13 |  | eqid 2737 | . . . . . 6
⊢
(Base‘𝑊) =
(Base‘𝑊) | 
| 14 |  | lindfind.s | . . . . . 6
⊢  · = (
·𝑠 ‘𝑊) | 
| 15 |  | lindfind.n | . . . . . 6
⊢ 𝑁 = (LSpan‘𝑊) | 
| 16 |  | lindfind.z | . . . . . 6
⊢  0 =
(0g‘𝐿) | 
| 17 | 13, 14, 15, 6, 7, 16 | islindf 21832 | . . . . 5
⊢ ((𝑊 ∈ V ∧ 𝐹 ∈ V) → (𝐹 LIndF 𝑊 ↔ (𝐹:dom 𝐹⟶(Base‘𝑊) ∧ ∀𝑒 ∈ dom 𝐹∀𝑎 ∈ (𝐾 ∖ { 0 }) ¬ (𝑎 · (𝐹‘𝑒)) ∈ (𝑁‘(𝐹 “ (dom 𝐹 ∖ {𝑒})))))) | 
| 18 | 9, 12, 17 | syl2anc 584 | . . . 4
⊢ (((𝐹 LIndF 𝑊 ∧ 𝐸 ∈ dom 𝐹) ∧ (𝐴 ∈ 𝐾 ∧ 𝐴 ≠ 0 )) → (𝐹 LIndF 𝑊 ↔ (𝐹:dom 𝐹⟶(Base‘𝑊) ∧ ∀𝑒 ∈ dom 𝐹∀𝑎 ∈ (𝐾 ∖ { 0 }) ¬ (𝑎 · (𝐹‘𝑒)) ∈ (𝑁‘(𝐹 “ (dom 𝐹 ∖ {𝑒})))))) | 
| 19 | 5, 18 | mpbid 232 | . . 3
⊢ (((𝐹 LIndF 𝑊 ∧ 𝐸 ∈ dom 𝐹) ∧ (𝐴 ∈ 𝐾 ∧ 𝐴 ≠ 0 )) → (𝐹:dom 𝐹⟶(Base‘𝑊) ∧ ∀𝑒 ∈ dom 𝐹∀𝑎 ∈ (𝐾 ∖ { 0 }) ¬ (𝑎 · (𝐹‘𝑒)) ∈ (𝑁‘(𝐹 “ (dom 𝐹 ∖ {𝑒}))))) | 
| 20 | 19 | simprd 495 | . 2
⊢ (((𝐹 LIndF 𝑊 ∧ 𝐸 ∈ dom 𝐹) ∧ (𝐴 ∈ 𝐾 ∧ 𝐴 ≠ 0 )) → ∀𝑒 ∈ dom 𝐹∀𝑎 ∈ (𝐾 ∖ { 0 }) ¬ (𝑎 · (𝐹‘𝑒)) ∈ (𝑁‘(𝐹 “ (dom 𝐹 ∖ {𝑒})))) | 
| 21 |  | fveq2 6906 | . . . . . 6
⊢ (𝑒 = 𝐸 → (𝐹‘𝑒) = (𝐹‘𝐸)) | 
| 22 | 21 | oveq2d 7447 | . . . . 5
⊢ (𝑒 = 𝐸 → (𝑎 · (𝐹‘𝑒)) = (𝑎 · (𝐹‘𝐸))) | 
| 23 |  | sneq 4636 | . . . . . . . 8
⊢ (𝑒 = 𝐸 → {𝑒} = {𝐸}) | 
| 24 | 23 | difeq2d 4126 | . . . . . . 7
⊢ (𝑒 = 𝐸 → (dom 𝐹 ∖ {𝑒}) = (dom 𝐹 ∖ {𝐸})) | 
| 25 | 24 | imaeq2d 6078 | . . . . . 6
⊢ (𝑒 = 𝐸 → (𝐹 “ (dom 𝐹 ∖ {𝑒})) = (𝐹 “ (dom 𝐹 ∖ {𝐸}))) | 
| 26 | 25 | fveq2d 6910 | . . . . 5
⊢ (𝑒 = 𝐸 → (𝑁‘(𝐹 “ (dom 𝐹 ∖ {𝑒}))) = (𝑁‘(𝐹 “ (dom 𝐹 ∖ {𝐸})))) | 
| 27 | 22, 26 | eleq12d 2835 | . . . 4
⊢ (𝑒 = 𝐸 → ((𝑎 · (𝐹‘𝑒)) ∈ (𝑁‘(𝐹 “ (dom 𝐹 ∖ {𝑒}))) ↔ (𝑎 · (𝐹‘𝐸)) ∈ (𝑁‘(𝐹 “ (dom 𝐹 ∖ {𝐸}))))) | 
| 28 | 27 | notbid 318 | . . 3
⊢ (𝑒 = 𝐸 → (¬ (𝑎 · (𝐹‘𝑒)) ∈ (𝑁‘(𝐹 “ (dom 𝐹 ∖ {𝑒}))) ↔ ¬ (𝑎 · (𝐹‘𝐸)) ∈ (𝑁‘(𝐹 “ (dom 𝐹 ∖ {𝐸}))))) | 
| 29 |  | oveq1 7438 | . . . . 5
⊢ (𝑎 = 𝐴 → (𝑎 · (𝐹‘𝐸)) = (𝐴 · (𝐹‘𝐸))) | 
| 30 | 29 | eleq1d 2826 | . . . 4
⊢ (𝑎 = 𝐴 → ((𝑎 · (𝐹‘𝐸)) ∈ (𝑁‘(𝐹 “ (dom 𝐹 ∖ {𝐸}))) ↔ (𝐴 · (𝐹‘𝐸)) ∈ (𝑁‘(𝐹 “ (dom 𝐹 ∖ {𝐸}))))) | 
| 31 | 30 | notbid 318 | . . 3
⊢ (𝑎 = 𝐴 → (¬ (𝑎 · (𝐹‘𝐸)) ∈ (𝑁‘(𝐹 “ (dom 𝐹 ∖ {𝐸}))) ↔ ¬ (𝐴 · (𝐹‘𝐸)) ∈ (𝑁‘(𝐹 “ (dom 𝐹 ∖ {𝐸}))))) | 
| 32 | 28, 31 | rspc2va 3634 | . 2
⊢ (((𝐸 ∈ dom 𝐹 ∧ 𝐴 ∈ (𝐾 ∖ { 0 })) ∧ ∀𝑒 ∈ dom 𝐹∀𝑎 ∈ (𝐾 ∖ { 0 }) ¬ (𝑎 · (𝐹‘𝑒)) ∈ (𝑁‘(𝐹 “ (dom 𝐹 ∖ {𝑒})))) → ¬ (𝐴 · (𝐹‘𝐸)) ∈ (𝑁‘(𝐹 “ (dom 𝐹 ∖ {𝐸})))) | 
| 33 | 1, 4, 20, 32 | syl21anc 838 | 1
⊢ (((𝐹 LIndF 𝑊 ∧ 𝐸 ∈ dom 𝐹) ∧ (𝐴 ∈ 𝐾 ∧ 𝐴 ≠ 0 )) → ¬ (𝐴 · (𝐹‘𝐸)) ∈ (𝑁‘(𝐹 “ (dom 𝐹 ∖ {𝐸})))) |