Step | Hyp | Ref
| Expression |
1 | | ipblnfi.9 |
. . . . . . 7
β’ π β
CPreHilOLD |
2 | 1 | phnvi 29800 |
. . . . . 6
β’ π β NrmCVec |
3 | | ipblnfi.1 |
. . . . . . 7
β’ π = (BaseSetβπ) |
4 | | ipblnfi.7 |
. . . . . . 7
β’ π =
(Β·πOLDβπ) |
5 | 3, 4 | dipcl 29696 |
. . . . . 6
β’ ((π β NrmCVec β§ π₯ β π β§ π΄ β π) β (π₯ππ΄) β β) |
6 | 2, 5 | mp3an1 1449 |
. . . . 5
β’ ((π₯ β π β§ π΄ β π) β (π₯ππ΄) β β) |
7 | 6 | ancoms 460 |
. . . 4
β’ ((π΄ β π β§ π₯ β π) β (π₯ππ΄) β β) |
8 | | ipblnfi.f |
. . . 4
β’ πΉ = (π₯ β π β¦ (π₯ππ΄)) |
9 | 7, 8 | fmptd 7067 |
. . 3
β’ (π΄ β π β πΉ:πβΆβ) |
10 | | eqid 2737 |
. . . . . . . . . . 11
β’ (
Β·π OLD βπ) = ( Β·π OLD
βπ) |
11 | 3, 10 | nvscl 29610 |
. . . . . . . . . 10
β’ ((π β NrmCVec β§ π¦ β β β§ π§ β π) β (π¦( Β·π OLD
βπ)π§) β π) |
12 | 2, 11 | mp3an1 1449 |
. . . . . . . . 9
β’ ((π¦ β β β§ π§ β π) β (π¦( Β·π OLD
βπ)π§) β π) |
13 | 12 | ad2ant2lr 747 |
. . . . . . . 8
β’ (((π΄ β π β§ π¦ β β) β§ (π§ β π β§ π€ β π)) β (π¦( Β·π OLD
βπ)π§) β π) |
14 | | simprr 772 |
. . . . . . . 8
β’ (((π΄ β π β§ π¦ β β) β§ (π§ β π β§ π€ β π)) β π€ β π) |
15 | | simpll 766 |
. . . . . . . 8
β’ (((π΄ β π β§ π¦ β β) β§ (π§ β π β§ π€ β π)) β π΄ β π) |
16 | | eqid 2737 |
. . . . . . . . . 10
β’ (
+π£ βπ) = ( +π£ βπ) |
17 | 3, 16, 4 | dipdir 29826 |
. . . . . . . . 9
β’ ((π β CPreHilOLD
β§ ((π¦(
Β·π OLD βπ)π§) β π β§ π€ β π β§ π΄ β π)) β (((π¦( Β·π OLD
βπ)π§)( +π£ βπ)π€)ππ΄) = (((π¦( Β·π OLD
βπ)π§)ππ΄) + (π€ππ΄))) |
18 | 1, 17 | mpan 689 |
. . . . . . . 8
β’ (((π¦(
Β·π OLD βπ)π§) β π β§ π€ β π β§ π΄ β π) β (((π¦( Β·π OLD
βπ)π§)( +π£ βπ)π€)ππ΄) = (((π¦( Β·π OLD
βπ)π§)ππ΄) + (π€ππ΄))) |
19 | 13, 14, 15, 18 | syl3anc 1372 |
. . . . . . 7
β’ (((π΄ β π β§ π¦ β β) β§ (π§ β π β§ π€ β π)) β (((π¦( Β·π OLD
βπ)π§)( +π£ βπ)π€)ππ΄) = (((π¦( Β·π OLD
βπ)π§)ππ΄) + (π€ππ΄))) |
20 | | simplr 768 |
. . . . . . . . 9
β’ (((π΄ β π β§ π¦ β β) β§ (π§ β π β§ π€ β π)) β π¦ β β) |
21 | | simprl 770 |
. . . . . . . . 9
β’ (((π΄ β π β§ π¦ β β) β§ (π§ β π β§ π€ β π)) β π§ β π) |
22 | 3, 16, 10, 4, 1 | ipassi 29825 |
. . . . . . . . 9
β’ ((π¦ β β β§ π§ β π β§ π΄ β π) β ((π¦( Β·π OLD
βπ)π§)ππ΄) = (π¦ Β· (π§ππ΄))) |
23 | 20, 21, 15, 22 | syl3anc 1372 |
. . . . . . . 8
β’ (((π΄ β π β§ π¦ β β) β§ (π§ β π β§ π€ β π)) β ((π¦( Β·π OLD
βπ)π§)ππ΄) = (π¦ Β· (π§ππ΄))) |
24 | 23 | oveq1d 7377 |
. . . . . . 7
β’ (((π΄ β π β§ π¦ β β) β§ (π§ β π β§ π€ β π)) β (((π¦( Β·π OLD
βπ)π§)ππ΄) + (π€ππ΄)) = ((π¦ Β· (π§ππ΄)) + (π€ππ΄))) |
25 | 19, 24 | eqtrd 2777 |
. . . . . 6
β’ (((π΄ β π β§ π¦ β β) β§ (π§ β π β§ π€ β π)) β (((π¦( Β·π OLD
βπ)π§)( +π£ βπ)π€)ππ΄) = ((π¦ Β· (π§ππ΄)) + (π€ππ΄))) |
26 | 12 | adantll 713 |
. . . . . . . . 9
β’ (((π΄ β π β§ π¦ β β) β§ π§ β π) β (π¦( Β·π OLD
βπ)π§) β π) |
27 | 3, 16 | nvgcl 29604 |
. . . . . . . . . 10
β’ ((π β NrmCVec β§ (π¦(
Β·π OLD βπ)π§) β π β§ π€ β π) β ((π¦( Β·π OLD
βπ)π§)( +π£ βπ)π€) β π) |
28 | 2, 27 | mp3an1 1449 |
. . . . . . . . 9
β’ (((π¦(
Β·π OLD βπ)π§) β π β§ π€ β π) β ((π¦( Β·π OLD
βπ)π§)( +π£ βπ)π€) β π) |
29 | 26, 28 | sylan 581 |
. . . . . . . 8
β’ ((((π΄ β π β§ π¦ β β) β§ π§ β π) β§ π€ β π) β ((π¦( Β·π OLD
βπ)π§)( +π£ βπ)π€) β π) |
30 | 29 | anasss 468 |
. . . . . . 7
β’ (((π΄ β π β§ π¦ β β) β§ (π§ β π β§ π€ β π)) β ((π¦( Β·π OLD
βπ)π§)( +π£ βπ)π€) β π) |
31 | | oveq1 7369 |
. . . . . . . 8
β’ (π₯ = ((π¦( Β·π OLD
βπ)π§)( +π£ βπ)π€) β (π₯ππ΄) = (((π¦( Β·π OLD
βπ)π§)( +π£ βπ)π€)ππ΄)) |
32 | | ovex 7395 |
. . . . . . . 8
β’ (((π¦(
Β·π OLD βπ)π§)( +π£ βπ)π€)ππ΄) β V |
33 | 31, 8, 32 | fvmpt 6953 |
. . . . . . 7
β’ (((π¦(
Β·π OLD βπ)π§)( +π£ βπ)π€) β π β (πΉβ((π¦( Β·π OLD
βπ)π§)( +π£ βπ)π€)) = (((π¦( Β·π OLD
βπ)π§)( +π£ βπ)π€)ππ΄)) |
34 | 30, 33 | syl 17 |
. . . . . 6
β’ (((π΄ β π β§ π¦ β β) β§ (π§ β π β§ π€ β π)) β (πΉβ((π¦( Β·π OLD
βπ)π§)( +π£ βπ)π€)) = (((π¦( Β·π OLD
βπ)π§)( +π£ βπ)π€)ππ΄)) |
35 | | oveq1 7369 |
. . . . . . . . . 10
β’ (π₯ = π§ β (π₯ππ΄) = (π§ππ΄)) |
36 | | ovex 7395 |
. . . . . . . . . 10
β’ (π§ππ΄) β V |
37 | 35, 8, 36 | fvmpt 6953 |
. . . . . . . . 9
β’ (π§ β π β (πΉβπ§) = (π§ππ΄)) |
38 | 37 | ad2antrl 727 |
. . . . . . . 8
β’ (((π΄ β π β§ π¦ β β) β§ (π§ β π β§ π€ β π)) β (πΉβπ§) = (π§ππ΄)) |
39 | 38 | oveq2d 7378 |
. . . . . . 7
β’ (((π΄ β π β§ π¦ β β) β§ (π§ β π β§ π€ β π)) β (π¦ Β· (πΉβπ§)) = (π¦ Β· (π§ππ΄))) |
40 | | oveq1 7369 |
. . . . . . . . 9
β’ (π₯ = π€ β (π₯ππ΄) = (π€ππ΄)) |
41 | | ovex 7395 |
. . . . . . . . 9
β’ (π€ππ΄) β V |
42 | 40, 8, 41 | fvmpt 6953 |
. . . . . . . 8
β’ (π€ β π β (πΉβπ€) = (π€ππ΄)) |
43 | 42 | ad2antll 728 |
. . . . . . 7
β’ (((π΄ β π β§ π¦ β β) β§ (π§ β π β§ π€ β π)) β (πΉβπ€) = (π€ππ΄)) |
44 | 39, 43 | oveq12d 7380 |
. . . . . 6
β’ (((π΄ β π β§ π¦ β β) β§ (π§ β π β§ π€ β π)) β ((π¦ Β· (πΉβπ§)) + (πΉβπ€)) = ((π¦ Β· (π§ππ΄)) + (π€ππ΄))) |
45 | 25, 34, 44 | 3eqtr4d 2787 |
. . . . 5
β’ (((π΄ β π β§ π¦ β β) β§ (π§ β π β§ π€ β π)) β (πΉβ((π¦( Β·π OLD
βπ)π§)( +π£ βπ)π€)) = ((π¦ Β· (πΉβπ§)) + (πΉβπ€))) |
46 | 45 | ralrimivva 3198 |
. . . 4
β’ ((π΄ β π β§ π¦ β β) β βπ§ β π βπ€ β π (πΉβ((π¦( Β·π OLD
βπ)π§)( +π£ βπ)π€)) = ((π¦ Β· (πΉβπ§)) + (πΉβπ€))) |
47 | 46 | ralrimiva 3144 |
. . 3
β’ (π΄ β π β βπ¦ β β βπ§ β π βπ€ β π (πΉβ((π¦( Β·π OLD
βπ)π§)( +π£ βπ)π€)) = ((π¦ Β· (πΉβπ§)) + (πΉβπ€))) |
48 | | ipblnfi.c |
. . . . 5
β’ πΆ = β¨β¨ + , Β·
β©, absβ© |
49 | 48 | cnnv 29661 |
. . . 4
β’ πΆ β NrmCVec |
50 | 48 | cnnvba 29663 |
. . . . 5
β’ β =
(BaseSetβπΆ) |
51 | 48 | cnnvg 29662 |
. . . . 5
β’ + = (
+π£ βπΆ) |
52 | 48 | cnnvs 29664 |
. . . . 5
β’ Β·
= ( Β·π OLD βπΆ) |
53 | | eqid 2737 |
. . . . 5
β’ (π LnOp πΆ) = (π LnOp πΆ) |
54 | 3, 50, 16, 51, 10, 52, 53 | islno 29737 |
. . . 4
β’ ((π β NrmCVec β§ πΆ β NrmCVec) β (πΉ β (π LnOp πΆ) β (πΉ:πβΆβ β§ βπ¦ β β βπ§ β π βπ€ β π (πΉβ((π¦( Β·π OLD
βπ)π§)( +π£ βπ)π€)) = ((π¦ Β· (πΉβπ§)) + (πΉβπ€))))) |
55 | 2, 49, 54 | mp2an 691 |
. . 3
β’ (πΉ β (π LnOp πΆ) β (πΉ:πβΆβ β§ βπ¦ β β βπ§ β π βπ€ β π (πΉβ((π¦( Β·π OLD
βπ)π§)( +π£ βπ)π€)) = ((π¦ Β· (πΉβπ§)) + (πΉβπ€)))) |
56 | 9, 47, 55 | sylanbrc 584 |
. 2
β’ (π΄ β π β πΉ β (π LnOp πΆ)) |
57 | | eqid 2737 |
. . . 4
β’
(normCVβπ) = (normCVβπ) |
58 | 3, 57 | nvcl 29645 |
. . 3
β’ ((π β NrmCVec β§ π΄ β π) β ((normCVβπ)βπ΄) β β) |
59 | 2, 58 | mpan 689 |
. 2
β’ (π΄ β π β ((normCVβπ)βπ΄) β β) |
60 | 3, 57, 4, 1 | sii 29838 |
. . . . 5
β’ ((π§ β π β§ π΄ β π) β (absβ(π§ππ΄)) β€ (((normCVβπ)βπ§) Β· ((normCVβπ)βπ΄))) |
61 | 60 | ancoms 460 |
. . . 4
β’ ((π΄ β π β§ π§ β π) β (absβ(π§ππ΄)) β€ (((normCVβπ)βπ§) Β· ((normCVβπ)βπ΄))) |
62 | 37 | adantl 483 |
. . . . 5
β’ ((π΄ β π β§ π§ β π) β (πΉβπ§) = (π§ππ΄)) |
63 | 62 | fveq2d 6851 |
. . . 4
β’ ((π΄ β π β§ π§ β π) β (absβ(πΉβπ§)) = (absβ(π§ππ΄))) |
64 | 59 | recnd 11190 |
. . . . 5
β’ (π΄ β π β ((normCVβπ)βπ΄) β β) |
65 | 3, 57 | nvcl 29645 |
. . . . . . 7
β’ ((π β NrmCVec β§ π§ β π) β ((normCVβπ)βπ§) β β) |
66 | 2, 65 | mpan 689 |
. . . . . 6
β’ (π§ β π β ((normCVβπ)βπ§) β β) |
67 | 66 | recnd 11190 |
. . . . 5
β’ (π§ β π β ((normCVβπ)βπ§) β β) |
68 | | mulcom 11144 |
. . . . 5
β’
((((normCVβπ)βπ΄) β β β§
((normCVβπ)βπ§) β β) β
(((normCVβπ)βπ΄) Β· ((normCVβπ)βπ§)) = (((normCVβπ)βπ§) Β· ((normCVβπ)βπ΄))) |
69 | 64, 67, 68 | syl2an 597 |
. . . 4
β’ ((π΄ β π β§ π§ β π) β (((normCVβπ)βπ΄) Β· ((normCVβπ)βπ§)) = (((normCVβπ)βπ§) Β· ((normCVβπ)βπ΄))) |
70 | 61, 63, 69 | 3brtr4d 5142 |
. . 3
β’ ((π΄ β π β§ π§ β π) β (absβ(πΉβπ§)) β€ (((normCVβπ)βπ΄) Β· ((normCVβπ)βπ§))) |
71 | 70 | ralrimiva 3144 |
. 2
β’ (π΄ β π β βπ§ β π (absβ(πΉβπ§)) β€ (((normCVβπ)βπ΄) Β· ((normCVβπ)βπ§))) |
72 | 48 | cnnvnm 29665 |
. . 3
β’ abs =
(normCVβπΆ) |
73 | | ipblnfi.l |
. . 3
β’ π΅ = (π BLnOp πΆ) |
74 | 3, 57, 72, 53, 73, 2, 49 | blo3i 29786 |
. 2
β’ ((πΉ β (π LnOp πΆ) β§ ((normCVβπ)βπ΄) β β β§ βπ§ β π (absβ(πΉβπ§)) β€ (((normCVβπ)βπ΄) Β· ((normCVβπ)βπ§))) β πΉ β π΅) |
75 | 56, 59, 71, 74 | syl3anc 1372 |
1
β’ (π΄ β π β πΉ β π΅) |