Step |
Hyp |
Ref |
Expression |
1 |
|
ipblnfi.1 |
โข ๐ = ( BaseSet โ ๐ ) |
2 |
|
ipblnfi.7 |
โข ๐ = ( ยท๐OLD โ ๐ ) |
3 |
|
ipblnfi.9 |
โข ๐ โ CPreHilOLD |
4 |
|
ipblnfi.c |
โข ๐ถ = โจ โจ + , ยท โฉ , abs โฉ |
5 |
|
ipblnfi.l |
โข ๐ต = ( ๐ BLnOp ๐ถ ) |
6 |
|
ipblnfi.f |
โข ๐น = ( ๐ฅ โ ๐ โฆ ( ๐ฅ ๐ ๐ด ) ) |
7 |
3
|
phnvi |
โข ๐ โ NrmCVec |
8 |
1 2
|
dipcl |
โข ( ( ๐ โ NrmCVec โง ๐ฅ โ ๐ โง ๐ด โ ๐ ) โ ( ๐ฅ ๐ ๐ด ) โ โ ) |
9 |
7 8
|
mp3an1 |
โข ( ( ๐ฅ โ ๐ โง ๐ด โ ๐ ) โ ( ๐ฅ ๐ ๐ด ) โ โ ) |
10 |
9
|
ancoms |
โข ( ( ๐ด โ ๐ โง ๐ฅ โ ๐ ) โ ( ๐ฅ ๐ ๐ด ) โ โ ) |
11 |
10 6
|
fmptd |
โข ( ๐ด โ ๐ โ ๐น : ๐ โถ โ ) |
12 |
|
eqid |
โข ( ยท๐ OLD โ ๐ ) = ( ยท๐ OLD โ ๐ ) |
13 |
1 12
|
nvscl |
โข ( ( ๐ โ NrmCVec โง ๐ฆ โ โ โง ๐ง โ ๐ ) โ ( ๐ฆ ( ยท๐ OLD โ ๐ ) ๐ง ) โ ๐ ) |
14 |
7 13
|
mp3an1 |
โข ( ( ๐ฆ โ โ โง ๐ง โ ๐ ) โ ( ๐ฆ ( ยท๐ OLD โ ๐ ) ๐ง ) โ ๐ ) |
15 |
14
|
ad2ant2lr |
โข ( ( ( ๐ด โ ๐ โง ๐ฆ โ โ ) โง ( ๐ง โ ๐ โง ๐ค โ ๐ ) ) โ ( ๐ฆ ( ยท๐ OLD โ ๐ ) ๐ง ) โ ๐ ) |
16 |
|
simprr |
โข ( ( ( ๐ด โ ๐ โง ๐ฆ โ โ ) โง ( ๐ง โ ๐ โง ๐ค โ ๐ ) ) โ ๐ค โ ๐ ) |
17 |
|
simpll |
โข ( ( ( ๐ด โ ๐ โง ๐ฆ โ โ ) โง ( ๐ง โ ๐ โง ๐ค โ ๐ ) ) โ ๐ด โ ๐ ) |
18 |
|
eqid |
โข ( +๐ฃ โ ๐ ) = ( +๐ฃ โ ๐ ) |
19 |
1 18 2
|
dipdir |
โข ( ( ๐ โ CPreHilOLD โง ( ( ๐ฆ ( ยท๐ OLD โ ๐ ) ๐ง ) โ ๐ โง ๐ค โ ๐ โง ๐ด โ ๐ ) ) โ ( ( ( ๐ฆ ( ยท๐ OLD โ ๐ ) ๐ง ) ( +๐ฃ โ ๐ ) ๐ค ) ๐ ๐ด ) = ( ( ( ๐ฆ ( ยท๐ OLD โ ๐ ) ๐ง ) ๐ ๐ด ) + ( ๐ค ๐ ๐ด ) ) ) |
20 |
3 19
|
mpan |
โข ( ( ( ๐ฆ ( ยท๐ OLD โ ๐ ) ๐ง ) โ ๐ โง ๐ค โ ๐ โง ๐ด โ ๐ ) โ ( ( ( ๐ฆ ( ยท๐ OLD โ ๐ ) ๐ง ) ( +๐ฃ โ ๐ ) ๐ค ) ๐ ๐ด ) = ( ( ( ๐ฆ ( ยท๐ OLD โ ๐ ) ๐ง ) ๐ ๐ด ) + ( ๐ค ๐ ๐ด ) ) ) |
21 |
15 16 17 20
|
syl3anc |
โข ( ( ( ๐ด โ ๐ โง ๐ฆ โ โ ) โง ( ๐ง โ ๐ โง ๐ค โ ๐ ) ) โ ( ( ( ๐ฆ ( ยท๐ OLD โ ๐ ) ๐ง ) ( +๐ฃ โ ๐ ) ๐ค ) ๐ ๐ด ) = ( ( ( ๐ฆ ( ยท๐ OLD โ ๐ ) ๐ง ) ๐ ๐ด ) + ( ๐ค ๐ ๐ด ) ) ) |
22 |
|
simplr |
โข ( ( ( ๐ด โ ๐ โง ๐ฆ โ โ ) โง ( ๐ง โ ๐ โง ๐ค โ ๐ ) ) โ ๐ฆ โ โ ) |
23 |
|
simprl |
โข ( ( ( ๐ด โ ๐ โง ๐ฆ โ โ ) โง ( ๐ง โ ๐ โง ๐ค โ ๐ ) ) โ ๐ง โ ๐ ) |
24 |
1 18 12 2 3
|
ipassi |
โข ( ( ๐ฆ โ โ โง ๐ง โ ๐ โง ๐ด โ ๐ ) โ ( ( ๐ฆ ( ยท๐ OLD โ ๐ ) ๐ง ) ๐ ๐ด ) = ( ๐ฆ ยท ( ๐ง ๐ ๐ด ) ) ) |
25 |
22 23 17 24
|
syl3anc |
โข ( ( ( ๐ด โ ๐ โง ๐ฆ โ โ ) โง ( ๐ง โ ๐ โง ๐ค โ ๐ ) ) โ ( ( ๐ฆ ( ยท๐ OLD โ ๐ ) ๐ง ) ๐ ๐ด ) = ( ๐ฆ ยท ( ๐ง ๐ ๐ด ) ) ) |
26 |
25
|
oveq1d |
โข ( ( ( ๐ด โ ๐ โง ๐ฆ โ โ ) โง ( ๐ง โ ๐ โง ๐ค โ ๐ ) ) โ ( ( ( ๐ฆ ( ยท๐ OLD โ ๐ ) ๐ง ) ๐ ๐ด ) + ( ๐ค ๐ ๐ด ) ) = ( ( ๐ฆ ยท ( ๐ง ๐ ๐ด ) ) + ( ๐ค ๐ ๐ด ) ) ) |
27 |
21 26
|
eqtrd |
โข ( ( ( ๐ด โ ๐ โง ๐ฆ โ โ ) โง ( ๐ง โ ๐ โง ๐ค โ ๐ ) ) โ ( ( ( ๐ฆ ( ยท๐ OLD โ ๐ ) ๐ง ) ( +๐ฃ โ ๐ ) ๐ค ) ๐ ๐ด ) = ( ( ๐ฆ ยท ( ๐ง ๐ ๐ด ) ) + ( ๐ค ๐ ๐ด ) ) ) |
28 |
14
|
adantll |
โข ( ( ( ๐ด โ ๐ โง ๐ฆ โ โ ) โง ๐ง โ ๐ ) โ ( ๐ฆ ( ยท๐ OLD โ ๐ ) ๐ง ) โ ๐ ) |
29 |
1 18
|
nvgcl |
โข ( ( ๐ โ NrmCVec โง ( ๐ฆ ( ยท๐ OLD โ ๐ ) ๐ง ) โ ๐ โง ๐ค โ ๐ ) โ ( ( ๐ฆ ( ยท๐ OLD โ ๐ ) ๐ง ) ( +๐ฃ โ ๐ ) ๐ค ) โ ๐ ) |
30 |
7 29
|
mp3an1 |
โข ( ( ( ๐ฆ ( ยท๐ OLD โ ๐ ) ๐ง ) โ ๐ โง ๐ค โ ๐ ) โ ( ( ๐ฆ ( ยท๐ OLD โ ๐ ) ๐ง ) ( +๐ฃ โ ๐ ) ๐ค ) โ ๐ ) |
31 |
28 30
|
sylan |
โข ( ( ( ( ๐ด โ ๐ โง ๐ฆ โ โ ) โง ๐ง โ ๐ ) โง ๐ค โ ๐ ) โ ( ( ๐ฆ ( ยท๐ OLD โ ๐ ) ๐ง ) ( +๐ฃ โ ๐ ) ๐ค ) โ ๐ ) |
32 |
31
|
anasss |
โข ( ( ( ๐ด โ ๐ โง ๐ฆ โ โ ) โง ( ๐ง โ ๐ โง ๐ค โ ๐ ) ) โ ( ( ๐ฆ ( ยท๐ OLD โ ๐ ) ๐ง ) ( +๐ฃ โ ๐ ) ๐ค ) โ ๐ ) |
33 |
|
oveq1 |
โข ( ๐ฅ = ( ( ๐ฆ ( ยท๐ OLD โ ๐ ) ๐ง ) ( +๐ฃ โ ๐ ) ๐ค ) โ ( ๐ฅ ๐ ๐ด ) = ( ( ( ๐ฆ ( ยท๐ OLD โ ๐ ) ๐ง ) ( +๐ฃ โ ๐ ) ๐ค ) ๐ ๐ด ) ) |
34 |
|
ovex |
โข ( ( ( ๐ฆ ( ยท๐ OLD โ ๐ ) ๐ง ) ( +๐ฃ โ ๐ ) ๐ค ) ๐ ๐ด ) โ V |
35 |
33 6 34
|
fvmpt |
โข ( ( ( ๐ฆ ( ยท๐ OLD โ ๐ ) ๐ง ) ( +๐ฃ โ ๐ ) ๐ค ) โ ๐ โ ( ๐น โ ( ( ๐ฆ ( ยท๐ OLD โ ๐ ) ๐ง ) ( +๐ฃ โ ๐ ) ๐ค ) ) = ( ( ( ๐ฆ ( ยท๐ OLD โ ๐ ) ๐ง ) ( +๐ฃ โ ๐ ) ๐ค ) ๐ ๐ด ) ) |
36 |
32 35
|
syl |
โข ( ( ( ๐ด โ ๐ โง ๐ฆ โ โ ) โง ( ๐ง โ ๐ โง ๐ค โ ๐ ) ) โ ( ๐น โ ( ( ๐ฆ ( ยท๐ OLD โ ๐ ) ๐ง ) ( +๐ฃ โ ๐ ) ๐ค ) ) = ( ( ( ๐ฆ ( ยท๐ OLD โ ๐ ) ๐ง ) ( +๐ฃ โ ๐ ) ๐ค ) ๐ ๐ด ) ) |
37 |
|
oveq1 |
โข ( ๐ฅ = ๐ง โ ( ๐ฅ ๐ ๐ด ) = ( ๐ง ๐ ๐ด ) ) |
38 |
|
ovex |
โข ( ๐ง ๐ ๐ด ) โ V |
39 |
37 6 38
|
fvmpt |
โข ( ๐ง โ ๐ โ ( ๐น โ ๐ง ) = ( ๐ง ๐ ๐ด ) ) |
40 |
39
|
ad2antrl |
โข ( ( ( ๐ด โ ๐ โง ๐ฆ โ โ ) โง ( ๐ง โ ๐ โง ๐ค โ ๐ ) ) โ ( ๐น โ ๐ง ) = ( ๐ง ๐ ๐ด ) ) |
41 |
40
|
oveq2d |
โข ( ( ( ๐ด โ ๐ โง ๐ฆ โ โ ) โง ( ๐ง โ ๐ โง ๐ค โ ๐ ) ) โ ( ๐ฆ ยท ( ๐น โ ๐ง ) ) = ( ๐ฆ ยท ( ๐ง ๐ ๐ด ) ) ) |
42 |
|
oveq1 |
โข ( ๐ฅ = ๐ค โ ( ๐ฅ ๐ ๐ด ) = ( ๐ค ๐ ๐ด ) ) |
43 |
|
ovex |
โข ( ๐ค ๐ ๐ด ) โ V |
44 |
42 6 43
|
fvmpt |
โข ( ๐ค โ ๐ โ ( ๐น โ ๐ค ) = ( ๐ค ๐ ๐ด ) ) |
45 |
44
|
ad2antll |
โข ( ( ( ๐ด โ ๐ โง ๐ฆ โ โ ) โง ( ๐ง โ ๐ โง ๐ค โ ๐ ) ) โ ( ๐น โ ๐ค ) = ( ๐ค ๐ ๐ด ) ) |
46 |
41 45
|
oveq12d |
โข ( ( ( ๐ด โ ๐ โง ๐ฆ โ โ ) โง ( ๐ง โ ๐ โง ๐ค โ ๐ ) ) โ ( ( ๐ฆ ยท ( ๐น โ ๐ง ) ) + ( ๐น โ ๐ค ) ) = ( ( ๐ฆ ยท ( ๐ง ๐ ๐ด ) ) + ( ๐ค ๐ ๐ด ) ) ) |
47 |
27 36 46
|
3eqtr4d |
โข ( ( ( ๐ด โ ๐ โง ๐ฆ โ โ ) โง ( ๐ง โ ๐ โง ๐ค โ ๐ ) ) โ ( ๐น โ ( ( ๐ฆ ( ยท๐ OLD โ ๐ ) ๐ง ) ( +๐ฃ โ ๐ ) ๐ค ) ) = ( ( ๐ฆ ยท ( ๐น โ ๐ง ) ) + ( ๐น โ ๐ค ) ) ) |
48 |
47
|
ralrimivva |
โข ( ( ๐ด โ ๐ โง ๐ฆ โ โ ) โ โ ๐ง โ ๐ โ ๐ค โ ๐ ( ๐น โ ( ( ๐ฆ ( ยท๐ OLD โ ๐ ) ๐ง ) ( +๐ฃ โ ๐ ) ๐ค ) ) = ( ( ๐ฆ ยท ( ๐น โ ๐ง ) ) + ( ๐น โ ๐ค ) ) ) |
49 |
48
|
ralrimiva |
โข ( ๐ด โ ๐ โ โ ๐ฆ โ โ โ ๐ง โ ๐ โ ๐ค โ ๐ ( ๐น โ ( ( ๐ฆ ( ยท๐ OLD โ ๐ ) ๐ง ) ( +๐ฃ โ ๐ ) ๐ค ) ) = ( ( ๐ฆ ยท ( ๐น โ ๐ง ) ) + ( ๐น โ ๐ค ) ) ) |
50 |
4
|
cnnv |
โข ๐ถ โ NrmCVec |
51 |
4
|
cnnvba |
โข โ = ( BaseSet โ ๐ถ ) |
52 |
4
|
cnnvg |
โข + = ( +๐ฃ โ ๐ถ ) |
53 |
4
|
cnnvs |
โข ยท = ( ยท๐ OLD โ ๐ถ ) |
54 |
|
eqid |
โข ( ๐ LnOp ๐ถ ) = ( ๐ LnOp ๐ถ ) |
55 |
1 51 18 52 12 53 54
|
islno |
โข ( ( ๐ โ NrmCVec โง ๐ถ โ NrmCVec ) โ ( ๐น โ ( ๐ LnOp ๐ถ ) โ ( ๐น : ๐ โถ โ โง โ ๐ฆ โ โ โ ๐ง โ ๐ โ ๐ค โ ๐ ( ๐น โ ( ( ๐ฆ ( ยท๐ OLD โ ๐ ) ๐ง ) ( +๐ฃ โ ๐ ) ๐ค ) ) = ( ( ๐ฆ ยท ( ๐น โ ๐ง ) ) + ( ๐น โ ๐ค ) ) ) ) ) |
56 |
7 50 55
|
mp2an |
โข ( ๐น โ ( ๐ LnOp ๐ถ ) โ ( ๐น : ๐ โถ โ โง โ ๐ฆ โ โ โ ๐ง โ ๐ โ ๐ค โ ๐ ( ๐น โ ( ( ๐ฆ ( ยท๐ OLD โ ๐ ) ๐ง ) ( +๐ฃ โ ๐ ) ๐ค ) ) = ( ( ๐ฆ ยท ( ๐น โ ๐ง ) ) + ( ๐น โ ๐ค ) ) ) ) |
57 |
11 49 56
|
sylanbrc |
โข ( ๐ด โ ๐ โ ๐น โ ( ๐ LnOp ๐ถ ) ) |
58 |
|
eqid |
โข ( normCV โ ๐ ) = ( normCV โ ๐ ) |
59 |
1 58
|
nvcl |
โข ( ( ๐ โ NrmCVec โง ๐ด โ ๐ ) โ ( ( normCV โ ๐ ) โ ๐ด ) โ โ ) |
60 |
7 59
|
mpan |
โข ( ๐ด โ ๐ โ ( ( normCV โ ๐ ) โ ๐ด ) โ โ ) |
61 |
1 58 2 3
|
sii |
โข ( ( ๐ง โ ๐ โง ๐ด โ ๐ ) โ ( abs โ ( ๐ง ๐ ๐ด ) ) โค ( ( ( normCV โ ๐ ) โ ๐ง ) ยท ( ( normCV โ ๐ ) โ ๐ด ) ) ) |
62 |
61
|
ancoms |
โข ( ( ๐ด โ ๐ โง ๐ง โ ๐ ) โ ( abs โ ( ๐ง ๐ ๐ด ) ) โค ( ( ( normCV โ ๐ ) โ ๐ง ) ยท ( ( normCV โ ๐ ) โ ๐ด ) ) ) |
63 |
39
|
adantl |
โข ( ( ๐ด โ ๐ โง ๐ง โ ๐ ) โ ( ๐น โ ๐ง ) = ( ๐ง ๐ ๐ด ) ) |
64 |
63
|
fveq2d |
โข ( ( ๐ด โ ๐ โง ๐ง โ ๐ ) โ ( abs โ ( ๐น โ ๐ง ) ) = ( abs โ ( ๐ง ๐ ๐ด ) ) ) |
65 |
60
|
recnd |
โข ( ๐ด โ ๐ โ ( ( normCV โ ๐ ) โ ๐ด ) โ โ ) |
66 |
1 58
|
nvcl |
โข ( ( ๐ โ NrmCVec โง ๐ง โ ๐ ) โ ( ( normCV โ ๐ ) โ ๐ง ) โ โ ) |
67 |
7 66
|
mpan |
โข ( ๐ง โ ๐ โ ( ( normCV โ ๐ ) โ ๐ง ) โ โ ) |
68 |
67
|
recnd |
โข ( ๐ง โ ๐ โ ( ( normCV โ ๐ ) โ ๐ง ) โ โ ) |
69 |
|
mulcom |
โข ( ( ( ( normCV โ ๐ ) โ ๐ด ) โ โ โง ( ( normCV โ ๐ ) โ ๐ง ) โ โ ) โ ( ( ( normCV โ ๐ ) โ ๐ด ) ยท ( ( normCV โ ๐ ) โ ๐ง ) ) = ( ( ( normCV โ ๐ ) โ ๐ง ) ยท ( ( normCV โ ๐ ) โ ๐ด ) ) ) |
70 |
65 68 69
|
syl2an |
โข ( ( ๐ด โ ๐ โง ๐ง โ ๐ ) โ ( ( ( normCV โ ๐ ) โ ๐ด ) ยท ( ( normCV โ ๐ ) โ ๐ง ) ) = ( ( ( normCV โ ๐ ) โ ๐ง ) ยท ( ( normCV โ ๐ ) โ ๐ด ) ) ) |
71 |
62 64 70
|
3brtr4d |
โข ( ( ๐ด โ ๐ โง ๐ง โ ๐ ) โ ( abs โ ( ๐น โ ๐ง ) ) โค ( ( ( normCV โ ๐ ) โ ๐ด ) ยท ( ( normCV โ ๐ ) โ ๐ง ) ) ) |
72 |
71
|
ralrimiva |
โข ( ๐ด โ ๐ โ โ ๐ง โ ๐ ( abs โ ( ๐น โ ๐ง ) ) โค ( ( ( normCV โ ๐ ) โ ๐ด ) ยท ( ( normCV โ ๐ ) โ ๐ง ) ) ) |
73 |
4
|
cnnvnm |
โข abs = ( normCV โ ๐ถ ) |
74 |
1 58 73 54 5 7 50
|
blo3i |
โข ( ( ๐น โ ( ๐ LnOp ๐ถ ) โง ( ( normCV โ ๐ ) โ ๐ด ) โ โ โง โ ๐ง โ ๐ ( abs โ ( ๐น โ ๐ง ) ) โค ( ( ( normCV โ ๐ ) โ ๐ด ) ยท ( ( normCV โ ๐ ) โ ๐ง ) ) ) โ ๐น โ ๐ต ) |
75 |
57 60 72 74
|
syl3anc |
โข ( ๐ด โ ๐ โ ๐น โ ๐ต ) |