Step | Hyp | Ref
| Expression |
1 | | lindsrng01.r |
. . . . . . . . 9
β’ π
= (Scalarβπ) |
2 | | lindsrng01.e |
. . . . . . . . 9
β’ πΈ = (Baseβπ
) |
3 | 1, 2 | lmodsn0 20484 |
. . . . . . . 8
β’ (π β LMod β πΈ β β
) |
4 | 2 | fvexi 6905 |
. . . . . . . . . 10
β’ πΈ β V |
5 | | hasheq0 14322 |
. . . . . . . . . 10
β’ (πΈ β V β
((β―βπΈ) = 0
β πΈ =
β
)) |
6 | 4, 5 | ax-mp 5 |
. . . . . . . . 9
β’
((β―βπΈ) =
0 β πΈ =
β
) |
7 | | eqneqall 2951 |
. . . . . . . . . 10
β’ (πΈ = β
β (πΈ β β
β π linIndS π)) |
8 | 7 | com12 32 |
. . . . . . . . 9
β’ (πΈ β β
β (πΈ = β
β π linIndS π)) |
9 | 6, 8 | biimtrid 241 |
. . . . . . . 8
β’ (πΈ β β
β
((β―βπΈ) = 0
β π linIndS π)) |
10 | 3, 9 | syl 17 |
. . . . . . 7
β’ (π β LMod β
((β―βπΈ) = 0
β π linIndS π)) |
11 | 10 | adantr 481 |
. . . . . 6
β’ ((π β LMod β§ π β π« π΅) β ((β―βπΈ) = 0 β π linIndS π)) |
12 | 11 | com12 32 |
. . . . 5
β’
((β―βπΈ) =
0 β ((π β LMod
β§ π β π«
π΅) β π linIndS π)) |
13 | 1 | lmodring 20478 |
. . . . . . . . 9
β’ (π β LMod β π
β Ring) |
14 | 13 | adantr 481 |
. . . . . . . 8
β’ ((π β LMod β§ π β π« π΅) β π
β Ring) |
15 | | eqid 2732 |
. . . . . . . . 9
β’
(0gβπ
) = (0gβπ
) |
16 | 2, 15 | 0ring 20302 |
. . . . . . . 8
β’ ((π
β Ring β§
(β―βπΈ) = 1)
β πΈ =
{(0gβπ
)}) |
17 | 14, 16 | sylan 580 |
. . . . . . 7
β’ (((π β LMod β§ π β π« π΅) β§ (β―βπΈ) = 1) β πΈ = {(0gβπ
)}) |
18 | | simpr 485 |
. . . . . . . . . 10
β’ ((π β LMod β§ π β π« π΅) β π β π« π΅) |
19 | 18 | adantr 481 |
. . . . . . . . 9
β’ (((π β LMod β§ π β π« π΅) β§ (β―βπΈ) = 1) β π β π« π΅) |
20 | 19 | adantl 482 |
. . . . . . . 8
β’ ((πΈ = {(0gβπ
)} β§ ((π β LMod β§ π β π« π΅) β§ (β―βπΈ) = 1)) β π β π« π΅) |
21 | | snex 5431 |
. . . . . . . . . . . . . 14
β’
{(0gβπ
)} β V |
22 | 19, 21 | jctil 520 |
. . . . . . . . . . . . 13
β’ (((π β LMod β§ π β π« π΅) β§ (β―βπΈ) = 1) β
({(0gβπ
)}
β V β§ π β
π« π΅)) |
23 | 22 | adantl 482 |
. . . . . . . . . . . 12
β’ ((πΈ = {(0gβπ
)} β§ ((π β LMod β§ π β π« π΅) β§ (β―βπΈ) = 1)) β ({(0gβπ
)} β V β§ π β π« π΅)) |
24 | | elmapg 8832 |
. . . . . . . . . . . 12
β’
(({(0gβπ
)} β V β§ π β π« π΅) β (π β ({(0gβπ
)} βm π) β π:πβΆ{(0gβπ
)})) |
25 | 23, 24 | syl 17 |
. . . . . . . . . . 11
β’ ((πΈ = {(0gβπ
)} β§ ((π β LMod β§ π β π« π΅) β§ (β―βπΈ) = 1)) β (π β ({(0gβπ
)} βm π) β π:πβΆ{(0gβπ
)})) |
26 | | fvex 6904 |
. . . . . . . . . . . . . 14
β’
(0gβπ
) β V |
27 | 26 | fconst2 7205 |
. . . . . . . . . . . . 13
β’ (π:πβΆ{(0gβπ
)} β π = (π Γ {(0gβπ
)})) |
28 | | fconstmpt 5738 |
. . . . . . . . . . . . . 14
β’ (π Γ
{(0gβπ
)})
= (π₯ β π β¦
(0gβπ
)) |
29 | 28 | eqeq2i 2745 |
. . . . . . . . . . . . 13
β’ (π = (π Γ {(0gβπ
)}) β π = (π₯ β π β¦ (0gβπ
))) |
30 | 27, 29 | bitri 274 |
. . . . . . . . . . . 12
β’ (π:πβΆ{(0gβπ
)} β π = (π₯ β π β¦ (0gβπ
))) |
31 | | eqidd 2733 |
. . . . . . . . . . . . . . . 16
β’ (((πΈ = {(0gβπ
)} β§ ((π β LMod β§ π β π« π΅) β§ (β―βπΈ) = 1)) β§ π£ β π) β (π₯ β π β¦ (0gβπ
)) = (π₯ β π β¦ (0gβπ
))) |
32 | | eqidd 2733 |
. . . . . . . . . . . . . . . 16
β’ ((((πΈ = {(0gβπ
)} β§ ((π β LMod β§ π β π« π΅) β§ (β―βπΈ) = 1)) β§ π£ β π) β§ π₯ = π£) β (0gβπ
) = (0gβπ
)) |
33 | | simpr 485 |
. . . . . . . . . . . . . . . 16
β’ (((πΈ = {(0gβπ
)} β§ ((π β LMod β§ π β π« π΅) β§ (β―βπΈ) = 1)) β§ π£ β π) β π£ β π) |
34 | | fvexd 6906 |
. . . . . . . . . . . . . . . 16
β’ (((πΈ = {(0gβπ
)} β§ ((π β LMod β§ π β π« π΅) β§ (β―βπΈ) = 1)) β§ π£ β π) β (0gβπ
) β V) |
35 | 31, 32, 33, 34 | fvmptd 7005 |
. . . . . . . . . . . . . . 15
β’ (((πΈ = {(0gβπ
)} β§ ((π β LMod β§ π β π« π΅) β§ (β―βπΈ) = 1)) β§ π£ β π) β ((π₯ β π β¦ (0gβπ
))βπ£) = (0gβπ
)) |
36 | 35 | ralrimiva 3146 |
. . . . . . . . . . . . . 14
β’ ((πΈ = {(0gβπ
)} β§ ((π β LMod β§ π β π« π΅) β§ (β―βπΈ) = 1)) β βπ£ β π ((π₯ β π β¦ (0gβπ
))βπ£) = (0gβπ
)) |
37 | 36 | a1d 25 |
. . . . . . . . . . . . 13
β’ ((πΈ = {(0gβπ
)} β§ ((π β LMod β§ π β π« π΅) β§ (β―βπΈ) = 1)) β (((π₯ β π β¦ (0gβπ
)) finSupp
(0gβπ
)
β§ ((π₯ β π β¦
(0gβπ
))(
linC βπ)π) = (0gβπ)) β βπ£ β π ((π₯ β π β¦ (0gβπ
))βπ£) = (0gβπ
))) |
38 | | breq1 5151 |
. . . . . . . . . . . . . . 15
β’ (π = (π₯ β π β¦ (0gβπ
)) β (π finSupp (0gβπ
) β (π₯ β π β¦ (0gβπ
)) finSupp
(0gβπ
))) |
39 | | oveq1 7415 |
. . . . . . . . . . . . . . . 16
β’ (π = (π₯ β π β¦ (0gβπ
)) β (π( linC βπ)π) = ((π₯ β π β¦ (0gβπ
))( linC βπ)π)) |
40 | 39 | eqeq1d 2734 |
. . . . . . . . . . . . . . 15
β’ (π = (π₯ β π β¦ (0gβπ
)) β ((π( linC βπ)π) = (0gβπ) β ((π₯ β π β¦ (0gβπ
))( linC βπ)π) = (0gβπ))) |
41 | 38, 40 | anbi12d 631 |
. . . . . . . . . . . . . 14
β’ (π = (π₯ β π β¦ (0gβπ
)) β ((π finSupp (0gβπ
) β§ (π( linC βπ)π) = (0gβπ)) β ((π₯ β π β¦ (0gβπ
)) finSupp
(0gβπ
)
β§ ((π₯ β π β¦
(0gβπ
))(
linC βπ)π) = (0gβπ)))) |
42 | | fveq1 6890 |
. . . . . . . . . . . . . . . 16
β’ (π = (π₯ β π β¦ (0gβπ
)) β (πβπ£) = ((π₯ β π β¦ (0gβπ
))βπ£)) |
43 | 42 | eqeq1d 2734 |
. . . . . . . . . . . . . . 15
β’ (π = (π₯ β π β¦ (0gβπ
)) β ((πβπ£) = (0gβπ
) β ((π₯ β π β¦ (0gβπ
))βπ£) = (0gβπ
))) |
44 | 43 | ralbidv 3177 |
. . . . . . . . . . . . . 14
β’ (π = (π₯ β π β¦ (0gβπ
)) β (βπ£ β π (πβπ£) = (0gβπ
) β βπ£ β π ((π₯ β π β¦ (0gβπ
))βπ£) = (0gβπ
))) |
45 | 41, 44 | imbi12d 344 |
. . . . . . . . . . . . 13
β’ (π = (π₯ β π β¦ (0gβπ
)) β (((π finSupp (0gβπ
) β§ (π( linC βπ)π) = (0gβπ)) β βπ£ β π (πβπ£) = (0gβπ
)) β (((π₯ β π β¦ (0gβπ
)) finSupp
(0gβπ
)
β§ ((π₯ β π β¦
(0gβπ
))(
linC βπ)π) = (0gβπ)) β βπ£ β π ((π₯ β π β¦ (0gβπ
))βπ£) = (0gβπ
)))) |
46 | 37, 45 | syl5ibrcom 246 |
. . . . . . . . . . . 12
β’ ((πΈ = {(0gβπ
)} β§ ((π β LMod β§ π β π« π΅) β§ (β―βπΈ) = 1)) β (π = (π₯ β π β¦ (0gβπ
)) β ((π finSupp (0gβπ
) β§ (π( linC βπ)π) = (0gβπ)) β βπ£ β π (πβπ£) = (0gβπ
)))) |
47 | 30, 46 | biimtrid 241 |
. . . . . . . . . . 11
β’ ((πΈ = {(0gβπ
)} β§ ((π β LMod β§ π β π« π΅) β§ (β―βπΈ) = 1)) β (π:πβΆ{(0gβπ
)} β ((π finSupp (0gβπ
) β§ (π( linC βπ)π) = (0gβπ)) β βπ£ β π (πβπ£) = (0gβπ
)))) |
48 | 25, 47 | sylbid 239 |
. . . . . . . . . 10
β’ ((πΈ = {(0gβπ
)} β§ ((π β LMod β§ π β π« π΅) β§ (β―βπΈ) = 1)) β (π β ({(0gβπ
)} βm π) β ((π finSupp (0gβπ
) β§ (π( linC βπ)π) = (0gβπ)) β βπ£ β π (πβπ£) = (0gβπ
)))) |
49 | 48 | ralrimiv 3145 |
. . . . . . . . 9
β’ ((πΈ = {(0gβπ
)} β§ ((π β LMod β§ π β π« π΅) β§ (β―βπΈ) = 1)) β βπ β ({(0gβπ
)} βm π)((π finSupp (0gβπ
) β§ (π( linC βπ)π) = (0gβπ)) β βπ£ β π (πβπ£) = (0gβπ
))) |
50 | | oveq1 7415 |
. . . . . . . . . . 11
β’ (πΈ = {(0gβπ
)} β (πΈ βm π) = ({(0gβπ
)} βm π)) |
51 | 50 | raleqdv 3325 |
. . . . . . . . . 10
β’ (πΈ = {(0gβπ
)} β (βπ β (πΈ βm π)((π finSupp (0gβπ
) β§ (π( linC βπ)π) = (0gβπ)) β βπ£ β π (πβπ£) = (0gβπ
)) β βπ β ({(0gβπ
)} βm π)((π finSupp (0gβπ
) β§ (π( linC βπ)π) = (0gβπ)) β βπ£ β π (πβπ£) = (0gβπ
)))) |
52 | 51 | adantr 481 |
. . . . . . . . 9
β’ ((πΈ = {(0gβπ
)} β§ ((π β LMod β§ π β π« π΅) β§ (β―βπΈ) = 1)) β (βπ β (πΈ βm π)((π finSupp (0gβπ
) β§ (π( linC βπ)π) = (0gβπ)) β βπ£ β π (πβπ£) = (0gβπ
)) β βπ β ({(0gβπ
)} βm π)((π finSupp (0gβπ
) β§ (π( linC βπ)π) = (0gβπ)) β βπ£ β π (πβπ£) = (0gβπ
)))) |
53 | 49, 52 | mpbird 256 |
. . . . . . . 8
β’ ((πΈ = {(0gβπ
)} β§ ((π β LMod β§ π β π« π΅) β§ (β―βπΈ) = 1)) β βπ β (πΈ βm π)((π finSupp (0gβπ
) β§ (π( linC βπ)π) = (0gβπ)) β βπ£ β π (πβπ£) = (0gβπ
))) |
54 | | simpl 483 |
. . . . . . . . . . 11
β’ (((π β LMod β§ π β π« π΅) β§ (β―βπΈ) = 1) β (π β LMod β§ π β π« π΅)) |
55 | 54 | ancomd 462 |
. . . . . . . . . 10
β’ (((π β LMod β§ π β π« π΅) β§ (β―βπΈ) = 1) β (π β π« π΅ β§ π β LMod)) |
56 | 55 | adantl 482 |
. . . . . . . . 9
β’ ((πΈ = {(0gβπ
)} β§ ((π β LMod β§ π β π« π΅) β§ (β―βπΈ) = 1)) β (π β π« π΅ β§ π β LMod)) |
57 | | lindsrng01.b |
. . . . . . . . . 10
β’ π΅ = (Baseβπ) |
58 | | eqid 2732 |
. . . . . . . . . 10
β’
(0gβπ) = (0gβπ) |
59 | 57, 58, 1, 2, 15 | islininds 47117 |
. . . . . . . . 9
β’ ((π β π« π΅ β§ π β LMod) β (π linIndS π β (π β π« π΅ β§ βπ β (πΈ βm π)((π finSupp (0gβπ
) β§ (π( linC βπ)π) = (0gβπ)) β βπ£ β π (πβπ£) = (0gβπ
))))) |
60 | 56, 59 | syl 17 |
. . . . . . . 8
β’ ((πΈ = {(0gβπ
)} β§ ((π β LMod β§ π β π« π΅) β§ (β―βπΈ) = 1)) β (π linIndS π β (π β π« π΅ β§ βπ β (πΈ βm π)((π finSupp (0gβπ
) β§ (π( linC βπ)π) = (0gβπ)) β βπ£ β π (πβπ£) = (0gβπ
))))) |
61 | 20, 53, 60 | mpbir2and 711 |
. . . . . . 7
β’ ((πΈ = {(0gβπ
)} β§ ((π β LMod β§ π β π« π΅) β§ (β―βπΈ) = 1)) β π linIndS π) |
62 | 17, 61 | mpancom 686 |
. . . . . 6
β’ (((π β LMod β§ π β π« π΅) β§ (β―βπΈ) = 1) β π linIndS π) |
63 | 62 | expcom 414 |
. . . . 5
β’
((β―βπΈ) =
1 β ((π β LMod
β§ π β π«
π΅) β π linIndS π)) |
64 | 12, 63 | jaoi 855 |
. . . 4
β’
(((β―βπΈ)
= 0 β¨ (β―βπΈ)
= 1) β ((π β LMod
β§ π β π«
π΅) β π linIndS π)) |
65 | 64 | expd 416 |
. . 3
β’
(((β―βπΈ)
= 0 β¨ (β―βπΈ)
= 1) β (π β LMod
β (π β π«
π΅ β π linIndS π))) |
66 | 65 | com12 32 |
. 2
β’ (π β LMod β
(((β―βπΈ) = 0
β¨ (β―βπΈ) = 1)
β (π β π«
π΅ β π linIndS π))) |
67 | 66 | 3imp 1111 |
1
β’ ((π β LMod β§
((β―βπΈ) = 0 β¨
(β―βπΈ) = 1)
β§ π β π«
π΅) β π linIndS π) |