Detailed syntax breakdown of Definition df-lindf
| Step | Hyp | Ref
| Expression |
| 1 | | clindf 21824 |
. 2
class
LIndF |
| 2 | | vf |
. . . . . . 7
setvar 𝑓 |
| 3 | 2 | cv 1539 |
. . . . . 6
class 𝑓 |
| 4 | 3 | cdm 5685 |
. . . . 5
class dom 𝑓 |
| 5 | | vw |
. . . . . . 7
setvar 𝑤 |
| 6 | 5 | cv 1539 |
. . . . . 6
class 𝑤 |
| 7 | | cbs 17247 |
. . . . . 6
class
Base |
| 8 | 6, 7 | cfv 6561 |
. . . . 5
class
(Base‘𝑤) |
| 9 | 4, 8, 3 | wf 6557 |
. . . 4
wff 𝑓:dom 𝑓⟶(Base‘𝑤) |
| 10 | | vk |
. . . . . . . . . . 11
setvar 𝑘 |
| 11 | 10 | cv 1539 |
. . . . . . . . . 10
class 𝑘 |
| 12 | | vx |
. . . . . . . . . . . 12
setvar 𝑥 |
| 13 | 12 | cv 1539 |
. . . . . . . . . . 11
class 𝑥 |
| 14 | 13, 3 | cfv 6561 |
. . . . . . . . . 10
class (𝑓‘𝑥) |
| 15 | | cvsca 17301 |
. . . . . . . . . . 11
class
·𝑠 |
| 16 | 6, 15 | cfv 6561 |
. . . . . . . . . 10
class (
·𝑠 ‘𝑤) |
| 17 | 11, 14, 16 | co 7431 |
. . . . . . . . 9
class (𝑘(
·𝑠 ‘𝑤)(𝑓‘𝑥)) |
| 18 | 13 | csn 4626 |
. . . . . . . . . . . 12
class {𝑥} |
| 19 | 4, 18 | cdif 3948 |
. . . . . . . . . . 11
class (dom
𝑓 ∖ {𝑥}) |
| 20 | 3, 19 | cima 5688 |
. . . . . . . . . 10
class (𝑓 “ (dom 𝑓 ∖ {𝑥})) |
| 21 | | clspn 20969 |
. . . . . . . . . . 11
class
LSpan |
| 22 | 6, 21 | cfv 6561 |
. . . . . . . . . 10
class
(LSpan‘𝑤) |
| 23 | 20, 22 | cfv 6561 |
. . . . . . . . 9
class
((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥}))) |
| 24 | 17, 23 | wcel 2108 |
. . . . . . . 8
wff (𝑘(
·𝑠 ‘𝑤)(𝑓‘𝑥)) ∈ ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥}))) |
| 25 | 24 | wn 3 |
. . . . . . 7
wff ¬
(𝑘(
·𝑠 ‘𝑤)(𝑓‘𝑥)) ∈ ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥}))) |
| 26 | | vs |
. . . . . . . . . 10
setvar 𝑠 |
| 27 | 26 | cv 1539 |
. . . . . . . . 9
class 𝑠 |
| 28 | 27, 7 | cfv 6561 |
. . . . . . . 8
class
(Base‘𝑠) |
| 29 | | c0g 17484 |
. . . . . . . . . 10
class
0g |
| 30 | 27, 29 | cfv 6561 |
. . . . . . . . 9
class
(0g‘𝑠) |
| 31 | 30 | csn 4626 |
. . . . . . . 8
class
{(0g‘𝑠)} |
| 32 | 28, 31 | cdif 3948 |
. . . . . . 7
class
((Base‘𝑠)
∖ {(0g‘𝑠)}) |
| 33 | 25, 10, 32 | wral 3061 |
. . . . . 6
wff
∀𝑘 ∈
((Base‘𝑠) ∖
{(0g‘𝑠)})
¬ (𝑘(
·𝑠 ‘𝑤)(𝑓‘𝑥)) ∈ ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥}))) |
| 34 | 33, 12, 4 | wral 3061 |
. . . . 5
wff
∀𝑥 ∈ dom
𝑓∀𝑘 ∈ ((Base‘𝑠) ∖ {(0g‘𝑠)}) ¬ (𝑘( ·𝑠
‘𝑤)(𝑓‘𝑥)) ∈ ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥}))) |
| 35 | | csca 17300 |
. . . . . 6
class
Scalar |
| 36 | 6, 35 | cfv 6561 |
. . . . 5
class
(Scalar‘𝑤) |
| 37 | 34, 26, 36 | wsbc 3788 |
. . . 4
wff
[(Scalar‘𝑤) / 𝑠]∀𝑥 ∈ dom 𝑓∀𝑘 ∈ ((Base‘𝑠) ∖ {(0g‘𝑠)}) ¬ (𝑘( ·𝑠
‘𝑤)(𝑓‘𝑥)) ∈ ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥}))) |
| 38 | 9, 37 | wa 395 |
. . 3
wff (𝑓:dom 𝑓⟶(Base‘𝑤) ∧ [(Scalar‘𝑤) / 𝑠]∀𝑥 ∈ dom 𝑓∀𝑘 ∈ ((Base‘𝑠) ∖ {(0g‘𝑠)}) ¬ (𝑘( ·𝑠
‘𝑤)(𝑓‘𝑥)) ∈ ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥})))) |
| 39 | 38, 2, 5 | copab 5205 |
. 2
class
{〈𝑓, 𝑤〉 ∣ (𝑓:dom 𝑓⟶(Base‘𝑤) ∧ [(Scalar‘𝑤) / 𝑠]∀𝑥 ∈ dom 𝑓∀𝑘 ∈ ((Base‘𝑠) ∖ {(0g‘𝑠)}) ¬ (𝑘( ·𝑠
‘𝑤)(𝑓‘𝑥)) ∈ ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥}))))} |
| 40 | 1, 39 | wceq 1540 |
1
wff LIndF =
{〈𝑓, 𝑤〉 ∣ (𝑓:dom 𝑓⟶(Base‘𝑤) ∧ [(Scalar‘𝑤) / 𝑠]∀𝑥 ∈ dom 𝑓∀𝑘 ∈ ((Base‘𝑠) ∖ {(0g‘𝑠)}) ¬ (𝑘( ·𝑠
‘𝑤)(𝑓‘𝑥)) ∈ ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥}))))} |