| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | feq1 6716 | . . . . . 6
⊢ (𝑓 = 𝐹 → (𝑓:dom 𝑓⟶(Base‘𝑤) ↔ 𝐹:dom 𝑓⟶(Base‘𝑤))) | 
| 2 | 1 | adantr 480 | . . . . 5
⊢ ((𝑓 = 𝐹 ∧ 𝑤 = 𝑊) → (𝑓:dom 𝑓⟶(Base‘𝑤) ↔ 𝐹:dom 𝑓⟶(Base‘𝑤))) | 
| 3 |  | dmeq 5914 | . . . . . . 7
⊢ (𝑓 = 𝐹 → dom 𝑓 = dom 𝐹) | 
| 4 | 3 | adantr 480 | . . . . . 6
⊢ ((𝑓 = 𝐹 ∧ 𝑤 = 𝑊) → dom 𝑓 = dom 𝐹) | 
| 5 |  | fveq2 6906 | . . . . . . . 8
⊢ (𝑤 = 𝑊 → (Base‘𝑤) = (Base‘𝑊)) | 
| 6 |  | islindf.b | . . . . . . . 8
⊢ 𝐵 = (Base‘𝑊) | 
| 7 | 5, 6 | eqtr4di 2795 | . . . . . . 7
⊢ (𝑤 = 𝑊 → (Base‘𝑤) = 𝐵) | 
| 8 | 7 | adantl 481 | . . . . . 6
⊢ ((𝑓 = 𝐹 ∧ 𝑤 = 𝑊) → (Base‘𝑤) = 𝐵) | 
| 9 | 4, 8 | feq23d 6731 | . . . . 5
⊢ ((𝑓 = 𝐹 ∧ 𝑤 = 𝑊) → (𝐹:dom 𝑓⟶(Base‘𝑤) ↔ 𝐹:dom 𝐹⟶𝐵)) | 
| 10 | 2, 9 | bitrd 279 | . . . 4
⊢ ((𝑓 = 𝐹 ∧ 𝑤 = 𝑊) → (𝑓:dom 𝑓⟶(Base‘𝑤) ↔ 𝐹:dom 𝐹⟶𝐵)) | 
| 11 |  | fvex 6919 | . . . . . 6
⊢
(Scalar‘𝑤)
∈ V | 
| 12 |  | fveq2 6906 | . . . . . . . . 9
⊢ (𝑠 = (Scalar‘𝑤) → (Base‘𝑠) =
(Base‘(Scalar‘𝑤))) | 
| 13 |  | fveq2 6906 | . . . . . . . . . 10
⊢ (𝑠 = (Scalar‘𝑤) →
(0g‘𝑠) =
(0g‘(Scalar‘𝑤))) | 
| 14 | 13 | sneqd 4638 | . . . . . . . . 9
⊢ (𝑠 = (Scalar‘𝑤) →
{(0g‘𝑠)} =
{(0g‘(Scalar‘𝑤))}) | 
| 15 | 12, 14 | difeq12d 4127 | . . . . . . . 8
⊢ (𝑠 = (Scalar‘𝑤) → ((Base‘𝑠) ∖
{(0g‘𝑠)})
= ((Base‘(Scalar‘𝑤)) ∖
{(0g‘(Scalar‘𝑤))})) | 
| 16 | 15 | raleqdv 3326 | . . . . . . 7
⊢ (𝑠 = (Scalar‘𝑤) → (∀𝑘 ∈ ((Base‘𝑠) ∖
{(0g‘𝑠)})
¬ (𝑘(
·𝑠 ‘𝑤)(𝑓‘𝑥)) ∈ ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥}))) ↔ ∀𝑘 ∈ ((Base‘(Scalar‘𝑤)) ∖
{(0g‘(Scalar‘𝑤))}) ¬ (𝑘( ·𝑠
‘𝑤)(𝑓‘𝑥)) ∈ ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥}))))) | 
| 17 | 16 | ralbidv 3178 | . . . . . 6
⊢ (𝑠 = (Scalar‘𝑤) → (∀𝑥 ∈ dom 𝑓∀𝑘 ∈ ((Base‘𝑠) ∖ {(0g‘𝑠)}) ¬ (𝑘( ·𝑠
‘𝑤)(𝑓‘𝑥)) ∈ ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥}))) ↔ ∀𝑥 ∈ dom 𝑓∀𝑘 ∈ ((Base‘(Scalar‘𝑤)) ∖
{(0g‘(Scalar‘𝑤))}) ¬ (𝑘( ·𝑠
‘𝑤)(𝑓‘𝑥)) ∈ ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥}))))) | 
| 18 | 11, 17 | sbcie 3830 | . . . . 5
⊢
([(Scalar‘𝑤) / 𝑠]∀𝑥 ∈ dom 𝑓∀𝑘 ∈ ((Base‘𝑠) ∖ {(0g‘𝑠)}) ¬ (𝑘( ·𝑠
‘𝑤)(𝑓‘𝑥)) ∈ ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥}))) ↔ ∀𝑥 ∈ dom 𝑓∀𝑘 ∈ ((Base‘(Scalar‘𝑤)) ∖
{(0g‘(Scalar‘𝑤))}) ¬ (𝑘( ·𝑠
‘𝑤)(𝑓‘𝑥)) ∈ ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥})))) | 
| 19 |  | fveq2 6906 | . . . . . . . . . . . 12
⊢ (𝑤 = 𝑊 → (Scalar‘𝑤) = (Scalar‘𝑊)) | 
| 20 |  | islindf.s | . . . . . . . . . . . 12
⊢ 𝑆 = (Scalar‘𝑊) | 
| 21 | 19, 20 | eqtr4di 2795 | . . . . . . . . . . 11
⊢ (𝑤 = 𝑊 → (Scalar‘𝑤) = 𝑆) | 
| 22 | 21 | fveq2d 6910 | . . . . . . . . . 10
⊢ (𝑤 = 𝑊 → (Base‘(Scalar‘𝑤)) = (Base‘𝑆)) | 
| 23 |  | islindf.n | . . . . . . . . . 10
⊢ 𝑁 = (Base‘𝑆) | 
| 24 | 22, 23 | eqtr4di 2795 | . . . . . . . . 9
⊢ (𝑤 = 𝑊 → (Base‘(Scalar‘𝑤)) = 𝑁) | 
| 25 | 21 | fveq2d 6910 | . . . . . . . . . . 11
⊢ (𝑤 = 𝑊 →
(0g‘(Scalar‘𝑤)) = (0g‘𝑆)) | 
| 26 |  | islindf.z | . . . . . . . . . . 11
⊢  0 =
(0g‘𝑆) | 
| 27 | 25, 26 | eqtr4di 2795 | . . . . . . . . . 10
⊢ (𝑤 = 𝑊 →
(0g‘(Scalar‘𝑤)) = 0 ) | 
| 28 | 27 | sneqd 4638 | . . . . . . . . 9
⊢ (𝑤 = 𝑊 →
{(0g‘(Scalar‘𝑤))} = { 0 }) | 
| 29 | 24, 28 | difeq12d 4127 | . . . . . . . 8
⊢ (𝑤 = 𝑊 → ((Base‘(Scalar‘𝑤)) ∖
{(0g‘(Scalar‘𝑤))}) = (𝑁 ∖ { 0 })) | 
| 30 | 29 | adantl 481 | . . . . . . 7
⊢ ((𝑓 = 𝐹 ∧ 𝑤 = 𝑊) → ((Base‘(Scalar‘𝑤)) ∖
{(0g‘(Scalar‘𝑤))}) = (𝑁 ∖ { 0 })) | 
| 31 |  | fveq2 6906 | . . . . . . . . . . . 12
⊢ (𝑤 = 𝑊 → (
·𝑠 ‘𝑤) = ( ·𝑠
‘𝑊)) | 
| 32 |  | islindf.v | . . . . . . . . . . . 12
⊢  · = (
·𝑠 ‘𝑊) | 
| 33 | 31, 32 | eqtr4di 2795 | . . . . . . . . . . 11
⊢ (𝑤 = 𝑊 → (
·𝑠 ‘𝑤) = · ) | 
| 34 | 33 | adantl 481 | . . . . . . . . . 10
⊢ ((𝑓 = 𝐹 ∧ 𝑤 = 𝑊) → (
·𝑠 ‘𝑤) = · ) | 
| 35 |  | eqidd 2738 | . . . . . . . . . 10
⊢ ((𝑓 = 𝐹 ∧ 𝑤 = 𝑊) → 𝑘 = 𝑘) | 
| 36 |  | fveq1 6905 | . . . . . . . . . . 11
⊢ (𝑓 = 𝐹 → (𝑓‘𝑥) = (𝐹‘𝑥)) | 
| 37 | 36 | adantr 480 | . . . . . . . . . 10
⊢ ((𝑓 = 𝐹 ∧ 𝑤 = 𝑊) → (𝑓‘𝑥) = (𝐹‘𝑥)) | 
| 38 | 34, 35, 37 | oveq123d 7452 | . . . . . . . . 9
⊢ ((𝑓 = 𝐹 ∧ 𝑤 = 𝑊) → (𝑘( ·𝑠
‘𝑤)(𝑓‘𝑥)) = (𝑘 · (𝐹‘𝑥))) | 
| 39 |  | fveq2 6906 | . . . . . . . . . . . 12
⊢ (𝑤 = 𝑊 → (LSpan‘𝑤) = (LSpan‘𝑊)) | 
| 40 |  | islindf.k | . . . . . . . . . . . 12
⊢ 𝐾 = (LSpan‘𝑊) | 
| 41 | 39, 40 | eqtr4di 2795 | . . . . . . . . . . 11
⊢ (𝑤 = 𝑊 → (LSpan‘𝑤) = 𝐾) | 
| 42 | 41 | adantl 481 | . . . . . . . . . 10
⊢ ((𝑓 = 𝐹 ∧ 𝑤 = 𝑊) → (LSpan‘𝑤) = 𝐾) | 
| 43 |  | imaeq1 6073 | . . . . . . . . . . . 12
⊢ (𝑓 = 𝐹 → (𝑓 “ (dom 𝑓 ∖ {𝑥})) = (𝐹 “ (dom 𝑓 ∖ {𝑥}))) | 
| 44 | 3 | difeq1d 4125 | . . . . . . . . . . . . 13
⊢ (𝑓 = 𝐹 → (dom 𝑓 ∖ {𝑥}) = (dom 𝐹 ∖ {𝑥})) | 
| 45 | 44 | imaeq2d 6078 | . . . . . . . . . . . 12
⊢ (𝑓 = 𝐹 → (𝐹 “ (dom 𝑓 ∖ {𝑥})) = (𝐹 “ (dom 𝐹 ∖ {𝑥}))) | 
| 46 | 43, 45 | eqtrd 2777 | . . . . . . . . . . 11
⊢ (𝑓 = 𝐹 → (𝑓 “ (dom 𝑓 ∖ {𝑥})) = (𝐹 “ (dom 𝐹 ∖ {𝑥}))) | 
| 47 | 46 | adantr 480 | . . . . . . . . . 10
⊢ ((𝑓 = 𝐹 ∧ 𝑤 = 𝑊) → (𝑓 “ (dom 𝑓 ∖ {𝑥})) = (𝐹 “ (dom 𝐹 ∖ {𝑥}))) | 
| 48 | 42, 47 | fveq12d 6913 | . . . . . . . . 9
⊢ ((𝑓 = 𝐹 ∧ 𝑤 = 𝑊) → ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥}))) = (𝐾‘(𝐹 “ (dom 𝐹 ∖ {𝑥})))) | 
| 49 | 38, 48 | eleq12d 2835 | . . . . . . . 8
⊢ ((𝑓 = 𝐹 ∧ 𝑤 = 𝑊) → ((𝑘( ·𝑠
‘𝑤)(𝑓‘𝑥)) ∈ ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥}))) ↔ (𝑘 · (𝐹‘𝑥)) ∈ (𝐾‘(𝐹 “ (dom 𝐹 ∖ {𝑥}))))) | 
| 50 | 49 | notbid 318 | . . . . . . 7
⊢ ((𝑓 = 𝐹 ∧ 𝑤 = 𝑊) → (¬ (𝑘( ·𝑠
‘𝑤)(𝑓‘𝑥)) ∈ ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥}))) ↔ ¬ (𝑘 · (𝐹‘𝑥)) ∈ (𝐾‘(𝐹 “ (dom 𝐹 ∖ {𝑥}))))) | 
| 51 | 30, 50 | raleqbidv 3346 | . . . . . 6
⊢ ((𝑓 = 𝐹 ∧ 𝑤 = 𝑊) → (∀𝑘 ∈ ((Base‘(Scalar‘𝑤)) ∖
{(0g‘(Scalar‘𝑤))}) ¬ (𝑘( ·𝑠
‘𝑤)(𝑓‘𝑥)) ∈ ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥}))) ↔ ∀𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · (𝐹‘𝑥)) ∈ (𝐾‘(𝐹 “ (dom 𝐹 ∖ {𝑥}))))) | 
| 52 | 4, 51 | raleqbidv 3346 | . . . . 5
⊢ ((𝑓 = 𝐹 ∧ 𝑤 = 𝑊) → (∀𝑥 ∈ dom 𝑓∀𝑘 ∈ ((Base‘(Scalar‘𝑤)) ∖
{(0g‘(Scalar‘𝑤))}) ¬ (𝑘( ·𝑠
‘𝑤)(𝑓‘𝑥)) ∈ ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥}))) ↔ ∀𝑥 ∈ dom 𝐹∀𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · (𝐹‘𝑥)) ∈ (𝐾‘(𝐹 “ (dom 𝐹 ∖ {𝑥}))))) | 
| 53 | 18, 52 | bitrid 283 | . . . 4
⊢ ((𝑓 = 𝐹 ∧ 𝑤 = 𝑊) → ([(Scalar‘𝑤) / 𝑠]∀𝑥 ∈ dom 𝑓∀𝑘 ∈ ((Base‘𝑠) ∖ {(0g‘𝑠)}) ¬ (𝑘( ·𝑠
‘𝑤)(𝑓‘𝑥)) ∈ ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥}))) ↔ ∀𝑥 ∈ dom 𝐹∀𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · (𝐹‘𝑥)) ∈ (𝐾‘(𝐹 “ (dom 𝐹 ∖ {𝑥}))))) | 
| 54 | 10, 53 | anbi12d 632 | . . 3
⊢ ((𝑓 = 𝐹 ∧ 𝑤 = 𝑊) → ((𝑓:dom 𝑓⟶(Base‘𝑤) ∧ [(Scalar‘𝑤) / 𝑠]∀𝑥 ∈ dom 𝑓∀𝑘 ∈ ((Base‘𝑠) ∖ {(0g‘𝑠)}) ¬ (𝑘( ·𝑠
‘𝑤)(𝑓‘𝑥)) ∈ ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥})))) ↔ (𝐹:dom 𝐹⟶𝐵 ∧ ∀𝑥 ∈ dom 𝐹∀𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · (𝐹‘𝑥)) ∈ (𝐾‘(𝐹 “ (dom 𝐹 ∖ {𝑥})))))) | 
| 55 |  | df-lindf 21826 | . . 3
⊢  LIndF =
{〈𝑓, 𝑤〉 ∣ (𝑓:dom 𝑓⟶(Base‘𝑤) ∧ [(Scalar‘𝑤) / 𝑠]∀𝑥 ∈ dom 𝑓∀𝑘 ∈ ((Base‘𝑠) ∖ {(0g‘𝑠)}) ¬ (𝑘( ·𝑠
‘𝑤)(𝑓‘𝑥)) ∈ ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥}))))} | 
| 56 | 54, 55 | brabga 5539 | . 2
⊢ ((𝐹 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌) → (𝐹 LIndF 𝑊 ↔ (𝐹:dom 𝐹⟶𝐵 ∧ ∀𝑥 ∈ dom 𝐹∀𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · (𝐹‘𝑥)) ∈ (𝐾‘(𝐹 “ (dom 𝐹 ∖ {𝑥})))))) | 
| 57 | 56 | ancoms 458 | 1
⊢ ((𝑊 ∈ 𝑌 ∧ 𝐹 ∈ 𝑋) → (𝐹 LIndF 𝑊 ↔ (𝐹:dom 𝐹⟶𝐵 ∧ ∀𝑥 ∈ dom 𝐹∀𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · (𝐹‘𝑥)) ∈ (𝐾‘(𝐹 “ (dom 𝐹 ∖ {𝑥})))))) |