Step | Hyp | Ref
| Expression |
1 | | blometi.u |
. . . . 5
β’ π β NrmCVec |
2 | | blometi.1 |
. . . . . 6
β’ π = (BaseSetβπ) |
3 | | eqid 2731 |
. . . . . 6
β’ (
βπ£ βπ) = ( βπ£
βπ) |
4 | 2, 3 | nvmcl 29685 |
. . . . 5
β’ ((π β NrmCVec β§ π β π β§ π β π) β (π( βπ£ βπ)π) β π) |
5 | 1, 4 | mp3an1 1448 |
. . . 4
β’ ((π β π β§ π β π) β (π( βπ£ βπ)π) β π) |
6 | | eqid 2731 |
. . . . 5
β’
(normCVβπ) = (normCVβπ) |
7 | | eqid 2731 |
. . . . 5
β’
(normCVβπ) = (normCVβπ) |
8 | | blometi.6 |
. . . . 5
β’ π = (π normOpOLD π) |
9 | | blometi.7 |
. . . . 5
β’ π΅ = (π BLnOp π) |
10 | | blometi.w |
. . . . 5
β’ π β NrmCVec |
11 | 2, 6, 7, 8, 9, 1, 10 | nmblolbi 29839 |
. . . 4
β’ ((π β π΅ β§ (π( βπ£ βπ)π) β π) β ((normCVβπ)β(πβ(π( βπ£ βπ)π))) β€ ((πβπ) Β· ((normCVβπ)β(π( βπ£ βπ)π)))) |
12 | 5, 11 | sylan2 593 |
. . 3
β’ ((π β π΅ β§ (π β π β§ π β π)) β ((normCVβπ)β(πβ(π( βπ£ βπ)π))) β€ ((πβπ) Β· ((normCVβπ)β(π( βπ£ βπ)π)))) |
13 | 12 | 3impb 1115 |
. 2
β’ ((π β π΅ β§ π β π β§ π β π) β ((normCVβπ)β(πβ(π( βπ£ βπ)π))) β€ ((πβπ) Β· ((normCVβπ)β(π( βπ£ βπ)π)))) |
14 | | blometi.2 |
. . . . . . . 8
β’ π = (BaseSetβπ) |
15 | 2, 14, 9 | blof 29824 |
. . . . . . 7
β’ ((π β NrmCVec β§ π β NrmCVec β§ π β π΅) β π:πβΆπ) |
16 | 1, 10, 15 | mp3an12 1451 |
. . . . . 6
β’ (π β π΅ β π:πβΆπ) |
17 | 16 | ffvelcdmda 7055 |
. . . . 5
β’ ((π β π΅ β§ π β π) β (πβπ) β π) |
18 | 17 | 3adant3 1132 |
. . . 4
β’ ((π β π΅ β§ π β π β§ π β π) β (πβπ) β π) |
19 | 16 | ffvelcdmda 7055 |
. . . . 5
β’ ((π β π΅ β§ π β π) β (πβπ) β π) |
20 | 19 | 3adant2 1131 |
. . . 4
β’ ((π β π΅ β§ π β π β§ π β π) β (πβπ) β π) |
21 | | eqid 2731 |
. . . . . 6
β’ (
βπ£ βπ) = ( βπ£
βπ) |
22 | | blometi.d |
. . . . . 6
β’ π· = (IndMetβπ) |
23 | 14, 21, 7, 22 | imsdval 29725 |
. . . . 5
β’ ((π β NrmCVec β§ (πβπ) β π β§ (πβπ) β π) β ((πβπ)π·(πβπ)) = ((normCVβπ)β((πβπ)( βπ£ βπ)(πβπ)))) |
24 | 10, 23 | mp3an1 1448 |
. . . 4
β’ (((πβπ) β π β§ (πβπ) β π) β ((πβπ)π·(πβπ)) = ((normCVβπ)β((πβπ)( βπ£ βπ)(πβπ)))) |
25 | 18, 20, 24 | syl2anc 584 |
. . 3
β’ ((π β π΅ β§ π β π β§ π β π) β ((πβπ)π·(πβπ)) = ((normCVβπ)β((πβπ)( βπ£ βπ)(πβπ)))) |
26 | | eqid 2731 |
. . . . . . 7
β’ (π LnOp π) = (π LnOp π) |
27 | 26, 9 | bloln 29823 |
. . . . . 6
β’ ((π β NrmCVec β§ π β NrmCVec β§ π β π΅) β π β (π LnOp π)) |
28 | 1, 10, 27 | mp3an12 1451 |
. . . . 5
β’ (π β π΅ β π β (π LnOp π)) |
29 | 2, 3, 21, 26 | lnosub 29798 |
. . . . . . . 8
β’ (((π β NrmCVec β§ π β NrmCVec β§ π β (π LnOp π)) β§ (π β π β§ π β π)) β (πβ(π( βπ£ βπ)π)) = ((πβπ)( βπ£ βπ)(πβπ))) |
30 | 1, 29 | mp3anl1 1455 |
. . . . . . 7
β’ (((π β NrmCVec β§ π β (π LnOp π)) β§ (π β π β§ π β π)) β (πβ(π( βπ£ βπ)π)) = ((πβπ)( βπ£ βπ)(πβπ))) |
31 | 10, 30 | mpanl1 698 |
. . . . . 6
β’ ((π β (π LnOp π) β§ (π β π β§ π β π)) β (πβ(π( βπ£ βπ)π)) = ((πβπ)( βπ£ βπ)(πβπ))) |
32 | 31 | 3impb 1115 |
. . . . 5
β’ ((π β (π LnOp π) β§ π β π β§ π β π) β (πβ(π( βπ£ βπ)π)) = ((πβπ)( βπ£ βπ)(πβπ))) |
33 | 28, 32 | syl3an1 1163 |
. . . 4
β’ ((π β π΅ β§ π β π β§ π β π) β (πβ(π( βπ£ βπ)π)) = ((πβπ)( βπ£ βπ)(πβπ))) |
34 | 33 | fveq2d 6866 |
. . 3
β’ ((π β π΅ β§ π β π β§ π β π) β ((normCVβπ)β(πβ(π( βπ£ βπ)π))) = ((normCVβπ)β((πβπ)( βπ£ βπ)(πβπ)))) |
35 | 25, 34 | eqtr4d 2774 |
. 2
β’ ((π β π΅ β§ π β π β§ π β π) β ((πβπ)π·(πβπ)) = ((normCVβπ)β(πβ(π( βπ£ βπ)π)))) |
36 | | blometi.8 |
. . . . . 6
β’ πΆ = (IndMetβπ) |
37 | 2, 3, 6, 36 | imsdval 29725 |
. . . . 5
β’ ((π β NrmCVec β§ π β π β§ π β π) β (ππΆπ) = ((normCVβπ)β(π( βπ£ βπ)π))) |
38 | 1, 37 | mp3an1 1448 |
. . . 4
β’ ((π β π β§ π β π) β (ππΆπ) = ((normCVβπ)β(π( βπ£ βπ)π))) |
39 | 38 | 3adant1 1130 |
. . 3
β’ ((π β π΅ β§ π β π β§ π β π) β (ππΆπ) = ((normCVβπ)β(π( βπ£ βπ)π))) |
40 | 39 | oveq2d 7393 |
. 2
β’ ((π β π΅ β§ π β π β§ π β π) β ((πβπ) Β· (ππΆπ)) = ((πβπ) Β· ((normCVβπ)β(π( βπ£ βπ)π)))) |
41 | 13, 35, 40 | 3brtr4d 5157 |
1
β’ ((π β π΅ β§ π β π β§ π β π) β ((πβπ)π·(πβπ)) β€ ((πβπ) Β· (ππΆπ))) |