Step | Hyp | Ref
| Expression |
1 | | df-ne 2941 |
. . . . 5
β’ ((π Β· π) β π β Β¬ (π Β· π) = π) |
2 | 1 | ralbii 3093 |
. . . 4
β’
(βπ β
(π β { 0 })(π Β· π) β π β βπ β (π β { 0 }) Β¬ (π Β· π) = π) |
3 | | raldifsni 4759 |
. . . 4
β’
(βπ β
(π β { 0 }) Β¬
(π Β· π) = π β βπ β π ((π Β· π) = π β π = 0 )) |
4 | 2, 3 | bitri 275 |
. . 3
β’
(βπ β
(π β { 0 })(π Β· π) β π β βπ β π ((π Β· π) = π β π = 0 )) |
5 | | simpl 484 |
. . . . . . . . . . . . 13
β’ ((π β LMod β§ π β π΅) β π β LMod) |
6 | 5 | adantr 482 |
. . . . . . . . . . . 12
β’ (((π β LMod β§ π β π΅) β§ βπ β π ((π Β· π) = π β π = 0 )) β π β LMod) |
7 | 6 | adantr 482 |
. . . . . . . . . . 11
β’ ((((π β LMod β§ π β π΅) β§ βπ β π ((π Β· π) = π β π = 0 )) β§ π β (π βm {π})) β π β LMod) |
8 | | snlindsntor.s |
. . . . . . . . . . . . . . . 16
β’ π = (Baseβπ
) |
9 | | snlindsntor.r |
. . . . . . . . . . . . . . . . 17
β’ π
= (Scalarβπ) |
10 | 9 | fveq2i 6849 |
. . . . . . . . . . . . . . . 16
β’
(Baseβπ
) =
(Baseβ(Scalarβπ)) |
11 | 8, 10 | eqtri 2761 |
. . . . . . . . . . . . . . 15
β’ π =
(Baseβ(Scalarβπ)) |
12 | 11 | oveq1i 7371 |
. . . . . . . . . . . . . 14
β’ (π βm {π}) =
((Baseβ(Scalarβπ)) βm {π}) |
13 | 12 | eleq2i 2826 |
. . . . . . . . . . . . 13
β’ (π β (π βm {π}) β π β ((Baseβ(Scalarβπ)) βm {π})) |
14 | 13 | biimpi 215 |
. . . . . . . . . . . 12
β’ (π β (π βm {π}) β π β ((Baseβ(Scalarβπ)) βm {π})) |
15 | 14 | adantl 483 |
. . . . . . . . . . 11
β’ ((((π β LMod β§ π β π΅) β§ βπ β π ((π Β· π) = π β π = 0 )) β§ π β (π βm {π})) β π β ((Baseβ(Scalarβπ)) βm {π})) |
16 | | snelpwi 5404 |
. . . . . . . . . . . . 13
β’ (π β (Baseβπ) β {π} β π« (Baseβπ)) |
17 | | snlindsntor.b |
. . . . . . . . . . . . 13
β’ π΅ = (Baseβπ) |
18 | 16, 17 | eleq2s 2852 |
. . . . . . . . . . . 12
β’ (π β π΅ β {π} β π« (Baseβπ)) |
19 | 18 | ad3antlr 730 |
. . . . . . . . . . 11
β’ ((((π β LMod β§ π β π΅) β§ βπ β π ((π Β· π) = π β π = 0 )) β§ π β (π βm {π})) β {π} β π« (Baseβπ)) |
20 | | lincval 46580 |
. . . . . . . . . . 11
β’ ((π β LMod β§ π β
((Baseβ(Scalarβπ)) βm {π}) β§ {π} β π« (Baseβπ)) β (π( linC βπ){π}) = (π Ξ£g (π₯ β {π} β¦ ((πβπ₯)( Β·π
βπ)π₯)))) |
21 | 7, 15, 19, 20 | syl3anc 1372 |
. . . . . . . . . 10
β’ ((((π β LMod β§ π β π΅) β§ βπ β π ((π Β· π) = π β π = 0 )) β§ π β (π βm {π})) β (π( linC βπ){π}) = (π Ξ£g (π₯ β {π} β¦ ((πβπ₯)( Β·π
βπ)π₯)))) |
22 | 21 | eqeq1d 2735 |
. . . . . . . . 9
β’ ((((π β LMod β§ π β π΅) β§ βπ β π ((π Β· π) = π β π = 0 )) β§ π β (π βm {π})) β ((π( linC βπ){π}) = π β (π Ξ£g (π₯ β {π} β¦ ((πβπ₯)( Β·π
βπ)π₯))) = π)) |
23 | 22 | anbi2d 630 |
. . . . . . . 8
β’ ((((π β LMod β§ π β π΅) β§ βπ β π ((π Β· π) = π β π = 0 )) β§ π β (π βm {π})) β ((π finSupp 0 β§ (π( linC βπ){π}) = π) β (π finSupp 0 β§ (π Ξ£g (π₯ β {π} β¦ ((πβπ₯)( Β·π
βπ)π₯))) = π))) |
24 | | lmodgrp 20372 |
. . . . . . . . . . . . . 14
β’ (π β LMod β π β Grp) |
25 | 24 | grpmndd 18768 |
. . . . . . . . . . . . 13
β’ (π β LMod β π β Mnd) |
26 | 25 | ad3antrrr 729 |
. . . . . . . . . . . 12
β’ ((((π β LMod β§ π β π΅) β§ βπ β π ((π Β· π) = π β π = 0 )) β§ π β (π βm {π})) β π β Mnd) |
27 | | simpllr 775 |
. . . . . . . . . . . 12
β’ ((((π β LMod β§ π β π΅) β§ βπ β π ((π Β· π) = π β π = 0 )) β§ π β (π βm {π})) β π β π΅) |
28 | | elmapi 8793 |
. . . . . . . . . . . . . 14
β’ (π β (π βm {π}) β π:{π}βΆπ) |
29 | 6 | adantl 483 |
. . . . . . . . . . . . . . . 16
β’ ((π:{π}βΆπ β§ ((π β LMod β§ π β π΅) β§ βπ β π ((π Β· π) = π β π = 0 ))) β π β LMod) |
30 | | snidg 4624 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β π΅ β π β {π}) |
31 | 30 | adantl 483 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β LMod β§ π β π΅) β π β {π}) |
32 | 31 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ (((π β LMod β§ π β π΅) β§ βπ β π ((π Β· π) = π β π = 0 )) β π β {π}) |
33 | | ffvelcdm 7036 |
. . . . . . . . . . . . . . . . 17
β’ ((π:{π}βΆπ β§ π β {π}) β (πβπ) β π) |
34 | 32, 33 | sylan2 594 |
. . . . . . . . . . . . . . . 16
β’ ((π:{π}βΆπ β§ ((π β LMod β§ π β π΅) β§ βπ β π ((π Β· π) = π β π = 0 ))) β (πβπ) β π) |
35 | | simprlr 779 |
. . . . . . . . . . . . . . . 16
β’ ((π:{π}βΆπ β§ ((π β LMod β§ π β π΅) β§ βπ β π ((π Β· π) = π β π = 0 ))) β π β π΅) |
36 | | eqid 2733 |
. . . . . . . . . . . . . . . . 17
β’ (
Β·π βπ) = ( Β·π
βπ) |
37 | 17, 9, 36, 8 | lmodvscl 20383 |
. . . . . . . . . . . . . . . 16
β’ ((π β LMod β§ (πβπ) β π β§ π β π΅) β ((πβπ)( Β·π
βπ)π) β π΅) |
38 | 29, 34, 35, 37 | syl3anc 1372 |
. . . . . . . . . . . . . . 15
β’ ((π:{π}βΆπ β§ ((π β LMod β§ π β π΅) β§ βπ β π ((π Β· π) = π β π = 0 ))) β ((πβπ)( Β·π
βπ)π) β π΅) |
39 | 38 | expcom 415 |
. . . . . . . . . . . . . 14
β’ (((π β LMod β§ π β π΅) β§ βπ β π ((π Β· π) = π β π = 0 )) β (π:{π}βΆπ β ((πβπ)( Β·π
βπ)π) β π΅)) |
40 | 28, 39 | syl5com 31 |
. . . . . . . . . . . . 13
β’ (π β (π βm {π}) β (((π β LMod β§ π β π΅) β§ βπ β π ((π Β· π) = π β π = 0 )) β ((πβπ)( Β·π
βπ)π) β π΅)) |
41 | 40 | impcom 409 |
. . . . . . . . . . . 12
β’ ((((π β LMod β§ π β π΅) β§ βπ β π ((π Β· π) = π β π = 0 )) β§ π β (π βm {π})) β ((πβπ)( Β·π
βπ)π) β π΅) |
42 | | fveq2 6846 |
. . . . . . . . . . . . . 14
β’ (π₯ = π β (πβπ₯) = (πβπ)) |
43 | | id 22 |
. . . . . . . . . . . . . 14
β’ (π₯ = π β π₯ = π) |
44 | 42, 43 | oveq12d 7379 |
. . . . . . . . . . . . 13
β’ (π₯ = π β ((πβπ₯)( Β·π
βπ)π₯) = ((πβπ)( Β·π
βπ)π)) |
45 | 17, 44 | gsumsn 19739 |
. . . . . . . . . . . 12
β’ ((π β Mnd β§ π β π΅ β§ ((πβπ)( Β·π
βπ)π) β π΅) β (π Ξ£g (π₯ β {π} β¦ ((πβπ₯)( Β·π
βπ)π₯))) = ((πβπ)( Β·π
βπ)π)) |
46 | 26, 27, 41, 45 | syl3anc 1372 |
. . . . . . . . . . 11
β’ ((((π β LMod β§ π β π΅) β§ βπ β π ((π Β· π) = π β π = 0 )) β§ π β (π βm {π})) β (π Ξ£g (π₯ β {π} β¦ ((πβπ₯)( Β·π
βπ)π₯))) = ((πβπ)( Β·π
βπ)π)) |
47 | 46 | eqeq1d 2735 |
. . . . . . . . . 10
β’ ((((π β LMod β§ π β π΅) β§ βπ β π ((π Β· π) = π β π = 0 )) β§ π β (π βm {π})) β ((π Ξ£g (π₯ β {π} β¦ ((πβπ₯)( Β·π
βπ)π₯))) = π β ((πβπ)( Β·π
βπ)π) = π)) |
48 | 30, 33 | sylan2 594 |
. . . . . . . . . . . . . . 15
β’ ((π:{π}βΆπ β§ π β π΅) β (πβπ) β π) |
49 | 48 | expcom 415 |
. . . . . . . . . . . . . 14
β’ (π β π΅ β (π:{π}βΆπ β (πβπ) β π)) |
50 | 49 | adantl 483 |
. . . . . . . . . . . . 13
β’ ((π β LMod β§ π β π΅) β (π:{π}βΆπ β (πβπ) β π)) |
51 | | snlindsntor.t |
. . . . . . . . . . . . . . . . 17
β’ Β· = (
Β·π βπ) |
52 | 51 | oveqi 7374 |
. . . . . . . . . . . . . . . 16
β’ ((πβπ) Β· π) = ((πβπ)( Β·π
βπ)π) |
53 | 52 | eqeq1i 2738 |
. . . . . . . . . . . . . . 15
β’ (((πβπ) Β· π) = π β ((πβπ)( Β·π
βπ)π) = π) |
54 | | oveq1 7368 |
. . . . . . . . . . . . . . . . . 18
β’ (π = (πβπ) β (π Β· π) = ((πβπ) Β· π)) |
55 | 54 | eqeq1d 2735 |
. . . . . . . . . . . . . . . . 17
β’ (π = (πβπ) β ((π Β· π) = π β ((πβπ) Β· π) = π)) |
56 | | eqeq1 2737 |
. . . . . . . . . . . . . . . . 17
β’ (π = (πβπ) β (π = 0 β (πβπ) = 0 )) |
57 | 55, 56 | imbi12d 345 |
. . . . . . . . . . . . . . . 16
β’ (π = (πβπ) β (((π Β· π) = π β π = 0 ) β (((πβπ) Β· π) = π β (πβπ) = 0 ))) |
58 | 57 | rspcva 3581 |
. . . . . . . . . . . . . . 15
β’ (((πβπ) β π β§ βπ β π ((π Β· π) = π β π = 0 )) β (((πβπ) Β· π) = π β (πβπ) = 0 )) |
59 | 53, 58 | biimtrrid 242 |
. . . . . . . . . . . . . 14
β’ (((πβπ) β π β§ βπ β π ((π Β· π) = π β π = 0 )) β (((πβπ)( Β·π
βπ)π) = π β (πβπ) = 0 )) |
60 | 59 | ex 414 |
. . . . . . . . . . . . 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 419 |
. . . . . . . . . 10
β’ ((((π β LMod β§ π β π΅) β§ βπ β π ((π Β· π) = π β π = 0 )) β§ π β (π βm {π})) β (((πβπ)( Β·π
βπ)π) = π β (πβπ) = 0 )) |
64 | 47, 63 | sylbid 239 |
. . . . . . . . 9
β’ ((((π β LMod β§ π β π΅) β§ βπ β π ((π Β· π) = π β π = 0 )) β§ π β (π βm {π})) β ((π Ξ£g (π₯ β {π} β¦ ((πβπ₯)( Β·π
βπ)π₯))) = π β (πβπ) = 0 )) |
65 | 64 | adantld 492 |
. . . . . . . 8
β’ ((((π β LMod β§ π β π΅) β§ βπ β π ((π Β· π) = π β π = 0 )) β§ π β (π βm {π})) β ((π finSupp 0 β§ (π Ξ£g (π₯ β {π} β¦ ((πβπ₯)( Β·π
βπ)π₯))) = π) β (πβπ) = 0 )) |
66 | 23, 65 | sylbid 239 |
. . . . . . 7
β’ ((((π β LMod β§ π β π΅) β§ βπ β π ((π Β· π) = π β π = 0 )) β§ π β (π βm {π})) β ((π finSupp 0 β§ (π( linC βπ){π}) = π) β (πβπ) = 0 )) |
67 | 66 | ralrimiva 3140 |
. . . . . 6
β’ (((π β LMod β§ π β π΅) β§ βπ β π ((π Β· π) = π β π = 0 )) β βπ β (π βm {π})((π finSupp 0 β§ (π( linC βπ){π}) = π) β (πβπ) = 0 )) |
68 | 67 | ex 414 |
. . . . 5
β’ ((π β LMod β§ π β π΅) β (βπ β π ((π Β· π) = π β π = 0 ) β βπ β (π βm {π})((π finSupp 0 β§ (π( linC βπ){π}) = π) β (πβπ) = 0 ))) |
69 | | impexp 452 |
. . . . . . . 8
β’ (((π finSupp 0 β§ (π( linC βπ){π}) = π) β (πβπ) = 0 ) β (π finSupp 0 β ((π( linC βπ){π}) = π β (πβπ) = 0 ))) |
70 | 28 | adantl 483 |
. . . . . . . . . 10
β’ (((π β LMod β§ π β π΅) β§ π β (π βm {π})) β π:{π}βΆπ) |
71 | | snfi 8994 |
. . . . . . . . . . 11
β’ {π} β Fin |
72 | 71 | a1i 11 |
. . . . . . . . . 10
β’ (((π β LMod β§ π β π΅) β§ π β (π βm {π})) β {π} β Fin) |
73 | | snlindsntor.0 |
. . . . . . . . . . . 12
β’ 0 =
(0gβπ
) |
74 | 73 | fvexi 6860 |
. . . . . . . . . . 11
β’ 0 β
V |
75 | 74 | a1i 11 |
. . . . . . . . . 10
β’ (((π β LMod β§ π β π΅) β§ π β (π βm {π})) β 0 β V) |
76 | 70, 72, 75 | fdmfifsupp 9323 |
. . . . . . . . 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 3161 |
. . . . . 6
β’ ((π β LMod β§ π β π΅) β (βπ β (π βm {π})((π finSupp 0 β§ (π( linC βπ){π}) = π) β (πβπ) = 0 ) β βπ β (π βm {π})((π( linC βπ){π}) = π β (πβπ) = 0 ))) |
81 | | snlindsntor.z |
. . . . . . 7
β’ π = (0gβπ) |
82 | 17, 9, 8, 73, 81, 51 | snlindsntorlem 46641 |
. . . . . 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 6855 |
. . . . . . . . 9
β’ (π¦ = π β ((πβπ¦) = 0 β (πβπ) = 0 )) |
86 | 85 | ralsng 4638 |
. . . . . . . 8
β’ (π β π΅ β (βπ¦ β {π} (πβπ¦) = 0 β (πβπ) = 0 )) |
87 | 86 | adantl 483 |
. . . . . . 7
β’ ((π β LMod β§ π β π΅) β (βπ¦ β {π} (πβπ¦) = 0 β (πβπ) = 0 )) |
88 | 87 | bicomd 222 |
. . . . . 6
β’ ((π β LMod β§ π β π΅) β ((πβπ) = 0 β βπ¦ β {π} (πβπ¦) = 0 )) |
89 | 88 | imbi2d 341 |
. . . . 5
β’ ((π β LMod β§ π β π΅) β (((π finSupp 0 β§ (π( linC βπ){π}) = π) β (πβπ) = 0 ) β ((π finSupp 0 β§ (π( linC βπ){π}) = π) β βπ¦ β {π} (πβπ¦) = 0 ))) |
90 | 89 | ralbidv 3171 |
. . . 4
β’ ((π β LMod β§ π β π΅) β (βπ β (π βm {π})((π finSupp 0 β§ (π( linC βπ){π}) = π) β (πβπ) = 0 ) β βπ β (π βm {π})((π finSupp 0 β§ (π( linC βπ){π}) = π) β βπ¦ β {π} (πβπ¦) = 0 ))) |
91 | | snelpwi 5404 |
. . . . . 6
β’ (π β π΅ β {π} β π« π΅) |
92 | 91 | adantl 483 |
. . . . 5
β’ ((π β LMod β§ π β π΅) β {π} β π« π΅) |
93 | 92 | biantrurd 534 |
. . . 4
β’ ((π β LMod β§ π β π΅) β (βπ β (π βm {π})((π finSupp 0 β§ (π( linC βπ){π}) = π) β βπ¦ β {π} (πβπ¦) = 0 ) β ({π} β π« π΅ β§ βπ β (π βm {π})((π finSupp 0 β§ (π( linC βπ){π}) = π) β βπ¦ β {π} (πβπ¦) = 0 )))) |
94 | 84, 90, 93 | 3bitrd 305 |
. . 3
β’ ((π β LMod β§ π β π΅) β (βπ β π ((π Β· π) = π β π = 0 ) β ({π} β π« π΅ β§ βπ β (π βm {π})((π finSupp 0 β§ (π( linC βπ){π}) = π) β βπ¦ β {π} (πβπ¦) = 0 )))) |
95 | 4, 94 | bitrid 283 |
. 2
β’ ((π β LMod β§ π β π΅) β (βπ β (π β { 0 })(π Β· π) β π β ({π} β π« π΅ β§ βπ β (π βm {π})((π finSupp 0 β§ (π( linC βπ){π}) = π) β βπ¦ β {π} (πβπ¦) = 0 )))) |
96 | | snex 5392 |
. . 3
β’ {π} β V |
97 | 17, 81, 9, 8, 73 | islininds 46617 |
. . 3
β’ (({π} β V β§ π β LMod) β ({π} linIndS π β ({π} β π« π΅ β§ βπ β (π βm {π})((π finSupp 0 β§ (π( linC βπ){π}) = π) β βπ¦ β {π} (πβπ¦) = 0 )))) |
98 | 96, 5, 97 | sylancr 588 |
. 2
β’ ((π β LMod β§ π β π΅) β ({π} linIndS π β ({π} β π« π΅ β§ βπ β (π βm {π})((π finSupp 0 β§ (π( linC βπ){π}) = π) β βπ¦ β {π} (πβπ¦) = 0 )))) |
99 | 95, 98 | bitr4d 282 |
1
β’ ((π β LMod β§ π β π΅) β (βπ β (π β { 0 })(π Β· π) β π β {π} linIndS π)) |