Step | Hyp | Ref
| Expression |
1 | | nlelch.1 |
. . 3
β’ π β LinFn |
2 | | nlelch.2 |
. . 3
β’ π β ContFn |
3 | 1, 2 | riesz3i 31053 |
. 2
β’
βπ€ β
β βπ£ β
β (πβπ£) = (π£ Β·ih π€) |
4 | | r19.26 3111 |
. . . . 5
β’
(βπ£ β
β ((πβπ£) = (π£ Β·ih π€) β§ (πβπ£) = (π£ Β·ih π’)) β (βπ£ β β (πβπ£) = (π£ Β·ih π€) β§ βπ£ β β (πβπ£) = (π£ Β·ih π’))) |
5 | | oveq12 7370 |
. . . . . . . 8
β’ (((πβπ£) = (π£ Β·ih π€) β§ (πβπ£) = (π£ Β·ih π’)) β ((πβπ£) β (πβπ£)) = ((π£ Β·ih π€) β (π£ Β·ih π’))) |
6 | 5 | adantl 483 |
. . . . . . 7
β’ ((π£ β β β§ ((πβπ£) = (π£ Β·ih π€) β§ (πβπ£) = (π£ Β·ih π’))) β ((πβπ£) β (πβπ£)) = ((π£ Β·ih π€) β (π£ Β·ih π’))) |
7 | 1 | lnfnfi 31032 |
. . . . . . . . . 10
β’ π:
ββΆβ |
8 | 7 | ffvelcdmi 7038 |
. . . . . . . . 9
β’ (π£ β β β (πβπ£) β β) |
9 | 8 | subidd 11508 |
. . . . . . . 8
β’ (π£ β β β ((πβπ£) β (πβπ£)) = 0) |
10 | 9 | adantr 482 |
. . . . . . 7
β’ ((π£ β β β§ ((πβπ£) = (π£ Β·ih π€) β§ (πβπ£) = (π£ Β·ih π’))) β ((πβπ£) β (πβπ£)) = 0) |
11 | 6, 10 | eqtr3d 2775 |
. . . . . 6
β’ ((π£ β β β§ ((πβπ£) = (π£ Β·ih π€) β§ (πβπ£) = (π£ Β·ih π’))) β ((π£ Β·ih π€) β (π£ Β·ih π’)) = 0) |
12 | 11 | ralimiaa 3082 |
. . . . 5
β’
(βπ£ β
β ((πβπ£) = (π£ Β·ih π€) β§ (πβπ£) = (π£ Β·ih π’)) β βπ£ β β ((π£
Β·ih π€) β (π£ Β·ih π’)) = 0) |
13 | 4, 12 | sylbir 234 |
. . . 4
β’
((βπ£ β
β (πβπ£) = (π£ Β·ih π€) β§ βπ£ β β (πβπ£) = (π£ Β·ih π’)) β βπ£ β β ((π£
Β·ih π€) β (π£ Β·ih π’)) = 0) |
14 | | hvsubcl 30008 |
. . . . . 6
β’ ((π€ β β β§ π’ β β) β (π€ ββ
π’) β
β) |
15 | | oveq1 7368 |
. . . . . . . . 9
β’ (π£ = (π€ ββ π’) β (π£ Β·ih π€) = ((π€ ββ π’)
Β·ih π€)) |
16 | | oveq1 7368 |
. . . . . . . . 9
β’ (π£ = (π€ ββ π’) β (π£ Β·ih π’) = ((π€ ββ π’)
Β·ih π’)) |
17 | 15, 16 | oveq12d 7379 |
. . . . . . . 8
β’ (π£ = (π€ ββ π’) β ((π£ Β·ih π€) β (π£ Β·ih π’)) = (((π€ ββ π’)
Β·ih π€) β ((π€ ββ π’)
Β·ih π’))) |
18 | 17 | eqeq1d 2735 |
. . . . . . 7
β’ (π£ = (π€ ββ π’) β (((π£ Β·ih π€) β (π£ Β·ih π’)) = 0 β (((π€ ββ
π’)
Β·ih π€) β ((π€ ββ π’)
Β·ih π’)) = 0)) |
19 | 18 | rspcv 3579 |
. . . . . 6
β’ ((π€ ββ
π’) β β β
(βπ£ β β
((π£
Β·ih π€) β (π£ Β·ih π’)) = 0 β (((π€ ββ
π’)
Β·ih π€) β ((π€ ββ π’)
Β·ih π’)) = 0)) |
20 | 14, 19 | syl 17 |
. . . . 5
β’ ((π€ β β β§ π’ β β) β
(βπ£ β β
((π£
Β·ih π€) β (π£ Β·ih π’)) = 0 β (((π€ ββ
π’)
Β·ih π€) β ((π€ ββ π’)
Β·ih π’)) = 0)) |
21 | | normcl 30116 |
. . . . . . . . . 10
β’ ((π€ ββ
π’) β β β
(normββ(π€ ββ π’)) β
β) |
22 | 21 | recnd 11191 |
. . . . . . . . 9
β’ ((π€ ββ
π’) β β β
(normββ(π€ ββ π’)) β
β) |
23 | | sqeq0 14034 |
. . . . . . . . 9
β’
((normββ(π€ ββ π’)) β β β
(((normββ(π€ ββ π’))β2) = 0 β
(normββ(π€ ββ π’)) = 0)) |
24 | 22, 23 | syl 17 |
. . . . . . . 8
β’ ((π€ ββ
π’) β β β
(((normββ(π€ ββ π’))β2) = 0 β
(normββ(π€ ββ π’)) = 0)) |
25 | | norm-i 30120 |
. . . . . . . 8
β’ ((π€ ββ
π’) β β β
((normββ(π€ ββ π’)) = 0 β (π€ ββ
π’) =
0β)) |
26 | 24, 25 | bitrd 279 |
. . . . . . 7
β’ ((π€ ββ
π’) β β β
(((normββ(π€ ββ π’))β2) = 0 β (π€ ββ
π’) =
0β)) |
27 | 14, 26 | syl 17 |
. . . . . 6
β’ ((π€ β β β§ π’ β β) β
(((normββ(π€ ββ π’))β2) = 0 β (π€ ββ
π’) =
0β)) |
28 | | normsq 30125 |
. . . . . . . . 9
β’ ((π€ ββ
π’) β β β
((normββ(π€ ββ π’))β2) = ((π€ ββ
π’)
Β·ih (π€ ββ π’))) |
29 | 14, 28 | syl 17 |
. . . . . . . 8
β’ ((π€ β β β§ π’ β β) β
((normββ(π€ ββ π’))β2) = ((π€ ββ
π’)
Β·ih (π€ ββ π’))) |
30 | | simpl 484 |
. . . . . . . . 9
β’ ((π€ β β β§ π’ β β) β π€ β
β) |
31 | | simpr 486 |
. . . . . . . . 9
β’ ((π€ β β β§ π’ β β) β π’ β
β) |
32 | | his2sub2 30084 |
. . . . . . . . 9
β’ (((π€ ββ
π’) β β β§
π€ β β β§
π’ β β) β
((π€
ββ π’) Β·ih (π€ ββ
π’)) = (((π€ ββ π’)
Β·ih π€) β ((π€ ββ π’)
Β·ih π’))) |
33 | 14, 30, 31, 32 | syl3anc 1372 |
. . . . . . . 8
β’ ((π€ β β β§ π’ β β) β ((π€ ββ
π’)
Β·ih (π€ ββ π’)) = (((π€ ββ π’)
Β·ih π€) β ((π€ ββ π’)
Β·ih π’))) |
34 | 29, 33 | eqtrd 2773 |
. . . . . . 7
β’ ((π€ β β β§ π’ β β) β
((normββ(π€ ββ π’))β2) = (((π€ ββ
π’)
Β·ih π€) β ((π€ ββ π’)
Β·ih π’))) |
35 | 34 | eqeq1d 2735 |
. . . . . 6
β’ ((π€ β β β§ π’ β β) β
(((normββ(π€ ββ π’))β2) = 0 β (((π€ ββ
π’)
Β·ih π€) β ((π€ ββ π’)
Β·ih π’)) = 0)) |
36 | | hvsubeq0 30059 |
. . . . . 6
β’ ((π€ β β β§ π’ β β) β ((π€ ββ
π’) = 0β
β π€ = π’)) |
37 | 27, 35, 36 | 3bitr3d 309 |
. . . . 5
β’ ((π€ β β β§ π’ β β) β
((((π€
ββ π’) Β·ih π€) β ((π€ ββ π’)
Β·ih π’)) = 0 β π€ = π’)) |
38 | 20, 37 | sylibd 238 |
. . . 4
β’ ((π€ β β β§ π’ β β) β
(βπ£ β β
((π£
Β·ih π€) β (π£ Β·ih π’)) = 0 β π€ = π’)) |
39 | 13, 38 | syl5 34 |
. . 3
β’ ((π€ β β β§ π’ β β) β
((βπ£ β β
(πβπ£) = (π£ Β·ih π€) β§ βπ£ β β (πβπ£) = (π£ Β·ih π’)) β π€ = π’)) |
40 | 39 | rgen2 3191 |
. 2
β’
βπ€ β
β βπ’ β
β ((βπ£ β
β (πβπ£) = (π£ Β·ih π€) β§ βπ£ β β (πβπ£) = (π£ Β·ih π’)) β π€ = π’) |
41 | | oveq2 7369 |
. . . . 5
β’ (π€ = π’ β (π£ Β·ih π€) = (π£ Β·ih π’)) |
42 | 41 | eqeq2d 2744 |
. . . 4
β’ (π€ = π’ β ((πβπ£) = (π£ Β·ih π€) β (πβπ£) = (π£ Β·ih π’))) |
43 | 42 | ralbidv 3171 |
. . 3
β’ (π€ = π’ β (βπ£ β β (πβπ£) = (π£ Β·ih π€) β βπ£ β β (πβπ£) = (π£ Β·ih π’))) |
44 | 43 | reu4 3693 |
. 2
β’
(β!π€ β
β βπ£ β
β (πβπ£) = (π£ Β·ih π€) β (βπ€ β β βπ£ β β (πβπ£) = (π£ Β·ih π€) β§ βπ€ β β βπ’ β β ((βπ£ β β (πβπ£) = (π£ Β·ih π€) β§ βπ£ β β (πβπ£) = (π£ Β·ih π’)) β π€ = π’))) |
45 | 3, 40, 44 | mpbir2an 710 |
1
β’
β!π€ β
β βπ£ β
β (πβπ£) = (π£ Β·ih π€) |