Step | Hyp | Ref
| Expression |
1 | | fveq1 6845 |
. . . . . 6
โข (๐ = if((๐ โ LinFn โง
(normfnโ๐)
โ โ), ๐, (
โ ร {0})) โ (๐โ๐ด) = (if((๐ โ LinFn โง
(normfnโ๐)
โ โ), ๐, (
โ ร {0}))โ๐ด)) |
2 | 1 | fveq2d 6850 |
. . . . 5
โข (๐ = if((๐ โ LinFn โง
(normfnโ๐)
โ โ), ๐, (
โ ร {0})) โ (absโ(๐โ๐ด)) = (absโ(if((๐ โ LinFn โง
(normfnโ๐)
โ โ), ๐, (
โ ร {0}))โ๐ด))) |
3 | | fveq2 6846 |
. . . . . 6
โข (๐ = if((๐ โ LinFn โง
(normfnโ๐)
โ โ), ๐, (
โ ร {0})) โ (normfnโ๐) = (normfnโif((๐ โ LinFn โง
(normfnโ๐)
โ โ), ๐, (
โ ร {0})))) |
4 | 3 | oveq1d 7376 |
. . . . 5
โข (๐ = if((๐ โ LinFn โง
(normfnโ๐)
โ โ), ๐, (
โ ร {0})) โ ((normfnโ๐) ยท
(normโโ๐ด)) = ((normfnโif((๐ โ LinFn โง
(normfnโ๐)
โ โ), ๐, (
โ ร {0}))) ยท (normโโ๐ด))) |
5 | 2, 4 | breq12d 5122 |
. . . 4
โข (๐ = if((๐ โ LinFn โง
(normfnโ๐)
โ โ), ๐, (
โ ร {0})) โ ((absโ(๐โ๐ด)) โค ((normfnโ๐) ยท
(normโโ๐ด)) โ (absโ(if((๐ โ LinFn โง
(normfnโ๐)
โ โ), ๐, (
โ ร {0}))โ๐ด)) โค ((normfnโif((๐ โ LinFn โง
(normfnโ๐)
โ โ), ๐, (
โ ร {0}))) ยท (normโโ๐ด)))) |
6 | 5 | imbi2d 341 |
. . 3
โข (๐ = if((๐ โ LinFn โง
(normfnโ๐)
โ โ), ๐, (
โ ร {0})) โ ((๐ด โ โ โ (absโ(๐โ๐ด)) โค ((normfnโ๐) ยท
(normโโ๐ด))) โ (๐ด โ โ โ (absโ(if((๐ โ LinFn โง
(normfnโ๐)
โ โ), ๐, (
โ ร {0}))โ๐ด)) โค ((normfnโif((๐ โ LinFn โง
(normfnโ๐)
โ โ), ๐, (
โ ร {0}))) ยท (normโโ๐ด))))) |
7 | | eleq1 2822 |
. . . . . 6
โข (๐ = if((๐ โ LinFn โง
(normfnโ๐)
โ โ), ๐, (
โ ร {0})) โ (๐ โ LinFn โ if((๐ โ LinFn โง
(normfnโ๐)
โ โ), ๐, (
โ ร {0})) โ LinFn)) |
8 | 3 | eleq1d 2819 |
. . . . . 6
โข (๐ = if((๐ โ LinFn โง
(normfnโ๐)
โ โ), ๐, (
โ ร {0})) โ ((normfnโ๐) โ โ โ
(normfnโif((๐ โ LinFn โง
(normfnโ๐)
โ โ), ๐, (
โ ร {0}))) โ โ)) |
9 | 7, 8 | anbi12d 632 |
. . . . 5
โข (๐ = if((๐ โ LinFn โง
(normfnโ๐)
โ โ), ๐, (
โ ร {0})) โ ((๐ โ LinFn โง
(normfnโ๐)
โ โ) โ (if((๐ โ LinFn โง
(normfnโ๐)
โ โ), ๐, (
โ ร {0})) โ LinFn โง (normfnโif((๐ โ LinFn โง
(normfnโ๐)
โ โ), ๐, (
โ ร {0}))) โ โ))) |
10 | | eleq1 2822 |
. . . . . 6
โข ((
โ ร {0}) = if((๐ โ LinFn โง
(normfnโ๐)
โ โ), ๐, (
โ ร {0})) โ (( โ ร {0}) โ LinFn โ
if((๐ โ LinFn โง
(normfnโ๐)
โ โ), ๐, (
โ ร {0})) โ LinFn)) |
11 | | fveq2 6846 |
. . . . . . 7
โข ((
โ ร {0}) = if((๐ โ LinFn โง
(normfnโ๐)
โ โ), ๐, (
โ ร {0})) โ (normfnโ( โ ร {0})) =
(normfnโif((๐ โ LinFn โง
(normfnโ๐)
โ โ), ๐, (
โ ร {0})))) |
12 | 11 | eleq1d 2819 |
. . . . . 6
โข ((
โ ร {0}) = if((๐ โ LinFn โง
(normfnโ๐)
โ โ), ๐, (
โ ร {0})) โ ((normfnโ( โ ร {0}))
โ โ โ (normfnโif((๐ โ LinFn โง
(normfnโ๐)
โ โ), ๐, (
โ ร {0}))) โ โ)) |
13 | 10, 12 | anbi12d 632 |
. . . . 5
โข ((
โ ร {0}) = if((๐ โ LinFn โง
(normfnโ๐)
โ โ), ๐, (
โ ร {0})) โ ((( โ ร {0}) โ LinFn โง
(normfnโ( โ ร {0})) โ โ) โ
(if((๐ โ LinFn โง
(normfnโ๐)
โ โ), ๐, (
โ ร {0})) โ LinFn โง (normfnโif((๐ โ LinFn โง
(normfnโ๐)
โ โ), ๐, (
โ ร {0}))) โ โ))) |
14 | | 0lnfn 30976 |
. . . . . 6
โข ( โ
ร {0}) โ LinFn |
15 | | nmfn0 30978 |
. . . . . . 7
โข
(normfnโ( โ ร {0})) = 0 |
16 | | 0re 11165 |
. . . . . . 7
โข 0 โ
โ |
17 | 15, 16 | eqeltri 2830 |
. . . . . 6
โข
(normfnโ( โ ร {0})) โ
โ |
18 | 14, 17 | pm3.2i 472 |
. . . . 5
โข ((
โ ร {0}) โ LinFn โง (normfnโ( โ
ร {0})) โ โ) |
19 | 9, 13, 18 | elimhyp 4555 |
. . . 4
โข
(if((๐ โ LinFn
โง (normfnโ๐) โ โ), ๐, ( โ ร {0})) โ LinFn โง
(normfnโif((๐ โ LinFn โง
(normfnโ๐)
โ โ), ๐, (
โ ร {0}))) โ โ) |
20 | 19 | nmbdfnlbi 31040 |
. . 3
โข (๐ด โ โ โ
(absโ(if((๐ โ
LinFn โง (normfnโ๐) โ โ), ๐, ( โ ร {0}))โ๐ด)) โค
((normfnโif((๐ โ LinFn โง
(normfnโ๐)
โ โ), ๐, (
โ ร {0}))) ยท (normโโ๐ด))) |
21 | 6, 20 | dedth 4548 |
. 2
โข ((๐ โ LinFn โง
(normfnโ๐)
โ โ) โ (๐ด
โ โ โ (absโ(๐โ๐ด)) โค ((normfnโ๐) ยท
(normโโ๐ด)))) |
22 | 21 | 3impia 1118 |
1
โข ((๐ โ LinFn โง
(normfnโ๐)
โ โ โง ๐ด
โ โ) โ (absโ(๐โ๐ด)) โค ((normfnโ๐) ยท
(normโโ๐ด))) |