Step | Hyp | Ref
| Expression |
1 | | pjdm2.v |
. . 3
β’ π = (Baseβπ) |
2 | | pjdm2.l |
. . 3
β’ πΏ = (LSubSpβπ) |
3 | | pjdm2.o |
. . 3
β’ β₯ =
(ocvβπ) |
4 | | eqid 2733 |
. . 3
β’
(proj1βπ) = (proj1βπ) |
5 | | pjdm2.k |
. . 3
β’ πΎ = (projβπ) |
6 | 1, 2, 3, 4, 5 | pjdm 21129 |
. 2
β’ (π β dom πΎ β (π β πΏ β§ (π(proj1βπ)( β₯ βπ)):πβΆπ)) |
7 | | eqid 2733 |
. . . . . 6
β’
(+gβπ) = (+gβπ) |
8 | | pjdm2.s |
. . . . . 6
β’ β =
(LSSumβπ) |
9 | | eqid 2733 |
. . . . . 6
β’
(0gβπ) = (0gβπ) |
10 | | eqid 2733 |
. . . . . 6
β’
(Cntzβπ) =
(Cntzβπ) |
11 | | phllmod 21050 |
. . . . . . . . 9
β’ (π β PreHil β π β LMod) |
12 | 11 | adantr 482 |
. . . . . . . 8
β’ ((π β PreHil β§ π β πΏ) β π β LMod) |
13 | 2 | lsssssubg 20434 |
. . . . . . . 8
β’ (π β LMod β πΏ β (SubGrpβπ)) |
14 | 12, 13 | syl 17 |
. . . . . . 7
β’ ((π β PreHil β§ π β πΏ) β πΏ β (SubGrpβπ)) |
15 | | simpr 486 |
. . . . . . 7
β’ ((π β PreHil β§ π β πΏ) β π β πΏ) |
16 | 14, 15 | sseldd 3946 |
. . . . . 6
β’ ((π β PreHil β§ π β πΏ) β π β (SubGrpβπ)) |
17 | 1, 2 | lssss 20412 |
. . . . . . . 8
β’ (π β πΏ β π β π) |
18 | 1, 3, 2 | ocvlss 21092 |
. . . . . . . 8
β’ ((π β PreHil β§ π β π) β ( β₯ βπ) β πΏ) |
19 | 17, 18 | sylan2 594 |
. . . . . . 7
β’ ((π β PreHil β§ π β πΏ) β ( β₯ βπ) β πΏ) |
20 | 14, 19 | sseldd 3946 |
. . . . . 6
β’ ((π β PreHil β§ π β πΏ) β ( β₯ βπ) β (SubGrpβπ)) |
21 | 3, 2, 9 | ocvin 21094 |
. . . . . 6
β’ ((π β PreHil β§ π β πΏ) β (π β© ( β₯ βπ)) = {(0gβπ)}) |
22 | | lmodabl 20384 |
. . . . . . . 8
β’ (π β LMod β π β Abel) |
23 | 12, 22 | syl 17 |
. . . . . . 7
β’ ((π β PreHil β§ π β πΏ) β π β Abel) |
24 | 10, 23, 16, 20 | ablcntzd 19640 |
. . . . . 6
β’ ((π β PreHil β§ π β πΏ) β π β ((Cntzβπ)β( β₯ βπ))) |
25 | 7, 8, 9, 10, 16, 20, 21, 24, 4 | pj1f 19484 |
. . . . 5
β’ ((π β PreHil β§ π β πΏ) β (π(proj1βπ)( β₯ βπ)):(π β ( β₯
βπ))βΆπ) |
26 | 17 | adantl 483 |
. . . . 5
β’ ((π β PreHil β§ π β πΏ) β π β π) |
27 | 25, 26 | fssd 6687 |
. . . 4
β’ ((π β PreHil β§ π β πΏ) β (π(proj1βπ)( β₯ βπ)):(π β ( β₯
βπ))βΆπ) |
28 | | fdm 6678 |
. . . . . . 7
β’ ((π(proj1βπ)( β₯ βπ)):(π β ( β₯
βπ))βΆπ β dom (π(proj1βπ)( β₯ βπ)) = (π β ( β₯
βπ))) |
29 | 28 | eqcomd 2739 |
. . . . . 6
β’ ((π(proj1βπ)( β₯ βπ)):(π β ( β₯
βπ))βΆπ β (π β ( β₯
βπ)) = dom (π(proj1βπ)( β₯ βπ))) |
30 | | fdm 6678 |
. . . . . . 7
β’ ((π(proj1βπ)( β₯ βπ)):πβΆπ β dom (π(proj1βπ)( β₯ βπ)) = π) |
31 | 30 | eqeq2d 2744 |
. . . . . 6
β’ ((π(proj1βπ)( β₯ βπ)):πβΆπ β ((π β ( β₯
βπ)) = dom (π(proj1βπ)( β₯ βπ)) β (π β ( β₯
βπ)) = π)) |
32 | 29, 31 | syl5ibcom 244 |
. . . . 5
β’ ((π(proj1βπ)( β₯ βπ)):(π β ( β₯
βπ))βΆπ β ((π(proj1βπ)( β₯ βπ)):πβΆπ β (π β ( β₯
βπ)) = π)) |
33 | | feq2 6651 |
. . . . . 6
β’ ((π β ( β₯
βπ)) = π β ((π(proj1βπ)( β₯ βπ)):(π β ( β₯
βπ))βΆπ β (π(proj1βπ)( β₯ βπ)):πβΆπ)) |
34 | 33 | biimpcd 249 |
. . . . 5
β’ ((π(proj1βπ)( β₯ βπ)):(π β ( β₯
βπ))βΆπ β ((π β ( β₯
βπ)) = π β (π(proj1βπ)( β₯ βπ)):πβΆπ)) |
35 | 32, 34 | impbid 211 |
. . . 4
β’ ((π(proj1βπ)( β₯ βπ)):(π β ( β₯
βπ))βΆπ β ((π(proj1βπ)( β₯ βπ)):πβΆπ β (π β ( β₯
βπ)) = π)) |
36 | 27, 35 | syl 17 |
. . 3
β’ ((π β PreHil β§ π β πΏ) β ((π(proj1βπ)( β₯ βπ)):πβΆπ β (π β ( β₯
βπ)) = π)) |
37 | 36 | pm5.32da 580 |
. 2
β’ (π β PreHil β ((π β πΏ β§ (π(proj1βπ)( β₯ βπ)):πβΆπ) β (π β πΏ β§ (π β ( β₯
βπ)) = π))) |
38 | 6, 37 | bitrid 283 |
1
β’ (π β PreHil β (π β dom πΎ β (π β πΏ β§ (π β ( β₯
βπ)) = π))) |