Step | Hyp | Ref
| Expression |
1 | | hmopre 30907 |
. . . . 5
โข ((๐ โ HrmOp โง ๐ฅ โ โ) โ ((๐โ๐ฅ) ยทih ๐ฅ) โ
โ) |
2 | 1 | adantlr 714 |
. . . 4
โข (((๐ โ HrmOp โง
(normopโ๐)
โ โ) โง ๐ฅ
โ โ) โ ((๐โ๐ฅ) ยทih ๐ฅ) โ
โ) |
3 | 1 | recnd 11188 |
. . . . . 6
โข ((๐ โ HrmOp โง ๐ฅ โ โ) โ ((๐โ๐ฅ) ยทih ๐ฅ) โ
โ) |
4 | 3 | abscld 15327 |
. . . . 5
โข ((๐ โ HrmOp โง ๐ฅ โ โ) โ
(absโ((๐โ๐ฅ)
ยทih ๐ฅ)) โ โ) |
5 | 4 | adantlr 714 |
. . . 4
โข (((๐ โ HrmOp โง
(normopโ๐)
โ โ) โง ๐ฅ
โ โ) โ (absโ((๐โ๐ฅ) ยทih ๐ฅ)) โ
โ) |
6 | | idhmop 30966 |
. . . . . . 7
โข
Iop โ HrmOp |
7 | | hmopm 31005 |
. . . . . . 7
โข
(((normopโ๐) โ โ โง Iop โ
HrmOp) โ ((normopโ๐) ยทop
Iop ) โ HrmOp) |
8 | 6, 7 | mpan2 690 |
. . . . . 6
โข
((normopโ๐) โ โ โ
((normopโ๐) ยทop
Iop ) โ HrmOp) |
9 | | hmopre 30907 |
. . . . . 6
โข
((((normopโ๐) ยทop
Iop ) โ HrmOp โง ๐ฅ โ โ) โ
((((normopโ๐) ยทop
Iop )โ๐ฅ)
ยทih ๐ฅ) โ โ) |
10 | 8, 9 | sylan 581 |
. . . . 5
โข
(((normopโ๐) โ โ โง ๐ฅ โ โ) โ
((((normopโ๐) ยทop
Iop )โ๐ฅ)
ยทih ๐ฅ) โ โ) |
11 | 10 | adantll 713 |
. . . 4
โข (((๐ โ HrmOp โง
(normopโ๐)
โ โ) โง ๐ฅ
โ โ) โ ((((normopโ๐) ยทop
Iop )โ๐ฅ)
ยทih ๐ฅ) โ โ) |
12 | 1 | leabsd 15305 |
. . . . 5
โข ((๐ โ HrmOp โง ๐ฅ โ โ) โ ((๐โ๐ฅ) ยทih ๐ฅ) โค (absโ((๐โ๐ฅ) ยทih ๐ฅ))) |
13 | 12 | adantlr 714 |
. . . 4
โข (((๐ โ HrmOp โง
(normopโ๐)
โ โ) โง ๐ฅ
โ โ) โ ((๐โ๐ฅ) ยทih ๐ฅ) โค (absโ((๐โ๐ฅ) ยทih ๐ฅ))) |
14 | | hmopf 30858 |
. . . . . . . 8
โข (๐ โ HrmOp โ ๐: โโถ
โ) |
15 | | ffvelcdm 7033 |
. . . . . . . . 9
โข ((๐: โโถ โ โง
๐ฅ โ โ) โ
(๐โ๐ฅ) โ โ) |
16 | | normcl 30109 |
. . . . . . . . 9
โข ((๐โ๐ฅ) โ โ โ
(normโโ(๐โ๐ฅ)) โ โ) |
17 | 15, 16 | syl 17 |
. . . . . . . 8
โข ((๐: โโถ โ โง
๐ฅ โ โ) โ
(normโโ(๐โ๐ฅ)) โ โ) |
18 | 14, 17 | sylan 581 |
. . . . . . 7
โข ((๐ โ HrmOp โง ๐ฅ โ โ) โ
(normโโ(๐โ๐ฅ)) โ โ) |
19 | 18 | adantlr 714 |
. . . . . 6
โข (((๐ โ HrmOp โง
(normopโ๐)
โ โ) โง ๐ฅ
โ โ) โ (normโโ(๐โ๐ฅ)) โ โ) |
20 | | normcl 30109 |
. . . . . . 7
โข (๐ฅ โ โ โ
(normโโ๐ฅ) โ โ) |
21 | 20 | adantl 483 |
. . . . . 6
โข (((๐ โ HrmOp โง
(normopโ๐)
โ โ) โง ๐ฅ
โ โ) โ (normโโ๐ฅ) โ โ) |
22 | 19, 21 | remulcld 11190 |
. . . . 5
โข (((๐ โ HrmOp โง
(normopโ๐)
โ โ) โง ๐ฅ
โ โ) โ ((normโโ(๐โ๐ฅ)) ยท
(normโโ๐ฅ)) โ โ) |
23 | 14, 15 | sylan 581 |
. . . . . . 7
โข ((๐ โ HrmOp โง ๐ฅ โ โ) โ (๐โ๐ฅ) โ โ) |
24 | | bcs 30165 |
. . . . . . 7
โข (((๐โ๐ฅ) โ โ โง ๐ฅ โ โ) โ (absโ((๐โ๐ฅ) ยทih ๐ฅ)) โค
((normโโ(๐โ๐ฅ)) ยท
(normโโ๐ฅ))) |
25 | 23, 24 | sylancom 589 |
. . . . . 6
โข ((๐ โ HrmOp โง ๐ฅ โ โ) โ
(absโ((๐โ๐ฅ)
ยทih ๐ฅ)) โค
((normโโ(๐โ๐ฅ)) ยท
(normโโ๐ฅ))) |
26 | 25 | adantlr 714 |
. . . . 5
โข (((๐ โ HrmOp โง
(normopโ๐)
โ โ) โง ๐ฅ
โ โ) โ (absโ((๐โ๐ฅ) ยทih ๐ฅ)) โค
((normโโ(๐โ๐ฅ)) ยท
(normโโ๐ฅ))) |
27 | | remulcl 11141 |
. . . . . . . . 9
โข
(((normopโ๐) โ โ โง
(normโโ๐ฅ) โ โ) โ
((normopโ๐) ยท
(normโโ๐ฅ)) โ โ) |
28 | 20, 27 | sylan2 594 |
. . . . . . . 8
โข
(((normopโ๐) โ โ โง ๐ฅ โ โ) โ
((normopโ๐) ยท
(normโโ๐ฅ)) โ โ) |
29 | 28 | adantll 713 |
. . . . . . 7
โข (((๐ โ HrmOp โง
(normopโ๐)
โ โ) โง ๐ฅ
โ โ) โ ((normopโ๐) ยท
(normโโ๐ฅ)) โ โ) |
30 | | normge0 30110 |
. . . . . . . . 9
โข (๐ฅ โ โ โ 0 โค
(normโโ๐ฅ)) |
31 | 20, 30 | jca 513 |
. . . . . . . 8
โข (๐ฅ โ โ โ
((normโโ๐ฅ) โ โ โง 0 โค
(normโโ๐ฅ))) |
32 | 31 | adantl 483 |
. . . . . . 7
โข (((๐ โ HrmOp โง
(normopโ๐)
โ โ) โง ๐ฅ
โ โ) โ ((normโโ๐ฅ) โ โ โง 0 โค
(normโโ๐ฅ))) |
33 | | hmoplin 30926 |
. . . . . . . . 9
โข (๐ โ HrmOp โ ๐ โ LinOp) |
34 | | elbdop2 30855 |
. . . . . . . . . 10
โข (๐ โ BndLinOp โ (๐ โ LinOp โง
(normopโ๐)
โ โ)) |
35 | 34 | biimpri 227 |
. . . . . . . . 9
โข ((๐ โ LinOp โง
(normopโ๐)
โ โ) โ ๐
โ BndLinOp) |
36 | 33, 35 | sylan 581 |
. . . . . . . 8
โข ((๐ โ HrmOp โง
(normopโ๐)
โ โ) โ ๐
โ BndLinOp) |
37 | | nmbdoplb 31009 |
. . . . . . . 8
โข ((๐ โ BndLinOp โง ๐ฅ โ โ) โ
(normโโ(๐โ๐ฅ)) โค ((normopโ๐) ยท
(normโโ๐ฅ))) |
38 | 36, 37 | sylan 581 |
. . . . . . 7
โข (((๐ โ HrmOp โง
(normopโ๐)
โ โ) โง ๐ฅ
โ โ) โ (normโโ(๐โ๐ฅ)) โค ((normopโ๐) ยท
(normโโ๐ฅ))) |
39 | | lemul1a 12014 |
. . . . . . 7
โข
((((normโโ(๐โ๐ฅ)) โ โ โง
((normopโ๐) ยท
(normโโ๐ฅ)) โ โ โง
((normโโ๐ฅ) โ โ โง 0 โค
(normโโ๐ฅ))) โง
(normโโ(๐โ๐ฅ)) โค ((normopโ๐) ยท
(normโโ๐ฅ))) โ
((normโโ(๐โ๐ฅ)) ยท
(normโโ๐ฅ)) โค (((normopโ๐) ยท
(normโโ๐ฅ)) ยท
(normโโ๐ฅ))) |
40 | 19, 29, 32, 38, 39 | syl31anc 1374 |
. . . . . 6
โข (((๐ โ HrmOp โง
(normopโ๐)
โ โ) โง ๐ฅ
โ โ) โ ((normโโ(๐โ๐ฅ)) ยท
(normโโ๐ฅ)) โค (((normopโ๐) ยท
(normโโ๐ฅ)) ยท
(normโโ๐ฅ))) |
41 | | recn 11146 |
. . . . . . . . . 10
โข
((normopโ๐) โ โ โ
(normopโ๐)
โ โ) |
42 | 41 | ad2antlr 726 |
. . . . . . . . 9
โข (((๐ โ HrmOp โง
(normopโ๐)
โ โ) โง ๐ฅ
โ โ) โ (normopโ๐) โ โ) |
43 | 21 | recnd 11188 |
. . . . . . . . 9
โข (((๐ โ HrmOp โง
(normopโ๐)
โ โ) โง ๐ฅ
โ โ) โ (normโโ๐ฅ) โ โ) |
44 | 42, 43, 43 | mulassd 11183 |
. . . . . . . 8
โข (((๐ โ HrmOp โง
(normopโ๐)
โ โ) โง ๐ฅ
โ โ) โ (((normopโ๐) ยท
(normโโ๐ฅ)) ยท
(normโโ๐ฅ)) = ((normopโ๐) ยท
((normโโ๐ฅ) ยท
(normโโ๐ฅ)))) |
45 | | simpr 486 |
. . . . . . . . . 10
โข (((๐ โ HrmOp โง
(normopโ๐)
โ โ) โง ๐ฅ
โ โ) โ ๐ฅ
โ โ) |
46 | | ax-his3 30068 |
. . . . . . . . . 10
โข
(((normopโ๐) โ โ โง ๐ฅ โ โ โง ๐ฅ โ โ) โ
(((normopโ๐) ยทโ ๐ฅ)
ยทih ๐ฅ) = ((normopโ๐) ยท (๐ฅ ยทih ๐ฅ))) |
47 | 42, 45, 45, 46 | syl3anc 1372 |
. . . . . . . . 9
โข (((๐ โ HrmOp โง
(normopโ๐)
โ โ) โง ๐ฅ
โ โ) โ (((normopโ๐) ยทโ ๐ฅ)
ยทih ๐ฅ) = ((normopโ๐) ยท (๐ฅ ยทih ๐ฅ))) |
48 | 20 | recnd 11188 |
. . . . . . . . . . . . 13
โข (๐ฅ โ โ โ
(normโโ๐ฅ) โ โ) |
49 | 48 | sqvald 14054 |
. . . . . . . . . . . 12
โข (๐ฅ โ โ โ
((normโโ๐ฅ)โ2) =
((normโโ๐ฅ) ยท
(normโโ๐ฅ))) |
50 | | normsq 30118 |
. . . . . . . . . . . 12
โข (๐ฅ โ โ โ
((normโโ๐ฅ)โ2) = (๐ฅ ยทih ๐ฅ)) |
51 | 49, 50 | eqtr3d 2775 |
. . . . . . . . . . 11
โข (๐ฅ โ โ โ
((normโโ๐ฅ) ยท
(normโโ๐ฅ)) = (๐ฅ ยทih ๐ฅ)) |
52 | 51 | oveq2d 7374 |
. . . . . . . . . 10
โข (๐ฅ โ โ โ
((normopโ๐) ยท
((normโโ๐ฅ) ยท
(normโโ๐ฅ))) = ((normopโ๐) ยท (๐ฅ ยทih ๐ฅ))) |
53 | 52 | adantl 483 |
. . . . . . . . 9
โข (((๐ โ HrmOp โง
(normopโ๐)
โ โ) โง ๐ฅ
โ โ) โ ((normopโ๐) ยท
((normโโ๐ฅ) ยท
(normโโ๐ฅ))) = ((normopโ๐) ยท (๐ฅ ยทih ๐ฅ))) |
54 | 47, 53 | eqtr4d 2776 |
. . . . . . . 8
โข (((๐ โ HrmOp โง
(normopโ๐)
โ โ) โง ๐ฅ
โ โ) โ (((normopโ๐) ยทโ ๐ฅ)
ยทih ๐ฅ) = ((normopโ๐) ยท
((normโโ๐ฅ) ยท
(normโโ๐ฅ)))) |
55 | 44, 54 | eqtr4d 2776 |
. . . . . . 7
โข (((๐ โ HrmOp โง
(normopโ๐)
โ โ) โง ๐ฅ
โ โ) โ (((normopโ๐) ยท
(normโโ๐ฅ)) ยท
(normโโ๐ฅ)) = (((normopโ๐)
ยทโ ๐ฅ) ยทih ๐ฅ)) |
56 | | hoif 30738 |
. . . . . . . . . . 11
โข
Iop : โโ1-1-ontoโ โ |
57 | | f1of 6785 |
. . . . . . . . . . 11
โข (
Iop : โโ1-1-ontoโ โ โ Iop :
โโถ โ) |
58 | 56, 57 | mp1i 13 |
. . . . . . . . . 10
โข (((๐ โ HrmOp โง
(normopโ๐)
โ โ) โง ๐ฅ
โ โ) โ Iop : โโถ
โ) |
59 | | homval 30725 |
. . . . . . . . . 10
โข
(((normopโ๐) โ โ โง Iop :
โโถ โ โง ๐ฅ โ โ) โ
(((normopโ๐) ยทop
Iop )โ๐ฅ) =
((normopโ๐) ยทโ (
Iop โ๐ฅ))) |
60 | 42, 58, 45, 59 | syl3anc 1372 |
. . . . . . . . 9
โข (((๐ โ HrmOp โง
(normopโ๐)
โ โ) โง ๐ฅ
โ โ) โ (((normopโ๐) ยทop
Iop )โ๐ฅ) =
((normopโ๐) ยทโ (
Iop โ๐ฅ))) |
61 | | hoival 30739 |
. . . . . . . . . . 11
โข (๐ฅ โ โ โ (
Iop โ๐ฅ) =
๐ฅ) |
62 | 61 | oveq2d 7374 |
. . . . . . . . . 10
โข (๐ฅ โ โ โ
((normopโ๐) ยทโ (
Iop โ๐ฅ)) =
((normopโ๐) ยทโ ๐ฅ)) |
63 | 62 | adantl 483 |
. . . . . . . . 9
โข (((๐ โ HrmOp โง
(normopโ๐)
โ โ) โง ๐ฅ
โ โ) โ ((normopโ๐) ยทโ (
Iop โ๐ฅ)) =
((normopโ๐) ยทโ ๐ฅ)) |
64 | 60, 63 | eqtrd 2773 |
. . . . . . . 8
โข (((๐ โ HrmOp โง
(normopโ๐)
โ โ) โง ๐ฅ
โ โ) โ (((normopโ๐) ยทop
Iop )โ๐ฅ) =
((normopโ๐) ยทโ ๐ฅ)) |
65 | 64 | oveq1d 7373 |
. . . . . . 7
โข (((๐ โ HrmOp โง
(normopโ๐)
โ โ) โง ๐ฅ
โ โ) โ ((((normopโ๐) ยทop
Iop )โ๐ฅ)
ยทih ๐ฅ) = (((normopโ๐)
ยทโ ๐ฅ) ยทih ๐ฅ)) |
66 | 55, 65 | eqtr4d 2776 |
. . . . . 6
โข (((๐ โ HrmOp โง
(normopโ๐)
โ โ) โง ๐ฅ
โ โ) โ (((normopโ๐) ยท
(normโโ๐ฅ)) ยท
(normโโ๐ฅ)) = ((((normopโ๐) ยทop
Iop )โ๐ฅ)
ยทih ๐ฅ)) |
67 | 40, 66 | breqtrd 5132 |
. . . . 5
โข (((๐ โ HrmOp โง
(normopโ๐)
โ โ) โง ๐ฅ
โ โ) โ ((normโโ(๐โ๐ฅ)) ยท
(normโโ๐ฅ)) โค ((((normopโ๐) ยทop
Iop )โ๐ฅ)
ยทih ๐ฅ)) |
68 | 5, 22, 11, 26, 67 | letrd 11317 |
. . . 4
โข (((๐ โ HrmOp โง
(normopโ๐)
โ โ) โง ๐ฅ
โ โ) โ (absโ((๐โ๐ฅ) ยทih ๐ฅ)) โค
((((normopโ๐) ยทop
Iop )โ๐ฅ)
ยทih ๐ฅ)) |
69 | 2, 5, 11, 13, 68 | letrd 11317 |
. . 3
โข (((๐ โ HrmOp โง
(normopโ๐)
โ โ) โง ๐ฅ
โ โ) โ ((๐โ๐ฅ) ยทih ๐ฅ) โค
((((normopโ๐) ยทop
Iop )โ๐ฅ)
ยทih ๐ฅ)) |
70 | 69 | ralrimiva 3140 |
. 2
โข ((๐ โ HrmOp โง
(normopโ๐)
โ โ) โ โ๐ฅ โ โ ((๐โ๐ฅ) ยทih ๐ฅ) โค
((((normopโ๐) ยทop
Iop )โ๐ฅ)
ยทih ๐ฅ)) |
71 | | leop2 31108 |
. . 3
โข ((๐ โ HrmOp โง
((normopโ๐) ยทop
Iop ) โ HrmOp) โ (๐ โคop
((normopโ๐) ยทop
Iop ) โ โ๐ฅ โ โ ((๐โ๐ฅ) ยทih ๐ฅ) โค
((((normopโ๐) ยทop
Iop )โ๐ฅ)
ยทih ๐ฅ))) |
72 | 8, 71 | sylan2 594 |
. 2
โข ((๐ โ HrmOp โง
(normopโ๐)
โ โ) โ (๐
โคop ((normopโ๐) ยทop
Iop ) โ โ๐ฅ โ โ ((๐โ๐ฅ) ยทih ๐ฅ) โค
((((normopโ๐) ยทop
Iop )โ๐ฅ)
ยทih ๐ฅ))) |
73 | 70, 72 | mpbird 257 |
1
โข ((๐ โ HrmOp โง
(normopโ๐)
โ โ) โ ๐
โคop ((normopโ๐) ยทop
Iop )) |