Step | Hyp | Ref
| Expression |
1 | | opsqrlem1.1 |
. . . . . . . 8
โข ๐ โ HrmOp |
2 | | hmopf 30858 |
. . . . . . . 8
โข (๐ โ HrmOp โ ๐: โโถ
โ) |
3 | 1, 2 | ax-mp 5 |
. . . . . . 7
โข ๐: โโถ
โ |
4 | | nmopge0 30895 |
. . . . . . 7
โข (๐: โโถ โ โ
0 โค (normopโ๐)) |
5 | 3, 4 | ax-mp 5 |
. . . . . 6
โข 0 โค
(normopโ๐) |
6 | | opsqrlem1.2 |
. . . . . . 7
โข
(normopโ๐) โ โ |
7 | 6 | sqrtcli 15262 |
. . . . . 6
โข (0 โค
(normopโ๐)
โ (โโ(normopโ๐)) โ โ) |
8 | 5, 7 | ax-mp 5 |
. . . . 5
โข
(โโ(normopโ๐)) โ โ |
9 | | hmopm 31005 |
. . . . 5
โข
(((โโ(normopโ๐)) โ โ โง ๐ข โ HrmOp) โ
((โโ(normopโ๐)) ยทop ๐ข) โ HrmOp) |
10 | 8, 9 | mpan 689 |
. . . 4
โข (๐ข โ HrmOp โ
((โโ(normopโ๐)) ยทop ๐ข) โ HrmOp) |
11 | 10 | ad2antlr 726 |
. . 3
โข (((๐ โ 0hop โง
๐ข โ HrmOp) โง (
0hop โคop ๐ข โง (๐ข โ ๐ข) = ๐
)) โ
((โโ(normopโ๐)) ยทop ๐ข) โ HrmOp) |
12 | 6 | sqrtge0i 15267 |
. . . . . . 7
โข (0 โค
(normopโ๐)
โ 0 โค (โโ(normopโ๐))) |
13 | 5, 12 | ax-mp 5 |
. . . . . 6
โข 0 โค
(โโ(normopโ๐)) |
14 | | leopmuli 31117 |
. . . . . 6
โข
((((โโ(normopโ๐)) โ โ โง ๐ข โ HrmOp) โง (0 โค
(โโ(normopโ๐)) โง 0hop โคop
๐ข)) โ 0hop
โคop ((โโ(normopโ๐)) ยทop ๐ข)) |
15 | 13, 14 | mpanr1 702 |
. . . . 5
โข
((((โโ(normopโ๐)) โ โ โง ๐ข โ HrmOp) โง 0hop
โคop ๐ข) โ
0hop โคop
((โโ(normopโ๐)) ยทop ๐ข)) |
16 | 8, 15 | mpanl1 699 |
. . . 4
โข ((๐ข โ HrmOp โง
0hop โคop ๐ข) โ 0hop โคop
((โโ(normopโ๐)) ยทop ๐ข)) |
17 | 16 | ad2ant2lr 747 |
. . 3
โข (((๐ โ 0hop โง
๐ข โ HrmOp) โง (
0hop โคop ๐ข โง (๐ข โ ๐ข) = ๐
)) โ 0hop โคop
((โโ(normopโ๐)) ยทop ๐ข)) |
18 | | hmopf 30858 |
. . . . . . . 8
โข (๐ข โ HrmOp โ ๐ข: โโถ
โ) |
19 | 8 | recni 11174 |
. . . . . . . . 9
โข
(โโ(normopโ๐)) โ โ |
20 | | homulcl 30743 |
. . . . . . . . 9
โข
(((โโ(normopโ๐)) โ โ โง ๐ข: โโถ โ) โ
((โโ(normopโ๐)) ยทop ๐ข): โโถ
โ) |
21 | 19, 20 | mpan 689 |
. . . . . . . 8
โข (๐ข: โโถ โ โ
((โโ(normopโ๐)) ยทop ๐ข): โโถ
โ) |
22 | | homco1 30785 |
. . . . . . . . 9
โข
(((โโ(normopโ๐)) โ โ โง ๐ข: โโถ โ โง
((โโ(normopโ๐)) ยทop ๐ข): โโถ โ)
โ (((โโ(normopโ๐)) ยทop ๐ข) โ
((โโ(normopโ๐)) ยทop ๐ข)) =
((โโ(normopโ๐)) ยทop (๐ข โ
((โโ(normopโ๐)) ยทop ๐ข)))) |
23 | 19, 22 | mp3an1 1449 |
. . . . . . . 8
โข ((๐ข: โโถ โ โง
((โโ(normopโ๐)) ยทop ๐ข): โโถ โ)
โ (((โโ(normopโ๐)) ยทop ๐ข) โ
((โโ(normopโ๐)) ยทop ๐ข)) =
((โโ(normopโ๐)) ยทop (๐ข โ
((โโ(normopโ๐)) ยทop ๐ข)))) |
24 | 18, 21, 23 | syl2anc2 586 |
. . . . . . 7
โข (๐ข โ HrmOp โ
(((โโ(normopโ๐)) ยทop ๐ข) โ
((โโ(normopโ๐)) ยทop ๐ข)) =
((โโ(normopโ๐)) ยทop (๐ข โ
((โโ(normopโ๐)) ยทop ๐ข)))) |
25 | | hmoplin 30926 |
. . . . . . . . 9
โข (๐ข โ HrmOp โ ๐ข โ LinOp) |
26 | | homco2 30961 |
. . . . . . . . . 10
โข
(((โโ(normopโ๐)) โ โ โง ๐ข โ LinOp โง ๐ข: โโถ โ) โ (๐ข โ
((โโ(normopโ๐)) ยทop ๐ข)) =
((โโ(normopโ๐)) ยทop (๐ข โ ๐ข))) |
27 | 19, 26 | mp3an1 1449 |
. . . . . . . . 9
โข ((๐ข โ LinOp โง ๐ข: โโถ โ)
โ (๐ข โ
((โโ(normopโ๐)) ยทop ๐ข)) =
((โโ(normopโ๐)) ยทop (๐ข โ ๐ข))) |
28 | 25, 18, 27 | syl2anc 585 |
. . . . . . . 8
โข (๐ข โ HrmOp โ (๐ข โ
((โโ(normopโ๐)) ยทop ๐ข)) =
((โโ(normopโ๐)) ยทop (๐ข โ ๐ข))) |
29 | 28 | oveq2d 7374 |
. . . . . . 7
โข (๐ข โ HrmOp โ
((โโ(normopโ๐)) ยทop (๐ข โ
((โโ(normopโ๐)) ยทop ๐ข))) =
((โโ(normopโ๐)) ยทop
((โโ(normopโ๐)) ยทop (๐ข โ ๐ข)))) |
30 | | fco 6693 |
. . . . . . . . . 10
โข ((๐ข: โโถ โ โง
๐ข: โโถ โ)
โ (๐ข โ ๐ข): โโถ
โ) |
31 | 18, 18, 30 | syl2anc 585 |
. . . . . . . . 9
โข (๐ข โ HrmOp โ (๐ข โ ๐ข): โโถ โ) |
32 | | homulass 30786 |
. . . . . . . . . 10
โข
(((โโ(normopโ๐)) โ โ โง
(โโ(normopโ๐)) โ โ โง (๐ข โ ๐ข): โโถ โ) โ
(((โโ(normopโ๐)) ยท
(โโ(normopโ๐))) ยทop (๐ข โ ๐ข)) =
((โโ(normopโ๐)) ยทop
((โโ(normopโ๐)) ยทop (๐ข โ ๐ข)))) |
33 | 19, 19, 32 | mp3an12 1452 |
. . . . . . . . 9
โข ((๐ข โ ๐ข): โโถ โ โ
(((โโ(normopโ๐)) ยท
(โโ(normopโ๐))) ยทop (๐ข โ ๐ข)) =
((โโ(normopโ๐)) ยทop
((โโ(normopโ๐)) ยทop (๐ข โ ๐ข)))) |
34 | 31, 33 | syl 17 |
. . . . . . . 8
โข (๐ข โ HrmOp โ
(((โโ(normopโ๐)) ยท
(โโ(normopโ๐))) ยทop (๐ข โ ๐ข)) =
((โโ(normopโ๐)) ยทop
((โโ(normopโ๐)) ยทop (๐ข โ ๐ข)))) |
35 | 6 | sqrtthi 15261 |
. . . . . . . . . 10
โข (0 โค
(normopโ๐)
โ ((โโ(normopโ๐)) ยท
(โโ(normopโ๐))) = (normopโ๐)) |
36 | 5, 35 | ax-mp 5 |
. . . . . . . . 9
โข
((โโ(normopโ๐)) ยท
(โโ(normopโ๐))) = (normopโ๐) |
37 | 36 | oveq1i 7368 |
. . . . . . . 8
โข
(((โโ(normopโ๐)) ยท
(โโ(normopโ๐))) ยทop (๐ข โ ๐ข)) = ((normopโ๐) ยทop
(๐ข โ ๐ข)) |
38 | 34, 37 | eqtr3di 2788 |
. . . . . . 7
โข (๐ข โ HrmOp โ
((โโ(normopโ๐)) ยทop
((โโ(normopโ๐)) ยทop (๐ข โ ๐ข))) = ((normopโ๐) ยทop
(๐ข โ ๐ข))) |
39 | 24, 29, 38 | 3eqtrd 2777 |
. . . . . 6
โข (๐ข โ HrmOp โ
(((โโ(normopโ๐)) ยทop ๐ข) โ
((โโ(normopโ๐)) ยทop ๐ข)) =
((normopโ๐) ยทop (๐ข โ ๐ข))) |
40 | 39 | ad2antlr 726 |
. . . . 5
โข (((๐ โ 0hop โง
๐ข โ HrmOp) โง
(๐ข โ ๐ข) = ๐
) โ
(((โโ(normopโ๐)) ยทop ๐ข) โ
((โโ(normopโ๐)) ยทop ๐ข)) =
((normopโ๐) ยทop (๐ข โ ๐ข))) |
41 | | id 22 |
. . . . . . . . 9
โข ((๐ข โ ๐ข) = ๐
โ (๐ข โ ๐ข) = ๐
) |
42 | | opsqrlem1.4 |
. . . . . . . . 9
โข ๐
= ((1 /
(normopโ๐)) ยทop ๐) |
43 | 41, 42 | eqtrdi 2789 |
. . . . . . . 8
โข ((๐ข โ ๐ข) = ๐
โ (๐ข โ ๐ข) = ((1 / (normopโ๐)) ยทop
๐)) |
44 | 43 | oveq2d 7374 |
. . . . . . 7
โข ((๐ข โ ๐ข) = ๐
โ ((normopโ๐) ยทop
(๐ข โ ๐ข)) =
((normopโ๐) ยทop ((1 /
(normopโ๐)) ยทop ๐))) |
45 | | hmoplin 30926 |
. . . . . . . . . . . 12
โข (๐ โ HrmOp โ ๐ โ LinOp) |
46 | 1, 45 | ax-mp 5 |
. . . . . . . . . . 11
โข ๐ โ LinOp |
47 | | nmlnopne0 30983 |
. . . . . . . . . . 11
โข (๐ โ LinOp โ
((normopโ๐) โ 0 โ ๐ โ 0hop )) |
48 | 46, 47 | ax-mp 5 |
. . . . . . . . . 10
โข
((normopโ๐) โ 0 โ ๐ โ 0hop ) |
49 | 6 | recni 11174 |
. . . . . . . . . . 11
โข
(normopโ๐) โ โ |
50 | 49 | recidzi 11887 |
. . . . . . . . . 10
โข
((normopโ๐) โ 0 โ
((normopโ๐) ยท (1 /
(normopโ๐))) = 1) |
51 | 48, 50 | sylbir 234 |
. . . . . . . . 9
โข (๐ โ 0hop โ
((normopโ๐) ยท (1 /
(normopโ๐))) = 1) |
52 | 51 | oveq1d 7373 |
. . . . . . . 8
โข (๐ โ 0hop โ
(((normopโ๐) ยท (1 /
(normopโ๐))) ยทop ๐) = (1
ยทop ๐)) |
53 | 6 | rerecclzi 11924 |
. . . . . . . . . . 11
โข
((normopโ๐) โ 0 โ (1 /
(normopโ๐)) โ โ) |
54 | 48, 53 | sylbir 234 |
. . . . . . . . . 10
โข (๐ โ 0hop โ (1
/ (normopโ๐)) โ โ) |
55 | 54 | recnd 11188 |
. . . . . . . . 9
โข (๐ โ 0hop โ (1
/ (normopโ๐)) โ โ) |
56 | | homulass 30786 |
. . . . . . . . . 10
โข
(((normopโ๐) โ โ โง (1 /
(normopโ๐)) โ โ โง ๐: โโถ โ) โ
(((normopโ๐) ยท (1 /
(normopโ๐))) ยทop ๐) =
((normopโ๐) ยทop ((1 /
(normopโ๐)) ยทop ๐))) |
57 | 49, 3, 56 | mp3an13 1453 |
. . . . . . . . 9
โข ((1 /
(normopโ๐)) โ โ โ
(((normopโ๐) ยท (1 /
(normopโ๐))) ยทop ๐) =
((normopโ๐) ยทop ((1 /
(normopโ๐)) ยทop ๐))) |
58 | 55, 57 | syl 17 |
. . . . . . . 8
โข (๐ โ 0hop โ
(((normopโ๐) ยท (1 /
(normopโ๐))) ยทop ๐) =
((normopโ๐) ยทop ((1 /
(normopโ๐)) ยทop ๐))) |
59 | | homulid2 30784 |
. . . . . . . . 9
โข (๐: โโถ โ โ
(1 ยทop ๐) = ๐) |
60 | 3, 59 | mp1i 13 |
. . . . . . . 8
โข (๐ โ 0hop โ (1
ยทop ๐) = ๐) |
61 | 52, 58, 60 | 3eqtr3d 2781 |
. . . . . . 7
โข (๐ โ 0hop โ
((normopโ๐) ยทop ((1 /
(normopโ๐)) ยทop ๐)) = ๐) |
62 | 44, 61 | sylan9eqr 2795 |
. . . . . 6
โข ((๐ โ 0hop โง
(๐ข โ ๐ข) = ๐
) โ ((normopโ๐) ยทop
(๐ข โ ๐ข)) = ๐) |
63 | 62 | adantlr 714 |
. . . . 5
โข (((๐ โ 0hop โง
๐ข โ HrmOp) โง
(๐ข โ ๐ข) = ๐
) โ ((normopโ๐) ยทop
(๐ข โ ๐ข)) = ๐) |
64 | 40, 63 | eqtrd 2773 |
. . . 4
โข (((๐ โ 0hop โง
๐ข โ HrmOp) โง
(๐ข โ ๐ข) = ๐
) โ
(((โโ(normopโ๐)) ยทop ๐ข) โ
((โโ(normopโ๐)) ยทop ๐ข)) = ๐) |
65 | 64 | adantrl 715 |
. . 3
โข (((๐ โ 0hop โง
๐ข โ HrmOp) โง (
0hop โคop ๐ข โง (๐ข โ ๐ข) = ๐
)) โ
(((โโ(normopโ๐)) ยทop ๐ข) โ
((โโ(normopโ๐)) ยทop ๐ข)) = ๐) |
66 | | breq2 5110 |
. . . . 5
โข (๐ฃ =
((โโ(normopโ๐)) ยทop ๐ข) โ ( 0hop
โคop ๐ฃ โ
0hop โคop
((โโ(normopโ๐)) ยทop ๐ข))) |
67 | | coeq1 5814 |
. . . . . . 7
โข (๐ฃ =
((โโ(normopโ๐)) ยทop ๐ข) โ (๐ฃ โ ๐ฃ) =
(((โโ(normopโ๐)) ยทop ๐ข) โ ๐ฃ)) |
68 | | coeq2 5815 |
. . . . . . 7
โข (๐ฃ =
((โโ(normopโ๐)) ยทop ๐ข) โ
(((โโ(normopโ๐)) ยทop ๐ข) โ ๐ฃ) =
(((โโ(normopโ๐)) ยทop ๐ข) โ
((โโ(normopโ๐)) ยทop ๐ข))) |
69 | 67, 68 | eqtrd 2773 |
. . . . . 6
โข (๐ฃ =
((โโ(normopโ๐)) ยทop ๐ข) โ (๐ฃ โ ๐ฃ) =
(((โโ(normopโ๐)) ยทop ๐ข) โ
((โโ(normopโ๐)) ยทop ๐ข))) |
70 | 69 | eqeq1d 2735 |
. . . . 5
โข (๐ฃ =
((โโ(normopโ๐)) ยทop ๐ข) โ ((๐ฃ โ ๐ฃ) = ๐ โ
(((โโ(normopโ๐)) ยทop ๐ข) โ
((โโ(normopโ๐)) ยทop ๐ข)) = ๐)) |
71 | 66, 70 | anbi12d 632 |
. . . 4
โข (๐ฃ =
((โโ(normopโ๐)) ยทop ๐ข) โ (( 0hop
โคop ๐ฃ โง
(๐ฃ โ ๐ฃ) = ๐) โ ( 0hop โคop
((โโ(normopโ๐)) ยทop ๐ข) โง
(((โโ(normopโ๐)) ยทop ๐ข) โ
((โโ(normopโ๐)) ยทop ๐ข)) = ๐))) |
72 | 71 | rspcev 3580 |
. . 3
โข
((((โโ(normopโ๐)) ยทop ๐ข) โ HrmOp โง (
0hop โคop
((โโ(normopโ๐)) ยทop ๐ข) โง
(((โโ(normopโ๐)) ยทop ๐ข) โ
((โโ(normopโ๐)) ยทop ๐ข)) = ๐)) โ โ๐ฃ โ HrmOp ( 0hop
โคop ๐ฃ โง
(๐ฃ โ ๐ฃ) = ๐)) |
73 | 11, 17, 65, 72 | syl12anc 836 |
. 2
โข (((๐ โ 0hop โง
๐ข โ HrmOp) โง (
0hop โคop ๐ข โง (๐ข โ ๐ข) = ๐
)) โ โ๐ฃ โ HrmOp ( 0hop
โคop ๐ฃ โง
(๐ฃ โ ๐ฃ) = ๐)) |
74 | | opsqrlem1.5 |
. 2
โข (๐ โ 0hop โ
โ๐ข โ HrmOp (
0hop โคop ๐ข โง (๐ข โ ๐ข) = ๐
)) |
75 | 73, 74 | r19.29a 3156 |
1
โข (๐ โ 0hop โ
โ๐ฃ โ HrmOp (
0hop โคop ๐ฃ โง (๐ฃ โ ๐ฃ) = ๐)) |