Step | Hyp | Ref
| Expression |
1 | | id 22 |
. . . . . . . . . . . 12
β’ ((π β LMod β§ π β π« π΅) β (π β LMod β§ π β π« π΅)) |
2 | 1 | 3adant3 1133 |
. . . . . . . . . . 11
β’ ((π β LMod β§ π β π« π΅ β§ π
β NzRing) β (π β LMod β§ π β π« π΅)) |
3 | 2 | ad3antrrr 729 |
. . . . . . . . . 10
β’
(((((π β LMod
β§ π β π«
π΅ β§ π
β NzRing) β§ π β π) β§ π β (πΈ βm (π β {π }))) β§ (π finSupp 0 β§ (π( linC βπ)(π β {π })) = π )) β (π β LMod β§ π β π« π΅)) |
4 | | nzrring 20199 |
. . . . . . . . . . . . . 14
β’ (π
β NzRing β π
β Ring) |
5 | | islindeps2.e |
. . . . . . . . . . . . . . 15
β’ πΈ = (Baseβπ
) |
6 | | eqid 2733 |
. . . . . . . . . . . . . . 15
β’
(1rβπ
) = (1rβπ
) |
7 | 5, 6 | ringidcl 19997 |
. . . . . . . . . . . . . 14
β’ (π
β Ring β
(1rβπ
)
β πΈ) |
8 | 4, 7 | syl 17 |
. . . . . . . . . . . . 13
β’ (π
β NzRing β
(1rβπ
)
β πΈ) |
9 | 8 | 3ad2ant3 1136 |
. . . . . . . . . . . 12
β’ ((π β LMod β§ π β π« π΅ β§ π
β NzRing) β
(1rβπ
)
β πΈ) |
10 | 9 | ad3antrrr 729 |
. . . . . . . . . . 11
β’
(((((π β LMod
β§ π β π«
π΅ β§ π
β NzRing) β§ π β π) β§ π β (πΈ βm (π β {π }))) β§ (π finSupp 0 β§ (π( linC βπ)(π β {π })) = π )) β (1rβπ
) β πΈ) |
11 | | simpllr 775 |
. . . . . . . . . . 11
β’
(((((π β LMod
β§ π β π«
π΅ β§ π
β NzRing) β§ π β π) β§ π β (πΈ βm (π β {π }))) β§ (π finSupp 0 β§ (π( linC βπ)(π β {π })) = π )) β π β π) |
12 | | simplr 768 |
. . . . . . . . . . 11
β’
(((((π β LMod
β§ π β π«
π΅ β§ π
β NzRing) β§ π β π) β§ π β (πΈ βm (π β {π }))) β§ (π finSupp 0 β§ (π( linC βπ)(π β {π })) = π )) β π β (πΈ βm (π β {π }))) |
13 | 10, 11, 12 | 3jca 1129 |
. . . . . . . . . 10
β’
(((((π β LMod
β§ π β π«
π΅ β§ π
β NzRing) β§ π β π) β§ π β (πΈ βm (π β {π }))) β§ (π finSupp 0 β§ (π( linC βπ)(π β {π })) = π )) β ((1rβπ
) β πΈ β§ π β π β§ π β (πΈ βm (π β {π })))) |
14 | | simprl 770 |
. . . . . . . . . 10
β’
(((((π β LMod
β§ π β π«
π΅ β§ π
β NzRing) β§ π β π) β§ π β (πΈ βm (π β {π }))) β§ (π finSupp 0 β§ (π( linC βπ)(π β {π })) = π )) β π finSupp 0 ) |
15 | | islindeps2.b |
. . . . . . . . . . 11
β’ π΅ = (Baseβπ) |
16 | | islindeps2.r |
. . . . . . . . . . 11
β’ π
= (Scalarβπ) |
17 | | islindeps2.0 |
. . . . . . . . . . 11
β’ 0 =
(0gβπ
) |
18 | | islindeps2.z |
. . . . . . . . . . 11
β’ π = (0gβπ) |
19 | | eqid 2733 |
. . . . . . . . . . 11
β’
(invgβπ
) = (invgβπ
) |
20 | | eqid 2733 |
. . . . . . . . . . 11
β’ (π§ β π β¦ if(π§ = π , ((invgβπ
)β(1rβπ
)), (πβπ§))) = (π§ β π β¦ if(π§ = π , ((invgβπ
)β(1rβπ
)), (πβπ§))) |
21 | 15, 16, 5, 17, 18, 19, 20 | lincext2 46626 |
. . . . . . . . . 10
β’ (((π β LMod β§ π β π« π΅) β§
((1rβπ
)
β πΈ β§ π β π β§ π β (πΈ βm (π β {π }))) β§ π finSupp 0 ) β (π§ β π β¦ if(π§ = π , ((invgβπ
)β(1rβπ
)), (πβπ§))) finSupp 0 ) |
22 | 3, 13, 14, 21 | syl3anc 1372 |
. . . . . . . . 9
β’
(((((π β LMod
β§ π β π«
π΅ β§ π
β NzRing) β§ π β π) β§ π β (πΈ βm (π β {π }))) β§ (π finSupp 0 β§ (π( linC βπ)(π β {π })) = π )) β (π§ β π β¦ if(π§ = π , ((invgβπ
)β(1rβπ
)), (πβπ§))) finSupp 0 ) |
23 | | simpl1 1192 |
. . . . . . . . . . . . 13
β’ (((π β LMod β§ π β π« π΅ β§ π
β NzRing) β§ π β π) β π β LMod) |
24 | | elelpwi 4574 |
. . . . . . . . . . . . . . . 16
β’ ((π β π β§ π β π« π΅) β π β π΅) |
25 | 24 | expcom 415 |
. . . . . . . . . . . . . . 15
β’ (π β π« π΅ β (π β π β π β π΅)) |
26 | 25 | 3ad2ant2 1135 |
. . . . . . . . . . . . . 14
β’ ((π β LMod β§ π β π« π΅ β§ π
β NzRing) β (π β π β π β π΅)) |
27 | 26 | imp 408 |
. . . . . . . . . . . . 13
β’ (((π β LMod β§ π β π« π΅ β§ π
β NzRing) β§ π β π) β π β π΅) |
28 | | eqid 2733 |
. . . . . . . . . . . . . 14
β’ (
Β·π βπ) = ( Β·π
βπ) |
29 | 15, 16, 28, 6 | lmodvs1 20394 |
. . . . . . . . . . . . 13
β’ ((π β LMod β§ π β π΅) β ((1rβπ
)(
Β·π βπ)π ) = π ) |
30 | 23, 27, 29 | syl2anc 585 |
. . . . . . . . . . . 12
β’ (((π β LMod β§ π β π« π΅ β§ π
β NzRing) β§ π β π) β ((1rβπ
)(
Β·π βπ)π ) = π ) |
31 | 30 | adantr 482 |
. . . . . . . . . . 11
β’ ((((π β LMod β§ π β π« π΅ β§ π
β NzRing) β§ π β π) β§ π β (πΈ βm (π β {π }))) β ((1rβπ
)(
Β·π βπ)π ) = π ) |
32 | | id 22 |
. . . . . . . . . . . . 13
β’ ((π( linC βπ)(π β {π })) = π β (π( linC βπ)(π β {π })) = π ) |
33 | 32 | eqcomd 2739 |
. . . . . . . . . . . 12
β’ ((π( linC βπ)(π β {π })) = π β π = (π( linC βπ)(π β {π }))) |
34 | 33 | adantl 483 |
. . . . . . . . . . 11
β’ ((π finSupp 0 β§ (π( linC βπ)(π β {π })) = π ) β π = (π( linC βπ)(π β {π }))) |
35 | 31, 34 | sylan9eq 2793 |
. . . . . . . . . 10
β’
(((((π β LMod
β§ π β π«
π΅ β§ π
β NzRing) β§ π β π) β§ π β (πΈ βm (π β {π }))) β§ (π finSupp 0 β§ (π( linC βπ)(π β {π })) = π )) β ((1rβπ
)(
Β·π βπ)π ) = (π( linC βπ)(π β {π }))) |
36 | 15, 16, 5, 17, 18, 19, 20 | lincext3 46627 |
. . . . . . . . . 10
β’ (((π β LMod β§ π β π« π΅) β§
((1rβπ
)
β πΈ β§ π β π β§ π β (πΈ βm (π β {π }))) β§ (π finSupp 0 β§
((1rβπ
)(
Β·π βπ)π ) = (π( linC βπ)(π β {π })))) β ((π§ β π β¦ if(π§ = π , ((invgβπ
)β(1rβπ
)), (πβπ§)))( linC βπ)π) = π) |
37 | 3, 13, 14, 35, 36 | syl112anc 1375 |
. . . . . . . . 9
β’
(((((π β LMod
β§ π β π«
π΅ β§ π
β NzRing) β§ π β π) β§ π β (πΈ βm (π β {π }))) β§ (π finSupp 0 β§ (π( linC βπ)(π β {π })) = π )) β ((π§ β π β¦ if(π§ = π , ((invgβπ
)β(1rβπ
)), (πβπ§)))( linC βπ)π) = π) |
38 | 22, 37 | jca 513 |
. . . . . . . 8
β’
(((((π β LMod
β§ π β π«
π΅ β§ π
β NzRing) β§ π β π) β§ π β (πΈ βm (π β {π }))) β§ (π finSupp 0 β§ (π( linC βπ)(π β {π })) = π )) β ((π§ β π β¦ if(π§ = π , ((invgβπ
)β(1rβπ
)), (πβπ§))) finSupp 0 β§ ((π§ β π β¦ if(π§ = π , ((invgβπ
)β(1rβπ
)), (πβπ§)))( linC βπ)π) = π)) |
39 | | eqidd 2734 |
. . . . . . . . . . . 12
β’ (((π β LMod β§ π β π« π΅ β§ π
β NzRing) β§ π β π) β (π§ β π β¦ if(π§ = π , ((invgβπ
)β(1rβπ
)), (πβπ§))) = (π§ β π β¦ if(π§ = π , ((invgβπ
)β(1rβπ
)), (πβπ§)))) |
40 | | iftrue 4496 |
. . . . . . . . . . . . 13
β’ (π§ = π β if(π§ = π , ((invgβπ
)β(1rβπ
)), (πβπ§)) = ((invgβπ
)β(1rβπ
))) |
41 | 40 | adantl 483 |
. . . . . . . . . . . 12
β’ ((((π β LMod β§ π β π« π΅ β§ π
β NzRing) β§ π β π) β§ π§ = π ) β if(π§ = π , ((invgβπ
)β(1rβπ
)), (πβπ§)) = ((invgβπ
)β(1rβπ
))) |
42 | | simpr 486 |
. . . . . . . . . . . 12
β’ (((π β LMod β§ π β π« π΅ β§ π
β NzRing) β§ π β π) β π β π) |
43 | | fvexd 6861 |
. . . . . . . . . . . 12
β’ (((π β LMod β§ π β π« π΅ β§ π
β NzRing) β§ π β π) β ((invgβπ
)β(1rβπ
)) β V) |
44 | 39, 41, 42, 43 | fvmptd 6959 |
. . . . . . . . . . 11
β’ (((π β LMod β§ π β π« π΅ β§ π
β NzRing) β§ π β π) β ((π§ β π β¦ if(π§ = π , ((invgβπ
)β(1rβπ
)), (πβπ§)))βπ ) = ((invgβπ
)β(1rβπ
))) |
45 | | nzrneg1ne0 46257 |
. . . . . . . . . . . . . 14
β’ (π
β NzRing β
((invgβπ
)β(1rβπ
)) β
(0gβπ
)) |
46 | 17 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (π
β NzRing β 0 =
(0gβπ
)) |
47 | 45, 46 | neeqtrrd 3015 |
. . . . . . . . . . . . 13
β’ (π
β NzRing β
((invgβπ
)β(1rβπ
)) β 0 ) |
48 | 47 | 3ad2ant3 1136 |
. . . . . . . . . . . 12
β’ ((π β LMod β§ π β π« π΅ β§ π
β NzRing) β
((invgβπ
)β(1rβπ
)) β 0 ) |
49 | 48 | adantr 482 |
. . . . . . . . . . 11
β’ (((π β LMod β§ π β π« π΅ β§ π
β NzRing) β§ π β π) β ((invgβπ
)β(1rβπ
)) β 0 ) |
50 | 44, 49 | eqnetrd 3008 |
. . . . . . . . . 10
β’ (((π β LMod β§ π β π« π΅ β§ π
β NzRing) β§ π β π) β ((π§ β π β¦ if(π§ = π , ((invgβπ
)β(1rβπ
)), (πβπ§)))βπ ) β 0 ) |
51 | 50 | adantr 482 |
. . . . . . . . 9
β’ ((((π β LMod β§ π β π« π΅ β§ π
β NzRing) β§ π β π) β§ π β (πΈ βm (π β {π }))) β ((π§ β π β¦ if(π§ = π , ((invgβπ
)β(1rβπ
)), (πβπ§)))βπ ) β 0 ) |
52 | 51 | adantr 482 |
. . . . . . . 8
β’
(((((π β LMod
β§ π β π«
π΅ β§ π
β NzRing) β§ π β π) β§ π β (πΈ βm (π β {π }))) β§ (π finSupp 0 β§ (π( linC βπ)(π β {π })) = π )) β ((π§ β π β¦ if(π§ = π , ((invgβπ
)β(1rβπ
)), (πβπ§)))βπ ) β 0 ) |
53 | 15, 16, 5, 17, 18, 19, 20 | lincext1 46625 |
. . . . . . . . . 10
β’ (((π β LMod β§ π β π« π΅) β§
((1rβπ
)
β πΈ β§ π β π β§ π β (πΈ βm (π β {π })))) β (π§ β π β¦ if(π§ = π , ((invgβπ
)β(1rβπ
)), (πβπ§))) β (πΈ βm π)) |
54 | 3, 13, 53 | syl2anc 585 |
. . . . . . . . 9
β’
(((((π β LMod
β§ π β π«
π΅ β§ π
β NzRing) β§ π β π) β§ π β (πΈ βm (π β {π }))) β§ (π finSupp 0 β§ (π( linC βπ)(π β {π })) = π )) β (π§ β π β¦ if(π§ = π , ((invgβπ
)β(1rβπ
)), (πβπ§))) β (πΈ βm π)) |
55 | | breq1 5112 |
. . . . . . . . . . . 12
β’ (π = (π§ β π β¦ if(π§ = π , ((invgβπ
)β(1rβπ
)), (πβπ§))) β (π finSupp 0 β (π§ β π β¦ if(π§ = π , ((invgβπ
)β(1rβπ
)), (πβπ§))) finSupp 0 )) |
56 | | oveq1 7368 |
. . . . . . . . . . . . 13
β’ (π = (π§ β π β¦ if(π§ = π , ((invgβπ
)β(1rβπ
)), (πβπ§))) β (π( linC βπ)π) = ((π§ β π β¦ if(π§ = π , ((invgβπ
)β(1rβπ
)), (πβπ§)))( linC βπ)π)) |
57 | 56 | eqeq1d 2735 |
. . . . . . . . . . . 12
β’ (π = (π§ β π β¦ if(π§ = π , ((invgβπ
)β(1rβπ
)), (πβπ§))) β ((π( linC βπ)π) = π β ((π§ β π β¦ if(π§ = π , ((invgβπ
)β(1rβπ
)), (πβπ§)))( linC βπ)π) = π)) |
58 | 55, 57 | anbi12d 632 |
. . . . . . . . . . 11
β’ (π = (π§ β π β¦ if(π§ = π , ((invgβπ
)β(1rβπ
)), (πβπ§))) β ((π finSupp 0 β§ (π( linC βπ)π) = π) β ((π§ β π β¦ if(π§ = π , ((invgβπ
)β(1rβπ
)), (πβπ§))) finSupp 0 β§ ((π§ β π β¦ if(π§ = π , ((invgβπ
)β(1rβπ
)), (πβπ§)))( linC βπ)π) = π))) |
59 | | fveq1 6845 |
. . . . . . . . . . . 12
β’ (π = (π§ β π β¦ if(π§ = π , ((invgβπ
)β(1rβπ
)), (πβπ§))) β (πβπ ) = ((π§ β π β¦ if(π§ = π , ((invgβπ
)β(1rβπ
)), (πβπ§)))βπ )) |
60 | 59 | neeq1d 3000 |
. . . . . . . . . . 11
β’ (π = (π§ β π β¦ if(π§ = π , ((invgβπ
)β(1rβπ
)), (πβπ§))) β ((πβπ ) β 0 β ((π§ β π β¦ if(π§ = π , ((invgβπ
)β(1rβπ
)), (πβπ§)))βπ ) β 0 )) |
61 | 58, 60 | anbi12d 632 |
. . . . . . . . . 10
β’ (π = (π§ β π β¦ if(π§ = π , ((invgβπ
)β(1rβπ
)), (πβπ§))) β (((π finSupp 0 β§ (π( linC βπ)π) = π) β§ (πβπ ) β 0 ) β (((π§ β π β¦ if(π§ = π , ((invgβπ
)β(1rβπ
)), (πβπ§))) finSupp 0 β§ ((π§ β π β¦ if(π§ = π , ((invgβπ
)β(1rβπ
)), (πβπ§)))( linC βπ)π) = π) β§ ((π§ β π β¦ if(π§ = π , ((invgβπ
)β(1rβπ
)), (πβπ§)))βπ ) β 0 ))) |
62 | 61 | adantl 483 |
. . . . . . . . 9
β’
((((((π β LMod
β§ π β π«
π΅ β§ π
β NzRing) β§ π β π) β§ π β (πΈ βm (π β {π }))) β§ (π finSupp 0 β§ (π( linC βπ)(π β {π })) = π )) β§ π = (π§ β π β¦ if(π§ = π , ((invgβπ
)β(1rβπ
)), (πβπ§)))) β (((π finSupp 0 β§ (π( linC βπ)π) = π) β§ (πβπ ) β 0 ) β (((π§ β π β¦ if(π§ = π , ((invgβπ
)β(1rβπ
)), (πβπ§))) finSupp 0 β§ ((π§ β π β¦ if(π§ = π , ((invgβπ
)β(1rβπ
)), (πβπ§)))( linC βπ)π) = π) β§ ((π§ β π β¦ if(π§ = π , ((invgβπ
)β(1rβπ
)), (πβπ§)))βπ ) β 0 ))) |
63 | 54, 62 | rspcedv 3576 |
. . . . . . . 8
β’
(((((π β LMod
β§ π β π«
π΅ β§ π
β NzRing) β§ π β π) β§ π β (πΈ βm (π β {π }))) β§ (π finSupp 0 β§ (π( linC βπ)(π β {π })) = π )) β ((((π§ β π β¦ if(π§ = π , ((invgβπ
)β(1rβπ
)), (πβπ§))) finSupp 0 β§ ((π§ β π β¦ if(π§ = π , ((invgβπ
)β(1rβπ
)), (πβπ§)))( linC βπ)π) = π) β§ ((π§ β π β¦ if(π§ = π , ((invgβπ
)β(1rβπ
)), (πβπ§)))βπ ) β 0 ) β βπ β (πΈ βm π)((π finSupp 0 β§ (π( linC βπ)π) = π) β§ (πβπ ) β 0 ))) |
64 | 38, 52, 63 | mp2and 698 |
. . . . . . 7
β’
(((((π β LMod
β§ π β π«
π΅ β§ π
β NzRing) β§ π β π) β§ π β (πΈ βm (π β {π }))) β§ (π finSupp 0 β§ (π( linC βπ)(π β {π })) = π )) β βπ β (πΈ βm π)((π finSupp 0 β§ (π( linC βπ)π) = π) β§ (πβπ ) β 0 )) |
65 | 64 | rexlimdva2 3151 |
. . . . . 6
β’ (((π β LMod β§ π β π« π΅ β§ π
β NzRing) β§ π β π) β (βπ β (πΈ βm (π β {π }))(π finSupp 0 β§ (π( linC βπ)(π β {π })) = π ) β βπ β (πΈ βm π)((π finSupp 0 β§ (π( linC βπ)π) = π) β§ (πβπ ) β 0 ))) |
66 | 65 | reximdva 3162 |
. . . . 5
β’ ((π β LMod β§ π β π« π΅ β§ π
β NzRing) β (βπ β π βπ β (πΈ βm (π β {π }))(π finSupp 0 β§ (π( linC βπ)(π β {π })) = π ) β βπ β π βπ β (πΈ βm π)((π finSupp 0 β§ (π( linC βπ)π) = π) β§ (πβπ ) β 0 ))) |
67 | 66 | imp 408 |
. . . 4
β’ (((π β LMod β§ π β π« π΅ β§ π
β NzRing) β§ βπ β π βπ β (πΈ βm (π β {π }))(π finSupp 0 β§ (π( linC βπ)(π β {π })) = π )) β βπ β π βπ β (πΈ βm π)((π finSupp 0 β§ (π( linC βπ)π) = π) β§ (πβπ ) β 0 )) |
68 | | df-3an 1090 |
. . . . . . 7
β’ ((π finSupp 0 β§ (π( linC βπ)π) = π β§ βπ β π (πβπ ) β 0 ) β ((π finSupp 0 β§ (π( linC βπ)π) = π) β§ βπ β π (πβπ ) β 0 )) |
69 | | r19.42v 3184 |
. . . . . . 7
β’
(βπ β
π ((π finSupp 0 β§ (π( linC βπ)π) = π) β§ (πβπ ) β 0 ) β ((π finSupp 0 β§ (π( linC βπ)π) = π) β§ βπ β π (πβπ ) β 0 )) |
70 | 68, 69 | bitr4i 278 |
. . . . . 6
β’ ((π finSupp 0 β§ (π( linC βπ)π) = π β§ βπ β π (πβπ ) β 0 ) β βπ β π ((π finSupp 0 β§ (π( linC βπ)π) = π) β§ (πβπ ) β 0 )) |
71 | 70 | rexbii 3094 |
. . . . 5
β’
(βπ β
(πΈ βm π)(π finSupp 0 β§ (π( linC βπ)π) = π β§ βπ β π (πβπ ) β 0 ) β βπ β (πΈ βm π)βπ β π ((π finSupp 0 β§ (π( linC βπ)π) = π) β§ (πβπ ) β 0 )) |
72 | | rexcom 3272 |
. . . . 5
β’
(βπ β
(πΈ βm π)βπ β π ((π finSupp 0 β§ (π( linC βπ)π) = π) β§ (πβπ ) β 0 ) β βπ β π βπ β (πΈ βm π)((π finSupp 0 β§ (π( linC βπ)π) = π) β§ (πβπ ) β 0 )) |
73 | 71, 72 | bitri 275 |
. . . 4
β’
(βπ β
(πΈ βm π)(π finSupp 0 β§ (π( linC βπ)π) = π β§ βπ β π (πβπ ) β 0 ) β βπ β π βπ β (πΈ βm π)((π finSupp 0 β§ (π( linC βπ)π) = π) β§ (πβπ ) β 0 )) |
74 | 67, 73 | sylibr 233 |
. . 3
β’ (((π β LMod β§ π β π« π΅ β§ π
β NzRing) β§ βπ β π βπ β (πΈ βm (π β {π }))(π finSupp 0 β§ (π( linC βπ)(π β {π })) = π )) β βπ β (πΈ βm π)(π finSupp 0 β§ (π( linC βπ)π) = π β§ βπ β π (πβπ ) β 0 )) |
75 | 15, 18, 16, 5, 17 | islindeps 46624 |
. . . . 5
β’ ((π β LMod β§ π β π« π΅) β (π linDepS π β βπ β (πΈ βm π)(π finSupp 0 β§ (π( linC βπ)π) = π β§ βπ β π (πβπ ) β 0 ))) |
76 | 75 | 3adant3 1133 |
. . . 4
β’ ((π β LMod β§ π β π« π΅ β§ π
β NzRing) β (π linDepS π β βπ β (πΈ βm π)(π finSupp 0 β§ (π( linC βπ)π) = π β§ βπ β π (πβπ ) β 0 ))) |
77 | 76 | adantr 482 |
. . 3
β’ (((π β LMod β§ π β π« π΅ β§ π
β NzRing) β§ βπ β π βπ β (πΈ βm (π β {π }))(π finSupp 0 β§ (π( linC βπ)(π β {π })) = π )) β (π linDepS π β βπ β (πΈ βm π)(π finSupp 0 β§ (π( linC βπ)π) = π β§ βπ β π (πβπ ) β 0 ))) |
78 | 74, 77 | mpbird 257 |
. 2
β’ (((π β LMod β§ π β π« π΅ β§ π
β NzRing) β§ βπ β π βπ β (πΈ βm (π β {π }))(π finSupp 0 β§ (π( linC βπ)(π β {π })) = π )) β π linDepS π) |
79 | 78 | ex 414 |
1
β’ ((π β LMod β§ π β π« π΅ β§ π
β NzRing) β (βπ β π βπ β (πΈ βm (π β {π }))(π finSupp 0 β§ (π( linC βπ)(π β {π })) = π ) β π linDepS π)) |