Step | Hyp | Ref
| Expression |
1 | | simpl2 1193 |
. . . . 5
β’ (((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β§ (π β π β§ π β 0 )) β π β NrmGrp) |
2 | | simpl3 1194 |
. . . . . . 7
β’ (((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β§ (π β π β§ π β 0 )) β πΉ β (π GrpHom π)) |
3 | | nmoi.2 |
. . . . . . . 8
β’ π = (Baseβπ) |
4 | | eqid 2733 |
. . . . . . . 8
β’
(Baseβπ) =
(Baseβπ) |
5 | 3, 4 | ghmf 19096 |
. . . . . . 7
β’ (πΉ β (π GrpHom π) β πΉ:πβΆ(Baseβπ)) |
6 | 2, 5 | syl 17 |
. . . . . 6
β’ (((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β§ (π β π β§ π β 0 )) β πΉ:πβΆ(Baseβπ)) |
7 | | simprl 770 |
. . . . . 6
β’ (((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β§ (π β π β§ π β 0 )) β π β π) |
8 | 6, 7 | ffvelcdmd 7088 |
. . . . 5
β’ (((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β§ (π β π β§ π β 0 )) β (πΉβπ) β (Baseβπ)) |
9 | | nmoi.4 |
. . . . . 6
β’ π = (normβπ) |
10 | 4, 9 | nmcl 24125 |
. . . . 5
β’ ((π β NrmGrp β§ (πΉβπ) β (Baseβπ)) β (πβ(πΉβπ)) β β) |
11 | 1, 8, 10 | syl2anc 585 |
. . . 4
β’ (((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β§ (π β π β§ π β 0 )) β (πβ(πΉβπ)) β β) |
12 | 11 | rexrd 11264 |
. . 3
β’ (((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β§ (π β π β§ π β 0 )) β (πβ(πΉβπ)) β
β*) |
13 | | nmofval.1 |
. . . . . 6
β’ π = (π normOp π) |
14 | 13 | nmocl 24237 |
. . . . 5
β’ ((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β (πβπΉ) β
β*) |
15 | 14 | adantr 482 |
. . . 4
β’ (((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β§ (π β π β§ π β 0 )) β (πβπΉ) β
β*) |
16 | | nmoi.3 |
. . . . . . . 8
β’ πΏ = (normβπ) |
17 | | nmoi2.z |
. . . . . . . 8
β’ 0 =
(0gβπ) |
18 | 3, 16, 17 | nmrpcl 24129 |
. . . . . . 7
β’ ((π β NrmGrp β§ π β π β§ π β 0 ) β (πΏβπ) β
β+) |
19 | 18 | 3expb 1121 |
. . . . . 6
β’ ((π β NrmGrp β§ (π β π β§ π β 0 )) β (πΏβπ) β
β+) |
20 | 19 | 3ad2antl1 1186 |
. . . . 5
β’ (((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β§ (π β π β§ π β 0 )) β (πΏβπ) β
β+) |
21 | 20 | rpxrd 13017 |
. . . 4
β’ (((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β§ (π β π β§ π β 0 )) β (πΏβπ) β
β*) |
22 | 15, 21 | xmulcld 13281 |
. . 3
β’ (((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β§ (π β π β§ π β 0 )) β ((πβπΉ) Β·e (πΏβπ)) β
β*) |
23 | 20 | rpreccld 13026 |
. . . . 5
β’ (((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β§ (π β π β§ π β 0 )) β (1 / (πΏβπ)) β
β+) |
24 | 23 | rpxrd 13017 |
. . . 4
β’ (((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β§ (π β π β§ π β 0 )) β (1 / (πΏβπ)) β
β*) |
25 | 23 | rpge0d 13020 |
. . . 4
β’ (((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β§ (π β π β§ π β 0 )) β 0 β€ (1 /
(πΏβπ))) |
26 | 24, 25 | jca 513 |
. . 3
β’ (((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β§ (π β π β§ π β 0 )) β ((1 / (πΏβπ)) β β* β§ 0 β€
(1 / (πΏβπ)))) |
27 | 13, 3, 16, 9 | nmoix 24246 |
. . . 4
β’ (((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β§ π β π) β (πβ(πΉβπ)) β€ ((πβπΉ) Β·e (πΏβπ))) |
28 | 27 | adantrr 716 |
. . 3
β’ (((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β§ (π β π β§ π β 0 )) β (πβ(πΉβπ)) β€ ((πβπΉ) Β·e (πΏβπ))) |
29 | | xlemul1a 13267 |
. . 3
β’ ((((πβ(πΉβπ)) β β* β§ ((πβπΉ) Β·e (πΏβπ)) β β* β§ ((1 /
(πΏβπ)) β β* β§ 0 β€
(1 / (πΏβπ)))) β§ (πβ(πΉβπ)) β€ ((πβπΉ) Β·e (πΏβπ))) β ((πβ(πΉβπ)) Β·e (1 / (πΏβπ))) β€ (((πβπΉ) Β·e (πΏβπ)) Β·e (1 / (πΏβπ)))) |
30 | 12, 22, 26, 28, 29 | syl31anc 1374 |
. 2
β’ (((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β§ (π β π β§ π β 0 )) β ((πβ(πΉβπ)) Β·e (1 / (πΏβπ))) β€ (((πβπΉ) Β·e (πΏβπ)) Β·e (1 / (πΏβπ)))) |
31 | 23 | rpred 13016 |
. . . 4
β’ (((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β§ (π β π β§ π β 0 )) β (1 / (πΏβπ)) β β) |
32 | | rexmul 13250 |
. . . 4
β’ (((πβ(πΉβπ)) β β β§ (1 / (πΏβπ)) β β) β ((πβ(πΉβπ)) Β·e (1 / (πΏβπ))) = ((πβ(πΉβπ)) Β· (1 / (πΏβπ)))) |
33 | 11, 31, 32 | syl2anc 585 |
. . 3
β’ (((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β§ (π β π β§ π β 0 )) β ((πβ(πΉβπ)) Β·e (1 / (πΏβπ))) = ((πβ(πΉβπ)) Β· (1 / (πΏβπ)))) |
34 | 11 | recnd 11242 |
. . . 4
β’ (((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β§ (π β π β§ π β 0 )) β (πβ(πΉβπ)) β β) |
35 | 20 | rpcnd 13018 |
. . . 4
β’ (((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β§ (π β π β§ π β 0 )) β (πΏβπ) β β) |
36 | 20 | rpne0d 13021 |
. . . 4
β’ (((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β§ (π β π β§ π β 0 )) β (πΏβπ) β 0) |
37 | 34, 35, 36 | divrecd 11993 |
. . 3
β’ (((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β§ (π β π β§ π β 0 )) β ((πβ(πΉβπ)) / (πΏβπ)) = ((πβ(πΉβπ)) Β· (1 / (πΏβπ)))) |
38 | 33, 37 | eqtr4d 2776 |
. 2
β’ (((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β§ (π β π β§ π β 0 )) β ((πβ(πΉβπ)) Β·e (1 / (πΏβπ))) = ((πβ(πΉβπ)) / (πΏβπ))) |
39 | | xmulass 13266 |
. . . 4
β’ (((πβπΉ) β β* β§ (πΏβπ) β β* β§ (1 /
(πΏβπ)) β β*) β
(((πβπΉ) Β·e (πΏβπ)) Β·e (1 / (πΏβπ))) = ((πβπΉ) Β·e ((πΏβπ) Β·e (1 / (πΏβπ))))) |
40 | 15, 21, 24, 39 | syl3anc 1372 |
. . 3
β’ (((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β§ (π β π β§ π β 0 )) β (((πβπΉ) Β·e (πΏβπ)) Β·e (1 / (πΏβπ))) = ((πβπΉ) Β·e ((πΏβπ) Β·e (1 / (πΏβπ))))) |
41 | 20 | rpred 13016 |
. . . . . 6
β’ (((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β§ (π β π β§ π β 0 )) β (πΏβπ) β β) |
42 | | rexmul 13250 |
. . . . . 6
β’ (((πΏβπ) β β β§ (1 / (πΏβπ)) β β) β ((πΏβπ) Β·e (1 / (πΏβπ))) = ((πΏβπ) Β· (1 / (πΏβπ)))) |
43 | 41, 31, 42 | syl2anc 585 |
. . . . 5
β’ (((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β§ (π β π β§ π β 0 )) β ((πΏβπ) Β·e (1 / (πΏβπ))) = ((πΏβπ) Β· (1 / (πΏβπ)))) |
44 | 35, 36 | recidd 11985 |
. . . . 5
β’ (((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β§ (π β π β§ π β 0 )) β ((πΏβπ) Β· (1 / (πΏβπ))) = 1) |
45 | 43, 44 | eqtrd 2773 |
. . . 4
β’ (((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β§ (π β π β§ π β 0 )) β ((πΏβπ) Β·e (1 / (πΏβπ))) = 1) |
46 | 45 | oveq2d 7425 |
. . 3
β’ (((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β§ (π β π β§ π β 0 )) β ((πβπΉ) Β·e ((πΏβπ) Β·e (1 / (πΏβπ)))) = ((πβπΉ) Β·e 1)) |
47 | | xmulrid 13258 |
. . . 4
β’ ((πβπΉ) β β* β ((πβπΉ) Β·e 1) = (πβπΉ)) |
48 | 15, 47 | syl 17 |
. . 3
β’ (((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β§ (π β π β§ π β 0 )) β ((πβπΉ) Β·e 1) = (πβπΉ)) |
49 | 40, 46, 48 | 3eqtrd 2777 |
. 2
β’ (((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β§ (π β π β§ π β 0 )) β (((πβπΉ) Β·e (πΏβπ)) Β·e (1 / (πΏβπ))) = (πβπΉ)) |
50 | 30, 38, 49 | 3brtr3d 5180 |
1
β’ (((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β§ (π β π β§ π β 0 )) β ((πβ(πΉβπ)) / (πΏβπ)) β€ (πβπΉ)) |