Step | Hyp | Ref
| Expression |
1 | | pjf.k |
. . 3
β’ πΎ = (projβπ) |
2 | | pjf.v |
. . 3
β’ π = (Baseβπ) |
3 | 1, 2 | pjf2 21136 |
. 2
β’ ((π β PreHil β§ π β dom πΎ) β (πΎβπ):πβΆπ) |
4 | 3 | frnd 6677 |
. . 3
β’ ((π β PreHil β§ π β dom πΎ) β ran (πΎβπ) β π) |
5 | | eqid 2733 |
. . . . . . . 8
β’
(ocvβπ) =
(ocvβπ) |
6 | | eqid 2733 |
. . . . . . . 8
β’
(proj1βπ) = (proj1βπ) |
7 | 5, 6, 1 | pjval 21132 |
. . . . . . 7
β’ (π β dom πΎ β (πΎβπ) = (π(proj1βπ)((ocvβπ)βπ))) |
8 | 7 | ad2antlr 726 |
. . . . . 6
β’ (((π β PreHil β§ π β dom πΎ) β§ π₯ β π) β (πΎβπ) = (π(proj1βπ)((ocvβπ)βπ))) |
9 | 8 | fveq1d 6845 |
. . . . 5
β’ (((π β PreHil β§ π β dom πΎ) β§ π₯ β π) β ((πΎβπ)βπ₯) = ((π(proj1βπ)((ocvβπ)βπ))βπ₯)) |
10 | | eqid 2733 |
. . . . . 6
β’
(+gβπ) = (+gβπ) |
11 | | eqid 2733 |
. . . . . 6
β’
(LSSumβπ) =
(LSSumβπ) |
12 | | eqid 2733 |
. . . . . 6
β’
(0gβπ) = (0gβπ) |
13 | | eqid 2733 |
. . . . . 6
β’
(Cntzβπ) =
(Cntzβπ) |
14 | | phllmod 21050 |
. . . . . . . . 9
β’ (π β PreHil β π β LMod) |
15 | 14 | adantr 482 |
. . . . . . . 8
β’ ((π β PreHil β§ π β dom πΎ) β π β LMod) |
16 | | eqid 2733 |
. . . . . . . . 9
β’
(LSubSpβπ) =
(LSubSpβπ) |
17 | 16 | lsssssubg 20434 |
. . . . . . . 8
β’ (π β LMod β
(LSubSpβπ) β
(SubGrpβπ)) |
18 | 15, 17 | syl 17 |
. . . . . . 7
β’ ((π β PreHil β§ π β dom πΎ) β (LSubSpβπ) β (SubGrpβπ)) |
19 | 2, 16, 5, 11, 1 | pjdm2 21133 |
. . . . . . . 8
β’ (π β PreHil β (π β dom πΎ β (π β (LSubSpβπ) β§ (π(LSSumβπ)((ocvβπ)βπ)) = π))) |
20 | 19 | simprbda 500 |
. . . . . . 7
β’ ((π β PreHil β§ π β dom πΎ) β π β (LSubSpβπ)) |
21 | 18, 20 | sseldd 3946 |
. . . . . 6
β’ ((π β PreHil β§ π β dom πΎ) β π β (SubGrpβπ)) |
22 | 2, 16 | lssss 20412 |
. . . . . . . . 9
β’ (π β (LSubSpβπ) β π β π) |
23 | 20, 22 | syl 17 |
. . . . . . . 8
β’ ((π β PreHil β§ π β dom πΎ) β π β π) |
24 | 2, 5, 16 | ocvlss 21092 |
. . . . . . . 8
β’ ((π β PreHil β§ π β π) β ((ocvβπ)βπ) β (LSubSpβπ)) |
25 | 23, 24 | syldan 592 |
. . . . . . 7
β’ ((π β PreHil β§ π β dom πΎ) β ((ocvβπ)βπ) β (LSubSpβπ)) |
26 | 18, 25 | sseldd 3946 |
. . . . . 6
β’ ((π β PreHil β§ π β dom πΎ) β ((ocvβπ)βπ) β (SubGrpβπ)) |
27 | 5, 16, 12 | ocvin 21094 |
. . . . . . 7
β’ ((π β PreHil β§ π β (LSubSpβπ)) β (π β© ((ocvβπ)βπ)) = {(0gβπ)}) |
28 | 20, 27 | syldan 592 |
. . . . . 6
β’ ((π β PreHil β§ π β dom πΎ) β (π β© ((ocvβπ)βπ)) = {(0gβπ)}) |
29 | | lmodabl 20384 |
. . . . . . . 8
β’ (π β LMod β π β Abel) |
30 | 15, 29 | syl 17 |
. . . . . . 7
β’ ((π β PreHil β§ π β dom πΎ) β π β Abel) |
31 | 13, 30, 21, 26 | ablcntzd 19640 |
. . . . . 6
β’ ((π β PreHil β§ π β dom πΎ) β π β ((Cntzβπ)β((ocvβπ)βπ))) |
32 | 10, 11, 12, 13, 21, 26, 28, 31, 6 | pj1lid 19488 |
. . . . 5
β’ (((π β PreHil β§ π β dom πΎ) β§ π₯ β π) β ((π(proj1βπ)((ocvβπ)βπ))βπ₯) = π₯) |
33 | 9, 32 | eqtrd 2773 |
. . . 4
β’ (((π β PreHil β§ π β dom πΎ) β§ π₯ β π) β ((πΎβπ)βπ₯) = π₯) |
34 | 3 | ffnd 6670 |
. . . . 5
β’ ((π β PreHil β§ π β dom πΎ) β (πΎβπ) Fn π) |
35 | 23 | sselda 3945 |
. . . . 5
β’ (((π β PreHil β§ π β dom πΎ) β§ π₯ β π) β π₯ β π) |
36 | | fnfvelrn 7032 |
. . . . 5
β’ (((πΎβπ) Fn π β§ π₯ β π) β ((πΎβπ)βπ₯) β ran (πΎβπ)) |
37 | 34, 35, 36 | syl2an2r 684 |
. . . 4
β’ (((π β PreHil β§ π β dom πΎ) β§ π₯ β π) β ((πΎβπ)βπ₯) β ran (πΎβπ)) |
38 | 33, 37 | eqeltrrd 2835 |
. . 3
β’ (((π β PreHil β§ π β dom πΎ) β§ π₯ β π) β π₯ β ran (πΎβπ)) |
39 | 4, 38 | eqelssd 3966 |
. 2
β’ ((π β PreHil β§ π β dom πΎ) β ran (πΎβπ) = π) |
40 | | dffo2 6761 |
. 2
β’ ((πΎβπ):πβontoβπ β ((πΎβπ):πβΆπ β§ ran (πΎβπ) = π)) |
41 | 3, 39, 40 | sylanbrc 584 |
1
β’ ((π β PreHil β§ π β dom πΎ) β (πΎβπ):πβontoβπ) |