Step | Hyp | Ref
| Expression |
1 | | nmoleub.2 |
. . . . . . . . 9
β’ (π β π β NrmGrp) |
2 | 1 | ad2antrr 724 |
. . . . . . . 8
β’ (((π β§ (πβπΉ) β€ π΄) β§ (π₯ β π β§ π₯ β 0 )) β π β NrmGrp) |
3 | | nmoleub.3 |
. . . . . . . . . . 11
β’ (π β πΉ β (π GrpHom π)) |
4 | | nmoi.2 |
. . . . . . . . . . . 12
β’ π = (Baseβπ) |
5 | | eqid 2732 |
. . . . . . . . . . . 12
β’
(Baseβπ) =
(Baseβπ) |
6 | 4, 5 | ghmf 19095 |
. . . . . . . . . . 11
β’ (πΉ β (π GrpHom π) β πΉ:πβΆ(Baseβπ)) |
7 | 3, 6 | syl 17 |
. . . . . . . . . 10
β’ (π β πΉ:πβΆ(Baseβπ)) |
8 | 7 | ad2antrr 724 |
. . . . . . . . 9
β’ (((π β§ (πβπΉ) β€ π΄) β§ (π₯ β π β§ π₯ β 0 )) β πΉ:πβΆ(Baseβπ)) |
9 | | simprl 769 |
. . . . . . . . 9
β’ (((π β§ (πβπΉ) β€ π΄) β§ (π₯ β π β§ π₯ β 0 )) β π₯ β π) |
10 | | ffvelcdm 7083 |
. . . . . . . . 9
β’ ((πΉ:πβΆ(Baseβπ) β§ π₯ β π) β (πΉβπ₯) β (Baseβπ)) |
11 | 8, 9, 10 | syl2anc 584 |
. . . . . . . 8
β’ (((π β§ (πβπΉ) β€ π΄) β§ (π₯ β π β§ π₯ β 0 )) β (πΉβπ₯) β (Baseβπ)) |
12 | | nmoi.4 |
. . . . . . . . 9
β’ π = (normβπ) |
13 | 5, 12 | nmcl 24124 |
. . . . . . . 8
β’ ((π β NrmGrp β§ (πΉβπ₯) β (Baseβπ)) β (πβ(πΉβπ₯)) β β) |
14 | 2, 11, 13 | syl2anc 584 |
. . . . . . 7
β’ (((π β§ (πβπΉ) β€ π΄) β§ (π₯ β π β§ π₯ β 0 )) β (πβ(πΉβπ₯)) β β) |
15 | | nmoleub.1 |
. . . . . . . . 9
β’ (π β π β NrmGrp) |
16 | 15 | adantr 481 |
. . . . . . . 8
β’ ((π β§ (πβπΉ) β€ π΄) β π β NrmGrp) |
17 | | nmoi.3 |
. . . . . . . . . 10
β’ πΏ = (normβπ) |
18 | | nmoi2.z |
. . . . . . . . . 10
β’ 0 =
(0gβπ) |
19 | 4, 17, 18 | nmrpcl 24128 |
. . . . . . . . 9
β’ ((π β NrmGrp β§ π₯ β π β§ π₯ β 0 ) β (πΏβπ₯) β
β+) |
20 | 19 | 3expb 1120 |
. . . . . . . 8
β’ ((π β NrmGrp β§ (π₯ β π β§ π₯ β 0 )) β (πΏβπ₯) β
β+) |
21 | 16, 20 | sylan 580 |
. . . . . . 7
β’ (((π β§ (πβπΉ) β€ π΄) β§ (π₯ β π β§ π₯ β 0 )) β (πΏβπ₯) β
β+) |
22 | 14, 21 | rerpdivcld 13046 |
. . . . . 6
β’ (((π β§ (πβπΉ) β€ π΄) β§ (π₯ β π β§ π₯ β 0 )) β ((πβ(πΉβπ₯)) / (πΏβπ₯)) β β) |
23 | 22 | rexrd 11263 |
. . . . 5
β’ (((π β§ (πβπΉ) β€ π΄) β§ (π₯ β π β§ π₯ β 0 )) β ((πβ(πΉβπ₯)) / (πΏβπ₯)) β
β*) |
24 | | nmofval.1 |
. . . . . . . 8
β’ π = (π normOp π) |
25 | 24 | nmocl 24236 |
. . . . . . 7
β’ ((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β (πβπΉ) β
β*) |
26 | 15, 1, 3, 25 | syl3anc 1371 |
. . . . . 6
β’ (π β (πβπΉ) β
β*) |
27 | 26 | ad2antrr 724 |
. . . . 5
β’ (((π β§ (πβπΉ) β€ π΄) β§ (π₯ β π β§ π₯ β 0 )) β (πβπΉ) β
β*) |
28 | | nmoleub.4 |
. . . . . 6
β’ (π β π΄ β
β*) |
29 | 28 | ad2antrr 724 |
. . . . 5
β’ (((π β§ (πβπΉ) β€ π΄) β§ (π₯ β π β§ π₯ β 0 )) β π΄ β
β*) |
30 | 15, 1, 3 | 3jca 1128 |
. . . . . . 7
β’ (π β (π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π))) |
31 | 30 | adantr 481 |
. . . . . 6
β’ ((π β§ (πβπΉ) β€ π΄) β (π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π))) |
32 | 24, 4, 17, 12, 18 | nmoi2 24246 |
. . . . . 6
β’ (((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β§ (π₯ β π β§ π₯ β 0 )) β ((πβ(πΉβπ₯)) / (πΏβπ₯)) β€ (πβπΉ)) |
33 | 31, 32 | sylan 580 |
. . . . 5
β’ (((π β§ (πβπΉ) β€ π΄) β§ (π₯ β π β§ π₯ β 0 )) β ((πβ(πΉβπ₯)) / (πΏβπ₯)) β€ (πβπΉ)) |
34 | | simplr 767 |
. . . . 5
β’ (((π β§ (πβπΉ) β€ π΄) β§ (π₯ β π β§ π₯ β 0 )) β (πβπΉ) β€ π΄) |
35 | 23, 27, 29, 33, 34 | xrletrd 13140 |
. . . 4
β’ (((π β§ (πβπΉ) β€ π΄) β§ (π₯ β π β§ π₯ β 0 )) β ((πβ(πΉβπ₯)) / (πΏβπ₯)) β€ π΄) |
36 | 35 | expr 457 |
. . 3
β’ (((π β§ (πβπΉ) β€ π΄) β§ π₯ β π) β (π₯ β 0 β ((πβ(πΉβπ₯)) / (πΏβπ₯)) β€ π΄)) |
37 | 36 | ralrimiva 3146 |
. 2
β’ ((π β§ (πβπΉ) β€ π΄) β βπ₯ β π (π₯ β 0 β ((πβ(πΉβπ₯)) / (πΏβπ₯)) β€ π΄)) |
38 | | 0le0 12312 |
. . . . . . . . . . 11
β’ 0 β€
0 |
39 | | simpllr 774 |
. . . . . . . . . . . . 13
β’ ((((π β§ π΄ β β) β§ π₯ β π) β§ π₯ = 0 ) β π΄ β β) |
40 | 39 | recnd 11241 |
. . . . . . . . . . . 12
β’ ((((π β§ π΄ β β) β§ π₯ β π) β§ π₯ = 0 ) β π΄ β β) |
41 | 40 | mul01d 11412 |
. . . . . . . . . . 11
β’ ((((π β§ π΄ β β) β§ π₯ β π) β§ π₯ = 0 ) β (π΄ Β· 0) =
0) |
42 | 38, 41 | breqtrrid 5186 |
. . . . . . . . . 10
β’ ((((π β§ π΄ β β) β§ π₯ β π) β§ π₯ = 0 ) β 0 β€ (π΄ Β· 0)) |
43 | | fveq2 6891 |
. . . . . . . . . . . . 13
β’ (π₯ = 0 β (πΉβπ₯) = (πΉβ 0 )) |
44 | 3 | ad2antrr 724 |
. . . . . . . . . . . . . 14
β’ (((π β§ π΄ β β) β§ π₯ β π) β πΉ β (π GrpHom π)) |
45 | | eqid 2732 |
. . . . . . . . . . . . . . 15
β’
(0gβπ) = (0gβπ) |
46 | 18, 45 | ghmid 19097 |
. . . . . . . . . . . . . 14
β’ (πΉ β (π GrpHom π) β (πΉβ 0 ) =
(0gβπ)) |
47 | 44, 46 | syl 17 |
. . . . . . . . . . . . 13
β’ (((π β§ π΄ β β) β§ π₯ β π) β (πΉβ 0 ) =
(0gβπ)) |
48 | 43, 47 | sylan9eqr 2794 |
. . . . . . . . . . . 12
β’ ((((π β§ π΄ β β) β§ π₯ β π) β§ π₯ = 0 ) β (πΉβπ₯) = (0gβπ)) |
49 | 48 | fveq2d 6895 |
. . . . . . . . . . 11
β’ ((((π β§ π΄ β β) β§ π₯ β π) β§ π₯ = 0 ) β (πβ(πΉβπ₯)) = (πβ(0gβπ))) |
50 | 1 | ad3antrrr 728 |
. . . . . . . . . . . 12
β’ ((((π β§ π΄ β β) β§ π₯ β π) β§ π₯ = 0 ) β π β NrmGrp) |
51 | 12, 45 | nm0 24137 |
. . . . . . . . . . . 12
β’ (π β NrmGrp β (πβ(0gβπ)) = 0) |
52 | 50, 51 | syl 17 |
. . . . . . . . . . 11
β’ ((((π β§ π΄ β β) β§ π₯ β π) β§ π₯ = 0 ) β (πβ(0gβπ)) = 0) |
53 | 49, 52 | eqtrd 2772 |
. . . . . . . . . 10
β’ ((((π β§ π΄ β β) β§ π₯ β π) β§ π₯ = 0 ) β (πβ(πΉβπ₯)) = 0) |
54 | | fveq2 6891 |
. . . . . . . . . . . 12
β’ (π₯ = 0 β (πΏβπ₯) = (πΏβ 0 )) |
55 | 15 | ad2antrr 724 |
. . . . . . . . . . . . 13
β’ (((π β§ π΄ β β) β§ π₯ β π) β π β NrmGrp) |
56 | 17, 18 | nm0 24137 |
. . . . . . . . . . . . 13
β’ (π β NrmGrp β (πΏβ 0 ) = 0) |
57 | 55, 56 | syl 17 |
. . . . . . . . . . . 12
β’ (((π β§ π΄ β β) β§ π₯ β π) β (πΏβ 0 ) = 0) |
58 | 54, 57 | sylan9eqr 2794 |
. . . . . . . . . . 11
β’ ((((π β§ π΄ β β) β§ π₯ β π) β§ π₯ = 0 ) β (πΏβπ₯) = 0) |
59 | 58 | oveq2d 7424 |
. . . . . . . . . 10
β’ ((((π β§ π΄ β β) β§ π₯ β π) β§ π₯ = 0 ) β (π΄ Β· (πΏβπ₯)) = (π΄ Β· 0)) |
60 | 42, 53, 59 | 3brtr4d 5180 |
. . . . . . . . 9
β’ ((((π β§ π΄ β β) β§ π₯ β π) β§ π₯ = 0 ) β (πβ(πΉβπ₯)) β€ (π΄ Β· (πΏβπ₯))) |
61 | 60 | a1d 25 |
. . . . . . . 8
β’ ((((π β§ π΄ β β) β§ π₯ β π) β§ π₯ = 0 ) β ((π₯ β 0 β ((πβ(πΉβπ₯)) / (πΏβπ₯)) β€ π΄) β (πβ(πΉβπ₯)) β€ (π΄ Β· (πΏβπ₯)))) |
62 | | simpr 485 |
. . . . . . . . 9
β’ ((((π β§ π΄ β β) β§ π₯ β π) β§ π₯ β 0 ) β π₯ β 0 ) |
63 | 1 | ad2antrr 724 |
. . . . . . . . . . . . 13
β’ (((π β§ π΄ β β) β§ π₯ β π) β π β NrmGrp) |
64 | 7 | adantr 481 |
. . . . . . . . . . . . . 14
β’ ((π β§ π΄ β β) β πΉ:πβΆ(Baseβπ)) |
65 | 64, 10 | sylan 580 |
. . . . . . . . . . . . 13
β’ (((π β§ π΄ β β) β§ π₯ β π) β (πΉβπ₯) β (Baseβπ)) |
66 | 63, 65, 13 | syl2anc 584 |
. . . . . . . . . . . 12
β’ (((π β§ π΄ β β) β§ π₯ β π) β (πβ(πΉβπ₯)) β β) |
67 | 66 | adantr 481 |
. . . . . . . . . . 11
β’ ((((π β§ π΄ β β) β§ π₯ β π) β§ π₯ β 0 ) β (πβ(πΉβπ₯)) β β) |
68 | | simpllr 774 |
. . . . . . . . . . 11
β’ ((((π β§ π΄ β β) β§ π₯ β π) β§ π₯ β 0 ) β π΄ β β) |
69 | 15 | adantr 481 |
. . . . . . . . . . . 12
β’ ((π β§ π΄ β β) β π β NrmGrp) |
70 | 19 | 3expa 1118 |
. . . . . . . . . . . 12
β’ (((π β NrmGrp β§ π₯ β π) β§ π₯ β 0 ) β (πΏβπ₯) β
β+) |
71 | 69, 70 | sylanl1 678 |
. . . . . . . . . . 11
β’ ((((π β§ π΄ β β) β§ π₯ β π) β§ π₯ β 0 ) β (πΏβπ₯) β
β+) |
72 | 67, 68, 71 | ledivmul2d 13069 |
. . . . . . . . . 10
β’ ((((π β§ π΄ β β) β§ π₯ β π) β§ π₯ β 0 ) β (((πβ(πΉβπ₯)) / (πΏβπ₯)) β€ π΄ β (πβ(πΉβπ₯)) β€ (π΄ Β· (πΏβπ₯)))) |
73 | 72 | biimpd 228 |
. . . . . . . . 9
β’ ((((π β§ π΄ β β) β§ π₯ β π) β§ π₯ β 0 ) β (((πβ(πΉβπ₯)) / (πΏβπ₯)) β€ π΄ β (πβ(πΉβπ₯)) β€ (π΄ Β· (πΏβπ₯)))) |
74 | 62, 73 | embantd 59 |
. . . . . . . 8
β’ ((((π β§ π΄ β β) β§ π₯ β π) β§ π₯ β 0 ) β ((π₯ β 0 β ((πβ(πΉβπ₯)) / (πΏβπ₯)) β€ π΄) β (πβ(πΉβπ₯)) β€ (π΄ Β· (πΏβπ₯)))) |
75 | 61, 74 | pm2.61dane 3029 |
. . . . . . 7
β’ (((π β§ π΄ β β) β§ π₯ β π) β ((π₯ β 0 β ((πβ(πΉβπ₯)) / (πΏβπ₯)) β€ π΄) β (πβ(πΉβπ₯)) β€ (π΄ Β· (πΏβπ₯)))) |
76 | 75 | ralimdva 3167 |
. . . . . 6
β’ ((π β§ π΄ β β) β (βπ₯ β π (π₯ β 0 β ((πβ(πΉβπ₯)) / (πΏβπ₯)) β€ π΄) β βπ₯ β π (πβ(πΉβπ₯)) β€ (π΄ Β· (πΏβπ₯)))) |
77 | 1 | adantr 481 |
. . . . . . 7
β’ ((π β§ π΄ β β) β π β NrmGrp) |
78 | 3 | adantr 481 |
. . . . . . 7
β’ ((π β§ π΄ β β) β πΉ β (π GrpHom π)) |
79 | | simpr 485 |
. . . . . . 7
β’ ((π β§ π΄ β β) β π΄ β β) |
80 | | nmoleub.5 |
. . . . . . . 8
β’ (π β 0 β€ π΄) |
81 | 80 | adantr 481 |
. . . . . . 7
β’ ((π β§ π΄ β β) β 0 β€ π΄) |
82 | 24, 4, 17, 12 | nmolb 24233 |
. . . . . . 7
β’ (((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β§ π΄ β β β§ 0 β€ π΄) β (βπ₯ β π (πβ(πΉβπ₯)) β€ (π΄ Β· (πΏβπ₯)) β (πβπΉ) β€ π΄)) |
83 | 69, 77, 78, 79, 81, 82 | syl311anc 1384 |
. . . . . 6
β’ ((π β§ π΄ β β) β (βπ₯ β π (πβ(πΉβπ₯)) β€ (π΄ Β· (πΏβπ₯)) β (πβπΉ) β€ π΄)) |
84 | 76, 83 | syld 47 |
. . . . 5
β’ ((π β§ π΄ β β) β (βπ₯ β π (π₯ β 0 β ((πβ(πΉβπ₯)) / (πΏβπ₯)) β€ π΄) β (πβπΉ) β€ π΄)) |
85 | 84 | imp 407 |
. . . 4
β’ (((π β§ π΄ β β) β§ βπ₯ β π (π₯ β 0 β ((πβ(πΉβπ₯)) / (πΏβπ₯)) β€ π΄)) β (πβπΉ) β€ π΄) |
86 | 85 | an32s 650 |
. . 3
β’ (((π β§ βπ₯ β π (π₯ β 0 β ((πβ(πΉβπ₯)) / (πΏβπ₯)) β€ π΄)) β§ π΄ β β) β (πβπΉ) β€ π΄) |
87 | 26 | ad2antrr 724 |
. . . . 5
β’ (((π β§ βπ₯ β π (π₯ β 0 β ((πβ(πΉβπ₯)) / (πΏβπ₯)) β€ π΄)) β§ π΄ = +β) β (πβπΉ) β
β*) |
88 | | pnfge 13109 |
. . . . 5
β’ ((πβπΉ) β β* β (πβπΉ) β€ +β) |
89 | 87, 88 | syl 17 |
. . . 4
β’ (((π β§ βπ₯ β π (π₯ β 0 β ((πβ(πΉβπ₯)) / (πΏβπ₯)) β€ π΄)) β§ π΄ = +β) β (πβπΉ) β€ +β) |
90 | | simpr 485 |
. . . 4
β’ (((π β§ βπ₯ β π (π₯ β 0 β ((πβ(πΉβπ₯)) / (πΏβπ₯)) β€ π΄)) β§ π΄ = +β) β π΄ = +β) |
91 | 89, 90 | breqtrrd 5176 |
. . 3
β’ (((π β§ βπ₯ β π (π₯ β 0 β ((πβ(πΉβπ₯)) / (πΏβπ₯)) β€ π΄)) β§ π΄ = +β) β (πβπΉ) β€ π΄) |
92 | | ge0nemnf 13151 |
. . . . . . 7
β’ ((π΄ β β*
β§ 0 β€ π΄) β
π΄ β
-β) |
93 | 28, 80, 92 | syl2anc 584 |
. . . . . 6
β’ (π β π΄ β -β) |
94 | 28, 93 | jca 512 |
. . . . 5
β’ (π β (π΄ β β* β§ π΄ β
-β)) |
95 | | xrnemnf 13096 |
. . . . 5
β’ ((π΄ β β*
β§ π΄ β -β)
β (π΄ β β
β¨ π΄ =
+β)) |
96 | 94, 95 | sylib 217 |
. . . 4
β’ (π β (π΄ β β β¨ π΄ = +β)) |
97 | 96 | adantr 481 |
. . 3
β’ ((π β§ βπ₯ β π (π₯ β 0 β ((πβ(πΉβπ₯)) / (πΏβπ₯)) β€ π΄)) β (π΄ β β β¨ π΄ = +β)) |
98 | 86, 91, 97 | mpjaodan 957 |
. 2
β’ ((π β§ βπ₯ β π (π₯ β 0 β ((πβ(πΉβπ₯)) / (πΏβπ₯)) β€ π΄)) β (πβπΉ) β€ π΄) |
99 | 37, 98 | impbida 799 |
1
β’ (π β ((πβπΉ) β€ π΄ β βπ₯ β π (π₯ β 0 β ((πβ(πΉβπ₯)) / (πΏβπ₯)) β€ π΄))) |