Step | Hyp | Ref
| Expression |
1 | | hmoplin 31182 |
. . . . 5
โข (๐ โ HrmOp โ ๐ โ LinOp) |
2 | | nmlnopne0 31239 |
. . . . . 6
โข (๐ โ LinOp โ
((normopโ๐) โ 0 โ ๐ โ 0hop )) |
3 | 2 | biimpar 478 |
. . . . 5
โข ((๐ โ LinOp โง ๐ โ 0hop ) โ
(normopโ๐)
โ 0) |
4 | 1, 3 | sylan 580 |
. . . 4
โข ((๐ โ HrmOp โง ๐ โ 0hop ) โ
(normopโ๐)
โ 0) |
5 | 4 | adantlr 713 |
. . 3
โข (((๐ โ HrmOp โง
(normopโ๐)
โ โ) โง ๐
โ 0hop ) โ (normopโ๐) โ 0) |
6 | | rereccl 11928 |
. . . . . 6
โข
(((normopโ๐) โ โ โง
(normopโ๐)
โ 0) โ (1 / (normopโ๐)) โ โ) |
7 | 6 | adantll 712 |
. . . . 5
โข (((๐ โ HrmOp โง
(normopโ๐)
โ โ) โง (normopโ๐) โ 0) โ (1 /
(normopโ๐)) โ โ) |
8 | | simpll 765 |
. . . . 5
โข (((๐ โ HrmOp โง
(normopโ๐)
โ โ) โง (normopโ๐) โ 0) โ ๐ โ HrmOp) |
9 | | idhmop 31222 |
. . . . . . 7
โข
Iop โ HrmOp |
10 | | hmopm 31261 |
. . . . . . 7
โข
(((normopโ๐) โ โ โง Iop โ
HrmOp) โ ((normopโ๐) ยทop
Iop ) โ HrmOp) |
11 | 9, 10 | mpan2 689 |
. . . . . 6
โข
((normopโ๐) โ โ โ
((normopโ๐) ยทop
Iop ) โ HrmOp) |
12 | 11 | ad2antlr 725 |
. . . . 5
โข (((๐ โ HrmOp โง
(normopโ๐)
โ โ) โง (normopโ๐) โ 0) โ
((normopโ๐) ยทop
Iop ) โ HrmOp) |
13 | | simplr 767 |
. . . . . . 7
โข (((๐ โ HrmOp โง
(normopโ๐)
โ โ) โง (normopโ๐) โ 0) โ
(normopโ๐)
โ โ) |
14 | | hmopf 31114 |
. . . . . . . . 9
โข (๐ โ HrmOp โ ๐: โโถ
โ) |
15 | | nmopgt0 31152 |
. . . . . . . . . 10
โข (๐: โโถ โ โ
((normopโ๐) โ 0 โ 0 <
(normopโ๐))) |
16 | 15 | biimpa 477 |
. . . . . . . . 9
โข ((๐: โโถ โ โง
(normopโ๐)
โ 0) โ 0 < (normopโ๐)) |
17 | 14, 16 | sylan 580 |
. . . . . . . 8
โข ((๐ โ HrmOp โง
(normopโ๐)
โ 0) โ 0 < (normopโ๐)) |
18 | 17 | adantlr 713 |
. . . . . . 7
โข (((๐ โ HrmOp โง
(normopโ๐)
โ โ) โง (normopโ๐) โ 0) โ 0 <
(normopโ๐)) |
19 | 13, 18 | recgt0d 12144 |
. . . . . 6
โข (((๐ โ HrmOp โง
(normopโ๐)
โ โ) โง (normopโ๐) โ 0) โ 0 < (1 /
(normopโ๐))) |
20 | | 0re 11212 |
. . . . . . . 8
โข 0 โ
โ |
21 | | ltle 11298 |
. . . . . . . 8
โข ((0
โ โ โง (1 / (normopโ๐)) โ โ) โ (0 < (1 /
(normopโ๐)) โ 0 โค (1 /
(normopโ๐)))) |
22 | 20, 6, 21 | sylancr 587 |
. . . . . . 7
โข
(((normopโ๐) โ โ โง
(normopโ๐)
โ 0) โ (0 < (1 / (normopโ๐)) โ 0 โค (1 /
(normopโ๐)))) |
23 | 22 | adantll 712 |
. . . . . 6
โข (((๐ โ HrmOp โง
(normopโ๐)
โ โ) โง (normopโ๐) โ 0) โ (0 < (1 /
(normopโ๐)) โ 0 โค (1 /
(normopโ๐)))) |
24 | 19, 23 | mpd 15 |
. . . . 5
โข (((๐ โ HrmOp โง
(normopโ๐)
โ โ) โง (normopโ๐) โ 0) โ 0 โค (1 /
(normopโ๐))) |
25 | | leopnmid 31378 |
. . . . . 6
โข ((๐ โ HrmOp โง
(normopโ๐)
โ โ) โ ๐
โคop ((normopโ๐) ยทop
Iop )) |
26 | 25 | adantr 481 |
. . . . 5
โข (((๐ โ HrmOp โง
(normopโ๐)
โ โ) โง (normopโ๐) โ 0) โ ๐ โคop
((normopโ๐) ยทop
Iop )) |
27 | | leopmul2i 31375 |
. . . . 5
โข ((((1 /
(normopโ๐)) โ โ โง ๐ โ HrmOp โง
((normopโ๐) ยทop
Iop ) โ HrmOp) โง (0 โค (1 /
(normopโ๐)) โง ๐ โคop
((normopโ๐) ยทop
Iop ))) โ ((1 / (normopโ๐)) ยทop ๐) โคop ((1 /
(normopโ๐)) ยทop
((normopโ๐) ยทop
Iop ))) |
28 | 7, 8, 12, 24, 26, 27 | syl32anc 1378 |
. . . 4
โข (((๐ โ HrmOp โง
(normopโ๐)
โ โ) โง (normopโ๐) โ 0) โ ((1 /
(normopโ๐)) ยทop ๐) โคop ((1 /
(normopโ๐)) ยทop
((normopโ๐) ยทop
Iop ))) |
29 | | recn 11196 |
. . . . . 6
โข
((normopโ๐) โ โ โ
(normopโ๐)
โ โ) |
30 | | reccl 11875 |
. . . . . . . . 9
โข
(((normopโ๐) โ โ โง
(normopโ๐)
โ 0) โ (1 / (normopโ๐)) โ โ) |
31 | | simpl 483 |
. . . . . . . . 9
โข
(((normopโ๐) โ โ โง
(normopโ๐)
โ 0) โ (normopโ๐) โ โ) |
32 | | hoif 30994 |
. . . . . . . . . . 11
โข
Iop : โโ1-1-ontoโ โ |
33 | | f1of 6830 |
. . . . . . . . . . 11
โข (
Iop : โโ1-1-ontoโ โ โ Iop :
โโถ โ) |
34 | 32, 33 | ax-mp 5 |
. . . . . . . . . 10
โข
Iop : โโถ โ |
35 | | homulass 31042 |
. . . . . . . . . 10
โข (((1 /
(normopโ๐)) โ โ โง
(normopโ๐)
โ โ โง Iop : โโถ โ) โ (((1 /
(normopโ๐)) ยท (normopโ๐)) ยทop
Iop ) = ((1 / (normopโ๐)) ยทop
((normopโ๐) ยทop
Iop ))) |
36 | 34, 35 | mp3an3 1450 |
. . . . . . . . 9
โข (((1 /
(normopโ๐)) โ โ โง
(normopโ๐)
โ โ) โ (((1 / (normopโ๐)) ยท (normopโ๐)) ยทop
Iop ) = ((1 / (normopโ๐)) ยทop
((normopโ๐) ยทop
Iop ))) |
37 | 30, 31, 36 | syl2anc 584 |
. . . . . . . 8
โข
(((normopโ๐) โ โ โง
(normopโ๐)
โ 0) โ (((1 / (normopโ๐)) ยท (normopโ๐)) ยทop
Iop ) = ((1 / (normopโ๐)) ยทop
((normopโ๐) ยทop
Iop ))) |
38 | | recid2 11883 |
. . . . . . . . 9
โข
(((normopโ๐) โ โ โง
(normopโ๐)
โ 0) โ ((1 / (normopโ๐)) ยท (normopโ๐)) = 1) |
39 | 38 | oveq1d 7420 |
. . . . . . . 8
โข
(((normopโ๐) โ โ โง
(normopโ๐)
โ 0) โ (((1 / (normopโ๐)) ยท (normopโ๐)) ยทop
Iop ) = (1 ยทop Iop
)) |
40 | 37, 39 | eqtr3d 2774 |
. . . . . . 7
โข
(((normopโ๐) โ โ โง
(normopโ๐)
โ 0) โ ((1 / (normopโ๐)) ยทop
((normopโ๐) ยทop
Iop )) = (1 ยทop Iop
)) |
41 | | homullid 31040 |
. . . . . . . 8
โข (
Iop : โโถ โ โ (1 ยทop
Iop ) = Iop ) |
42 | 34, 41 | ax-mp 5 |
. . . . . . 7
โข (1
ยทop Iop ) = Iop |
43 | 40, 42 | eqtrdi 2788 |
. . . . . 6
โข
(((normopโ๐) โ โ โง
(normopโ๐)
โ 0) โ ((1 / (normopโ๐)) ยทop
((normopโ๐) ยทop
Iop )) = Iop ) |
44 | 29, 43 | sylan 580 |
. . . . 5
โข
(((normopโ๐) โ โ โง
(normopโ๐)
โ 0) โ ((1 / (normopโ๐)) ยทop
((normopโ๐) ยทop
Iop )) = Iop ) |
45 | 44 | adantll 712 |
. . . 4
โข (((๐ โ HrmOp โง
(normopโ๐)
โ โ) โง (normopโ๐) โ 0) โ ((1 /
(normopโ๐)) ยทop
((normopโ๐) ยทop
Iop )) = Iop ) |
46 | 28, 45 | breqtrd 5173 |
. . 3
โข (((๐ โ HrmOp โง
(normopโ๐)
โ โ) โง (normopโ๐) โ 0) โ ((1 /
(normopโ๐)) ยทop ๐) โคop
Iop ) |
47 | 5, 46 | syldan 591 |
. 2
โข (((๐ โ HrmOp โง
(normopโ๐)
โ โ) โง ๐
โ 0hop ) โ ((1 / (normopโ๐)) ยทop ๐) โคop
Iop ) |
48 | 47 | 3impa 1110 |
1
โข ((๐ โ HrmOp โง
(normopโ๐)
โ โ โง ๐ โ
0hop ) โ ((1 / (normopโ๐)) ยทop ๐) โคop
Iop ) |