Step | Hyp | Ref
| Expression |
1 | | hmoplin 30926 |
. . . . 5
โข (๐ โ HrmOp โ ๐ โ LinOp) |
2 | | nmlnopne0 30983 |
. . . . . 6
โข (๐ โ LinOp โ
((normopโ๐) โ 0 โ ๐ โ 0hop )) |
3 | 2 | biimpar 479 |
. . . . 5
โข ((๐ โ LinOp โง ๐ โ 0hop ) โ
(normopโ๐)
โ 0) |
4 | 1, 3 | sylan 581 |
. . . 4
โข ((๐ โ HrmOp โง ๐ โ 0hop ) โ
(normopโ๐)
โ 0) |
5 | 4 | adantlr 714 |
. . 3
โข (((๐ โ HrmOp โง
(normopโ๐)
โ โ) โง ๐
โ 0hop ) โ (normopโ๐) โ 0) |
6 | | rereccl 11878 |
. . . . . 6
โข
(((normopโ๐) โ โ โง
(normopโ๐)
โ 0) โ (1 / (normopโ๐)) โ โ) |
7 | 6 | adantll 713 |
. . . . 5
โข (((๐ โ HrmOp โง
(normopโ๐)
โ โ) โง (normopโ๐) โ 0) โ (1 /
(normopโ๐)) โ โ) |
8 | | simpll 766 |
. . . . 5
โข (((๐ โ HrmOp โง
(normopโ๐)
โ โ) โง (normopโ๐) โ 0) โ ๐ โ HrmOp) |
9 | | idhmop 30966 |
. . . . . . 7
โข
Iop โ HrmOp |
10 | | hmopm 31005 |
. . . . . . 7
โข
(((normopโ๐) โ โ โง Iop โ
HrmOp) โ ((normopโ๐) ยทop
Iop ) โ HrmOp) |
11 | 9, 10 | mpan2 690 |
. . . . . 6
โข
((normopโ๐) โ โ โ
((normopโ๐) ยทop
Iop ) โ HrmOp) |
12 | 11 | ad2antlr 726 |
. . . . 5
โข (((๐ โ HrmOp โง
(normopโ๐)
โ โ) โง (normopโ๐) โ 0) โ
((normopโ๐) ยทop
Iop ) โ HrmOp) |
13 | | simplr 768 |
. . . . . . 7
โข (((๐ โ HrmOp โง
(normopโ๐)
โ โ) โง (normopโ๐) โ 0) โ
(normopโ๐)
โ โ) |
14 | | hmopf 30858 |
. . . . . . . . 9
โข (๐ โ HrmOp โ ๐: โโถ
โ) |
15 | | nmopgt0 30896 |
. . . . . . . . . 10
โข (๐: โโถ โ โ
((normopโ๐) โ 0 โ 0 <
(normopโ๐))) |
16 | 15 | biimpa 478 |
. . . . . . . . 9
โข ((๐: โโถ โ โง
(normopโ๐)
โ 0) โ 0 < (normopโ๐)) |
17 | 14, 16 | sylan 581 |
. . . . . . . 8
โข ((๐ โ HrmOp โง
(normopโ๐)
โ 0) โ 0 < (normopโ๐)) |
18 | 17 | adantlr 714 |
. . . . . . 7
โข (((๐ โ HrmOp โง
(normopโ๐)
โ โ) โง (normopโ๐) โ 0) โ 0 <
(normopโ๐)) |
19 | 13, 18 | recgt0d 12094 |
. . . . . 6
โข (((๐ โ HrmOp โง
(normopโ๐)
โ โ) โง (normopโ๐) โ 0) โ 0 < (1 /
(normopโ๐))) |
20 | | 0re 11162 |
. . . . . . . 8
โข 0 โ
โ |
21 | | ltle 11248 |
. . . . . . . 8
โข ((0
โ โ โง (1 / (normopโ๐)) โ โ) โ (0 < (1 /
(normopโ๐)) โ 0 โค (1 /
(normopโ๐)))) |
22 | 20, 6, 21 | sylancr 588 |
. . . . . . 7
โข
(((normopโ๐) โ โ โง
(normopโ๐)
โ 0) โ (0 < (1 / (normopโ๐)) โ 0 โค (1 /
(normopโ๐)))) |
23 | 22 | adantll 713 |
. . . . . 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 31122 |
. . . . . 6
โข ((๐ โ HrmOp โง
(normopโ๐)
โ โ) โ ๐
โคop ((normopโ๐) ยทop
Iop )) |
26 | 25 | adantr 482 |
. . . . 5
โข (((๐ โ HrmOp โง
(normopโ๐)
โ โ) โง (normopโ๐) โ 0) โ ๐ โคop
((normopโ๐) ยทop
Iop )) |
27 | | leopmul2i 31119 |
. . . . 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 1379 |
. . . 4
โข (((๐ โ HrmOp โง
(normopโ๐)
โ โ) โง (normopโ๐) โ 0) โ ((1 /
(normopโ๐)) ยทop ๐) โคop ((1 /
(normopโ๐)) ยทop
((normopโ๐) ยทop
Iop ))) |
29 | | recn 11146 |
. . . . . 6
โข
((normopโ๐) โ โ โ
(normopโ๐)
โ โ) |
30 | | reccl 11825 |
. . . . . . . . 9
โข
(((normopโ๐) โ โ โง
(normopโ๐)
โ 0) โ (1 / (normopโ๐)) โ โ) |
31 | | simpl 484 |
. . . . . . . . 9
โข
(((normopโ๐) โ โ โง
(normopโ๐)
โ 0) โ (normopโ๐) โ โ) |
32 | | hoif 30738 |
. . . . . . . . . . 11
โข
Iop : โโ1-1-ontoโ โ |
33 | | f1of 6785 |
. . . . . . . . . . 11
โข (
Iop : โโ1-1-ontoโ โ โ Iop :
โโถ โ) |
34 | 32, 33 | ax-mp 5 |
. . . . . . . . . 10
โข
Iop : โโถ โ |
35 | | homulass 30786 |
. . . . . . . . . 10
โข (((1 /
(normopโ๐)) โ โ โง
(normopโ๐)
โ โ โง Iop : โโถ โ) โ (((1 /
(normopโ๐)) ยท (normopโ๐)) ยทop
Iop ) = ((1 / (normopโ๐)) ยทop
((normopโ๐) ยทop
Iop ))) |
36 | 34, 35 | mp3an3 1451 |
. . . . . . . . 9
โข (((1 /
(normopโ๐)) โ โ โง
(normopโ๐)
โ โ) โ (((1 / (normopโ๐)) ยท (normopโ๐)) ยทop
Iop ) = ((1 / (normopโ๐)) ยทop
((normopโ๐) ยทop
Iop ))) |
37 | 30, 31, 36 | syl2anc 585 |
. . . . . . . 8
โข
(((normopโ๐) โ โ โง
(normopโ๐)
โ 0) โ (((1 / (normopโ๐)) ยท (normopโ๐)) ยทop
Iop ) = ((1 / (normopโ๐)) ยทop
((normopโ๐) ยทop
Iop ))) |
38 | | recid2 11833 |
. . . . . . . . 9
โข
(((normopโ๐) โ โ โง
(normopโ๐)
โ 0) โ ((1 / (normopโ๐)) ยท (normopโ๐)) = 1) |
39 | 38 | oveq1d 7373 |
. . . . . . . 8
โข
(((normopโ๐) โ โ โง
(normopโ๐)
โ 0) โ (((1 / (normopโ๐)) ยท (normopโ๐)) ยทop
Iop ) = (1 ยทop Iop
)) |
40 | 37, 39 | eqtr3d 2775 |
. . . . . . 7
โข
(((normopโ๐) โ โ โง
(normopโ๐)
โ 0) โ ((1 / (normopโ๐)) ยทop
((normopโ๐) ยทop
Iop )) = (1 ยทop Iop
)) |
41 | | homulid2 30784 |
. . . . . . . 8
โข (
Iop : โโถ โ โ (1 ยทop
Iop ) = Iop ) |
42 | 34, 41 | ax-mp 5 |
. . . . . . 7
โข (1
ยทop Iop ) = Iop |
43 | 40, 42 | eqtrdi 2789 |
. . . . . 6
โข
(((normopโ๐) โ โ โง
(normopโ๐)
โ 0) โ ((1 / (normopโ๐)) ยทop
((normopโ๐) ยทop
Iop )) = Iop ) |
44 | 29, 43 | sylan 581 |
. . . . 5
โข
(((normopโ๐) โ โ โง
(normopโ๐)
โ 0) โ ((1 / (normopโ๐)) ยทop
((normopโ๐) ยทop
Iop )) = Iop ) |
45 | 44 | adantll 713 |
. . . 4
โข (((๐ โ HrmOp โง
(normopโ๐)
โ โ) โง (normopโ๐) โ 0) โ ((1 /
(normopโ๐)) ยทop
((normopโ๐) ยทop
Iop )) = Iop ) |
46 | 28, 45 | breqtrd 5132 |
. . 3
โข (((๐ โ HrmOp โง
(normopโ๐)
โ โ) โง (normopโ๐) โ 0) โ ((1 /
(normopโ๐)) ยทop ๐) โคop
Iop ) |
47 | 5, 46 | syldan 592 |
. 2
โข (((๐ โ HrmOp โง
(normopโ๐)
โ โ) โง ๐
โ 0hop ) โ ((1 / (normopโ๐)) ยทop ๐) โคop
Iop ) |
48 | 47 | 3impa 1111 |
1
โข ((๐ โ HrmOp โง
(normopโ๐)
โ โ โง ๐ โ
0hop ) โ ((1 / (normopโ๐)) ยทop ๐) โคop
Iop ) |