Step | Hyp | Ref
| Expression |
1 | | lnfncnbd 31048 |
. 2
โข (๐ โ LinFn โ (๐ โ ContFn โ
(normfnโ๐)
โ โ)) |
2 | | elin 3930 |
. . . . 5
โข (๐ โ (LinFn โฉ ContFn)
โ (๐ โ LinFn
โง ๐ โ
ContFn)) |
3 | | fveq1 6845 |
. . . . . . . 8
โข (๐ = if(๐ โ (LinFn โฉ ContFn), ๐, ( โ ร {0})) โ
(๐โ๐ฅ) = (if(๐ โ (LinFn โฉ ContFn), ๐, ( โ ร
{0}))โ๐ฅ)) |
4 | 3 | eqeq1d 2735 |
. . . . . . 7
โข (๐ = if(๐ โ (LinFn โฉ ContFn), ๐, ( โ ร {0})) โ
((๐โ๐ฅ) = (๐ฅ ยทih ๐ฆ) โ (if(๐ โ (LinFn โฉ ContFn), ๐, ( โ ร
{0}))โ๐ฅ) = (๐ฅ
ยทih ๐ฆ))) |
5 | 4 | rexralbidv 3211 |
. . . . . 6
โข (๐ = if(๐ โ (LinFn โฉ ContFn), ๐, ( โ ร {0})) โ
(โ๐ฆ โ โ
โ๐ฅ โ โ
(๐โ๐ฅ) = (๐ฅ ยทih ๐ฆ) โ โ๐ฆ โ โ โ๐ฅ โ โ (if(๐ โ (LinFn โฉ ContFn),
๐, ( โ ร
{0}))โ๐ฅ) = (๐ฅ
ยทih ๐ฆ))) |
6 | | inss1 4192 |
. . . . . . . 8
โข (LinFn
โฉ ContFn) โ LinFn |
7 | | 0lnfn 30976 |
. . . . . . . . . 10
โข ( โ
ร {0}) โ LinFn |
8 | | 0cnfn 30971 |
. . . . . . . . . 10
โข ( โ
ร {0}) โ ContFn |
9 | | elin 3930 |
. . . . . . . . . 10
โข ((
โ ร {0}) โ (LinFn โฉ ContFn) โ (( โ ร {0})
โ LinFn โง ( โ ร {0}) โ ContFn)) |
10 | 7, 8, 9 | mpbir2an 710 |
. . . . . . . . 9
โข ( โ
ร {0}) โ (LinFn โฉ ContFn) |
11 | 10 | elimel 4559 |
. . . . . . . 8
โข if(๐ โ (LinFn โฉ ContFn),
๐, ( โ ร {0}))
โ (LinFn โฉ ContFn) |
12 | 6, 11 | sselii 3945 |
. . . . . . 7
โข if(๐ โ (LinFn โฉ ContFn),
๐, ( โ ร {0}))
โ LinFn |
13 | | inss2 4193 |
. . . . . . . 8
โข (LinFn
โฉ ContFn) โ ContFn |
14 | 13, 11 | sselii 3945 |
. . . . . . 7
โข if(๐ โ (LinFn โฉ ContFn),
๐, ( โ ร {0}))
โ ContFn |
15 | 12, 14 | riesz3i 31053 |
. . . . . 6
โข
โ๐ฆ โ
โ โ๐ฅ โ
โ (if(๐ โ (LinFn
โฉ ContFn), ๐, ( โ
ร {0}))โ๐ฅ) =
(๐ฅ
ยทih ๐ฆ) |
16 | 5, 15 | dedth 4548 |
. . . . 5
โข (๐ โ (LinFn โฉ ContFn)
โ โ๐ฆ โ
โ โ๐ฅ โ
โ (๐โ๐ฅ) = (๐ฅ ยทih ๐ฆ)) |
17 | 2, 16 | sylbir 234 |
. . . 4
โข ((๐ โ LinFn โง ๐ โ ContFn) โ
โ๐ฆ โ โ
โ๐ฅ โ โ
(๐โ๐ฅ) = (๐ฅ ยทih ๐ฆ)) |
18 | 17 | ex 414 |
. . 3
โข (๐ โ LinFn โ (๐ โ ContFn โ
โ๐ฆ โ โ
โ๐ฅ โ โ
(๐โ๐ฅ) = (๐ฅ ยทih ๐ฆ))) |
19 | | normcl 30116 |
. . . . . . 7
โข (๐ฆ โ โ โ
(normโโ๐ฆ) โ โ) |
20 | 19 | adantl 483 |
. . . . . 6
โข ((๐ โ LinFn โง ๐ฆ โ โ) โ
(normโโ๐ฆ) โ โ) |
21 | | fveq2 6846 |
. . . . . . . . . . 11
โข ((๐โ๐ฅ) = (๐ฅ ยทih ๐ฆ) โ (absโ(๐โ๐ฅ)) = (absโ(๐ฅ ยทih ๐ฆ))) |
22 | 21 | adantl 483 |
. . . . . . . . . 10
โข ((((๐ โ LinFn โง ๐ฅ โ โ) โง ๐ฆ โ โ) โง (๐โ๐ฅ) = (๐ฅ ยทih ๐ฆ)) โ (absโ(๐โ๐ฅ)) = (absโ(๐ฅ ยทih ๐ฆ))) |
23 | | bcs 30172 |
. . . . . . . . . . . . 13
โข ((๐ฅ โ โ โง ๐ฆ โ โ) โ
(absโ(๐ฅ
ยทih ๐ฆ)) โค ((normโโ๐ฅ) ยท
(normโโ๐ฆ))) |
24 | | normcl 30116 |
. . . . . . . . . . . . . 14
โข (๐ฅ โ โ โ
(normโโ๐ฅ) โ โ) |
25 | | recn 11149 |
. . . . . . . . . . . . . . 15
โข
((normโโ๐ฅ) โ โ โ
(normโโ๐ฅ) โ โ) |
26 | | recn 11149 |
. . . . . . . . . . . . . . 15
โข
((normโโ๐ฆ) โ โ โ
(normโโ๐ฆ) โ โ) |
27 | | mulcom 11145 |
. . . . . . . . . . . . . . 15
โข
(((normโโ๐ฅ) โ โ โง
(normโโ๐ฆ) โ โ) โ
((normโโ๐ฅ) ยท
(normโโ๐ฆ)) = ((normโโ๐ฆ) ยท
(normโโ๐ฅ))) |
28 | 25, 26, 27 | syl2an 597 |
. . . . . . . . . . . . . 14
โข
(((normโโ๐ฅ) โ โ โง
(normโโ๐ฆ) โ โ) โ
((normโโ๐ฅ) ยท
(normโโ๐ฆ)) = ((normโโ๐ฆ) ยท
(normโโ๐ฅ))) |
29 | 24, 19, 28 | syl2an 597 |
. . . . . . . . . . . . 13
โข ((๐ฅ โ โ โง ๐ฆ โ โ) โ
((normโโ๐ฅ) ยท
(normโโ๐ฆ)) = ((normโโ๐ฆ) ยท
(normโโ๐ฅ))) |
30 | 23, 29 | breqtrd 5135 |
. . . . . . . . . . . 12
โข ((๐ฅ โ โ โง ๐ฆ โ โ) โ
(absโ(๐ฅ
ยทih ๐ฆ)) โค ((normโโ๐ฆ) ยท
(normโโ๐ฅ))) |
31 | 30 | adantll 713 |
. . . . . . . . . . 11
โข (((๐ โ LinFn โง ๐ฅ โ โ) โง ๐ฆ โ โ) โ
(absโ(๐ฅ
ยทih ๐ฆ)) โค ((normโโ๐ฆ) ยท
(normโโ๐ฅ))) |
32 | 31 | adantr 482 |
. . . . . . . . . 10
โข ((((๐ โ LinFn โง ๐ฅ โ โ) โง ๐ฆ โ โ) โง (๐โ๐ฅ) = (๐ฅ ยทih ๐ฆ)) โ (absโ(๐ฅ
ยทih ๐ฆ)) โค ((normโโ๐ฆ) ยท
(normโโ๐ฅ))) |
33 | 22, 32 | eqbrtrd 5131 |
. . . . . . . . 9
โข ((((๐ โ LinFn โง ๐ฅ โ โ) โง ๐ฆ โ โ) โง (๐โ๐ฅ) = (๐ฅ ยทih ๐ฆ)) โ (absโ(๐โ๐ฅ)) โค ((normโโ๐ฆ) ยท
(normโโ๐ฅ))) |
34 | 33 | ex 414 |
. . . . . . . 8
โข (((๐ โ LinFn โง ๐ฅ โ โ) โง ๐ฆ โ โ) โ ((๐โ๐ฅ) = (๐ฅ ยทih ๐ฆ) โ (absโ(๐โ๐ฅ)) โค ((normโโ๐ฆ) ยท
(normโโ๐ฅ)))) |
35 | 34 | an32s 651 |
. . . . . . 7
โข (((๐ โ LinFn โง ๐ฆ โ โ) โง ๐ฅ โ โ) โ ((๐โ๐ฅ) = (๐ฅ ยทih ๐ฆ) โ (absโ(๐โ๐ฅ)) โค ((normโโ๐ฆ) ยท
(normโโ๐ฅ)))) |
36 | 35 | ralimdva 3161 |
. . . . . 6
โข ((๐ โ LinFn โง ๐ฆ โ โ) โ
(โ๐ฅ โ โ
(๐โ๐ฅ) = (๐ฅ ยทih ๐ฆ) โ โ๐ฅ โ โ
(absโ(๐โ๐ฅ)) โค
((normโโ๐ฆ) ยท
(normโโ๐ฅ)))) |
37 | | oveq1 7368 |
. . . . . . . . 9
โข (๐ง =
(normโโ๐ฆ) โ (๐ง ยท
(normโโ๐ฅ)) = ((normโโ๐ฆ) ยท
(normโโ๐ฅ))) |
38 | 37 | breq2d 5121 |
. . . . . . . 8
โข (๐ง =
(normโโ๐ฆ) โ ((absโ(๐โ๐ฅ)) โค (๐ง ยท
(normโโ๐ฅ)) โ (absโ(๐โ๐ฅ)) โค ((normโโ๐ฆ) ยท
(normโโ๐ฅ)))) |
39 | 38 | ralbidv 3171 |
. . . . . . 7
โข (๐ง =
(normโโ๐ฆ) โ (โ๐ฅ โ โ (absโ(๐โ๐ฅ)) โค (๐ง ยท
(normโโ๐ฅ)) โ โ๐ฅ โ โ (absโ(๐โ๐ฅ)) โค ((normโโ๐ฆ) ยท
(normโโ๐ฅ)))) |
40 | 39 | rspcev 3583 |
. . . . . 6
โข
(((normโโ๐ฆ) โ โ โง โ๐ฅ โ โ
(absโ(๐โ๐ฅ)) โค
((normโโ๐ฆ) ยท
(normโโ๐ฅ))) โ โ๐ง โ โ โ๐ฅ โ โ (absโ(๐โ๐ฅ)) โค (๐ง ยท
(normโโ๐ฅ))) |
41 | 20, 36, 40 | syl6an 683 |
. . . . 5
โข ((๐ โ LinFn โง ๐ฆ โ โ) โ
(โ๐ฅ โ โ
(๐โ๐ฅ) = (๐ฅ ยทih ๐ฆ) โ โ๐ง โ โ โ๐ฅ โ โ
(absโ(๐โ๐ฅ)) โค (๐ง ยท
(normโโ๐ฅ)))) |
42 | 41 | rexlimdva 3149 |
. . . 4
โข (๐ โ LinFn โ
(โ๐ฆ โ โ
โ๐ฅ โ โ
(๐โ๐ฅ) = (๐ฅ ยทih ๐ฆ) โ โ๐ง โ โ โ๐ฅ โ โ
(absโ(๐โ๐ฅ)) โค (๐ง ยท
(normโโ๐ฅ)))) |
43 | | lnfncon 31047 |
. . . 4
โข (๐ โ LinFn โ (๐ โ ContFn โ
โ๐ง โ โ
โ๐ฅ โ โ
(absโ(๐โ๐ฅ)) โค (๐ง ยท
(normโโ๐ฅ)))) |
44 | 42, 43 | sylibrd 259 |
. . 3
โข (๐ โ LinFn โ
(โ๐ฆ โ โ
โ๐ฅ โ โ
(๐โ๐ฅ) = (๐ฅ ยทih ๐ฆ) โ ๐ โ ContFn)) |
45 | 18, 44 | impbid 211 |
. 2
โข (๐ โ LinFn โ (๐ โ ContFn โ
โ๐ฆ โ โ
โ๐ฅ โ โ
(๐โ๐ฅ) = (๐ฅ ยทih ๐ฆ))) |
46 | 1, 45 | bitr3d 281 |
1
โข (๐ โ LinFn โ
((normfnโ๐) โ โ โ โ๐ฆ โ โ โ๐ฅ โ โ (๐โ๐ฅ) = (๐ฅ ยทih ๐ฆ))) |