Step | Hyp | Ref
| Expression |
1 | | dvivth.1 |
. . . . . . . . . 10
β’ (π β π β (π΄(,)π΅)) |
2 | 1 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ (π < π β§ π₯ β (((β D πΉ)βπ)[,]((β D πΉ)βπ)))) β π β (π΄(,)π΅)) |
3 | | dvivth.2 |
. . . . . . . . . 10
β’ (π β π β (π΄(,)π΅)) |
4 | 3 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ (π < π β§ π₯ β (((β D πΉ)βπ)[,]((β D πΉ)βπ)))) β π β (π΄(,)π΅)) |
5 | | dvivth.3 |
. . . . . . . . . . . . . . 15
β’ (π β πΉ β ((π΄(,)π΅)βcnββ)) |
6 | | cncff 24409 |
. . . . . . . . . . . . . . 15
β’ (πΉ β ((π΄(,)π΅)βcnββ) β πΉ:(π΄(,)π΅)βΆβ) |
7 | 5, 6 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π β πΉ:(π΄(,)π΅)βΆβ) |
8 | 7 | ffvelcdmda 7087 |
. . . . . . . . . . . . 13
β’ ((π β§ π€ β (π΄(,)π΅)) β (πΉβπ€) β β) |
9 | 8 | renegcld 11641 |
. . . . . . . . . . . 12
β’ ((π β§ π€ β (π΄(,)π΅)) β -(πΉβπ€) β β) |
10 | 9 | fmpttd 7115 |
. . . . . . . . . . 11
β’ (π β (π€ β (π΄(,)π΅) β¦ -(πΉβπ€)):(π΄(,)π΅)βΆβ) |
11 | | ax-resscn 11167 |
. . . . . . . . . . . 12
β’ β
β β |
12 | | ssid 4005 |
. . . . . . . . . . . . . . 15
β’ β
β β |
13 | | cncfss 24415 |
. . . . . . . . . . . . . . 15
β’ ((β
β β β§ β β β) β ((π΄(,)π΅)βcnββ) β ((π΄(,)π΅)βcnββ)) |
14 | 11, 12, 13 | mp2an 691 |
. . . . . . . . . . . . . 14
β’ ((π΄(,)π΅)βcnββ) β ((π΄(,)π΅)βcnββ) |
15 | 14, 5 | sselid 3981 |
. . . . . . . . . . . . 13
β’ (π β πΉ β ((π΄(,)π΅)βcnββ)) |
16 | | eqid 2733 |
. . . . . . . . . . . . . 14
β’ (π€ β (π΄(,)π΅) β¦ -(πΉβπ€)) = (π€ β (π΄(,)π΅) β¦ -(πΉβπ€)) |
17 | 16 | negfcncf 24439 |
. . . . . . . . . . . . 13
β’ (πΉ β ((π΄(,)π΅)βcnββ) β (π€ β (π΄(,)π΅) β¦ -(πΉβπ€)) β ((π΄(,)π΅)βcnββ)) |
18 | 15, 17 | syl 17 |
. . . . . . . . . . . 12
β’ (π β (π€ β (π΄(,)π΅) β¦ -(πΉβπ€)) β ((π΄(,)π΅)βcnββ)) |
19 | | cncfcdm 24414 |
. . . . . . . . . . . 12
β’ ((β
β β β§ (π€
β (π΄(,)π΅) β¦ -(πΉβπ€)) β ((π΄(,)π΅)βcnββ)) β ((π€ β (π΄(,)π΅) β¦ -(πΉβπ€)) β ((π΄(,)π΅)βcnββ) β (π€ β (π΄(,)π΅) β¦ -(πΉβπ€)):(π΄(,)π΅)βΆβ)) |
20 | 11, 18, 19 | sylancr 588 |
. . . . . . . . . . 11
β’ (π β ((π€ β (π΄(,)π΅) β¦ -(πΉβπ€)) β ((π΄(,)π΅)βcnββ) β (π€ β (π΄(,)π΅) β¦ -(πΉβπ€)):(π΄(,)π΅)βΆβ)) |
21 | 10, 20 | mpbird 257 |
. . . . . . . . . 10
β’ (π β (π€ β (π΄(,)π΅) β¦ -(πΉβπ€)) β ((π΄(,)π΅)βcnββ)) |
22 | 21 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ (π < π β§ π₯ β (((β D πΉ)βπ)[,]((β D πΉ)βπ)))) β (π€ β (π΄(,)π΅) β¦ -(πΉβπ€)) β ((π΄(,)π΅)βcnββ)) |
23 | | reelprrecn 11202 |
. . . . . . . . . . . . 13
β’ β
β {β, β} |
24 | 23 | a1i 11 |
. . . . . . . . . . . 12
β’ ((π β§ (π < π β§ π₯ β (((β D πΉ)βπ)[,]((β D πΉ)βπ)))) β β β {β,
β}) |
25 | 7 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π < π β§ π₯ β (((β D πΉ)βπ)[,]((β D πΉ)βπ)))) β πΉ:(π΄(,)π΅)βΆβ) |
26 | 25 | ffvelcdmda 7087 |
. . . . . . . . . . . . 13
β’ (((π β§ (π < π β§ π₯ β (((β D πΉ)βπ)[,]((β D πΉ)βπ)))) β§ π€ β (π΄(,)π΅)) β (πΉβπ€) β β) |
27 | 26 | recnd 11242 |
. . . . . . . . . . . 12
β’ (((π β§ (π < π β§ π₯ β (((β D πΉ)βπ)[,]((β D πΉ)βπ)))) β§ π€ β (π΄(,)π΅)) β (πΉβπ€) β β) |
28 | | fvexd 6907 |
. . . . . . . . . . . 12
β’ (((π β§ (π < π β§ π₯ β (((β D πΉ)βπ)[,]((β D πΉ)βπ)))) β§ π€ β (π΄(,)π΅)) β ((β D πΉ)βπ€) β V) |
29 | 25 | feqmptd 6961 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π < π β§ π₯ β (((β D πΉ)βπ)[,]((β D πΉ)βπ)))) β πΉ = (π€ β (π΄(,)π΅) β¦ (πΉβπ€))) |
30 | 29 | oveq2d 7425 |
. . . . . . . . . . . . 13
β’ ((π β§ (π < π β§ π₯ β (((β D πΉ)βπ)[,]((β D πΉ)βπ)))) β (β D πΉ) = (β D (π€ β (π΄(,)π΅) β¦ (πΉβπ€)))) |
31 | | ioossre 13385 |
. . . . . . . . . . . . . . . . 17
β’ (π΄(,)π΅) β β |
32 | | dvfre 25468 |
. . . . . . . . . . . . . . . . 17
β’ ((πΉ:(π΄(,)π΅)βΆβ β§ (π΄(,)π΅) β β) β (β D πΉ):dom (β D πΉ)βΆβ) |
33 | 7, 31, 32 | sylancl 587 |
. . . . . . . . . . . . . . . 16
β’ (π β (β D πΉ):dom (β D πΉ)βΆβ) |
34 | | dvivth.4 |
. . . . . . . . . . . . . . . . 17
β’ (π β dom (β D πΉ) = (π΄(,)π΅)) |
35 | 34 | feq2d 6704 |
. . . . . . . . . . . . . . . 16
β’ (π β ((β D πΉ):dom (β D πΉ)βΆβ β (β
D πΉ):(π΄(,)π΅)βΆβ)) |
36 | 33, 35 | mpbid 231 |
. . . . . . . . . . . . . . 15
β’ (π β (β D πΉ):(π΄(,)π΅)βΆβ) |
37 | 36 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π < π β§ π₯ β (((β D πΉ)βπ)[,]((β D πΉ)βπ)))) β (β D πΉ):(π΄(,)π΅)βΆβ) |
38 | 37 | feqmptd 6961 |
. . . . . . . . . . . . 13
β’ ((π β§ (π < π β§ π₯ β (((β D πΉ)βπ)[,]((β D πΉ)βπ)))) β (β D πΉ) = (π€ β (π΄(,)π΅) β¦ ((β D πΉ)βπ€))) |
39 | 30, 38 | eqtr3d 2775 |
. . . . . . . . . . . 12
β’ ((π β§ (π < π β§ π₯ β (((β D πΉ)βπ)[,]((β D πΉ)βπ)))) β (β D (π€ β (π΄(,)π΅) β¦ (πΉβπ€))) = (π€ β (π΄(,)π΅) β¦ ((β D πΉ)βπ€))) |
40 | 24, 27, 28, 39 | dvmptneg 25483 |
. . . . . . . . . . 11
β’ ((π β§ (π < π β§ π₯ β (((β D πΉ)βπ)[,]((β D πΉ)βπ)))) β (β D (π€ β (π΄(,)π΅) β¦ -(πΉβπ€))) = (π€ β (π΄(,)π΅) β¦ -((β D πΉ)βπ€))) |
41 | 40 | dmeqd 5906 |
. . . . . . . . . 10
β’ ((π β§ (π < π β§ π₯ β (((β D πΉ)βπ)[,]((β D πΉ)βπ)))) β dom (β D (π€ β (π΄(,)π΅) β¦ -(πΉβπ€))) = dom (π€ β (π΄(,)π΅) β¦ -((β D πΉ)βπ€))) |
42 | | dmmptg 6242 |
. . . . . . . . . . 11
β’
(βπ€ β
(π΄(,)π΅)-((β D πΉ)βπ€) β V β dom (π€ β (π΄(,)π΅) β¦ -((β D πΉ)βπ€)) = (π΄(,)π΅)) |
43 | | negex 11458 |
. . . . . . . . . . . 12
β’
-((β D πΉ)βπ€) β V |
44 | 43 | a1i 11 |
. . . . . . . . . . 11
β’ (π€ β (π΄(,)π΅) β -((β D πΉ)βπ€) β V) |
45 | 42, 44 | mprg 3068 |
. . . . . . . . . 10
β’ dom
(π€ β (π΄(,)π΅) β¦ -((β D πΉ)βπ€)) = (π΄(,)π΅) |
46 | 41, 45 | eqtrdi 2789 |
. . . . . . . . 9
β’ ((π β§ (π < π β§ π₯ β (((β D πΉ)βπ)[,]((β D πΉ)βπ)))) β dom (β D (π€ β (π΄(,)π΅) β¦ -(πΉβπ€))) = (π΄(,)π΅)) |
47 | | simprl 770 |
. . . . . . . . 9
β’ ((π β§ (π < π β§ π₯ β (((β D πΉ)βπ)[,]((β D πΉ)βπ)))) β π < π) |
48 | | simprr 772 |
. . . . . . . . . . 11
β’ ((π β§ (π < π β§ π₯ β (((β D πΉ)βπ)[,]((β D πΉ)βπ)))) β π₯ β (((β D πΉ)βπ)[,]((β D πΉ)βπ))) |
49 | 36, 1 | ffvelcdmd 7088 |
. . . . . . . . . . . . 13
β’ (π β ((β D πΉ)βπ) β β) |
50 | 49 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ (π < π β§ π₯ β (((β D πΉ)βπ)[,]((β D πΉ)βπ)))) β ((β D πΉ)βπ) β β) |
51 | 3, 34 | eleqtrrd 2837 |
. . . . . . . . . . . . . 14
β’ (π β π β dom (β D πΉ)) |
52 | 33, 51 | ffvelcdmd 7088 |
. . . . . . . . . . . . 13
β’ (π β ((β D πΉ)βπ) β β) |
53 | 52 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ (π < π β§ π₯ β (((β D πΉ)βπ)[,]((β D πΉ)βπ)))) β ((β D πΉ)βπ) β β) |
54 | | iccssre 13406 |
. . . . . . . . . . . . . . 15
β’
((((β D πΉ)βπ) β β β§ ((β D πΉ)βπ) β β) β (((β D πΉ)βπ)[,]((β D πΉ)βπ)) β β) |
55 | 49, 52, 54 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ (π β (((β D πΉ)βπ)[,]((β D πΉ)βπ)) β β) |
56 | 55 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ (π < π β§ π₯ β (((β D πΉ)βπ)[,]((β D πΉ)βπ)))) β (((β D πΉ)βπ)[,]((β D πΉ)βπ)) β β) |
57 | 56, 48 | sseldd 3984 |
. . . . . . . . . . . 12
β’ ((π β§ (π < π β§ π₯ β (((β D πΉ)βπ)[,]((β D πΉ)βπ)))) β π₯ β β) |
58 | | iccneg 13449 |
. . . . . . . . . . . 12
β’
((((β D πΉ)βπ) β β β§ ((β D πΉ)βπ) β β β§ π₯ β β) β (π₯ β (((β D πΉ)βπ)[,]((β D πΉ)βπ)) β -π₯ β (-((β D πΉ)βπ)[,]-((β D πΉ)βπ)))) |
59 | 50, 53, 57, 58 | syl3anc 1372 |
. . . . . . . . . . 11
β’ ((π β§ (π < π β§ π₯ β (((β D πΉ)βπ)[,]((β D πΉ)βπ)))) β (π₯ β (((β D πΉ)βπ)[,]((β D πΉ)βπ)) β -π₯ β (-((β D πΉ)βπ)[,]-((β D πΉ)βπ)))) |
60 | 48, 59 | mpbid 231 |
. . . . . . . . . 10
β’ ((π β§ (π < π β§ π₯ β (((β D πΉ)βπ)[,]((β D πΉ)βπ)))) β -π₯ β (-((β D πΉ)βπ)[,]-((β D πΉ)βπ))) |
61 | 40 | fveq1d 6894 |
. . . . . . . . . . . 12
β’ ((π β§ (π < π β§ π₯ β (((β D πΉ)βπ)[,]((β D πΉ)βπ)))) β ((β D (π€ β (π΄(,)π΅) β¦ -(πΉβπ€)))βπ) = ((π€ β (π΄(,)π΅) β¦ -((β D πΉ)βπ€))βπ)) |
62 | | fveq2 6892 |
. . . . . . . . . . . . . . 15
β’ (π€ = π β ((β D πΉ)βπ€) = ((β D πΉ)βπ)) |
63 | 62 | negeqd 11454 |
. . . . . . . . . . . . . 14
β’ (π€ = π β -((β D πΉ)βπ€) = -((β D πΉ)βπ)) |
64 | | eqid 2733 |
. . . . . . . . . . . . . 14
β’ (π€ β (π΄(,)π΅) β¦ -((β D πΉ)βπ€)) = (π€ β (π΄(,)π΅) β¦ -((β D πΉ)βπ€)) |
65 | | negex 11458 |
. . . . . . . . . . . . . 14
β’
-((β D πΉ)βπ) β V |
66 | 63, 64, 65 | fvmpt 6999 |
. . . . . . . . . . . . 13
β’ (π β (π΄(,)π΅) β ((π€ β (π΄(,)π΅) β¦ -((β D πΉ)βπ€))βπ) = -((β D πΉ)βπ)) |
67 | 4, 66 | syl 17 |
. . . . . . . . . . . 12
β’ ((π β§ (π < π β§ π₯ β (((β D πΉ)βπ)[,]((β D πΉ)βπ)))) β ((π€ β (π΄(,)π΅) β¦ -((β D πΉ)βπ€))βπ) = -((β D πΉ)βπ)) |
68 | 61, 67 | eqtrd 2773 |
. . . . . . . . . . 11
β’ ((π β§ (π < π β§ π₯ β (((β D πΉ)βπ)[,]((β D πΉ)βπ)))) β ((β D (π€ β (π΄(,)π΅) β¦ -(πΉβπ€)))βπ) = -((β D πΉ)βπ)) |
69 | 40 | fveq1d 6894 |
. . . . . . . . . . . 12
β’ ((π β§ (π < π β§ π₯ β (((β D πΉ)βπ)[,]((β D πΉ)βπ)))) β ((β D (π€ β (π΄(,)π΅) β¦ -(πΉβπ€)))βπ) = ((π€ β (π΄(,)π΅) β¦ -((β D πΉ)βπ€))βπ)) |
70 | | fveq2 6892 |
. . . . . . . . . . . . . . 15
β’ (π€ = π β ((β D πΉ)βπ€) = ((β D πΉ)βπ)) |
71 | 70 | negeqd 11454 |
. . . . . . . . . . . . . 14
β’ (π€ = π β -((β D πΉ)βπ€) = -((β D πΉ)βπ)) |
72 | | negex 11458 |
. . . . . . . . . . . . . 14
β’
-((β D πΉ)βπ) β V |
73 | 71, 64, 72 | fvmpt 6999 |
. . . . . . . . . . . . 13
β’ (π β (π΄(,)π΅) β ((π€ β (π΄(,)π΅) β¦ -((β D πΉ)βπ€))βπ) = -((β D πΉ)βπ)) |
74 | 2, 73 | syl 17 |
. . . . . . . . . . . 12
β’ ((π β§ (π < π β§ π₯ β (((β D πΉ)βπ)[,]((β D πΉ)βπ)))) β ((π€ β (π΄(,)π΅) β¦ -((β D πΉ)βπ€))βπ) = -((β D πΉ)βπ)) |
75 | 69, 74 | eqtrd 2773 |
. . . . . . . . . . 11
β’ ((π β§ (π < π β§ π₯ β (((β D πΉ)βπ)[,]((β D πΉ)βπ)))) β ((β D (π€ β (π΄(,)π΅) β¦ -(πΉβπ€)))βπ) = -((β D πΉ)βπ)) |
76 | 68, 75 | oveq12d 7427 |
. . . . . . . . . 10
β’ ((π β§ (π < π β§ π₯ β (((β D πΉ)βπ)[,]((β D πΉ)βπ)))) β (((β D (π€ β (π΄(,)π΅) β¦ -(πΉβπ€)))βπ)[,]((β D (π€ β (π΄(,)π΅) β¦ -(πΉβπ€)))βπ)) = (-((β D πΉ)βπ)[,]-((β D πΉ)βπ))) |
77 | 60, 76 | eleqtrrd 2837 |
. . . . . . . . 9
β’ ((π β§ (π < π β§ π₯ β (((β D πΉ)βπ)[,]((β D πΉ)βπ)))) β -π₯ β (((β D (π€ β (π΄(,)π΅) β¦ -(πΉβπ€)))βπ)[,]((β D (π€ β (π΄(,)π΅) β¦ -(πΉβπ€)))βπ))) |
78 | | eqid 2733 |
. . . . . . . . 9
β’ (π¦ β (π΄(,)π΅) β¦ (((π€ β (π΄(,)π΅) β¦ -(πΉβπ€))βπ¦) β (-π₯ Β· π¦))) = (π¦ β (π΄(,)π΅) β¦ (((π€ β (π΄(,)π΅) β¦ -(πΉβπ€))βπ¦) β (-π₯ Β· π¦))) |
79 | 2, 4, 22, 46, 47, 77, 78 | dvivthlem2 25526 |
. . . . . . . 8
β’ ((π β§ (π < π β§ π₯ β (((β D πΉ)βπ)[,]((β D πΉ)βπ)))) β -π₯ β ran (β D (π€ β (π΄(,)π΅) β¦ -(πΉβπ€)))) |
80 | 40 | rneqd 5938 |
. . . . . . . 8
β’ ((π β§ (π < π β§ π₯ β (((β D πΉ)βπ)[,]((β D πΉ)βπ)))) β ran (β D (π€ β (π΄(,)π΅) β¦ -(πΉβπ€))) = ran (π€ β (π΄(,)π΅) β¦ -((β D πΉ)βπ€))) |
81 | 79, 80 | eleqtrd 2836 |
. . . . . . 7
β’ ((π β§ (π < π β§ π₯ β (((β D πΉ)βπ)[,]((β D πΉ)βπ)))) β -π₯ β ran (π€ β (π΄(,)π΅) β¦ -((β D πΉ)βπ€))) |
82 | | negex 11458 |
. . . . . . . 8
β’ -π₯ β V |
83 | 64 | elrnmpt 5956 |
. . . . . . . 8
β’ (-π₯ β V β (-π₯ β ran (π€ β (π΄(,)π΅) β¦ -((β D πΉ)βπ€)) β βπ€ β (π΄(,)π΅)-π₯ = -((β D πΉ)βπ€))) |
84 | 82, 83 | ax-mp 5 |
. . . . . . 7
β’ (-π₯ β ran (π€ β (π΄(,)π΅) β¦ -((β D πΉ)βπ€)) β βπ€ β (π΄(,)π΅)-π₯ = -((β D πΉ)βπ€)) |
85 | 81, 84 | sylib 217 |
. . . . . 6
β’ ((π β§ (π < π β§ π₯ β (((β D πΉ)βπ)[,]((β D πΉ)βπ)))) β βπ€ β (π΄(,)π΅)-π₯ = -((β D πΉ)βπ€)) |
86 | 57 | recnd 11242 |
. . . . . . . . . 10
β’ ((π β§ (π < π β§ π₯ β (((β D πΉ)βπ)[,]((β D πΉ)βπ)))) β π₯ β β) |
87 | 86 | adantr 482 |
. . . . . . . . 9
β’ (((π β§ (π < π β§ π₯ β (((β D πΉ)βπ)[,]((β D πΉ)βπ)))) β§ π€ β (π΄(,)π΅)) β π₯ β β) |
88 | 24, 27, 28, 39 | dvmptcl 25476 |
. . . . . . . . 9
β’ (((π β§ (π < π β§ π₯ β (((β D πΉ)βπ)[,]((β D πΉ)βπ)))) β§ π€ β (π΄(,)π΅)) β ((β D πΉ)βπ€) β β) |
89 | 87, 88 | neg11ad 11567 |
. . . . . . . 8
β’ (((π β§ (π < π β§ π₯ β (((β D πΉ)βπ)[,]((β D πΉ)βπ)))) β§ π€ β (π΄(,)π΅)) β (-π₯ = -((β D πΉ)βπ€) β π₯ = ((β D πΉ)βπ€))) |
90 | | eqcom 2740 |
. . . . . . . 8
β’ (π₯ = ((β D πΉ)βπ€) β ((β D πΉ)βπ€) = π₯) |
91 | 89, 90 | bitrdi 287 |
. . . . . . 7
β’ (((π β§ (π < π β§ π₯ β (((β D πΉ)βπ)[,]((β D πΉ)βπ)))) β§ π€ β (π΄(,)π΅)) β (-π₯ = -((β D πΉ)βπ€) β ((β D πΉ)βπ€) = π₯)) |
92 | 91 | rexbidva 3177 |
. . . . . 6
β’ ((π β§ (π < π β§ π₯ β (((β D πΉ)βπ)[,]((β D πΉ)βπ)))) β (βπ€ β (π΄(,)π΅)-π₯ = -((β D πΉ)βπ€) β βπ€ β (π΄(,)π΅)((β D πΉ)βπ€) = π₯)) |
93 | 85, 92 | mpbid 231 |
. . . . 5
β’ ((π β§ (π < π β§ π₯ β (((β D πΉ)βπ)[,]((β D πΉ)βπ)))) β βπ€ β (π΄(,)π΅)((β D πΉ)βπ€) = π₯) |
94 | 37 | ffnd 6719 |
. . . . . 6
β’ ((π β§ (π < π β§ π₯ β (((β D πΉ)βπ)[,]((β D πΉ)βπ)))) β (β D πΉ) Fn (π΄(,)π΅)) |
95 | | fvelrnb 6953 |
. . . . . 6
β’ ((β
D πΉ) Fn (π΄(,)π΅) β (π₯ β ran (β D πΉ) β βπ€ β (π΄(,)π΅)((β D πΉ)βπ€) = π₯)) |
96 | 94, 95 | syl 17 |
. . . . 5
β’ ((π β§ (π < π β§ π₯ β (((β D πΉ)βπ)[,]((β D πΉ)βπ)))) β (π₯ β ran (β D πΉ) β βπ€ β (π΄(,)π΅)((β D πΉ)βπ€) = π₯)) |
97 | 93, 96 | mpbird 257 |
. . . 4
β’ ((π β§ (π < π β§ π₯ β (((β D πΉ)βπ)[,]((β D πΉ)βπ)))) β π₯ β ran (β D πΉ)) |
98 | 97 | expr 458 |
. . 3
β’ ((π β§ π < π) β (π₯ β (((β D πΉ)βπ)[,]((β D πΉ)βπ)) β π₯ β ran (β D πΉ))) |
99 | 98 | ssrdv 3989 |
. 2
β’ ((π β§ π < π) β (((β D πΉ)βπ)[,]((β D πΉ)βπ)) β ran (β D πΉ)) |
100 | | fveq2 6892 |
. . . . 5
β’ (π = π β ((β D πΉ)βπ) = ((β D πΉ)βπ)) |
101 | 100 | oveq1d 7424 |
. . . 4
β’ (π = π β (((β D πΉ)βπ)[,]((β D πΉ)βπ)) = (((β D πΉ)βπ)[,]((β D πΉ)βπ))) |
102 | 52 | rexrd 11264 |
. . . . 5
β’ (π β ((β D πΉ)βπ) β
β*) |
103 | | iccid 13369 |
. . . . 5
β’
(((β D πΉ)βπ) β β* β
(((β D πΉ)βπ)[,]((β D πΉ)βπ)) = {((β D πΉ)βπ)}) |
104 | 102, 103 | syl 17 |
. . . 4
β’ (π β (((β D πΉ)βπ)[,]((β D πΉ)βπ)) = {((β D πΉ)βπ)}) |
105 | 101, 104 | sylan9eqr 2795 |
. . 3
β’ ((π β§ π = π) β (((β D πΉ)βπ)[,]((β D πΉ)βπ)) = {((β D πΉ)βπ)}) |
106 | 33 | ffnd 6719 |
. . . . . 6
β’ (π β (β D πΉ) Fn dom (β D πΉ)) |
107 | | fnfvelrn 7083 |
. . . . . 6
β’
(((β D πΉ) Fn
dom (β D πΉ) β§
π β dom (β D
πΉ)) β ((β D
πΉ)βπ) β ran (β D πΉ)) |
108 | 106, 51, 107 | syl2anc 585 |
. . . . 5
β’ (π β ((β D πΉ)βπ) β ran (β D πΉ)) |
109 | 108 | snssd 4813 |
. . . 4
β’ (π β {((β D πΉ)βπ)} β ran (β D πΉ)) |
110 | 109 | adantr 482 |
. . 3
β’ ((π β§ π = π) β {((β D πΉ)βπ)} β ran (β D πΉ)) |
111 | 105, 110 | eqsstrd 4021 |
. 2
β’ ((π β§ π = π) β (((β D πΉ)βπ)[,]((β D πΉ)βπ)) β ran (β D πΉ)) |
112 | 3 | adantr 482 |
. . . . 5
β’ ((π β§ (π < π β§ π₯ β (((β D πΉ)βπ)[,]((β D πΉ)βπ)))) β π β (π΄(,)π΅)) |
113 | 1 | adantr 482 |
. . . . 5
β’ ((π β§ (π < π β§ π₯ β (((β D πΉ)βπ)[,]((β D πΉ)βπ)))) β π β (π΄(,)π΅)) |
114 | 5 | adantr 482 |
. . . . 5
β’ ((π β§ (π < π β§ π₯ β (((β D πΉ)βπ)[,]((β D πΉ)βπ)))) β πΉ β ((π΄(,)π΅)βcnββ)) |
115 | 34 | adantr 482 |
. . . . 5
β’ ((π β§ (π < π β§ π₯ β (((β D πΉ)βπ)[,]((β D πΉ)βπ)))) β dom (β D πΉ) = (π΄(,)π΅)) |
116 | | simprl 770 |
. . . . 5
β’ ((π β§ (π < π β§ π₯ β (((β D πΉ)βπ)[,]((β D πΉ)βπ)))) β π < π) |
117 | | simprr 772 |
. . . . 5
β’ ((π β§ (π < π β§ π₯ β (((β D πΉ)βπ)[,]((β D πΉ)βπ)))) β π₯ β (((β D πΉ)βπ)[,]((β D πΉ)βπ))) |
118 | | eqid 2733 |
. . . . 5
β’ (π¦ β (π΄(,)π΅) β¦ ((πΉβπ¦) β (π₯ Β· π¦))) = (π¦ β (π΄(,)π΅) β¦ ((πΉβπ¦) β (π₯ Β· π¦))) |
119 | 112, 113,
114, 115, 116, 117, 118 | dvivthlem2 25526 |
. . . 4
β’ ((π β§ (π < π β§ π₯ β (((β D πΉ)βπ)[,]((β D πΉ)βπ)))) β π₯ β ran (β D πΉ)) |
120 | 119 | expr 458 |
. . 3
β’ ((π β§ π < π) β (π₯ β (((β D πΉ)βπ)[,]((β D πΉ)βπ)) β π₯ β ran (β D πΉ))) |
121 | 120 | ssrdv 3989 |
. 2
β’ ((π β§ π < π) β (((β D πΉ)βπ)[,]((β D πΉ)βπ)) β ran (β D πΉ)) |
122 | 31, 1 | sselid 3981 |
. . 3
β’ (π β π β β) |
123 | 31, 3 | sselid 3981 |
. . 3
β’ (π β π β β) |
124 | 122, 123 | lttri4d 11355 |
. 2
β’ (π β (π < π β¨ π = π β¨ π < π)) |
125 | 99, 111, 121, 124 | mpjao3dan 1432 |
1
β’ (π β (((β D πΉ)βπ)[,]((β D πΉ)βπ)) β ran (β D πΉ)) |