Step | Hyp | Ref
| Expression |
1 | | df-ne 2941 |
. . . . 5
β’ ((π Β· π) β π β Β¬ (π Β· π) = π) |
2 | 1 | ralbii 3093 |
. . . 4
β’
(βπ β
(π β { 0 })(π Β· π) β π β βπ β (π β { 0 }) Β¬ (π Β· π) = π) |
3 | | raldifsni 4798 |
. . . 4
β’
(βπ β
(π β { 0 }) Β¬
(π Β· π) = π β βπ β π ((π Β· π) = π β π = 0 )) |
4 | 2, 3 | bitri 274 |
. . 3
β’
(βπ β
(π β { 0 })(π Β· π) β π β βπ β π ((π Β· π) = π β π = 0 )) |
5 | | simpl 483 |
. . . . . . . . . . . . 13
β’ ((π β LMod β§ π β π΅) β π β LMod) |
6 | 5 | adantr 481 |
. . . . . . . . . . . 12
β’ (((π β LMod β§ π β π΅) β§ βπ β π ((π Β· π) = π β π = 0 )) β π β LMod) |
7 | 6 | adantr 481 |
. . . . . . . . . . 11
β’ ((((π β LMod β§ π β π΅) β§ βπ β π ((π Β· π) = π β π = 0 )) β§ π β (π βm {π})) β π β LMod) |
8 | | snlindsntor.s |
. . . . . . . . . . . . . . . 16
β’ π = (Baseβπ
) |
9 | | snlindsntor.r |
. . . . . . . . . . . . . . . . 17
β’ π
= (Scalarβπ) |
10 | 9 | fveq2i 6894 |
. . . . . . . . . . . . . . . 16
β’
(Baseβπ
) =
(Baseβ(Scalarβπ)) |
11 | 8, 10 | eqtri 2760 |
. . . . . . . . . . . . . . 15
β’ π =
(Baseβ(Scalarβπ)) |
12 | 11 | oveq1i 7421 |
. . . . . . . . . . . . . 14
β’ (π βm {π}) =
((Baseβ(Scalarβπ)) βm {π}) |
13 | 12 | eleq2i 2825 |
. . . . . . . . . . . . 13
β’ (π β (π βm {π}) β π β ((Baseβ(Scalarβπ)) βm {π})) |
14 | 13 | biimpi 215 |
. . . . . . . . . . . 12
β’ (π β (π βm {π}) β π β ((Baseβ(Scalarβπ)) βm {π})) |
15 | 14 | adantl 482 |
. . . . . . . . . . 11
β’ ((((π β LMod β§ π β π΅) β§ βπ β π ((π Β· π) = π β π = 0 )) β§ π β (π βm {π})) β π β ((Baseβ(Scalarβπ)) βm {π})) |
16 | | snelpwi 5443 |
. . . . . . . . . . . . 13
β’ (π β (Baseβπ) β {π} β π« (Baseβπ)) |
17 | | snlindsntor.b |
. . . . . . . . . . . . 13
β’ π΅ = (Baseβπ) |
18 | 16, 17 | eleq2s 2851 |
. . . . . . . . . . . 12
β’ (π β π΅ β {π} β π« (Baseβπ)) |
19 | 18 | ad3antlr 729 |
. . . . . . . . . . 11
β’ ((((π β LMod β§ π β π΅) β§ βπ β π ((π Β· π) = π β π = 0 )) β§ π β (π βm {π})) β {π} β π« (Baseβπ)) |
20 | | lincval 47174 |
. . . . . . . . . . 11
β’ ((π β LMod β§ π β
((Baseβ(Scalarβπ)) βm {π}) β§ {π} β π« (Baseβπ)) β (π( linC βπ){π}) = (π Ξ£g (π₯ β {π} β¦ ((πβπ₯)( Β·π
βπ)π₯)))) |
21 | 7, 15, 19, 20 | syl3anc 1371 |
. . . . . . . . . 10
β’ ((((π β LMod β§ π β π΅) β§ βπ β π ((π Β· π) = π β π = 0 )) β§ π β (π βm {π})) β (π( linC βπ){π}) = (π Ξ£g (π₯ β {π} β¦ ((πβπ₯)( Β·π
βπ)π₯)))) |
22 | 21 | eqeq1d 2734 |
. . . . . . . . 9
β’ ((((π β LMod β§ π β π΅) β§ βπ β π ((π Β· π) = π β π = 0 )) β§ π β (π βm {π})) β ((π( linC βπ){π}) = π β (π Ξ£g (π₯ β {π} β¦ ((πβπ₯)( Β·π
βπ)π₯))) = π)) |
23 | 22 | anbi2d 629 |
. . . . . . . 8
β’ ((((π β LMod β§ π β π΅) β§ βπ β π ((π Β· π) = π β π = 0 )) β§ π β (π βm {π})) β ((π finSupp 0 β§ (π( linC βπ){π}) = π) β (π finSupp 0 β§ (π Ξ£g (π₯ β {π} β¦ ((πβπ₯)( Β·π
βπ)π₯))) = π))) |
24 | | lmodgrp 20482 |
. . . . . . . . . . . . . 14
β’ (π β LMod β π β Grp) |
25 | 24 | grpmndd 18834 |
. . . . . . . . . . . . 13
β’ (π β LMod β π β Mnd) |
26 | 25 | ad3antrrr 728 |
. . . . . . . . . . . 12
β’ ((((π β LMod β§ π β π΅) β§ βπ β π ((π Β· π) = π β π = 0 )) β§ π β (π βm {π})) β π β Mnd) |
27 | | simpllr 774 |
. . . . . . . . . . . 12
β’ ((((π β LMod β§ π β π΅) β§ βπ β π ((π Β· π) = π β π = 0 )) β§ π β (π βm {π})) β π β π΅) |
28 | | elmapi 8845 |
. . . . . . . . . . . . . 14
β’ (π β (π βm {π}) β π:{π}βΆπ) |
29 | 6 | adantl 482 |
. . . . . . . . . . . . . . . 16
β’ ((π:{π}βΆπ β§ ((π β LMod β§ π β π΅) β§ βπ β π ((π Β· π) = π β π = 0 ))) β π β LMod) |
30 | | snidg 4662 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β π΅ β π β {π}) |
31 | 30 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β LMod β§ π β π΅) β π β {π}) |
32 | 31 | adantr 481 |
. . . . . . . . . . . . . . . . 17
β’ (((π β LMod β§ π β π΅) β§ βπ β π ((π Β· π) = π β π = 0 )) β π β {π}) |
33 | | ffvelcdm 7083 |
. . . . . . . . . . . . . . . . 17
β’ ((π:{π}βΆπ β§ π β {π}) β (πβπ) β π) |
34 | 32, 33 | sylan2 593 |
. . . . . . . . . . . . . . . 16
β’ ((π:{π}βΆπ β§ ((π β LMod β§ π β π΅) β§ βπ β π ((π Β· π) = π β π = 0 ))) β (πβπ) β π) |
35 | | simprlr 778 |
. . . . . . . . . . . . . . . 16
β’ ((π:{π}βΆπ β§ ((π β LMod β§ π β π΅) β§ βπ β π ((π Β· π) = π β π = 0 ))) β π β π΅) |
36 | | eqid 2732 |
. . . . . . . . . . . . . . . . 17
β’ (
Β·π βπ) = ( Β·π
βπ) |
37 | 17, 9, 36, 8 | lmodvscl 20493 |
. . . . . . . . . . . . . . . 16
β’ ((π β LMod β§ (πβπ) β π β§ π β π΅) β ((πβπ)( Β·π
βπ)π) β π΅) |
38 | 29, 34, 35, 37 | syl3anc 1371 |
. . . . . . . . . . . . . . 15
β’ ((π:{π}βΆπ β§ ((π β LMod β§ π β π΅) β§ βπ β π ((π Β· π) = π β π = 0 ))) β ((πβπ)( Β·π
βπ)π) β π΅) |
39 | 38 | expcom 414 |
. . . . . . . . . . . . . 14
β’ (((π β LMod β§ π β π΅) β§ βπ β π ((π Β· π) = π β π = 0 )) β (π:{π}βΆπ β ((πβπ)( Β·π
βπ)π) β π΅)) |
40 | 28, 39 | syl5com 31 |
. . . . . . . . . . . . 13
β’ (π β (π βm {π}) β (((π β LMod β§ π β π΅) β§ βπ β π ((π Β· π) = π β π = 0 )) β ((πβπ)( Β·π
βπ)π) β π΅)) |
41 | 40 | impcom 408 |
. . . . . . . . . . . 12
β’ ((((π β LMod β§ π β π΅) β§ βπ β π ((π Β· π) = π β π = 0 )) β§ π β (π βm {π})) β ((πβπ)( Β·π
βπ)π) β π΅) |
42 | | fveq2 6891 |
. . . . . . . . . . . . . 14
β’ (π₯ = π β (πβπ₯) = (πβπ)) |
43 | | id 22 |
. . . . . . . . . . . . . 14
β’ (π₯ = π β π₯ = π) |
44 | 42, 43 | oveq12d 7429 |
. . . . . . . . . . . . 13
β’ (π₯ = π β ((πβπ₯)( Β·π
βπ)π₯) = ((πβπ)( Β·π
βπ)π)) |
45 | 17, 44 | gsumsn 19824 |
. . . . . . . . . . . 12
β’ ((π β Mnd β§ π β π΅ β§ ((πβπ)( Β·π
βπ)π) β π΅) β (π Ξ£g (π₯ β {π} β¦ ((πβπ₯)( Β·π
βπ)π₯))) = ((πβπ)( Β·π
βπ)π)) |
46 | 26, 27, 41, 45 | syl3anc 1371 |
. . . . . . . . . . 11
β’ ((((π β LMod β§ π β π΅) β§ βπ β π ((π Β· π) = π β π = 0 )) β§ π β (π βm {π})) β (π Ξ£g (π₯ β {π} β¦ ((πβπ₯)( Β·π
βπ)π₯))) = ((πβπ)( Β·π
βπ)π)) |
47 | 46 | eqeq1d 2734 |
. . . . . . . . . 10
β’ ((((π β LMod β§ π β π΅) β§ βπ β π ((π Β· π) = π β π = 0 )) β§ π β (π βm {π})) β ((π Ξ£g (π₯ β {π} β¦ ((πβπ₯)( Β·π
βπ)π₯))) = π β ((πβπ)( Β·π
βπ)π) = π)) |
48 | 30, 33 | sylan2 593 |
. . . . . . . . . . . . . . 15
β’ ((π:{π}βΆπ β§ π β π΅) β (πβπ) β π) |
49 | 48 | expcom 414 |
. . . . . . . . . . . . . 14
β’ (π β π΅ β (π:{π}βΆπ β (πβπ) β π)) |
50 | 49 | adantl 482 |
. . . . . . . . . . . . 13
β’ ((π β LMod β§ π β π΅) β (π:{π}βΆπ β (πβπ) β π)) |
51 | | snlindsntor.t |
. . . . . . . . . . . . . . . . 17
β’ Β· = (
Β·π βπ) |
52 | 51 | oveqi 7424 |
. . . . . . . . . . . . . . . 16
β’ ((πβπ) Β· π) = ((πβπ)( Β·π
βπ)π) |
53 | 52 | eqeq1i 2737 |
. . . . . . . . . . . . . . 15
β’ (((πβπ) Β· π) = π β ((πβπ)( Β·π
βπ)π) = π) |
54 | | oveq1 7418 |
. . . . . . . . . . . . . . . . . 18
β’ (π = (πβπ) β (π Β· π) = ((πβπ) Β· π)) |
55 | 54 | eqeq1d 2734 |
. . . . . . . . . . . . . . . . 17
β’ (π = (πβπ) β ((π Β· π) = π β ((πβπ) Β· π) = π)) |
56 | | eqeq1 2736 |
. . . . . . . . . . . . . . . . 17
β’ (π = (πβπ) β (π = 0 β (πβπ) = 0 )) |
57 | 55, 56 | imbi12d 344 |
. . . . . . . . . . . . . . . 16
β’ (π = (πβπ) β (((π Β· π) = π β π = 0 ) β (((πβπ) Β· π) = π β (πβπ) = 0 ))) |
58 | 57 | rspcva 3610 |
. . . . . . . . . . . . . . 15
β’ (((πβπ) β π β§ βπ β π ((π Β· π) = π β π = 0 )) β (((πβπ) Β· π) = π β (πβπ) = 0 )) |
59 | 53, 58 | biimtrrid 242 |
. . . . . . . . . . . . . 14
β’ (((πβπ) β π β§ βπ β π ((π Β· π) = π β π = 0 )) β (((πβπ)( Β·π
βπ)π) = π β (πβπ) = 0 )) |
60 | 59 | ex 413 |
. . . . . . . . . . . . 13
β’ ((πβπ) β π β (βπ β π ((π Β· π) = π β π = 0 ) β (((πβπ)( Β·π
βπ)π) = π β (πβπ) = 0 ))) |
61 | 28, 50, 60 | syl56 36 |
. . . . . . . . . . . 12
β’ ((π β LMod β§ π β π΅) β (π β (π βm {π}) β (βπ β π ((π Β· π) = π β π = 0 ) β (((πβπ)( Β·π
βπ)π) = π β (πβπ) = 0 )))) |
62 | 61 | com23 86 |
. . . . . . . . . . 11
β’ ((π β LMod β§ π β π΅) β (βπ β π ((π Β· π) = π β π = 0 ) β (π β (π βm {π}) β (((πβπ)( Β·π
βπ)π) = π β (πβπ) = 0 )))) |
63 | 62 | imp31 418 |
. . . . . . . . . 10
β’ ((((π β LMod β§ π β π΅) β§ βπ β π ((π Β· π) = π β π = 0 )) β§ π β (π βm {π})) β (((πβπ)( Β·π
βπ)π) = π β (πβπ) = 0 )) |
64 | 47, 63 | sylbid 239 |
. . . . . . . . 9
β’ ((((π β LMod β§ π β π΅) β§ βπ β π ((π Β· π) = π β π = 0 )) β§ π β (π βm {π})) β ((π Ξ£g (π₯ β {π} β¦ ((πβπ₯)( Β·π
βπ)π₯))) = π β (πβπ) = 0 )) |
65 | 64 | adantld 491 |
. . . . . . . 8
β’ ((((π β LMod β§ π β π΅) β§ βπ β π ((π Β· π) = π β π = 0 )) β§ π β (π βm {π})) β ((π finSupp 0 β§ (π Ξ£g (π₯ β {π} β¦ ((πβπ₯)( Β·π
βπ)π₯))) = π) β (πβπ) = 0 )) |
66 | 23, 65 | sylbid 239 |
. . . . . . 7
β’ ((((π β LMod β§ π β π΅) β§ βπ β π ((π Β· π) = π β π = 0 )) β§ π β (π βm {π})) β ((π finSupp 0 β§ (π( linC βπ){π}) = π) β (πβπ) = 0 )) |
67 | 66 | ralrimiva 3146 |
. . . . . 6
β’ (((π β LMod β§ π β π΅) β§ βπ β π ((π Β· π) = π β π = 0 )) β βπ β (π βm {π})((π finSupp 0 β§ (π( linC βπ){π}) = π) β (πβπ) = 0 )) |
68 | 67 | ex 413 |
. . . . 5
β’ ((π β LMod β§ π β π΅) β (βπ β π ((π Β· π) = π β π = 0 ) β βπ β (π βm {π})((π finSupp 0 β§ (π( linC βπ){π}) = π) β (πβπ) = 0 ))) |
69 | | impexp 451 |
. . . . . . . 8
β’ (((π finSupp 0 β§ (π( linC βπ){π}) = π) β (πβπ) = 0 ) β (π finSupp 0 β ((π( linC βπ){π}) = π β (πβπ) = 0 ))) |
70 | 28 | adantl 482 |
. . . . . . . . . 10
β’ (((π β LMod β§ π β π΅) β§ π β (π βm {π})) β π:{π}βΆπ) |
71 | | snfi 9046 |
. . . . . . . . . . 11
β’ {π} β Fin |
72 | 71 | a1i 11 |
. . . . . . . . . 10
β’ (((π β LMod β§ π β π΅) β§ π β (π βm {π})) β {π} β Fin) |
73 | | snlindsntor.0 |
. . . . . . . . . . . 12
β’ 0 =
(0gβπ
) |
74 | 73 | fvexi 6905 |
. . . . . . . . . . 11
β’ 0 β
V |
75 | 74 | a1i 11 |
. . . . . . . . . 10
β’ (((π β LMod β§ π β π΅) β§ π β (π βm {π})) β 0 β V) |
76 | 70, 72, 75 | fdmfifsupp 9375 |
. . . . . . . . 9
β’ (((π β LMod β§ π β π΅) β§ π β (π βm {π})) β π finSupp 0 ) |
77 | | pm2.27 42 |
. . . . . . . . 9
β’ (π finSupp 0 β ((π finSupp 0 β ((π( linC βπ){π}) = π β (πβπ) = 0 )) β ((π( linC βπ){π}) = π β (πβπ) = 0 ))) |
78 | 76, 77 | syl 17 |
. . . . . . . 8
β’ (((π β LMod β§ π β π΅) β§ π β (π βm {π})) β ((π finSupp 0 β ((π( linC βπ){π}) = π β (πβπ) = 0 )) β ((π( linC βπ){π}) = π β (πβπ) = 0 ))) |
79 | 69, 78 | biimtrid 241 |
. . . . . . 7
β’ (((π β LMod β§ π β π΅) β§ π β (π βm {π})) β (((π finSupp 0 β§ (π( linC βπ){π}) = π) β (πβπ) = 0 ) β ((π( linC βπ){π}) = π β (πβπ) = 0 ))) |
80 | 79 | ralimdva 3167 |
. . . . . 6
β’ ((π β LMod β§ π β π΅) β (βπ β (π βm {π})((π finSupp 0 β§ (π( linC βπ){π}) = π) β (πβπ) = 0 ) β βπ β (π βm {π})((π( linC βπ){π}) = π β (πβπ) = 0 ))) |
81 | | snlindsntor.z |
. . . . . . 7
β’ π = (0gβπ) |
82 | 17, 9, 8, 73, 81, 51 | snlindsntorlem 47235 |
. . . . . 6
β’ ((π β LMod β§ π β π΅) β (βπ β (π βm {π})((π( linC βπ){π}) = π β (πβπ) = 0 ) β βπ β π ((π Β· π) = π β π = 0 ))) |
83 | 80, 82 | syld 47 |
. . . . 5
β’ ((π β LMod β§ π β π΅) β (βπ β (π βm {π})((π finSupp 0 β§ (π( linC βπ){π}) = π) β (πβπ) = 0 ) β βπ β π ((π Β· π) = π β π = 0 ))) |
84 | 68, 83 | impbid 211 |
. . . 4
β’ ((π β LMod β§ π β π΅) β (βπ β π ((π Β· π) = π β π = 0 ) β βπ β (π βm {π})((π finSupp 0 β§ (π( linC βπ){π}) = π) β (πβπ) = 0 ))) |
85 | | fveqeq2 6900 |
. . . . . . . . 9
β’ (π¦ = π β ((πβπ¦) = 0 β (πβπ) = 0 )) |
86 | 85 | ralsng 4677 |
. . . . . . . 8
β’ (π β π΅ β (βπ¦ β {π} (πβπ¦) = 0 β (πβπ) = 0 )) |
87 | 86 | adantl 482 |
. . . . . . 7
β’ ((π β LMod β§ π β π΅) β (βπ¦ β {π} (πβπ¦) = 0 β (πβπ) = 0 )) |
88 | 87 | bicomd 222 |
. . . . . 6
β’ ((π β LMod β§ π β π΅) β ((πβπ) = 0 β βπ¦ β {π} (πβπ¦) = 0 )) |
89 | 88 | imbi2d 340 |
. . . . 5
β’ ((π β LMod β§ π β π΅) β (((π finSupp 0 β§ (π( linC βπ){π}) = π) β (πβπ) = 0 ) β ((π finSupp 0 β§ (π( linC βπ){π}) = π) β βπ¦ β {π} (πβπ¦) = 0 ))) |
90 | 89 | ralbidv 3177 |
. . . 4
β’ ((π β LMod β§ π β π΅) β (βπ β (π βm {π})((π finSupp 0 β§ (π( linC βπ){π}) = π) β (πβπ) = 0 ) β βπ β (π βm {π})((π finSupp 0 β§ (π( linC βπ){π}) = π) β βπ¦ β {π} (πβπ¦) = 0 ))) |
91 | | snelpwi 5443 |
. . . . . 6
β’ (π β π΅ β {π} β π« π΅) |
92 | 91 | adantl 482 |
. . . . 5
β’ ((π β LMod β§ π β π΅) β {π} β π« π΅) |
93 | 92 | biantrurd 533 |
. . . 4
β’ ((π β LMod β§ π β π΅) β (βπ β (π βm {π})((π finSupp 0 β§ (π( linC βπ){π}) = π) β βπ¦ β {π} (πβπ¦) = 0 ) β ({π} β π« π΅ β§ βπ β (π βm {π})((π finSupp 0 β§ (π( linC βπ){π}) = π) β βπ¦ β {π} (πβπ¦) = 0 )))) |
94 | 84, 90, 93 | 3bitrd 304 |
. . 3
β’ ((π β LMod β§ π β π΅) β (βπ β π ((π Β· π) = π β π = 0 ) β ({π} β π« π΅ β§ βπ β (π βm {π})((π finSupp 0 β§ (π( linC βπ){π}) = π) β βπ¦ β {π} (πβπ¦) = 0 )))) |
95 | 4, 94 | bitrid 282 |
. 2
β’ ((π β LMod β§ π β π΅) β (βπ β (π β { 0 })(π Β· π) β π β ({π} β π« π΅ β§ βπ β (π βm {π})((π finSupp 0 β§ (π( linC βπ){π}) = π) β βπ¦ β {π} (πβπ¦) = 0 )))) |
96 | | snex 5431 |
. . 3
β’ {π} β V |
97 | 17, 81, 9, 8, 73 | islininds 47211 |
. . 3
β’ (({π} β V β§ π β LMod) β ({π} linIndS π β ({π} β π« π΅ β§ βπ β (π βm {π})((π finSupp 0 β§ (π( linC βπ){π}) = π) β βπ¦ β {π} (πβπ¦) = 0 )))) |
98 | 96, 5, 97 | sylancr 587 |
. 2
β’ ((π β LMod β§ π β π΅) β ({π} linIndS π β ({π} β π« π΅ β§ βπ β (π βm {π})((π finSupp 0 β§ (π( linC βπ){π}) = π) β βπ¦ β {π} (πβπ¦) = 0 )))) |
99 | 95, 98 | bitr4d 281 |
1
β’ ((π β LMod β§ π β π΅) β (βπ β (π β { 0 })(π Β· π) β π β {π} linIndS π)) |