Step | Hyp | Ref
| Expression |
1 | | dveq0.c |
. . . 4
β’ (π β πΉ β ((π΄[,]π΅)βcnββ)) |
2 | | cncff 24279 |
. . . 4
β’ (πΉ β ((π΄[,]π΅)βcnββ) β πΉ:(π΄[,]π΅)βΆβ) |
3 | 1, 2 | syl 17 |
. . 3
β’ (π β πΉ:(π΄[,]π΅)βΆβ) |
4 | 3 | ffnd 6673 |
. 2
β’ (π β πΉ Fn (π΄[,]π΅)) |
5 | | fvex 6859 |
. . 3
β’ (πΉβπ΄) β V |
6 | | fnconstg 6734 |
. . 3
β’ ((πΉβπ΄) β V β ((π΄[,]π΅) Γ {(πΉβπ΄)}) Fn (π΄[,]π΅)) |
7 | 5, 6 | mp1i 13 |
. 2
β’ (π β ((π΄[,]π΅) Γ {(πΉβπ΄)}) Fn (π΄[,]π΅)) |
8 | 5 | fvconst2 7157 |
. . . 4
β’ (π₯ β (π΄[,]π΅) β (((π΄[,]π΅) Γ {(πΉβπ΄)})βπ₯) = (πΉβπ΄)) |
9 | 8 | adantl 483 |
. . 3
β’ ((π β§ π₯ β (π΄[,]π΅)) β (((π΄[,]π΅) Γ {(πΉβπ΄)})βπ₯) = (πΉβπ΄)) |
10 | 3 | adantr 482 |
. . . . 5
β’ ((π β§ π₯ β (π΄[,]π΅)) β πΉ:(π΄[,]π΅)βΆβ) |
11 | | dveq0.a |
. . . . . . . 8
β’ (π β π΄ β β) |
12 | 11 | adantr 482 |
. . . . . . 7
β’ ((π β§ π₯ β (π΄[,]π΅)) β π΄ β β) |
13 | 12 | rexrd 11213 |
. . . . . 6
β’ ((π β§ π₯ β (π΄[,]π΅)) β π΄ β
β*) |
14 | | dveq0.b |
. . . . . . . 8
β’ (π β π΅ β β) |
15 | 14 | adantr 482 |
. . . . . . 7
β’ ((π β§ π₯ β (π΄[,]π΅)) β π΅ β β) |
16 | 15 | rexrd 11213 |
. . . . . 6
β’ ((π β§ π₯ β (π΄[,]π΅)) β π΅ β
β*) |
17 | | elicc2 13338 |
. . . . . . . . . 10
β’ ((π΄ β β β§ π΅ β β) β (π₯ β (π΄[,]π΅) β (π₯ β β β§ π΄ β€ π₯ β§ π₯ β€ π΅))) |
18 | 11, 14, 17 | syl2anc 585 |
. . . . . . . . 9
β’ (π β (π₯ β (π΄[,]π΅) β (π₯ β β β§ π΄ β€ π₯ β§ π₯ β€ π΅))) |
19 | 18 | biimpa 478 |
. . . . . . . 8
β’ ((π β§ π₯ β (π΄[,]π΅)) β (π₯ β β β§ π΄ β€ π₯ β§ π₯ β€ π΅)) |
20 | 19 | simp1d 1143 |
. . . . . . 7
β’ ((π β§ π₯ β (π΄[,]π΅)) β π₯ β β) |
21 | 19 | simp2d 1144 |
. . . . . . 7
β’ ((π β§ π₯ β (π΄[,]π΅)) β π΄ β€ π₯) |
22 | 19 | simp3d 1145 |
. . . . . . 7
β’ ((π β§ π₯ β (π΄[,]π΅)) β π₯ β€ π΅) |
23 | 12, 20, 15, 21, 22 | letrd 11320 |
. . . . . 6
β’ ((π β§ π₯ β (π΄[,]π΅)) β π΄ β€ π΅) |
24 | | lbicc2 13390 |
. . . . . 6
β’ ((π΄ β β*
β§ π΅ β
β* β§ π΄
β€ π΅) β π΄ β (π΄[,]π΅)) |
25 | 13, 16, 23, 24 | syl3anc 1372 |
. . . . 5
β’ ((π β§ π₯ β (π΄[,]π΅)) β π΄ β (π΄[,]π΅)) |
26 | 10, 25 | ffvelcdmd 7040 |
. . . 4
β’ ((π β§ π₯ β (π΄[,]π΅)) β (πΉβπ΄) β β) |
27 | 3 | ffvelcdmda 7039 |
. . . 4
β’ ((π β§ π₯ β (π΄[,]π΅)) β (πΉβπ₯) β β) |
28 | 26, 27 | subcld 11520 |
. . . . 5
β’ ((π β§ π₯ β (π΄[,]π΅)) β ((πΉβπ΄) β (πΉβπ₯)) β β) |
29 | | simpr 486 |
. . . . . . . . 9
β’ ((π β§ π₯ β (π΄[,]π΅)) β π₯ β (π΄[,]π΅)) |
30 | 25, 29 | jca 513 |
. . . . . . . 8
β’ ((π β§ π₯ β (π΄[,]π΅)) β (π΄ β (π΄[,]π΅) β§ π₯ β (π΄[,]π΅))) |
31 | | dveq0.d |
. . . . . . . . . . 11
β’ (π β (β D πΉ) = ((π΄(,)π΅) Γ {0})) |
32 | 31 | dmeqd 5865 |
. . . . . . . . . 10
β’ (π β dom (β D πΉ) = dom ((π΄(,)π΅) Γ {0})) |
33 | | c0ex 11157 |
. . . . . . . . . . . 12
β’ 0 β
V |
34 | 33 | snnz 4741 |
. . . . . . . . . . 11
β’ {0} β
β
|
35 | | dmxp 5888 |
. . . . . . . . . . 11
β’ ({0} β
β
β dom ((π΄(,)π΅) Γ {0}) = (π΄(,)π΅)) |
36 | 34, 35 | ax-mp 5 |
. . . . . . . . . 10
β’ dom
((π΄(,)π΅) Γ {0}) = (π΄(,)π΅) |
37 | 32, 36 | eqtrdi 2789 |
. . . . . . . . 9
β’ (π β dom (β D πΉ) = (π΄(,)π΅)) |
38 | | 0red 11166 |
. . . . . . . . 9
β’ (π β 0 β
β) |
39 | 31 | fveq1d 6848 |
. . . . . . . . . . . 12
β’ (π β ((β D πΉ)βπ¦) = (((π΄(,)π΅) Γ {0})βπ¦)) |
40 | 33 | fvconst2 7157 |
. . . . . . . . . . . 12
β’ (π¦ β (π΄(,)π΅) β (((π΄(,)π΅) Γ {0})βπ¦) = 0) |
41 | 39, 40 | sylan9eq 2793 |
. . . . . . . . . . 11
β’ ((π β§ π¦ β (π΄(,)π΅)) β ((β D πΉ)βπ¦) = 0) |
42 | 41 | abs00bd 15185 |
. . . . . . . . . 10
β’ ((π β§ π¦ β (π΄(,)π΅)) β (absβ((β D πΉ)βπ¦)) = 0) |
43 | | 0le0 12262 |
. . . . . . . . . 10
β’ 0 β€
0 |
44 | 42, 43 | eqbrtrdi 5148 |
. . . . . . . . 9
β’ ((π β§ π¦ β (π΄(,)π΅)) β (absβ((β D πΉ)βπ¦)) β€ 0) |
45 | 11, 14, 1, 37, 38, 44 | dvlip 25380 |
. . . . . . . 8
β’ ((π β§ (π΄ β (π΄[,]π΅) β§ π₯ β (π΄[,]π΅))) β (absβ((πΉβπ΄) β (πΉβπ₯))) β€ (0 Β· (absβ(π΄ β π₯)))) |
46 | 30, 45 | syldan 592 |
. . . . . . 7
β’ ((π β§ π₯ β (π΄[,]π΅)) β (absβ((πΉβπ΄) β (πΉβπ₯))) β€ (0 Β· (absβ(π΄ β π₯)))) |
47 | 12 | recnd 11191 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β (π΄[,]π΅)) β π΄ β β) |
48 | 20 | recnd 11191 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β (π΄[,]π΅)) β π₯ β β) |
49 | 47, 48 | subcld 11520 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (π΄[,]π΅)) β (π΄ β π₯) β β) |
50 | 49 | abscld 15330 |
. . . . . . . . 9
β’ ((π β§ π₯ β (π΄[,]π΅)) β (absβ(π΄ β π₯)) β β) |
51 | 50 | recnd 11191 |
. . . . . . . 8
β’ ((π β§ π₯ β (π΄[,]π΅)) β (absβ(π΄ β π₯)) β β) |
52 | 51 | mul02d 11361 |
. . . . . . 7
β’ ((π β§ π₯ β (π΄[,]π΅)) β (0 Β· (absβ(π΄ β π₯))) = 0) |
53 | 46, 52 | breqtrd 5135 |
. . . . . 6
β’ ((π β§ π₯ β (π΄[,]π΅)) β (absβ((πΉβπ΄) β (πΉβπ₯))) β€ 0) |
54 | 28 | absge0d 15338 |
. . . . . 6
β’ ((π β§ π₯ β (π΄[,]π΅)) β 0 β€ (absβ((πΉβπ΄) β (πΉβπ₯)))) |
55 | 28 | abscld 15330 |
. . . . . . 7
β’ ((π β§ π₯ β (π΄[,]π΅)) β (absβ((πΉβπ΄) β (πΉβπ₯))) β β) |
56 | | 0re 11165 |
. . . . . . 7
β’ 0 β
β |
57 | | letri3 11248 |
. . . . . . 7
β’
(((absβ((πΉβπ΄) β (πΉβπ₯))) β β β§ 0 β β)
β ((absβ((πΉβπ΄) β (πΉβπ₯))) = 0 β ((absβ((πΉβπ΄) β (πΉβπ₯))) β€ 0 β§ 0 β€ (absβ((πΉβπ΄) β (πΉβπ₯)))))) |
58 | 55, 56, 57 | sylancl 587 |
. . . . . 6
β’ ((π β§ π₯ β (π΄[,]π΅)) β ((absβ((πΉβπ΄) β (πΉβπ₯))) = 0 β ((absβ((πΉβπ΄) β (πΉβπ₯))) β€ 0 β§ 0 β€ (absβ((πΉβπ΄) β (πΉβπ₯)))))) |
59 | 53, 54, 58 | mpbir2and 712 |
. . . . 5
β’ ((π β§ π₯ β (π΄[,]π΅)) β (absβ((πΉβπ΄) β (πΉβπ₯))) = 0) |
60 | 28, 59 | abs00d 15340 |
. . . 4
β’ ((π β§ π₯ β (π΄[,]π΅)) β ((πΉβπ΄) β (πΉβπ₯)) = 0) |
61 | 26, 27, 60 | subeq0d 11528 |
. . 3
β’ ((π β§ π₯ β (π΄[,]π΅)) β (πΉβπ΄) = (πΉβπ₯)) |
62 | 9, 61 | eqtr2d 2774 |
. 2
β’ ((π β§ π₯ β (π΄[,]π΅)) β (πΉβπ₯) = (((π΄[,]π΅) Γ {(πΉβπ΄)})βπ₯)) |
63 | 4, 7, 62 | eqfnfvd 6989 |
1
β’ (π β πΉ = ((π΄[,]π΅) Γ {(πΉβπ΄)})) |