Step | Hyp | Ref
| Expression |
1 | | pjthlem.v |
. . . 4
β’ π = (Baseβπ) |
2 | | pjthlem.m |
. . . 4
β’ β =
(-gβπ) |
3 | | pjthlem.n |
. . . 4
β’ π = (normβπ) |
4 | | pjthlem.1 |
. . . . 5
β’ (π β π β βHil) |
5 | | hlcph 24880 |
. . . . 5
β’ (π β βHil β π β
βPreHil) |
6 | 4, 5 | syl 17 |
. . . 4
β’ (π β π β βPreHil) |
7 | | pjthlem.2 |
. . . . 5
β’ (π β π β πΏ) |
8 | | pjthlem.l |
. . . . 5
β’ πΏ = (LSubSpβπ) |
9 | 7, 8 | eleqtrdi 2843 |
. . . 4
β’ (π β π β (LSubSpβπ)) |
10 | | pjthlem.3 |
. . . . 5
β’ (π β π β (Clsdβπ½)) |
11 | | hlcms 24882 |
. . . . . . 7
β’ (π β βHil β π β CMetSp) |
12 | 4, 11 | syl 17 |
. . . . . 6
β’ (π β π β CMetSp) |
13 | 1, 8 | lssss 20546 |
. . . . . . 7
β’ (π β πΏ β π β π) |
14 | 7, 13 | syl 17 |
. . . . . 6
β’ (π β π β π) |
15 | | eqid 2732 |
. . . . . . 7
β’ (π βΎs π) = (π βΎs π) |
16 | | pjthlem.j |
. . . . . . 7
β’ π½ = (TopOpenβπ) |
17 | 15, 1, 16 | cmsss 24867 |
. . . . . 6
β’ ((π β CMetSp β§ π β π) β ((π βΎs π) β CMetSp β π β (Clsdβπ½))) |
18 | 12, 14, 17 | syl2anc 584 |
. . . . 5
β’ (π β ((π βΎs π) β CMetSp β π β (Clsdβπ½))) |
19 | 10, 18 | mpbird 256 |
. . . 4
β’ (π β (π βΎs π) β CMetSp) |
20 | | pjthlem.4 |
. . . 4
β’ (π β π΄ β π) |
21 | 1, 2, 3, 6, 9, 19,
20 | minvec 24952 |
. . 3
β’ (π β β!π₯ β π βπ¦ β π (πβ(π΄ β π₯)) β€ (πβ(π΄ β π¦))) |
22 | | reurex 3380 |
. . 3
β’
(β!π₯ β
π βπ¦ β π (πβ(π΄ β π₯)) β€ (πβ(π΄ β π¦)) β βπ₯ β π βπ¦ β π (πβ(π΄ β π₯)) β€ (πβ(π΄ β π¦))) |
23 | 21, 22 | syl 17 |
. 2
β’ (π β βπ₯ β π βπ¦ β π (πβ(π΄ β π₯)) β€ (πβ(π΄ β π¦))) |
24 | 6 | adantr 481 |
. . . . . 6
β’ ((π β§ (π₯ β π β§ βπ¦ β π (πβ(π΄ β π₯)) β€ (πβ(π΄ β π¦)))) β π β βPreHil) |
25 | | cphlmod 24690 |
. . . . . 6
β’ (π β βPreHil β
π β
LMod) |
26 | 24, 25 | syl 17 |
. . . . 5
β’ ((π β§ (π₯ β π β§ βπ¦ β π (πβ(π΄ β π₯)) β€ (πβ(π΄ β π¦)))) β π β LMod) |
27 | | lmodabl 20518 |
. . . . 5
β’ (π β LMod β π β Abel) |
28 | 26, 27 | syl 17 |
. . . 4
β’ ((π β§ (π₯ β π β§ βπ¦ β π (πβ(π΄ β π₯)) β€ (πβ(π΄ β π¦)))) β π β Abel) |
29 | 7 | adantr 481 |
. . . . . 6
β’ ((π β§ (π₯ β π β§ βπ¦ β π (πβ(π΄ β π₯)) β€ (πβ(π΄ β π¦)))) β π β πΏ) |
30 | 29, 13 | syl 17 |
. . . . 5
β’ ((π β§ (π₯ β π β§ βπ¦ β π (πβ(π΄ β π₯)) β€ (πβ(π΄ β π¦)))) β π β π) |
31 | | simprl 769 |
. . . . 5
β’ ((π β§ (π₯ β π β§ βπ¦ β π (πβ(π΄ β π₯)) β€ (πβ(π΄ β π¦)))) β π₯ β π) |
32 | 30, 31 | sseldd 3983 |
. . . 4
β’ ((π β§ (π₯ β π β§ βπ¦ β π (πβ(π΄ β π₯)) β€ (πβ(π΄ β π¦)))) β π₯ β π) |
33 | 20 | adantr 481 |
. . . 4
β’ ((π β§ (π₯ β π β§ βπ¦ β π (πβ(π΄ β π₯)) β€ (πβ(π΄ β π¦)))) β π΄ β π) |
34 | | pjthlem.p |
. . . . 5
β’ + =
(+gβπ) |
35 | 1, 34, 2 | ablpncan3 19683 |
. . . 4
β’ ((π β Abel β§ (π₯ β π β§ π΄ β π)) β (π₯ + (π΄ β π₯)) = π΄) |
36 | 28, 32, 33, 35 | syl12anc 835 |
. . 3
β’ ((π β§ (π₯ β π β§ βπ¦ β π (πβ(π΄ β π₯)) β€ (πβ(π΄ β π¦)))) β (π₯ + (π΄ β π₯)) = π΄) |
37 | 8 | lsssssubg 20568 |
. . . . . 6
β’ (π β LMod β πΏ β (SubGrpβπ)) |
38 | 26, 37 | syl 17 |
. . . . 5
β’ ((π β§ (π₯ β π β§ βπ¦ β π (πβ(π΄ β π₯)) β€ (πβ(π΄ β π¦)))) β πΏ β (SubGrpβπ)) |
39 | 38, 29 | sseldd 3983 |
. . . 4
β’ ((π β§ (π₯ β π β§ βπ¦ β π (πβ(π΄ β π₯)) β€ (πβ(π΄ β π¦)))) β π β (SubGrpβπ)) |
40 | | cphphl 24687 |
. . . . . . 7
β’ (π β βPreHil β
π β
PreHil) |
41 | 24, 40 | syl 17 |
. . . . . 6
β’ ((π β§ (π₯ β π β§ βπ¦ β π (πβ(π΄ β π₯)) β€ (πβ(π΄ β π¦)))) β π β PreHil) |
42 | | pjthlem.o |
. . . . . . 7
β’ π = (ocvβπ) |
43 | 1, 42, 8 | ocvlss 21224 |
. . . . . 6
β’ ((π β PreHil β§ π β π) β (πβπ) β πΏ) |
44 | 41, 30, 43 | syl2anc 584 |
. . . . 5
β’ ((π β§ (π₯ β π β§ βπ¦ β π (πβ(π΄ β π₯)) β€ (πβ(π΄ β π¦)))) β (πβπ) β πΏ) |
45 | 38, 44 | sseldd 3983 |
. . . 4
β’ ((π β§ (π₯ β π β§ βπ¦ β π (πβ(π΄ β π₯)) β€ (πβ(π΄ β π¦)))) β (πβπ) β (SubGrpβπ)) |
46 | 1, 2 | lmodvsubcl 20516 |
. . . . . 6
β’ ((π β LMod β§ π΄ β π β§ π₯ β π) β (π΄ β π₯) β π) |
47 | 26, 33, 32, 46 | syl3anc 1371 |
. . . . 5
β’ ((π β§ (π₯ β π β§ βπ¦ β π (πβ(π΄ β π₯)) β€ (πβ(π΄ β π¦)))) β (π΄ β π₯) β π) |
48 | | pjthlem.h |
. . . . . . . 8
β’ , =
(Β·πβπ) |
49 | 4 | ad2antrr 724 |
. . . . . . . 8
β’ (((π β§ (π₯ β π β§ βπ¦ β π (πβ(π΄ β π₯)) β€ (πβ(π΄ β π¦)))) β§ π§ β π) β π β βHil) |
50 | 29 | adantr 481 |
. . . . . . . 8
β’ (((π β§ (π₯ β π β§ βπ¦ β π (πβ(π΄ β π₯)) β€ (πβ(π΄ β π¦)))) β§ π§ β π) β π β πΏ) |
51 | 47 | adantr 481 |
. . . . . . . 8
β’ (((π β§ (π₯ β π β§ βπ¦ β π (πβ(π΄ β π₯)) β€ (πβ(π΄ β π¦)))) β§ π§ β π) β (π΄ β π₯) β π) |
52 | | simpr 485 |
. . . . . . . 8
β’ (((π β§ (π₯ β π β§ βπ¦ β π (πβ(π΄ β π₯)) β€ (πβ(π΄ β π¦)))) β§ π§ β π) β π§ β π) |
53 | | oveq2 7416 |
. . . . . . . . . . . . . 14
β’ (π¦ = (π€ + π₯) β (π΄ β π¦) = (π΄ β (π€ + π₯))) |
54 | 53 | fveq2d 6895 |
. . . . . . . . . . . . 13
β’ (π¦ = (π€ + π₯) β (πβ(π΄ β π¦)) = (πβ(π΄ β (π€ + π₯)))) |
55 | 54 | breq2d 5160 |
. . . . . . . . . . . 12
β’ (π¦ = (π€ + π₯) β ((πβ(π΄ β π₯)) β€ (πβ(π΄ β π¦)) β (πβ(π΄ β π₯)) β€ (πβ(π΄ β (π€ + π₯))))) |
56 | | simplrr 776 |
. . . . . . . . . . . 12
β’ (((π β§ (π₯ β π β§ βπ¦ β π (πβ(π΄ β π₯)) β€ (πβ(π΄ β π¦)))) β§ π€ β π) β βπ¦ β π (πβ(π΄ β π₯)) β€ (πβ(π΄ β π¦))) |
57 | 26 | adantr 481 |
. . . . . . . . . . . . 13
β’ (((π β§ (π₯ β π β§ βπ¦ β π (πβ(π΄ β π₯)) β€ (πβ(π΄ β π¦)))) β§ π€ β π) β π β LMod) |
58 | 29 | adantr 481 |
. . . . . . . . . . . . 13
β’ (((π β§ (π₯ β π β§ βπ¦ β π (πβ(π΄ β π₯)) β€ (πβ(π΄ β π¦)))) β§ π€ β π) β π β πΏ) |
59 | | simpr 485 |
. . . . . . . . . . . . 13
β’ (((π β§ (π₯ β π β§ βπ¦ β π (πβ(π΄ β π₯)) β€ (πβ(π΄ β π¦)))) β§ π€ β π) β π€ β π) |
60 | 31 | adantr 481 |
. . . . . . . . . . . . 13
β’ (((π β§ (π₯ β π β§ βπ¦ β π (πβ(π΄ β π₯)) β€ (πβ(π΄ β π¦)))) β§ π€ β π) β π₯ β π) |
61 | 34, 8 | lssvacl 20564 |
. . . . . . . . . . . . 13
β’ (((π β LMod β§ π β πΏ) β§ (π€ β π β§ π₯ β π)) β (π€ + π₯) β π) |
62 | 57, 58, 59, 60, 61 | syl22anc 837 |
. . . . . . . . . . . 12
β’ (((π β§ (π₯ β π β§ βπ¦ β π (πβ(π΄ β π₯)) β€ (πβ(π΄ β π¦)))) β§ π€ β π) β (π€ + π₯) β π) |
63 | 55, 56, 62 | rspcdva 3613 |
. . . . . . . . . . 11
β’ (((π β§ (π₯ β π β§ βπ¦ β π (πβ(π΄ β π₯)) β€ (πβ(π΄ β π¦)))) β§ π€ β π) β (πβ(π΄ β π₯)) β€ (πβ(π΄ β (π€ + π₯)))) |
64 | | lmodgrp 20477 |
. . . . . . . . . . . . . . 15
β’ (π β LMod β π β Grp) |
65 | 26, 64 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π₯ β π β§ βπ¦ β π (πβ(π΄ β π₯)) β€ (πβ(π΄ β π¦)))) β π β Grp) |
66 | 65 | adantr 481 |
. . . . . . . . . . . . 13
β’ (((π β§ (π₯ β π β§ βπ¦ β π (πβ(π΄ β π₯)) β€ (πβ(π΄ β π¦)))) β§ π€ β π) β π β Grp) |
67 | 33 | adantr 481 |
. . . . . . . . . . . . 13
β’ (((π β§ (π₯ β π β§ βπ¦ β π (πβ(π΄ β π₯)) β€ (πβ(π΄ β π¦)))) β§ π€ β π) β π΄ β π) |
68 | 32 | adantr 481 |
. . . . . . . . . . . . 13
β’ (((π β§ (π₯ β π β§ βπ¦ β π (πβ(π΄ β π₯)) β€ (πβ(π΄ β π¦)))) β§ π€ β π) β π₯ β π) |
69 | 30 | sselda 3982 |
. . . . . . . . . . . . 13
β’ (((π β§ (π₯ β π β§ βπ¦ β π (πβ(π΄ β π₯)) β€ (πβ(π΄ β π¦)))) β§ π€ β π) β π€ β π) |
70 | 1, 34, 2 | grpsubsub4 18915 |
. . . . . . . . . . . . 13
β’ ((π β Grp β§ (π΄ β π β§ π₯ β π β§ π€ β π)) β ((π΄ β π₯) β π€) = (π΄ β (π€ + π₯))) |
71 | 66, 67, 68, 69, 70 | syl13anc 1372 |
. . . . . . . . . . . 12
β’ (((π β§ (π₯ β π β§ βπ¦ β π (πβ(π΄ β π₯)) β€ (πβ(π΄ β π¦)))) β§ π€ β π) β ((π΄ β π₯) β π€) = (π΄ β (π€ + π₯))) |
72 | 71 | fveq2d 6895 |
. . . . . . . . . . 11
β’ (((π β§ (π₯ β π β§ βπ¦ β π (πβ(π΄ β π₯)) β€ (πβ(π΄ β π¦)))) β§ π€ β π) β (πβ((π΄ β π₯) β π€)) = (πβ(π΄ β (π€ + π₯)))) |
73 | 63, 72 | breqtrrd 5176 |
. . . . . . . . . 10
β’ (((π β§ (π₯ β π β§ βπ¦ β π (πβ(π΄ β π₯)) β€ (πβ(π΄ β π¦)))) β§ π€ β π) β (πβ(π΄ β π₯)) β€ (πβ((π΄ β π₯) β π€))) |
74 | 73 | ralrimiva 3146 |
. . . . . . . . 9
β’ ((π β§ (π₯ β π β§ βπ¦ β π (πβ(π΄ β π₯)) β€ (πβ(π΄ β π¦)))) β βπ€ β π (πβ(π΄ β π₯)) β€ (πβ((π΄ β π₯) β π€))) |
75 | 74 | adantr 481 |
. . . . . . . 8
β’ (((π β§ (π₯ β π β§ βπ¦ β π (πβ(π΄ β π₯)) β€ (πβ(π΄ β π¦)))) β§ π§ β π) β βπ€ β π (πβ(π΄ β π₯)) β€ (πβ((π΄ β π₯) β π€))) |
76 | | eqid 2732 |
. . . . . . . 8
β’ (((π΄ β π₯) , π§) / ((π§ , π§) + 1)) = (((π΄ β π₯) , π§) / ((π§ , π§) + 1)) |
77 | 1, 3, 34, 2, 48, 8, 49, 50, 51, 52, 75, 76 | pjthlem1 24953 |
. . . . . . 7
β’ (((π β§ (π₯ β π β§ βπ¦ β π (πβ(π΄ β π₯)) β€ (πβ(π΄ β π¦)))) β§ π§ β π) β ((π΄ β π₯) , π§) = 0) |
78 | 24 | adantr 481 |
. . . . . . . . 9
β’ (((π β§ (π₯ β π β§ βπ¦ β π (πβ(π΄ β π₯)) β€ (πβ(π΄ β π¦)))) β§ π§ β π) β π β βPreHil) |
79 | | cphclm 24705 |
. . . . . . . . 9
β’ (π β βPreHil β
π β
βMod) |
80 | 78, 79 | syl 17 |
. . . . . . . 8
β’ (((π β§ (π₯ β π β§ βπ¦ β π (πβ(π΄ β π₯)) β€ (πβ(π΄ β π¦)))) β§ π§ β π) β π β βMod) |
81 | | eqid 2732 |
. . . . . . . . 9
β’
(Scalarβπ) =
(Scalarβπ) |
82 | 81 | clm0 24587 |
. . . . . . . 8
β’ (π β βMod β 0 =
(0gβ(Scalarβπ))) |
83 | 80, 82 | syl 17 |
. . . . . . 7
β’ (((π β§ (π₯ β π β§ βπ¦ β π (πβ(π΄ β π₯)) β€ (πβ(π΄ β π¦)))) β§ π§ β π) β 0 =
(0gβ(Scalarβπ))) |
84 | 77, 83 | eqtrd 2772 |
. . . . . 6
β’ (((π β§ (π₯ β π β§ βπ¦ β π (πβ(π΄ β π₯)) β€ (πβ(π΄ β π¦)))) β§ π§ β π) β ((π΄ β π₯) , π§) = (0gβ(Scalarβπ))) |
85 | 84 | ralrimiva 3146 |
. . . . 5
β’ ((π β§ (π₯ β π β§ βπ¦ β π (πβ(π΄ β π₯)) β€ (πβ(π΄ β π¦)))) β βπ§ β π ((π΄ β π₯) , π§) = (0gβ(Scalarβπ))) |
86 | | eqid 2732 |
. . . . . 6
β’
(0gβ(Scalarβπ)) =
(0gβ(Scalarβπ)) |
87 | 1, 48, 81, 86, 42 | elocv 21220 |
. . . . 5
β’ ((π΄ β π₯) β (πβπ) β (π β π β§ (π΄ β π₯) β π β§ βπ§ β π ((π΄ β π₯) , π§) = (0gβ(Scalarβπ)))) |
88 | 30, 47, 85, 87 | syl3anbrc 1343 |
. . . 4
β’ ((π β§ (π₯ β π β§ βπ¦ β π (πβ(π΄ β π₯)) β€ (πβ(π΄ β π¦)))) β (π΄ β π₯) β (πβπ)) |
89 | | pjthlem.s |
. . . . 5
β’ β =
(LSSumβπ) |
90 | 34, 89 | lsmelvali 19517 |
. . . 4
β’ (((π β (SubGrpβπ) β§ (πβπ) β (SubGrpβπ)) β§ (π₯ β π β§ (π΄ β π₯) β (πβπ))) β (π₯ + (π΄ β π₯)) β (π β (πβπ))) |
91 | 39, 45, 31, 88, 90 | syl22anc 837 |
. . 3
β’ ((π β§ (π₯ β π β§ βπ¦ β π (πβ(π΄ β π₯)) β€ (πβ(π΄ β π¦)))) β (π₯ + (π΄ β π₯)) β (π β (πβπ))) |
92 | 36, 91 | eqeltrrd 2834 |
. 2
β’ ((π β§ (π₯ β π β§ βπ¦ β π (πβ(π΄ β π₯)) β€ (πβ(π΄ β π¦)))) β π΄ β (π β (πβπ))) |
93 | 23, 92 | rexlimddv 3161 |
1
β’ (π β π΄ β (π β (πβπ))) |