Step |
Hyp |
Ref |
Expression |
0 |
|
clininds |
⊢ linIndS |
1 |
|
vs |
⊢ 𝑠 |
2 |
|
vm |
⊢ 𝑚 |
3 |
1
|
cv |
⊢ 𝑠 |
4 |
|
cbs |
⊢ Base |
5 |
2
|
cv |
⊢ 𝑚 |
6 |
5 4
|
cfv |
⊢ ( Base ‘ 𝑚 ) |
7 |
6
|
cpw |
⊢ 𝒫 ( Base ‘ 𝑚 ) |
8 |
3 7
|
wcel |
⊢ 𝑠 ∈ 𝒫 ( Base ‘ 𝑚 ) |
9 |
|
vf |
⊢ 𝑓 |
10 |
|
csca |
⊢ Scalar |
11 |
5 10
|
cfv |
⊢ ( Scalar ‘ 𝑚 ) |
12 |
11 4
|
cfv |
⊢ ( Base ‘ ( Scalar ‘ 𝑚 ) ) |
13 |
|
cmap |
⊢ ↑m |
14 |
12 3 13
|
co |
⊢ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m 𝑠 ) |
15 |
9
|
cv |
⊢ 𝑓 |
16 |
|
cfsupp |
⊢ finSupp |
17 |
|
c0g |
⊢ 0g |
18 |
11 17
|
cfv |
⊢ ( 0g ‘ ( Scalar ‘ 𝑚 ) ) |
19 |
15 18 16
|
wbr |
⊢ 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) ) |
20 |
|
clinc |
⊢ linC |
21 |
5 20
|
cfv |
⊢ ( linC ‘ 𝑚 ) |
22 |
15 3 21
|
co |
⊢ ( 𝑓 ( linC ‘ 𝑚 ) 𝑠 ) |
23 |
5 17
|
cfv |
⊢ ( 0g ‘ 𝑚 ) |
24 |
22 23
|
wceq |
⊢ ( 𝑓 ( linC ‘ 𝑚 ) 𝑠 ) = ( 0g ‘ 𝑚 ) |
25 |
19 24
|
wa |
⊢ ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) ) ∧ ( 𝑓 ( linC ‘ 𝑚 ) 𝑠 ) = ( 0g ‘ 𝑚 ) ) |
26 |
|
vx |
⊢ 𝑥 |
27 |
26
|
cv |
⊢ 𝑥 |
28 |
27 15
|
cfv |
⊢ ( 𝑓 ‘ 𝑥 ) |
29 |
28 18
|
wceq |
⊢ ( 𝑓 ‘ 𝑥 ) = ( 0g ‘ ( Scalar ‘ 𝑚 ) ) |
30 |
29 26 3
|
wral |
⊢ ∀ 𝑥 ∈ 𝑠 ( 𝑓 ‘ 𝑥 ) = ( 0g ‘ ( Scalar ‘ 𝑚 ) ) |
31 |
25 30
|
wi |
⊢ ( ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) ) ∧ ( 𝑓 ( linC ‘ 𝑚 ) 𝑠 ) = ( 0g ‘ 𝑚 ) ) → ∀ 𝑥 ∈ 𝑠 ( 𝑓 ‘ 𝑥 ) = ( 0g ‘ ( Scalar ‘ 𝑚 ) ) ) |
32 |
31 9 14
|
wral |
⊢ ∀ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m 𝑠 ) ( ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) ) ∧ ( 𝑓 ( linC ‘ 𝑚 ) 𝑠 ) = ( 0g ‘ 𝑚 ) ) → ∀ 𝑥 ∈ 𝑠 ( 𝑓 ‘ 𝑥 ) = ( 0g ‘ ( Scalar ‘ 𝑚 ) ) ) |
33 |
8 32
|
wa |
⊢ ( 𝑠 ∈ 𝒫 ( Base ‘ 𝑚 ) ∧ ∀ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m 𝑠 ) ( ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) ) ∧ ( 𝑓 ( linC ‘ 𝑚 ) 𝑠 ) = ( 0g ‘ 𝑚 ) ) → ∀ 𝑥 ∈ 𝑠 ( 𝑓 ‘ 𝑥 ) = ( 0g ‘ ( Scalar ‘ 𝑚 ) ) ) ) |
34 |
33 1 2
|
copab |
⊢ { 〈 𝑠 , 𝑚 〉 ∣ ( 𝑠 ∈ 𝒫 ( Base ‘ 𝑚 ) ∧ ∀ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m 𝑠 ) ( ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) ) ∧ ( 𝑓 ( linC ‘ 𝑚 ) 𝑠 ) = ( 0g ‘ 𝑚 ) ) → ∀ 𝑥 ∈ 𝑠 ( 𝑓 ‘ 𝑥 ) = ( 0g ‘ ( Scalar ‘ 𝑚 ) ) ) ) } |
35 |
0 34
|
wceq |
⊢ linIndS = { 〈 𝑠 , 𝑚 〉 ∣ ( 𝑠 ∈ 𝒫 ( Base ‘ 𝑚 ) ∧ ∀ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m 𝑠 ) ( ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) ) ∧ ( 𝑓 ( linC ‘ 𝑚 ) 𝑠 ) = ( 0g ‘ 𝑚 ) ) → ∀ 𝑥 ∈ 𝑠 ( 𝑓 ‘ 𝑥 ) = ( 0g ‘ ( Scalar ‘ 𝑚 ) ) ) ) } |