Step | Hyp | Ref
| Expression |
1 | | oveq1 7365 |
. . . . 5
β’ (π = if(π β CBan, π, β¨β¨ + , Β· β©,
absβ©) β (π BLnOp
π) = (if(π β CBan, π, β¨β¨ + , Β· β©,
absβ©) BLnOp π)) |
2 | 1 | sseq2d 3977 |
. . . 4
β’ (π = if(π β CBan, π, β¨β¨ + , Β· β©,
absβ©) β (π
β (π BLnOp π) β π β (if(π β CBan, π, β¨β¨ + , Β· β©,
absβ©) BLnOp π))) |
3 | | ubth.1 |
. . . . . . 7
β’ π = (BaseSetβπ) |
4 | | fveq2 6843 |
. . . . . . 7
β’ (π = if(π β CBan, π, β¨β¨ + , Β· β©,
absβ©) β (BaseSetβπ) = (BaseSetβif(π β CBan, π, β¨β¨ + , Β· β©,
absβ©))) |
5 | 3, 4 | eqtrid 2785 |
. . . . . 6
β’ (π = if(π β CBan, π, β¨β¨ + , Β· β©,
absβ©) β π =
(BaseSetβif(π β
CBan, π, β¨β¨ + ,
Β· β©, absβ©))) |
6 | 5 | raleqdv 3312 |
. . . . 5
β’ (π = if(π β CBan, π, β¨β¨ + , Β· β©,
absβ©) β (βπ₯ β π βπ β β βπ‘ β π (πβ(π‘βπ₯)) β€ π β βπ₯ β (BaseSetβif(π β CBan, π, β¨β¨ + , Β· β©,
absβ©))βπ β
β βπ‘ β
π (πβ(π‘βπ₯)) β€ π)) |
7 | | ubth.3 |
. . . . . . . . 9
β’ π = (π normOpOLD π) |
8 | | oveq1 7365 |
. . . . . . . . 9
β’ (π = if(π β CBan, π, β¨β¨ + , Β· β©,
absβ©) β (π
normOpOLD π) =
(if(π β CBan, π, β¨β¨ + , Β·
β©, absβ©) normOpOLD π)) |
9 | 7, 8 | eqtrid 2785 |
. . . . . . . 8
β’ (π = if(π β CBan, π, β¨β¨ + , Β· β©,
absβ©) β π =
(if(π β CBan, π, β¨β¨ + , Β·
β©, absβ©) normOpOLD π)) |
10 | 9 | fveq1d 6845 |
. . . . . . 7
β’ (π = if(π β CBan, π, β¨β¨ + , Β· β©,
absβ©) β (πβπ‘) = ((if(π β CBan, π, β¨β¨ + , Β· β©,
absβ©) normOpOLD π)βπ‘)) |
11 | 10 | breq1d 5116 |
. . . . . 6
β’ (π = if(π β CBan, π, β¨β¨ + , Β· β©,
absβ©) β ((πβπ‘) β€ π β ((if(π β CBan, π, β¨β¨ + , Β· β©,
absβ©) normOpOLD π)βπ‘) β€ π)) |
12 | 11 | rexralbidv 3211 |
. . . . 5
β’ (π = if(π β CBan, π, β¨β¨ + , Β· β©,
absβ©) β (βπ
β β βπ‘
β π (πβπ‘) β€ π β βπ β β βπ‘ β π ((if(π β CBan, π, β¨β¨ + , Β· β©,
absβ©) normOpOLD π)βπ‘) β€ π)) |
13 | 6, 12 | bibi12d 346 |
. . . 4
β’ (π = if(π β CBan, π, β¨β¨ + , Β· β©,
absβ©) β ((βπ₯ β π βπ β β βπ‘ β π (πβ(π‘βπ₯)) β€ π β βπ β β βπ‘ β π (πβπ‘) β€ π) β (βπ₯ β (BaseSetβif(π β CBan, π, β¨β¨ + , Β· β©,
absβ©))βπ β
β βπ‘ β
π (πβ(π‘βπ₯)) β€ π β βπ β β βπ‘ β π ((if(π β CBan, π, β¨β¨ + , Β· β©,
absβ©) normOpOLD π)βπ‘) β€ π))) |
14 | 2, 13 | imbi12d 345 |
. . 3
β’ (π = if(π β CBan, π, β¨β¨ + , Β· β©,
absβ©) β ((π
β (π BLnOp π) β (βπ₯ β π βπ β β βπ‘ β π (πβ(π‘βπ₯)) β€ π β βπ β β βπ‘ β π (πβπ‘) β€ π)) β (π β (if(π β CBan, π, β¨β¨ + , Β· β©,
absβ©) BLnOp π) β
(βπ₯ β
(BaseSetβif(π β
CBan, π, β¨β¨ + ,
Β· β©, absβ©))βπ β β βπ‘ β π (πβ(π‘βπ₯)) β€ π β βπ β β βπ‘ β π ((if(π β CBan, π, β¨β¨ + , Β· β©,
absβ©) normOpOLD π)βπ‘) β€ π)))) |
15 | | oveq2 7366 |
. . . . 5
β’ (π = if(π β NrmCVec, π, β¨β¨ + , Β· β©,
absβ©) β (if(π
β CBan, π,
β¨β¨ + , Β· β©, absβ©) BLnOp π) = (if(π β CBan, π, β¨β¨ + , Β· β©,
absβ©) BLnOp if(π
β NrmCVec, π,
β¨β¨ + , Β· β©, absβ©))) |
16 | 15 | sseq2d 3977 |
. . . 4
β’ (π = if(π β NrmCVec, π, β¨β¨ + , Β· β©,
absβ©) β (π
β (if(π β CBan,
π, β¨β¨ + ,
Β· β©, absβ©) BLnOp π) β π β (if(π β CBan, π, β¨β¨ + , Β· β©,
absβ©) BLnOp if(π
β NrmCVec, π,
β¨β¨ + , Β· β©, absβ©)))) |
17 | | ubth.2 |
. . . . . . . . . 10
β’ π =
(normCVβπ) |
18 | | fveq2 6843 |
. . . . . . . . . 10
β’ (π = if(π β NrmCVec, π, β¨β¨ + , Β· β©,
absβ©) β (normCVβπ) = (normCVβif(π β NrmCVec, π, β¨β¨ + , Β·
β©, absβ©))) |
19 | 17, 18 | eqtrid 2785 |
. . . . . . . . 9
β’ (π = if(π β NrmCVec, π, β¨β¨ + , Β· β©,
absβ©) β π =
(normCVβif(π β NrmCVec, π, β¨β¨ + , Β· β©,
absβ©))) |
20 | 19 | fveq1d 6845 |
. . . . . . . 8
β’ (π = if(π β NrmCVec, π, β¨β¨ + , Β· β©,
absβ©) β (πβ(π‘βπ₯)) = ((normCVβif(π β NrmCVec, π, β¨β¨ + , Β·
β©, absβ©))β(π‘βπ₯))) |
21 | 20 | breq1d 5116 |
. . . . . . 7
β’ (π = if(π β NrmCVec, π, β¨β¨ + , Β· β©,
absβ©) β ((πβ(π‘βπ₯)) β€ π β ((normCVβif(π β NrmCVec, π, β¨β¨ + , Β·
β©, absβ©))β(π‘βπ₯)) β€ π)) |
22 | 21 | rexralbidv 3211 |
. . . . . 6
β’ (π = if(π β NrmCVec, π, β¨β¨ + , Β· β©,
absβ©) β (βπ
β β βπ‘
β π (πβ(π‘βπ₯)) β€ π β βπ β β βπ‘ β π ((normCVβif(π β NrmCVec, π, β¨β¨ + , Β·
β©, absβ©))β(π‘βπ₯)) β€ π)) |
23 | 22 | ralbidv 3171 |
. . . . 5
β’ (π = if(π β NrmCVec, π, β¨β¨ + , Β· β©,
absβ©) β (βπ₯ β (BaseSetβif(π β CBan, π, β¨β¨ + , Β· β©,
absβ©))βπ β
β βπ‘ β
π (πβ(π‘βπ₯)) β€ π β βπ₯ β (BaseSetβif(π β CBan, π, β¨β¨ + , Β· β©,
absβ©))βπ β
β βπ‘ β
π
((normCVβif(π β NrmCVec, π, β¨β¨ + , Β· β©,
absβ©))β(π‘βπ₯)) β€ π)) |
24 | | oveq2 7366 |
. . . . . . . 8
β’ (π = if(π β NrmCVec, π, β¨β¨ + , Β· β©,
absβ©) β (if(π
β CBan, π,
β¨β¨ + , Β· β©, absβ©) normOpOLD π) = (if(π β CBan, π, β¨β¨ + , Β· β©,
absβ©) normOpOLD if(π β NrmCVec, π, β¨β¨ + , Β· β©,
absβ©))) |
25 | 24 | fveq1d 6845 |
. . . . . . 7
β’ (π = if(π β NrmCVec, π, β¨β¨ + , Β· β©,
absβ©) β ((if(π
β CBan, π,
β¨β¨ + , Β· β©, absβ©) normOpOLD π)βπ‘) = ((if(π β CBan, π, β¨β¨ + , Β· β©,
absβ©) normOpOLD if(π β NrmCVec, π, β¨β¨ + , Β· β©,
absβ©))βπ‘)) |
26 | 25 | breq1d 5116 |
. . . . . 6
β’ (π = if(π β NrmCVec, π, β¨β¨ + , Β· β©,
absβ©) β (((if(π
β CBan, π,
β¨β¨ + , Β· β©, absβ©) normOpOLD π)βπ‘) β€ π β ((if(π β CBan, π, β¨β¨ + , Β· β©,
absβ©) normOpOLD if(π β NrmCVec, π, β¨β¨ + , Β· β©,
absβ©))βπ‘) β€
π)) |
27 | 26 | rexralbidv 3211 |
. . . . 5
β’ (π = if(π β NrmCVec, π, β¨β¨ + , Β· β©,
absβ©) β (βπ
β β βπ‘
β π ((if(π β CBan, π, β¨β¨ + , Β· β©,
absβ©) normOpOLD π)βπ‘) β€ π β βπ β β βπ‘ β π ((if(π β CBan, π, β¨β¨ + , Β· β©,
absβ©) normOpOLD if(π β NrmCVec, π, β¨β¨ + , Β· β©,
absβ©))βπ‘) β€
π)) |
28 | 23, 27 | bibi12d 346 |
. . . 4
β’ (π = if(π β NrmCVec, π, β¨β¨ + , Β· β©,
absβ©) β ((βπ₯ β (BaseSetβif(π β CBan, π, β¨β¨ + , Β· β©,
absβ©))βπ β
β βπ‘ β
π (πβ(π‘βπ₯)) β€ π β βπ β β βπ‘ β π ((if(π β CBan, π, β¨β¨ + , Β· β©,
absβ©) normOpOLD π)βπ‘) β€ π) β (βπ₯ β (BaseSetβif(π β CBan, π, β¨β¨ + , Β· β©,
absβ©))βπ β
β βπ‘ β
π
((normCVβif(π β NrmCVec, π, β¨β¨ + , Β· β©,
absβ©))β(π‘βπ₯)) β€ π β βπ β β βπ‘ β π ((if(π β CBan, π, β¨β¨ + , Β· β©,
absβ©) normOpOLD if(π β NrmCVec, π, β¨β¨ + , Β· β©,
absβ©))βπ‘) β€
π))) |
29 | 16, 28 | imbi12d 345 |
. . 3
β’ (π = if(π β NrmCVec, π, β¨β¨ + , Β· β©,
absβ©) β ((π
β (if(π β CBan,
π, β¨β¨ + ,
Β· β©, absβ©) BLnOp π) β (βπ₯ β (BaseSetβif(π β CBan, π, β¨β¨ + , Β· β©,
absβ©))βπ β
β βπ‘ β
π (πβ(π‘βπ₯)) β€ π β βπ β β βπ‘ β π ((if(π β CBan, π, β¨β¨ + , Β· β©,
absβ©) normOpOLD π)βπ‘) β€ π)) β (π β (if(π β CBan, π, β¨β¨ + , Β· β©,
absβ©) BLnOp if(π
β NrmCVec, π,
β¨β¨ + , Β· β©, absβ©)) β (βπ₯ β (BaseSetβif(π β CBan, π, β¨β¨ + , Β· β©,
absβ©))βπ β
β βπ‘ β
π
((normCVβif(π β NrmCVec, π, β¨β¨ + , Β· β©,
absβ©))β(π‘βπ₯)) β€ π β βπ β β βπ‘ β π ((if(π β CBan, π, β¨β¨ + , Β· β©,
absβ©) normOpOLD if(π β NrmCVec, π, β¨β¨ + , Β· β©,
absβ©))βπ‘) β€
π)))) |
30 | | eqid 2733 |
. . . 4
β’
(BaseSetβif(π
β CBan, π,
β¨β¨ + , Β· β©, absβ©)) = (BaseSetβif(π β CBan, π, β¨β¨ + , Β· β©,
absβ©)) |
31 | | eqid 2733 |
. . . 4
β’
(normCVβif(π β NrmCVec, π, β¨β¨ + , Β· β©,
absβ©)) = (normCVβif(π β NrmCVec, π, β¨β¨ + , Β· β©,
absβ©)) |
32 | | eqid 2733 |
. . . 4
β’
(IndMetβif(π
β CBan, π,
β¨β¨ + , Β· β©, absβ©)) = (IndMetβif(π β CBan, π, β¨β¨ + , Β· β©,
absβ©)) |
33 | | eqid 2733 |
. . . 4
β’
(MetOpenβ(IndMetβif(π β CBan, π, β¨β¨ + , Β· β©,
absβ©))) = (MetOpenβ(IndMetβif(π β CBan, π, β¨β¨ + , Β· β©,
absβ©))) |
34 | | eqid 2733 |
. . . . . 6
β’
β¨β¨ + , Β· β©, absβ© = β¨β¨ + , Β·
β©, absβ© |
35 | 34 | cnbn 29853 |
. . . . 5
β’
β¨β¨ + , Β· β©, absβ© β CBan |
36 | 35 | elimel 4556 |
. . . 4
β’ if(π β CBan, π, β¨β¨ + , Β· β©,
absβ©) β CBan |
37 | | elimnvu 29668 |
. . . 4
β’ if(π β NrmCVec, π, β¨β¨ + , Β·
β©, absβ©) β NrmCVec |
38 | | id 22 |
. . . 4
β’ (π β (if(π β CBan, π, β¨β¨ + , Β· β©,
absβ©) BLnOp if(π
β NrmCVec, π,
β¨β¨ + , Β· β©, absβ©)) β π β (if(π β CBan, π, β¨β¨ + , Β· β©,
absβ©) BLnOp if(π
β NrmCVec, π,
β¨β¨ + , Β· β©, absβ©))) |
39 | 30, 31, 32, 33, 36, 37, 38 | ubthlem3 29856 |
. . 3
β’ (π β (if(π β CBan, π, β¨β¨ + , Β· β©,
absβ©) BLnOp if(π
β NrmCVec, π,
β¨β¨ + , Β· β©, absβ©)) β (βπ₯ β (BaseSetβif(π β CBan, π, β¨β¨ + , Β· β©,
absβ©))βπ β
β βπ‘ β
π
((normCVβif(π β NrmCVec, π, β¨β¨ + , Β· β©,
absβ©))β(π‘βπ₯)) β€ π β βπ β β βπ‘ β π ((if(π β CBan, π, β¨β¨ + , Β· β©,
absβ©) normOpOLD if(π β NrmCVec, π, β¨β¨ + , Β· β©,
absβ©))βπ‘) β€
π)) |
40 | 14, 29, 39 | dedth2h 4546 |
. 2
β’ ((π β CBan β§ π β NrmCVec) β (π β (π BLnOp π) β (βπ₯ β π βπ β β βπ‘ β π (πβ(π‘βπ₯)) β€ π β βπ β β βπ‘ β π (πβπ‘) β€ π))) |
41 | 40 | 3impia 1118 |
1
β’ ((π β CBan β§ π β NrmCVec β§ π β (π BLnOp π)) β (βπ₯ β π βπ β β βπ‘ β π (πβ(π‘βπ₯)) β€ π β βπ β β βπ‘ β π (πβπ‘) β€ π)) |