Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . . 4
β’
(Baseβπ) =
(Baseβπ) |
2 | | eqid 2733 |
. . . 4
β’
(Scalarβπ) =
(Scalarβπ) |
3 | | eqid 2733 |
. . . 4
β’
(0gβ(Scalarβπ)) =
(0gβ(Scalarβπ)) |
4 | | lkrlss.f |
. . . 4
β’ πΉ = (LFnlβπ) |
5 | | lkrlss.k |
. . . 4
β’ πΎ = (LKerβπ) |
6 | 1, 2, 3, 4, 5 | lkrval2 37598 |
. . 3
β’ ((π β LMod β§ πΊ β πΉ) β (πΎβπΊ) = {π₯ β (Baseβπ) β£ (πΊβπ₯) = (0gβ(Scalarβπ))}) |
7 | | ssrab2 4038 |
. . 3
β’ {π₯ β (Baseβπ) β£ (πΊβπ₯) = (0gβ(Scalarβπ))} β (Baseβπ) |
8 | 6, 7 | eqsstrdi 3999 |
. 2
β’ ((π β LMod β§ πΊ β πΉ) β (πΎβπΊ) β (Baseβπ)) |
9 | | eqid 2733 |
. . . . . 6
β’
(0gβπ) = (0gβπ) |
10 | 1, 9 | lmod0vcl 20366 |
. . . . 5
β’ (π β LMod β
(0gβπ)
β (Baseβπ)) |
11 | 10 | adantr 482 |
. . . 4
β’ ((π β LMod β§ πΊ β πΉ) β (0gβπ) β (Baseβπ)) |
12 | 2, 3, 9, 4 | lfl0 37573 |
. . . 4
β’ ((π β LMod β§ πΊ β πΉ) β (πΊβ(0gβπ)) =
(0gβ(Scalarβπ))) |
13 | 1, 2, 3, 4, 5 | ellkr 37597 |
. . . 4
β’ ((π β LMod β§ πΊ β πΉ) β ((0gβπ) β (πΎβπΊ) β ((0gβπ) β (Baseβπ) β§ (πΊβ(0gβπ)) =
(0gβ(Scalarβπ))))) |
14 | 11, 12, 13 | mpbir2and 712 |
. . 3
β’ ((π β LMod β§ πΊ β πΉ) β (0gβπ) β (πΎβπΊ)) |
15 | 14 | ne0d 4296 |
. 2
β’ ((π β LMod β§ πΊ β πΉ) β (πΎβπΊ) β β
) |
16 | | simplll 774 |
. . . . . 6
β’ ((((π β LMod β§ πΊ β πΉ) β§ π β (Baseβ(Scalarβπ))) β§ (π₯ β (πΎβπΊ) β§ π¦ β (πΎβπΊ))) β π β LMod) |
17 | | simplr 768 |
. . . . . . 7
β’ ((((π β LMod β§ πΊ β πΉ) β§ π β (Baseβ(Scalarβπ))) β§ (π₯ β (πΎβπΊ) β§ π¦ β (πΎβπΊ))) β π β (Baseβ(Scalarβπ))) |
18 | | simpllr 775 |
. . . . . . . 8
β’ ((((π β LMod β§ πΊ β πΉ) β§ π β (Baseβ(Scalarβπ))) β§ (π₯ β (πΎβπΊ) β§ π¦ β (πΎβπΊ))) β πΊ β πΉ) |
19 | | simprl 770 |
. . . . . . . 8
β’ ((((π β LMod β§ πΊ β πΉ) β§ π β (Baseβ(Scalarβπ))) β§ (π₯ β (πΎβπΊ) β§ π¦ β (πΎβπΊ))) β π₯ β (πΎβπΊ)) |
20 | 1, 4, 5 | lkrcl 37600 |
. . . . . . . 8
β’ ((π β LMod β§ πΊ β πΉ β§ π₯ β (πΎβπΊ)) β π₯ β (Baseβπ)) |
21 | 16, 18, 19, 20 | syl3anc 1372 |
. . . . . . 7
β’ ((((π β LMod β§ πΊ β πΉ) β§ π β (Baseβ(Scalarβπ))) β§ (π₯ β (πΎβπΊ) β§ π¦ β (πΎβπΊ))) β π₯ β (Baseβπ)) |
22 | | eqid 2733 |
. . . . . . . 8
β’ (
Β·π βπ) = ( Β·π
βπ) |
23 | | eqid 2733 |
. . . . . . . 8
β’
(Baseβ(Scalarβπ)) = (Baseβ(Scalarβπ)) |
24 | 1, 2, 22, 23 | lmodvscl 20354 |
. . . . . . 7
β’ ((π β LMod β§ π β
(Baseβ(Scalarβπ)) β§ π₯ β (Baseβπ)) β (π( Β·π
βπ)π₯) β (Baseβπ)) |
25 | 16, 17, 21, 24 | syl3anc 1372 |
. . . . . 6
β’ ((((π β LMod β§ πΊ β πΉ) β§ π β (Baseβ(Scalarβπ))) β§ (π₯ β (πΎβπΊ) β§ π¦ β (πΎβπΊ))) β (π( Β·π
βπ)π₯) β (Baseβπ)) |
26 | | simprr 772 |
. . . . . . 7
β’ ((((π β LMod β§ πΊ β πΉ) β§ π β (Baseβ(Scalarβπ))) β§ (π₯ β (πΎβπΊ) β§ π¦ β (πΎβπΊ))) β π¦ β (πΎβπΊ)) |
27 | 1, 4, 5 | lkrcl 37600 |
. . . . . . 7
β’ ((π β LMod β§ πΊ β πΉ β§ π¦ β (πΎβπΊ)) β π¦ β (Baseβπ)) |
28 | 16, 18, 26, 27 | syl3anc 1372 |
. . . . . 6
β’ ((((π β LMod β§ πΊ β πΉ) β§ π β (Baseβ(Scalarβπ))) β§ (π₯ β (πΎβπΊ) β§ π¦ β (πΎβπΊ))) β π¦ β (Baseβπ)) |
29 | | eqid 2733 |
. . . . . . 7
β’
(+gβπ) = (+gβπ) |
30 | 1, 29 | lmodvacl 20351 |
. . . . . 6
β’ ((π β LMod β§ (π(
Β·π βπ)π₯) β (Baseβπ) β§ π¦ β (Baseβπ)) β ((π( Β·π
βπ)π₯)(+gβπ)π¦) β (Baseβπ)) |
31 | 16, 25, 28, 30 | syl3anc 1372 |
. . . . 5
β’ ((((π β LMod β§ πΊ β πΉ) β§ π β (Baseβ(Scalarβπ))) β§ (π₯ β (πΎβπΊ) β§ π¦ β (πΎβπΊ))) β ((π( Β·π
βπ)π₯)(+gβπ)π¦) β (Baseβπ)) |
32 | | eqid 2733 |
. . . . . . . 8
β’
(+gβ(Scalarβπ)) =
(+gβ(Scalarβπ)) |
33 | | eqid 2733 |
. . . . . . . 8
β’
(.rβ(Scalarβπ)) =
(.rβ(Scalarβπ)) |
34 | 1, 29, 2, 22, 23, 32, 33, 4 | lfli 37569 |
. . . . . . 7
β’ ((π β LMod β§ πΊ β πΉ β§ (π β (Baseβ(Scalarβπ)) β§ π₯ β (Baseβπ) β§ π¦ β (Baseβπ))) β (πΊβ((π( Β·π
βπ)π₯)(+gβπ)π¦)) = ((π(.rβ(Scalarβπ))(πΊβπ₯))(+gβ(Scalarβπ))(πΊβπ¦))) |
35 | 16, 18, 17, 21, 28, 34 | syl113anc 1383 |
. . . . . 6
β’ ((((π β LMod β§ πΊ β πΉ) β§ π β (Baseβ(Scalarβπ))) β§ (π₯ β (πΎβπΊ) β§ π¦ β (πΎβπΊ))) β (πΊβ((π( Β·π
βπ)π₯)(+gβπ)π¦)) = ((π(.rβ(Scalarβπ))(πΊβπ₯))(+gβ(Scalarβπ))(πΊβπ¦))) |
36 | 2, 3, 4, 5 | lkrf0 37601 |
. . . . . . . . . 10
β’ ((π β LMod β§ πΊ β πΉ β§ π₯ β (πΎβπΊ)) β (πΊβπ₯) = (0gβ(Scalarβπ))) |
37 | 16, 18, 19, 36 | syl3anc 1372 |
. . . . . . . . 9
β’ ((((π β LMod β§ πΊ β πΉ) β§ π β (Baseβ(Scalarβπ))) β§ (π₯ β (πΎβπΊ) β§ π¦ β (πΎβπΊ))) β (πΊβπ₯) = (0gβ(Scalarβπ))) |
38 | 37 | oveq2d 7374 |
. . . . . . . 8
β’ ((((π β LMod β§ πΊ β πΉ) β§ π β (Baseβ(Scalarβπ))) β§ (π₯ β (πΎβπΊ) β§ π¦ β (πΎβπΊ))) β (π(.rβ(Scalarβπ))(πΊβπ₯)) = (π(.rβ(Scalarβπ))(0gβ(Scalarβπ)))) |
39 | 2 | lmodring 20344 |
. . . . . . . . . 10
β’ (π β LMod β
(Scalarβπ) β
Ring) |
40 | 16, 39 | syl 17 |
. . . . . . . . 9
β’ ((((π β LMod β§ πΊ β πΉ) β§ π β (Baseβ(Scalarβπ))) β§ (π₯ β (πΎβπΊ) β§ π¦ β (πΎβπΊ))) β (Scalarβπ) β Ring) |
41 | 23, 33, 3 | ringrz 20017 |
. . . . . . . . 9
β’
(((Scalarβπ)
β Ring β§ π β
(Baseβ(Scalarβπ))) β (π(.rβ(Scalarβπ))(0gβ(Scalarβπ))) =
(0gβ(Scalarβπ))) |
42 | 40, 17, 41 | syl2anc 585 |
. . . . . . . 8
β’ ((((π β LMod β§ πΊ β πΉ) β§ π β (Baseβ(Scalarβπ))) β§ (π₯ β (πΎβπΊ) β§ π¦ β (πΎβπΊ))) β (π(.rβ(Scalarβπ))(0gβ(Scalarβπ))) =
(0gβ(Scalarβπ))) |
43 | 38, 42 | eqtrd 2773 |
. . . . . . 7
β’ ((((π β LMod β§ πΊ β πΉ) β§ π β (Baseβ(Scalarβπ))) β§ (π₯ β (πΎβπΊ) β§ π¦ β (πΎβπΊ))) β (π(.rβ(Scalarβπ))(πΊβπ₯)) = (0gβ(Scalarβπ))) |
44 | 2, 3, 4, 5 | lkrf0 37601 |
. . . . . . . 8
β’ ((π β LMod β§ πΊ β πΉ β§ π¦ β (πΎβπΊ)) β (πΊβπ¦) = (0gβ(Scalarβπ))) |
45 | 16, 18, 26, 44 | syl3anc 1372 |
. . . . . . 7
β’ ((((π β LMod β§ πΊ β πΉ) β§ π β (Baseβ(Scalarβπ))) β§ (π₯ β (πΎβπΊ) β§ π¦ β (πΎβπΊ))) β (πΊβπ¦) = (0gβ(Scalarβπ))) |
46 | 43, 45 | oveq12d 7376 |
. . . . . 6
β’ ((((π β LMod β§ πΊ β πΉ) β§ π β (Baseβ(Scalarβπ))) β§ (π₯ β (πΎβπΊ) β§ π¦ β (πΎβπΊ))) β ((π(.rβ(Scalarβπ))(πΊβπ₯))(+gβ(Scalarβπ))(πΊβπ¦)) =
((0gβ(Scalarβπ))(+gβ(Scalarβπ))(0gβ(Scalarβπ)))) |
47 | 2 | lmodfgrp 20345 |
. . . . . . . 8
β’ (π β LMod β
(Scalarβπ) β
Grp) |
48 | 16, 47 | syl 17 |
. . . . . . 7
β’ ((((π β LMod β§ πΊ β πΉ) β§ π β (Baseβ(Scalarβπ))) β§ (π₯ β (πΎβπΊ) β§ π¦ β (πΎβπΊ))) β (Scalarβπ) β Grp) |
49 | 23, 3 | grpidcl 18783 |
. . . . . . 7
β’
((Scalarβπ)
β Grp β (0gβ(Scalarβπ)) β (Baseβ(Scalarβπ))) |
50 | 23, 32, 3 | grplid 18785 |
. . . . . . 7
β’
(((Scalarβπ)
β Grp β§ (0gβ(Scalarβπ)) β (Baseβ(Scalarβπ))) β
((0gβ(Scalarβπ))(+gβ(Scalarβπ))(0gβ(Scalarβπ))) =
(0gβ(Scalarβπ))) |
51 | 48, 49, 50 | syl2anc2 586 |
. . . . . 6
β’ ((((π β LMod β§ πΊ β πΉ) β§ π β (Baseβ(Scalarβπ))) β§ (π₯ β (πΎβπΊ) β§ π¦ β (πΎβπΊ))) β
((0gβ(Scalarβπ))(+gβ(Scalarβπ))(0gβ(Scalarβπ))) =
(0gβ(Scalarβπ))) |
52 | 35, 46, 51 | 3eqtrd 2777 |
. . . . 5
β’ ((((π β LMod β§ πΊ β πΉ) β§ π β (Baseβ(Scalarβπ))) β§ (π₯ β (πΎβπΊ) β§ π¦ β (πΎβπΊ))) β (πΊβ((π( Β·π
βπ)π₯)(+gβπ)π¦)) = (0gβ(Scalarβπ))) |
53 | 1, 2, 3, 4, 5 | ellkr 37597 |
. . . . . 6
β’ ((π β LMod β§ πΊ β πΉ) β (((π( Β·π
βπ)π₯)(+gβπ)π¦) β (πΎβπΊ) β (((π( Β·π
βπ)π₯)(+gβπ)π¦) β (Baseβπ) β§ (πΊβ((π( Β·π
βπ)π₯)(+gβπ)π¦)) = (0gβ(Scalarβπ))))) |
54 | 53 | ad2antrr 725 |
. . . . 5
β’ ((((π β LMod β§ πΊ β πΉ) β§ π β (Baseβ(Scalarβπ))) β§ (π₯ β (πΎβπΊ) β§ π¦ β (πΎβπΊ))) β (((π( Β·π
βπ)π₯)(+gβπ)π¦) β (πΎβπΊ) β (((π( Β·π
βπ)π₯)(+gβπ)π¦) β (Baseβπ) β§ (πΊβ((π( Β·π
βπ)π₯)(+gβπ)π¦)) = (0gβ(Scalarβπ))))) |
55 | 31, 52, 54 | mpbir2and 712 |
. . . 4
β’ ((((π β LMod β§ πΊ β πΉ) β§ π β (Baseβ(Scalarβπ))) β§ (π₯ β (πΎβπΊ) β§ π¦ β (πΎβπΊ))) β ((π( Β·π
βπ)π₯)(+gβπ)π¦) β (πΎβπΊ)) |
56 | 55 | ralrimivva 3194 |
. . 3
β’ (((π β LMod β§ πΊ β πΉ) β§ π β (Baseβ(Scalarβπ))) β βπ₯ β (πΎβπΊ)βπ¦ β (πΎβπΊ)((π( Β·π
βπ)π₯)(+gβπ)π¦) β (πΎβπΊ)) |
57 | 56 | ralrimiva 3140 |
. 2
β’ ((π β LMod β§ πΊ β πΉ) β βπ β (Baseβ(Scalarβπ))βπ₯ β (πΎβπΊ)βπ¦ β (πΎβπΊ)((π( Β·π
βπ)π₯)(+gβπ)π¦) β (πΎβπΊ)) |
58 | | lkrlss.s |
. . 3
β’ π = (LSubSpβπ) |
59 | 2, 23, 1, 29, 22, 58 | islss 20410 |
. 2
β’ ((πΎβπΊ) β π β ((πΎβπΊ) β (Baseβπ) β§ (πΎβπΊ) β β
β§ βπ β
(Baseβ(Scalarβπ))βπ₯ β (πΎβπΊ)βπ¦ β (πΎβπΊ)((π( Β·π
βπ)π₯)(+gβπ)π¦) β (πΎβπΊ))) |
60 | 8, 15, 57, 59 | syl3anbrc 1344 |
1
β’ ((π β LMod β§ πΊ β πΉ) β (πΎβπΊ) β π) |