Detailed syntax breakdown of Definition df-lininds
Step | Hyp | Ref
| Expression |
1 | | clininds 42023 |
. 2
class
linIndS |
2 | | vs |
. . . . . 6
setvar 𝑠 |
3 | 2 | cv 1474 |
. . . . 5
class 𝑠 |
4 | | vm |
. . . . . . . 8
setvar 𝑚 |
5 | 4 | cv 1474 |
. . . . . . 7
class 𝑚 |
6 | | cbs 15695 |
. . . . . . 7
class
Base |
7 | 5, 6 | cfv 5804 |
. . . . . 6
class
(Base‘𝑚) |
8 | 7 | cpw 4108 |
. . . . 5
class 𝒫
(Base‘𝑚) |
9 | 3, 8 | wcel 1977 |
. . . 4
wff 𝑠 ∈ 𝒫
(Base‘𝑚) |
10 | | vf |
. . . . . . . . 9
setvar 𝑓 |
11 | 10 | cv 1474 |
. . . . . . . 8
class 𝑓 |
12 | | csca 15771 |
. . . . . . . . . 10
class
Scalar |
13 | 5, 12 | cfv 5804 |
. . . . . . . . 9
class
(Scalar‘𝑚) |
14 | | c0g 15923 |
. . . . . . . . 9
class
0g |
15 | 13, 14 | cfv 5804 |
. . . . . . . 8
class
(0g‘(Scalar‘𝑚)) |
16 | | cfsupp 8158 |
. . . . . . . 8
class
finSupp |
17 | 11, 15, 16 | wbr 4583 |
. . . . . . 7
wff 𝑓 finSupp
(0g‘(Scalar‘𝑚)) |
18 | | clinc 41987 |
. . . . . . . . . 10
class
linC |
19 | 5, 18 | cfv 5804 |
. . . . . . . . 9
class ( linC
‘𝑚) |
20 | 11, 3, 19 | co 6549 |
. . . . . . . 8
class (𝑓( linC ‘𝑚)𝑠) |
21 | 5, 14 | cfv 5804 |
. . . . . . . 8
class
(0g‘𝑚) |
22 | 20, 21 | wceq 1475 |
. . . . . . 7
wff (𝑓( linC ‘𝑚)𝑠) = (0g‘𝑚) |
23 | 17, 22 | wa 383 |
. . . . . 6
wff (𝑓 finSupp
(0g‘(Scalar‘𝑚)) ∧ (𝑓( linC ‘𝑚)𝑠) = (0g‘𝑚)) |
24 | | vx |
. . . . . . . . . 10
setvar 𝑥 |
25 | 24 | cv 1474 |
. . . . . . . . 9
class 𝑥 |
26 | 25, 11 | cfv 5804 |
. . . . . . . 8
class (𝑓‘𝑥) |
27 | 26, 15 | wceq 1475 |
. . . . . . 7
wff (𝑓‘𝑥) = (0g‘(Scalar‘𝑚)) |
28 | 27, 24, 3 | wral 2896 |
. . . . . 6
wff
∀𝑥 ∈
𝑠 (𝑓‘𝑥) = (0g‘(Scalar‘𝑚)) |
29 | 23, 28 | wi 4 |
. . . . 5
wff ((𝑓 finSupp
(0g‘(Scalar‘𝑚)) ∧ (𝑓( linC ‘𝑚)𝑠) = (0g‘𝑚)) → ∀𝑥 ∈ 𝑠 (𝑓‘𝑥) = (0g‘(Scalar‘𝑚))) |
30 | 13, 6 | cfv 5804 |
. . . . . 6
class
(Base‘(Scalar‘𝑚)) |
31 | | cmap 7744 |
. . . . . 6
class
↑𝑚 |
32 | 30, 3, 31 | co 6549 |
. . . . 5
class
((Base‘(Scalar‘𝑚)) ↑𝑚 𝑠) |
33 | 29, 10, 32 | wral 2896 |
. . . 4
wff
∀𝑓 ∈
((Base‘(Scalar‘𝑚)) ↑𝑚 𝑠)((𝑓 finSupp
(0g‘(Scalar‘𝑚)) ∧ (𝑓( linC ‘𝑚)𝑠) = (0g‘𝑚)) → ∀𝑥 ∈ 𝑠 (𝑓‘𝑥) = (0g‘(Scalar‘𝑚))) |
34 | 9, 33 | wa 383 |
. . 3
wff (𝑠 ∈ 𝒫
(Base‘𝑚) ∧
∀𝑓 ∈
((Base‘(Scalar‘𝑚)) ↑𝑚 𝑠)((𝑓 finSupp
(0g‘(Scalar‘𝑚)) ∧ (𝑓( linC ‘𝑚)𝑠) = (0g‘𝑚)) → ∀𝑥 ∈ 𝑠 (𝑓‘𝑥) = (0g‘(Scalar‘𝑚)))) |
35 | 34, 2, 4 | copab 4642 |
. 2
class
{〈𝑠, 𝑚〉 ∣ (𝑠 ∈ 𝒫
(Base‘𝑚) ∧
∀𝑓 ∈
((Base‘(Scalar‘𝑚)) ↑𝑚 𝑠)((𝑓 finSupp
(0g‘(Scalar‘𝑚)) ∧ (𝑓( linC ‘𝑚)𝑠) = (0g‘𝑚)) → ∀𝑥 ∈ 𝑠 (𝑓‘𝑥) = (0g‘(Scalar‘𝑚))))} |
36 | 1, 35 | wceq 1475 |
1
wff linIndS =
{〈𝑠, 𝑚〉 ∣ (𝑠 ∈ 𝒫
(Base‘𝑚) ∧
∀𝑓 ∈
((Base‘(Scalar‘𝑚)) ↑𝑚 𝑠)((𝑓 finSupp
(0g‘(Scalar‘𝑚)) ∧ (𝑓( linC ‘𝑚)𝑠) = (0g‘𝑚)) → ∀𝑥 ∈ 𝑠 (𝑓‘𝑥) = (0g‘(Scalar‘𝑚))))} |