Step | Hyp | Ref
| Expression |
1 | | nmofval.1 |
. . . . . . 7
β’ π = (π normOp π) |
2 | 1 | isnghm2 24126 |
. . . . . 6
β’ ((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β (πΉ β (π NGHom π) β (πβπΉ) β β)) |
3 | 2 | biimpar 479 |
. . . . 5
β’ (((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β§ (πβπΉ) β β) β πΉ β (π NGHom π)) |
4 | | nmoi.2 |
. . . . . 6
β’ π = (Baseβπ) |
5 | | nmoi.3 |
. . . . . 6
β’ πΏ = (normβπ) |
6 | | nmoi.4 |
. . . . . 6
β’ π = (normβπ) |
7 | 1, 4, 5, 6 | nmoi 24130 |
. . . . 5
β’ ((πΉ β (π NGHom π) β§ π β π) β (πβ(πΉβπ)) β€ ((πβπΉ) Β· (πΏβπ))) |
8 | 3, 7 | sylan 581 |
. . . 4
β’ ((((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β§ (πβπΉ) β β) β§ π β π) β (πβ(πΉβπ)) β€ ((πβπΉ) Β· (πΏβπ))) |
9 | 8 | an32s 651 |
. . 3
β’ ((((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β§ π β π) β§ (πβπΉ) β β) β (πβ(πΉβπ)) β€ ((πβπΉ) Β· (πΏβπ))) |
10 | | id 22 |
. . . 4
β’ ((πβπΉ) β β β (πβπΉ) β β) |
11 | 4, 5 | nmcl 24010 |
. . . . 5
β’ ((π β NrmGrp β§ π β π) β (πΏβπ) β β) |
12 | 11 | 3ad2antl1 1186 |
. . . 4
β’ (((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β§ π β π) β (πΏβπ) β β) |
13 | | rexmul 13201 |
. . . 4
β’ (((πβπΉ) β β β§ (πΏβπ) β β) β ((πβπΉ) Β·e (πΏβπ)) = ((πβπΉ) Β· (πΏβπ))) |
14 | 10, 12, 13 | syl2anr 598 |
. . 3
β’ ((((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β§ π β π) β§ (πβπΉ) β β) β ((πβπΉ) Β·e (πΏβπ)) = ((πβπΉ) Β· (πΏβπ))) |
15 | 9, 14 | breqtrrd 5139 |
. 2
β’ ((((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β§ π β π) β§ (πβπΉ) β β) β (πβ(πΉβπ)) β€ ((πβπΉ) Β·e (πΏβπ))) |
16 | | fveq2 6848 |
. . . . . . 7
β’ (π = (0gβπ) β (πΉβπ) = (πΉβ(0gβπ))) |
17 | 16 | fveq2d 6852 |
. . . . . 6
β’ (π = (0gβπ) β (πβ(πΉβπ)) = (πβ(πΉβ(0gβπ)))) |
18 | | fveq2 6848 |
. . . . . . 7
β’ (π = (0gβπ) β (πΏβπ) = (πΏβ(0gβπ))) |
19 | 18 | oveq2d 7379 |
. . . . . 6
β’ (π = (0gβπ) β (+β
Β·e (πΏβπ)) = (+β Β·e (πΏβ(0gβπ)))) |
20 | 17, 19 | breq12d 5124 |
. . . . 5
β’ (π = (0gβπ) β ((πβ(πΉβπ)) β€ (+β Β·e
(πΏβπ)) β (πβ(πΉβ(0gβπ))) β€ (+β
Β·e (πΏβ(0gβπ))))) |
21 | | simpl2 1193 |
. . . . . . . . . 10
β’ (((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β§ π β π) β π β NrmGrp) |
22 | | eqid 2732 |
. . . . . . . . . . . . 13
β’
(Baseβπ) =
(Baseβπ) |
23 | 4, 22 | ghmf 19027 |
. . . . . . . . . . . 12
β’ (πΉ β (π GrpHom π) β πΉ:πβΆ(Baseβπ)) |
24 | 23 | ffvelcdmda 7041 |
. . . . . . . . . . 11
β’ ((πΉ β (π GrpHom π) β§ π β π) β (πΉβπ) β (Baseβπ)) |
25 | 24 | 3ad2antl3 1188 |
. . . . . . . . . 10
β’ (((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β§ π β π) β (πΉβπ) β (Baseβπ)) |
26 | 22, 6 | nmcl 24010 |
. . . . . . . . . 10
β’ ((π β NrmGrp β§ (πΉβπ) β (Baseβπ)) β (πβ(πΉβπ)) β β) |
27 | 21, 25, 26 | syl2anc 585 |
. . . . . . . . 9
β’ (((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β§ π β π) β (πβ(πΉβπ)) β β) |
28 | 27 | adantr 482 |
. . . . . . . 8
β’ ((((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β§ π β π) β§ π β (0gβπ)) β (πβ(πΉβπ)) β β) |
29 | 28 | rexrd 11215 |
. . . . . . 7
β’ ((((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β§ π β π) β§ π β (0gβπ)) β (πβ(πΉβπ)) β
β*) |
30 | | pnfge 13061 |
. . . . . . 7
β’ ((πβ(πΉβπ)) β β* β (πβ(πΉβπ)) β€ +β) |
31 | 29, 30 | syl 17 |
. . . . . 6
β’ ((((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β§ π β π) β§ π β (0gβπ)) β (πβ(πΉβπ)) β€ +β) |
32 | | simp1 1137 |
. . . . . . . 8
β’ ((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β π β NrmGrp) |
33 | | eqid 2732 |
. . . . . . . . . 10
β’
(0gβπ) = (0gβπ) |
34 | 4, 5, 33 | nmrpcl 24014 |
. . . . . . . . 9
β’ ((π β NrmGrp β§ π β π β§ π β (0gβπ)) β (πΏβπ) β
β+) |
35 | 34 | 3expa 1119 |
. . . . . . . 8
β’ (((π β NrmGrp β§ π β π) β§ π β (0gβπ)) β (πΏβπ) β
β+) |
36 | 32, 35 | sylanl1 679 |
. . . . . . 7
β’ ((((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β§ π β π) β§ π β (0gβπ)) β (πΏβπ) β
β+) |
37 | | rpxr 12934 |
. . . . . . . 8
β’ ((πΏβπ) β β+ β (πΏβπ) β
β*) |
38 | | rpgt0 12937 |
. . . . . . . 8
β’ ((πΏβπ) β β+ β 0 <
(πΏβπ)) |
39 | | xmulpnf2 13205 |
. . . . . . . 8
β’ (((πΏβπ) β β* β§ 0 <
(πΏβπ)) β (+β Β·e
(πΏβπ)) = +β) |
40 | 37, 38, 39 | syl2anc 585 |
. . . . . . 7
β’ ((πΏβπ) β β+ β
(+β Β·e (πΏβπ)) = +β) |
41 | 36, 40 | syl 17 |
. . . . . 6
β’ ((((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β§ π β π) β§ π β (0gβπ)) β (+β Β·e
(πΏβπ)) = +β) |
42 | 31, 41 | breqtrrd 5139 |
. . . . 5
β’ ((((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β§ π β π) β§ π β (0gβπ)) β (πβ(πΉβπ)) β€ (+β Β·e
(πΏβπ))) |
43 | | 0le0 12264 |
. . . . . 6
β’ 0 β€
0 |
44 | | simpl3 1194 |
. . . . . . . . . 10
β’ (((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β§ π β π) β πΉ β (π GrpHom π)) |
45 | | eqid 2732 |
. . . . . . . . . . 11
β’
(0gβπ) = (0gβπ) |
46 | 33, 45 | ghmid 19029 |
. . . . . . . . . 10
β’ (πΉ β (π GrpHom π) β (πΉβ(0gβπ)) = (0gβπ)) |
47 | 44, 46 | syl 17 |
. . . . . . . . 9
β’ (((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β§ π β π) β (πΉβ(0gβπ)) = (0gβπ)) |
48 | 47 | fveq2d 6852 |
. . . . . . . 8
β’ (((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β§ π β π) β (πβ(πΉβ(0gβπ))) = (πβ(0gβπ))) |
49 | 6, 45 | nm0 24023 |
. . . . . . . . 9
β’ (π β NrmGrp β (πβ(0gβπ)) = 0) |
50 | 21, 49 | syl 17 |
. . . . . . . 8
β’ (((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β§ π β π) β (πβ(0gβπ)) = 0) |
51 | 48, 50 | eqtrd 2772 |
. . . . . . 7
β’ (((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β§ π β π) β (πβ(πΉβ(0gβπ))) = 0) |
52 | | simpl1 1192 |
. . . . . . . . . 10
β’ (((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β§ π β π) β π β NrmGrp) |
53 | 5, 33 | nm0 24023 |
. . . . . . . . . 10
β’ (π β NrmGrp β (πΏβ(0gβπ)) = 0) |
54 | 52, 53 | syl 17 |
. . . . . . . . 9
β’ (((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β§ π β π) β (πΏβ(0gβπ)) = 0) |
55 | 54 | oveq2d 7379 |
. . . . . . . 8
β’ (((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β§ π β π) β (+β Β·e
(πΏβ(0gβπ))) = (+β
Β·e 0)) |
56 | | pnfxr 11219 |
. . . . . . . . 9
β’ +β
β β* |
57 | | xmul01 13197 |
. . . . . . . . 9
β’ (+β
β β* β (+β Β·e 0) =
0) |
58 | 56, 57 | ax-mp 5 |
. . . . . . . 8
β’ (+β
Β·e 0) = 0 |
59 | 55, 58 | eqtrdi 2788 |
. . . . . . 7
β’ (((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β§ π β π) β (+β Β·e
(πΏβ(0gβπ))) = 0) |
60 | 51, 59 | breq12d 5124 |
. . . . . 6
β’ (((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β§ π β π) β ((πβ(πΉβ(0gβπ))) β€ (+β
Β·e (πΏβ(0gβπ))) β 0 β€
0)) |
61 | 43, 60 | mpbiri 258 |
. . . . 5
β’ (((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β§ π β π) β (πβ(πΉβ(0gβπ))) β€ (+β
Β·e (πΏβ(0gβπ)))) |
62 | 20, 42, 61 | pm2.61ne 3027 |
. . . 4
β’ (((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β§ π β π) β (πβ(πΉβπ)) β€ (+β Β·e
(πΏβπ))) |
63 | 62 | adantr 482 |
. . 3
β’ ((((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β§ π β π) β§ (πβπΉ) = +β) β (πβ(πΉβπ)) β€ (+β Β·e
(πΏβπ))) |
64 | | simpr 486 |
. . . 4
β’ ((((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β§ π β π) β§ (πβπΉ) = +β) β (πβπΉ) = +β) |
65 | 64 | oveq1d 7378 |
. . 3
β’ ((((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β§ π β π) β§ (πβπΉ) = +β) β ((πβπΉ) Β·e (πΏβπ)) = (+β Β·e (πΏβπ))) |
66 | 63, 65 | breqtrrd 5139 |
. 2
β’ ((((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β§ π β π) β§ (πβπΉ) = +β) β (πβ(πΉβπ)) β€ ((πβπΉ) Β·e (πΏβπ))) |
67 | 1 | nmocl 24122 |
. . . . 5
β’ ((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β (πβπΉ) β
β*) |
68 | 1 | nmoge0 24123 |
. . . . . 6
β’ ((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β 0 β€ (πβπΉ)) |
69 | | ge0nemnf 13103 |
. . . . . 6
β’ (((πβπΉ) β β* β§ 0 β€
(πβπΉ)) β (πβπΉ) β -β) |
70 | 67, 68, 69 | syl2anc 585 |
. . . . 5
β’ ((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β (πβπΉ) β -β) |
71 | 67, 70 | jca 513 |
. . . 4
β’ ((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β ((πβπΉ) β β* β§ (πβπΉ) β -β)) |
72 | | xrnemnf 13048 |
. . . 4
β’ (((πβπΉ) β β* β§ (πβπΉ) β -β) β ((πβπΉ) β β β¨ (πβπΉ) = +β)) |
73 | 71, 72 | sylib 217 |
. . 3
β’ ((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β ((πβπΉ) β β β¨ (πβπΉ) = +β)) |
74 | 73 | adantr 482 |
. 2
β’ (((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β§ π β π) β ((πβπΉ) β β β¨ (πβπΉ) = +β)) |
75 | 15, 66, 74 | mpjaodan 958 |
1
β’ (((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β§ π β π) β (πβ(πΉβπ)) β€ ((πβπΉ) Β·e (πΏβπ))) |