Step | Hyp | Ref
| Expression |
1 | | nmoleub2lem.7 |
. . . . 5
β’ ((π β§ π₯ β π) β (π β (πΏβπ₯) β€ π
)) |
2 | 1 | adantlr 713 |
. . . 4
β’ (((π β§ (πβπΉ) β€ π΄) β§ π₯ β π) β (π β (πΏβπ₯) β€ π
)) |
3 | | nmoleub2.t |
. . . . . . . . . . . 12
β’ (π β π β (NrmMod β©
βMod)) |
4 | 3 | elin1d 4197 |
. . . . . . . . . . 11
β’ (π β π β NrmMod) |
5 | | nlmngp 24185 |
. . . . . . . . . . 11
β’ (π β NrmMod β π β NrmGrp) |
6 | 4, 5 | syl 17 |
. . . . . . . . . 10
β’ (π β π β NrmGrp) |
7 | 6 | ad2antrr 724 |
. . . . . . . . 9
β’ (((π β§ (πβπΉ) β€ π΄) β§ (π₯ β π β§ (πΏβπ₯) β€ π
)) β π β NrmGrp) |
8 | | nmoleub2.f |
. . . . . . . . . . . 12
β’ (π β πΉ β (π LMHom π)) |
9 | | nmoleub2.v |
. . . . . . . . . . . . 13
β’ π = (Baseβπ) |
10 | | eqid 2732 |
. . . . . . . . . . . . 13
β’
(Baseβπ) =
(Baseβπ) |
11 | 9, 10 | lmhmf 20637 |
. . . . . . . . . . . 12
β’ (πΉ β (π LMHom π) β πΉ:πβΆ(Baseβπ)) |
12 | 8, 11 | syl 17 |
. . . . . . . . . . 11
β’ (π β πΉ:πβΆ(Baseβπ)) |
13 | 12 | ad2antrr 724 |
. . . . . . . . . 10
β’ (((π β§ (πβπΉ) β€ π΄) β§ (π₯ β π β§ (πΏβπ₯) β€ π
)) β πΉ:πβΆ(Baseβπ)) |
14 | | simprl 769 |
. . . . . . . . . 10
β’ (((π β§ (πβπΉ) β€ π΄) β§ (π₯ β π β§ (πΏβπ₯) β€ π
)) β π₯ β π) |
15 | 13, 14 | ffvelcdmd 7084 |
. . . . . . . . 9
β’ (((π β§ (πβπΉ) β€ π΄) β§ (π₯ β π β§ (πΏβπ₯) β€ π
)) β (πΉβπ₯) β (Baseβπ)) |
16 | | nmoleub2.m |
. . . . . . . . . 10
β’ π = (normβπ) |
17 | 10, 16 | nmcl 24116 |
. . . . . . . . 9
β’ ((π β NrmGrp β§ (πΉβπ₯) β (Baseβπ)) β (πβ(πΉβπ₯)) β β) |
18 | 7, 15, 17 | syl2anc 584 |
. . . . . . . 8
β’ (((π β§ (πβπΉ) β€ π΄) β§ (π₯ β π β§ (πΏβπ₯) β€ π
)) β (πβ(πΉβπ₯)) β β) |
19 | | nmoleub2.r |
. . . . . . . . 9
β’ (π β π
β
β+) |
20 | 19 | ad2antrr 724 |
. . . . . . . 8
β’ (((π β§ (πβπΉ) β€ π΄) β§ (π₯ β π β§ (πΏβπ₯) β€ π
)) β π
β
β+) |
21 | 18, 20 | rerpdivcld 13043 |
. . . . . . 7
β’ (((π β§ (πβπΉ) β€ π΄) β§ (π₯ β π β§ (πΏβπ₯) β€ π
)) β ((πβ(πΉβπ₯)) / π
) β β) |
22 | 21 | rexrd 11260 |
. . . . . 6
β’ (((π β§ (πβπΉ) β€ π΄) β§ (π₯ β π β§ (πΏβπ₯) β€ π
)) β ((πβ(πΉβπ₯)) / π
) β
β*) |
23 | | nmoleub2.s |
. . . . . . . . . 10
β’ (π β π β (NrmMod β©
βMod)) |
24 | 23 | elin1d 4197 |
. . . . . . . . 9
β’ (π β π β NrmMod) |
25 | | nlmngp 24185 |
. . . . . . . . 9
β’ (π β NrmMod β π β NrmGrp) |
26 | 24, 25 | syl 17 |
. . . . . . . 8
β’ (π β π β NrmGrp) |
27 | | lmghm 20634 |
. . . . . . . . 9
β’ (πΉ β (π LMHom π) β πΉ β (π GrpHom π)) |
28 | 8, 27 | syl 17 |
. . . . . . . 8
β’ (π β πΉ β (π GrpHom π)) |
29 | | nmoleub2.n |
. . . . . . . . 9
β’ π = (π normOp π) |
30 | 29 | nmocl 24228 |
. . . . . . . 8
β’ ((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β (πβπΉ) β
β*) |
31 | 26, 6, 28, 30 | syl3anc 1371 |
. . . . . . 7
β’ (π β (πβπΉ) β
β*) |
32 | 31 | ad2antrr 724 |
. . . . . 6
β’ (((π β§ (πβπΉ) β€ π΄) β§ (π₯ β π β§ (πΏβπ₯) β€ π
)) β (πβπΉ) β
β*) |
33 | | nmoleub2.a |
. . . . . . 7
β’ (π β π΄ β
β*) |
34 | 33 | ad2antrr 724 |
. . . . . 6
β’ (((π β§ (πβπΉ) β€ π΄) β§ (π₯ β π β§ (πΏβπ₯) β€ π
)) β π΄ β
β*) |
35 | 20 | rpred 13012 |
. . . . . . . . . 10
β’ (((π β§ (πβπΉ) β€ π΄) β§ (π₯ β π β§ (πΏβπ₯) β€ π
)) β π
β β) |
36 | | rexmul 13246 |
. . . . . . . . . 10
β’ ((((πβ(πΉβπ₯)) / π
) β β β§ π
β β) β (((πβ(πΉβπ₯)) / π
) Β·e π
) = (((πβ(πΉβπ₯)) / π
) Β· π
)) |
37 | 21, 35, 36 | syl2anc 584 |
. . . . . . . . 9
β’ (((π β§ (πβπΉ) β€ π΄) β§ (π₯ β π β§ (πΏβπ₯) β€ π
)) β (((πβ(πΉβπ₯)) / π
) Β·e π
) = (((πβ(πΉβπ₯)) / π
) Β· π
)) |
38 | 18 | recnd 11238 |
. . . . . . . . . 10
β’ (((π β§ (πβπΉ) β€ π΄) β§ (π₯ β π β§ (πΏβπ₯) β€ π
)) β (πβ(πΉβπ₯)) β β) |
39 | 35 | recnd 11238 |
. . . . . . . . . 10
β’ (((π β§ (πβπΉ) β€ π΄) β§ (π₯ β π β§ (πΏβπ₯) β€ π
)) β π
β β) |
40 | 20 | rpne0d 13017 |
. . . . . . . . . 10
β’ (((π β§ (πβπΉ) β€ π΄) β§ (π₯ β π β§ (πΏβπ₯) β€ π
)) β π
β 0) |
41 | 38, 39, 40 | divcan1d 11987 |
. . . . . . . . 9
β’ (((π β§ (πβπΉ) β€ π΄) β§ (π₯ β π β§ (πΏβπ₯) β€ π
)) β (((πβ(πΉβπ₯)) / π
) Β· π
) = (πβ(πΉβπ₯))) |
42 | 37, 41 | eqtrd 2772 |
. . . . . . . 8
β’ (((π β§ (πβπΉ) β€ π΄) β§ (π₯ β π β§ (πΏβπ₯) β€ π
)) β (((πβ(πΉβπ₯)) / π
) Β·e π
) = (πβ(πΉβπ₯))) |
43 | 18 | rexrd 11260 |
. . . . . . . . 9
β’ (((π β§ (πβπΉ) β€ π΄) β§ (π₯ β π β§ (πΏβπ₯) β€ π
)) β (πβ(πΉβπ₯)) β
β*) |
44 | 26 | ad2antrr 724 |
. . . . . . . . . . . 12
β’ (((π β§ (πβπΉ) β€ π΄) β§ (π₯ β π β§ (πΏβπ₯) β€ π
)) β π β NrmGrp) |
45 | | nmoleub2.l |
. . . . . . . . . . . . 13
β’ πΏ = (normβπ) |
46 | 9, 45 | nmcl 24116 |
. . . . . . . . . . . 12
β’ ((π β NrmGrp β§ π₯ β π) β (πΏβπ₯) β β) |
47 | 44, 14, 46 | syl2anc 584 |
. . . . . . . . . . 11
β’ (((π β§ (πβπΉ) β€ π΄) β§ (π₯ β π β§ (πΏβπ₯) β€ π
)) β (πΏβπ₯) β β) |
48 | 47 | rexrd 11260 |
. . . . . . . . . 10
β’ (((π β§ (πβπΉ) β€ π΄) β§ (π₯ β π β§ (πΏβπ₯) β€ π
)) β (πΏβπ₯) β
β*) |
49 | 32, 48 | xmulcld 13277 |
. . . . . . . . 9
β’ (((π β§ (πβπΉ) β€ π΄) β§ (π₯ β π β§ (πΏβπ₯) β€ π
)) β ((πβπΉ) Β·e (πΏβπ₯)) β
β*) |
50 | 20 | rpxrd 13013 |
. . . . . . . . . 10
β’ (((π β§ (πβπΉ) β€ π΄) β§ (π₯ β π β§ (πΏβπ₯) β€ π
)) β π
β
β*) |
51 | 32, 50 | xmulcld 13277 |
. . . . . . . . 9
β’ (((π β§ (πβπΉ) β€ π΄) β§ (π₯ β π β§ (πΏβπ₯) β€ π
)) β ((πβπΉ) Β·e π
) β
β*) |
52 | 28 | ad2antrr 724 |
. . . . . . . . . 10
β’ (((π β§ (πβπΉ) β€ π΄) β§ (π₯ β π β§ (πΏβπ₯) β€ π
)) β πΉ β (π GrpHom π)) |
53 | 29, 9, 45, 16 | nmoix 24237 |
. . . . . . . . . 10
β’ (((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β§ π₯ β π) β (πβ(πΉβπ₯)) β€ ((πβπΉ) Β·e (πΏβπ₯))) |
54 | 44, 7, 52, 14, 53 | syl31anc 1373 |
. . . . . . . . 9
β’ (((π β§ (πβπΉ) β€ π΄) β§ (π₯ β π β§ (πΏβπ₯) β€ π
)) β (πβ(πΉβπ₯)) β€ ((πβπΉ) Β·e (πΏβπ₯))) |
55 | 29 | nmoge0 24229 |
. . . . . . . . . . . . 13
β’ ((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β 0 β€ (πβπΉ)) |
56 | 26, 6, 28, 55 | syl3anc 1371 |
. . . . . . . . . . . 12
β’ (π β 0 β€ (πβπΉ)) |
57 | 31, 56 | jca 512 |
. . . . . . . . . . 11
β’ (π β ((πβπΉ) β β* β§ 0 β€
(πβπΉ))) |
58 | 57 | ad2antrr 724 |
. . . . . . . . . 10
β’ (((π β§ (πβπΉ) β€ π΄) β§ (π₯ β π β§ (πΏβπ₯) β€ π
)) β ((πβπΉ) β β* β§ 0 β€
(πβπΉ))) |
59 | | simprr 771 |
. . . . . . . . . 10
β’ (((π β§ (πβπΉ) β€ π΄) β§ (π₯ β π β§ (πΏβπ₯) β€ π
)) β (πΏβπ₯) β€ π
) |
60 | | xlemul2a 13264 |
. . . . . . . . . 10
β’ ((((πΏβπ₯) β β* β§ π
β β*
β§ ((πβπΉ) β β*
β§ 0 β€ (πβπΉ))) β§ (πΏβπ₯) β€ π
) β ((πβπΉ) Β·e (πΏβπ₯)) β€ ((πβπΉ) Β·e π
)) |
61 | 48, 50, 58, 59, 60 | syl31anc 1373 |
. . . . . . . . 9
β’ (((π β§ (πβπΉ) β€ π΄) β§ (π₯ β π β§ (πΏβπ₯) β€ π
)) β ((πβπΉ) Β·e (πΏβπ₯)) β€ ((πβπΉ) Β·e π
)) |
62 | 43, 49, 51, 54, 61 | xrletrd 13137 |
. . . . . . . 8
β’ (((π β§ (πβπΉ) β€ π΄) β§ (π₯ β π β§ (πΏβπ₯) β€ π
)) β (πβ(πΉβπ₯)) β€ ((πβπΉ) Β·e π
)) |
63 | 42, 62 | eqbrtrd 5169 |
. . . . . . 7
β’ (((π β§ (πβπΉ) β€ π΄) β§ (π₯ β π β§ (πΏβπ₯) β€ π
)) β (((πβ(πΉβπ₯)) / π
) Β·e π
) β€ ((πβπΉ) Β·e π
)) |
64 | | xlemul1 13265 |
. . . . . . . 8
β’ ((((πβ(πΉβπ₯)) / π
) β β* β§ (πβπΉ) β β* β§ π
β β+)
β (((πβ(πΉβπ₯)) / π
) β€ (πβπΉ) β (((πβ(πΉβπ₯)) / π
) Β·e π
) β€ ((πβπΉ) Β·e π
))) |
65 | 22, 32, 20, 64 | syl3anc 1371 |
. . . . . . 7
β’ (((π β§ (πβπΉ) β€ π΄) β§ (π₯ β π β§ (πΏβπ₯) β€ π
)) β (((πβ(πΉβπ₯)) / π
) β€ (πβπΉ) β (((πβ(πΉβπ₯)) / π
) Β·e π
) β€ ((πβπΉ) Β·e π
))) |
66 | 63, 65 | mpbird 256 |
. . . . . 6
β’ (((π β§ (πβπΉ) β€ π΄) β§ (π₯ β π β§ (πΏβπ₯) β€ π
)) β ((πβ(πΉβπ₯)) / π
) β€ (πβπΉ)) |
67 | | simplr 767 |
. . . . . 6
β’ (((π β§ (πβπΉ) β€ π΄) β§ (π₯ β π β§ (πΏβπ₯) β€ π
)) β (πβπΉ) β€ π΄) |
68 | 22, 32, 34, 66, 67 | xrletrd 13137 |
. . . . 5
β’ (((π β§ (πβπΉ) β€ π΄) β§ (π₯ β π β§ (πΏβπ₯) β€ π
)) β ((πβ(πΉβπ₯)) / π
) β€ π΄) |
69 | 68 | expr 457 |
. . . 4
β’ (((π β§ (πβπΉ) β€ π΄) β§ π₯ β π) β ((πΏβπ₯) β€ π
β ((πβ(πΉβπ₯)) / π
) β€ π΄)) |
70 | 2, 69 | syld 47 |
. . 3
β’ (((π β§ (πβπΉ) β€ π΄) β§ π₯ β π) β (π β ((πβ(πΉβπ₯)) / π
) β€ π΄)) |
71 | 70 | ralrimiva 3146 |
. 2
β’ ((π β§ (πβπΉ) β€ π΄) β βπ₯ β π (π β ((πβ(πΉβπ₯)) / π
) β€ π΄)) |
72 | | eqid 2732 |
. . . 4
β’
(0gβπ) = (0gβπ) |
73 | 26 | ad2antrr 724 |
. . . 4
β’ (((π β§ βπ₯ β π (π β ((πβ(πΉβπ₯)) / π
) β€ π΄)) β§ π΄ β β) β π β NrmGrp) |
74 | 6 | ad2antrr 724 |
. . . 4
β’ (((π β§ βπ₯ β π (π β ((πβ(πΉβπ₯)) / π
) β€ π΄)) β§ π΄ β β) β π β NrmGrp) |
75 | 28 | ad2antrr 724 |
. . . 4
β’ (((π β§ βπ₯ β π (π β ((πβ(πΉβπ₯)) / π
) β€ π΄)) β§ π΄ β β) β πΉ β (π GrpHom π)) |
76 | | simpr 485 |
. . . 4
β’ (((π β§ βπ₯ β π (π β ((πβ(πΉβπ₯)) / π
) β€ π΄)) β§ π΄ β β) β π΄ β β) |
77 | | nmoleub2lem.5 |
. . . . 5
β’ ((π β§ βπ₯ β π (π β ((πβ(πΉβπ₯)) / π
) β€ π΄)) β 0 β€ π΄) |
78 | 77 | adantr 481 |
. . . 4
β’ (((π β§ βπ₯ β π (π β ((πβ(πΉβπ₯)) / π
) β€ π΄)) β§ π΄ β β) β 0 β€ π΄) |
79 | | nmoleub2lem.6 |
. . . 4
β’ ((((π β§ βπ₯ β π (π β ((πβ(πΉβπ₯)) / π
) β€ π΄)) β§ π΄ β β) β§ (π¦ β π β§ π¦ β (0gβπ))) β (πβ(πΉβπ¦)) β€ (π΄ Β· (πΏβπ¦))) |
80 | 29, 9, 45, 16, 72, 73, 74, 75, 76, 78, 79 | nmolb2d 24226 |
. . 3
β’ (((π β§ βπ₯ β π (π β ((πβ(πΉβπ₯)) / π
) β€ π΄)) β§ π΄ β β) β (πβπΉ) β€ π΄) |
81 | 31 | ad2antrr 724 |
. . . . 5
β’ (((π β§ βπ₯ β π (π β ((πβ(πΉβπ₯)) / π
) β€ π΄)) β§ π΄ = +β) β (πβπΉ) β
β*) |
82 | | pnfge 13106 |
. . . . 5
β’ ((πβπΉ) β β* β (πβπΉ) β€ +β) |
83 | 81, 82 | syl 17 |
. . . 4
β’ (((π β§ βπ₯ β π (π β ((πβ(πΉβπ₯)) / π
) β€ π΄)) β§ π΄ = +β) β (πβπΉ) β€ +β) |
84 | | simpr 485 |
. . . 4
β’ (((π β§ βπ₯ β π (π β ((πβ(πΉβπ₯)) / π
) β€ π΄)) β§ π΄ = +β) β π΄ = +β) |
85 | 83, 84 | breqtrrd 5175 |
. . 3
β’ (((π β§ βπ₯ β π (π β ((πβ(πΉβπ₯)) / π
) β€ π΄)) β§ π΄ = +β) β (πβπΉ) β€ π΄) |
86 | 33 | adantr 481 |
. . . . 5
β’ ((π β§ βπ₯ β π (π β ((πβ(πΉβπ₯)) / π
) β€ π΄)) β π΄ β
β*) |
87 | | ge0nemnf 13148 |
. . . . . 6
β’ ((π΄ β β*
β§ 0 β€ π΄) β
π΄ β
-β) |
88 | 86, 77, 87 | syl2anc 584 |
. . . . 5
β’ ((π β§ βπ₯ β π (π β ((πβ(πΉβπ₯)) / π
) β€ π΄)) β π΄ β -β) |
89 | 86, 88 | jca 512 |
. . . 4
β’ ((π β§ βπ₯ β π (π β ((πβ(πΉβπ₯)) / π
) β€ π΄)) β (π΄ β β* β§ π΄ β
-β)) |
90 | | xrnemnf 13093 |
. . . 4
β’ ((π΄ β β*
β§ π΄ β -β)
β (π΄ β β
β¨ π΄ =
+β)) |
91 | 89, 90 | sylib 217 |
. . 3
β’ ((π β§ βπ₯ β π (π β ((πβ(πΉβπ₯)) / π
) β€ π΄)) β (π΄ β β β¨ π΄ = +β)) |
92 | 80, 85, 91 | mpjaodan 957 |
. 2
β’ ((π β§ βπ₯ β π (π β ((πβ(πΉβπ₯)) / π
) β€ π΄)) β (πβπΉ) β€ π΄) |
93 | 71, 92 | impbida 799 |
1
β’ (π β ((πβπΉ) β€ π΄ β βπ₯ β π (π β ((πβ(πΉβπ₯)) / π
) β€ π΄))) |