Step | Hyp | Ref
| Expression |
1 | | rolle.a |
. . . 4
β’ (π β π΄ β β) |
2 | | rolle.b |
. . . 4
β’ (π β π΅ β β) |
3 | | rolle.lt |
. . . . 5
β’ (π β π΄ < π΅) |
4 | 1, 2, 3 | ltled 11362 |
. . . 4
β’ (π β π΄ β€ π΅) |
5 | | rolle.f |
. . . 4
β’ (π β πΉ β ((π΄[,]π΅)βcnββ)) |
6 | 1, 2, 4, 5 | evthicc 24976 |
. . 3
β’ (π β (βπ’ β (π΄[,]π΅)βπ¦ β (π΄[,]π΅)(πΉβπ¦) β€ (πΉβπ’) β§ βπ£ β (π΄[,]π΅)βπ¦ β (π΄[,]π΅)(πΉβπ£) β€ (πΉβπ¦))) |
7 | | reeanv 3227 |
. . 3
β’
(βπ’ β
(π΄[,]π΅)βπ£ β (π΄[,]π΅)(βπ¦ β (π΄[,]π΅)(πΉβπ¦) β€ (πΉβπ’) β§ βπ¦ β (π΄[,]π΅)(πΉβπ£) β€ (πΉβπ¦)) β (βπ’ β (π΄[,]π΅)βπ¦ β (π΄[,]π΅)(πΉβπ¦) β€ (πΉβπ’) β§ βπ£ β (π΄[,]π΅)βπ¦ β (π΄[,]π΅)(πΉβπ£) β€ (πΉβπ¦))) |
8 | 6, 7 | sylibr 233 |
. 2
β’ (π β βπ’ β (π΄[,]π΅)βπ£ β (π΄[,]π΅)(βπ¦ β (π΄[,]π΅)(πΉβπ¦) β€ (πΉβπ’) β§ βπ¦ β (π΄[,]π΅)(πΉβπ£) β€ (πΉβπ¦))) |
9 | | r19.26 3112 |
. . . 4
β’
(βπ¦ β
(π΄[,]π΅)((πΉβπ¦) β€ (πΉβπ’) β§ (πΉβπ£) β€ (πΉβπ¦)) β (βπ¦ β (π΄[,]π΅)(πΉβπ¦) β€ (πΉβπ’) β§ βπ¦ β (π΄[,]π΅)(πΉβπ£) β€ (πΉβπ¦))) |
10 | 1 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ (π’ β (π΄[,]π΅) β§ π£ β (π΄[,]π΅))) β§ (βπ¦ β (π΄[,]π΅)((πΉβπ¦) β€ (πΉβπ’) β§ (πΉβπ£) β€ (πΉβπ¦)) β§ Β¬ π’ β {π΄, π΅})) β π΄ β β) |
11 | 2 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ (π’ β (π΄[,]π΅) β§ π£ β (π΄[,]π΅))) β§ (βπ¦ β (π΄[,]π΅)((πΉβπ¦) β€ (πΉβπ’) β§ (πΉβπ£) β€ (πΉβπ¦)) β§ Β¬ π’ β {π΄, π΅})) β π΅ β β) |
12 | 3 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ (π’ β (π΄[,]π΅) β§ π£ β (π΄[,]π΅))) β§ (βπ¦ β (π΄[,]π΅)((πΉβπ¦) β€ (πΉβπ’) β§ (πΉβπ£) β€ (πΉβπ¦)) β§ Β¬ π’ β {π΄, π΅})) β π΄ < π΅) |
13 | 5 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ (π’ β (π΄[,]π΅) β§ π£ β (π΄[,]π΅))) β§ (βπ¦ β (π΄[,]π΅)((πΉβπ¦) β€ (πΉβπ’) β§ (πΉβπ£) β€ (πΉβπ¦)) β§ Β¬ π’ β {π΄, π΅})) β πΉ β ((π΄[,]π΅)βcnββ)) |
14 | | rolle.d |
. . . . . . . . 9
β’ (π β dom (β D πΉ) = (π΄(,)π΅)) |
15 | 14 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ (π’ β (π΄[,]π΅) β§ π£ β (π΄[,]π΅))) β§ (βπ¦ β (π΄[,]π΅)((πΉβπ¦) β€ (πΉβπ’) β§ (πΉβπ£) β€ (πΉβπ¦)) β§ Β¬ π’ β {π΄, π΅})) β dom (β D πΉ) = (π΄(,)π΅)) |
16 | | simpl 484 |
. . . . . . . . . . 11
β’ (((πΉβπ¦) β€ (πΉβπ’) β§ (πΉβπ£) β€ (πΉβπ¦)) β (πΉβπ¦) β€ (πΉβπ’)) |
17 | 16 | ralimi 3084 |
. . . . . . . . . 10
β’
(βπ¦ β
(π΄[,]π΅)((πΉβπ¦) β€ (πΉβπ’) β§ (πΉβπ£) β€ (πΉβπ¦)) β βπ¦ β (π΄[,]π΅)(πΉβπ¦) β€ (πΉβπ’)) |
18 | | fveq2 6892 |
. . . . . . . . . . . 12
β’ (π¦ = π‘ β (πΉβπ¦) = (πΉβπ‘)) |
19 | 18 | breq1d 5159 |
. . . . . . . . . . 11
β’ (π¦ = π‘ β ((πΉβπ¦) β€ (πΉβπ’) β (πΉβπ‘) β€ (πΉβπ’))) |
20 | 19 | cbvralvw 3235 |
. . . . . . . . . 10
β’
(βπ¦ β
(π΄[,]π΅)(πΉβπ¦) β€ (πΉβπ’) β βπ‘ β (π΄[,]π΅)(πΉβπ‘) β€ (πΉβπ’)) |
21 | 17, 20 | sylib 217 |
. . . . . . . . 9
β’
(βπ¦ β
(π΄[,]π΅)((πΉβπ¦) β€ (πΉβπ’) β§ (πΉβπ£) β€ (πΉβπ¦)) β βπ‘ β (π΄[,]π΅)(πΉβπ‘) β€ (πΉβπ’)) |
22 | 21 | ad2antrl 727 |
. . . . . . . 8
β’ (((π β§ (π’ β (π΄[,]π΅) β§ π£ β (π΄[,]π΅))) β§ (βπ¦ β (π΄[,]π΅)((πΉβπ¦) β€ (πΉβπ’) β§ (πΉβπ£) β€ (πΉβπ¦)) β§ Β¬ π’ β {π΄, π΅})) β βπ‘ β (π΄[,]π΅)(πΉβπ‘) β€ (πΉβπ’)) |
23 | | simplrl 776 |
. . . . . . . 8
β’ (((π β§ (π’ β (π΄[,]π΅) β§ π£ β (π΄[,]π΅))) β§ (βπ¦ β (π΄[,]π΅)((πΉβπ¦) β€ (πΉβπ’) β§ (πΉβπ£) β€ (πΉβπ¦)) β§ Β¬ π’ β {π΄, π΅})) β π’ β (π΄[,]π΅)) |
24 | | simprr 772 |
. . . . . . . 8
β’ (((π β§ (π’ β (π΄[,]π΅) β§ π£ β (π΄[,]π΅))) β§ (βπ¦ β (π΄[,]π΅)((πΉβπ¦) β€ (πΉβπ’) β§ (πΉβπ£) β€ (πΉβπ¦)) β§ Β¬ π’ β {π΄, π΅})) β Β¬ π’ β {π΄, π΅}) |
25 | 10, 11, 12, 13, 15, 22, 23, 24 | rollelem 25506 |
. . . . . . 7
β’ (((π β§ (π’ β (π΄[,]π΅) β§ π£ β (π΄[,]π΅))) β§ (βπ¦ β (π΄[,]π΅)((πΉβπ¦) β€ (πΉβπ’) β§ (πΉβπ£) β€ (πΉβπ¦)) β§ Β¬ π’ β {π΄, π΅})) β βπ₯ β (π΄(,)π΅)((β D πΉ)βπ₯) = 0) |
26 | 25 | expr 458 |
. . . . . 6
β’ (((π β§ (π’ β (π΄[,]π΅) β§ π£ β (π΄[,]π΅))) β§ βπ¦ β (π΄[,]π΅)((πΉβπ¦) β€ (πΉβπ’) β§ (πΉβπ£) β€ (πΉβπ¦))) β (Β¬ π’ β {π΄, π΅} β βπ₯ β (π΄(,)π΅)((β D πΉ)βπ₯) = 0)) |
27 | 1 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ (π’ β (π΄[,]π΅) β§ π£ β (π΄[,]π΅))) β§ (βπ¦ β (π΄[,]π΅)((πΉβπ¦) β€ (πΉβπ’) β§ (πΉβπ£) β€ (πΉβπ¦)) β§ Β¬ π£ β {π΄, π΅})) β π΄ β β) |
28 | 2 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ (π’ β (π΄[,]π΅) β§ π£ β (π΄[,]π΅))) β§ (βπ¦ β (π΄[,]π΅)((πΉβπ¦) β€ (πΉβπ’) β§ (πΉβπ£) β€ (πΉβπ¦)) β§ Β¬ π£ β {π΄, π΅})) β π΅ β β) |
29 | 3 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ (π’ β (π΄[,]π΅) β§ π£ β (π΄[,]π΅))) β§ (βπ¦ β (π΄[,]π΅)((πΉβπ¦) β€ (πΉβπ’) β§ (πΉβπ£) β€ (πΉβπ¦)) β§ Β¬ π£ β {π΄, π΅})) β π΄ < π΅) |
30 | | cncff 24409 |
. . . . . . . . . . . . . . 15
β’ (πΉ β ((π΄[,]π΅)βcnββ) β πΉ:(π΄[,]π΅)βΆβ) |
31 | 5, 30 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π β πΉ:(π΄[,]π΅)βΆβ) |
32 | 31 | ffvelcdmda 7087 |
. . . . . . . . . . . . 13
β’ ((π β§ π’ β (π΄[,]π΅)) β (πΉβπ’) β β) |
33 | 32 | renegcld 11641 |
. . . . . . . . . . . 12
β’ ((π β§ π’ β (π΄[,]π΅)) β -(πΉβπ’) β β) |
34 | 33 | fmpttd 7115 |
. . . . . . . . . . 11
β’ (π β (π’ β (π΄[,]π΅) β¦ -(πΉβπ’)):(π΄[,]π΅)βΆβ) |
35 | | ax-resscn 11167 |
. . . . . . . . . . . 12
β’ β
β β |
36 | | ssid 4005 |
. . . . . . . . . . . . . . 15
β’ β
β β |
37 | | cncfss 24415 |
. . . . . . . . . . . . . . 15
β’ ((β
β β β§ β β β) β ((π΄[,]π΅)βcnββ) β ((π΄[,]π΅)βcnββ)) |
38 | 35, 36, 37 | mp2an 691 |
. . . . . . . . . . . . . 14
β’ ((π΄[,]π΅)βcnββ) β ((π΄[,]π΅)βcnββ) |
39 | 38, 5 | sselid 3981 |
. . . . . . . . . . . . 13
β’ (π β πΉ β ((π΄[,]π΅)βcnββ)) |
40 | | eqid 2733 |
. . . . . . . . . . . . . 14
β’ (π’ β (π΄[,]π΅) β¦ -(πΉβπ’)) = (π’ β (π΄[,]π΅) β¦ -(πΉβπ’)) |
41 | 40 | negfcncf 24439 |
. . . . . . . . . . . . 13
β’ (πΉ β ((π΄[,]π΅)βcnββ) β (π’ β (π΄[,]π΅) β¦ -(πΉβπ’)) β ((π΄[,]π΅)βcnββ)) |
42 | 39, 41 | syl 17 |
. . . . . . . . . . . 12
β’ (π β (π’ β (π΄[,]π΅) β¦ -(πΉβπ’)) β ((π΄[,]π΅)βcnββ)) |
43 | | cncfcdm 24414 |
. . . . . . . . . . . 12
β’ ((β
β β β§ (π’
β (π΄[,]π΅) β¦ -(πΉβπ’)) β ((π΄[,]π΅)βcnββ)) β ((π’ β (π΄[,]π΅) β¦ -(πΉβπ’)) β ((π΄[,]π΅)βcnββ) β (π’ β (π΄[,]π΅) β¦ -(πΉβπ’)):(π΄[,]π΅)βΆβ)) |
44 | 35, 42, 43 | sylancr 588 |
. . . . . . . . . . 11
β’ (π β ((π’ β (π΄[,]π΅) β¦ -(πΉβπ’)) β ((π΄[,]π΅)βcnββ) β (π’ β (π΄[,]π΅) β¦ -(πΉβπ’)):(π΄[,]π΅)βΆβ)) |
45 | 34, 44 | mpbird 257 |
. . . . . . . . . 10
β’ (π β (π’ β (π΄[,]π΅) β¦ -(πΉβπ’)) β ((π΄[,]π΅)βcnββ)) |
46 | 45 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ (π’ β (π΄[,]π΅) β§ π£ β (π΄[,]π΅))) β§ (βπ¦ β (π΄[,]π΅)((πΉβπ¦) β€ (πΉβπ’) β§ (πΉβπ£) β€ (πΉβπ¦)) β§ Β¬ π£ β {π΄, π΅})) β (π’ β (π΄[,]π΅) β¦ -(πΉβπ’)) β ((π΄[,]π΅)βcnββ)) |
47 | 35 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (π β β β
β) |
48 | | iccssre 13406 |
. . . . . . . . . . . . . . 15
β’ ((π΄ β β β§ π΅ β β) β (π΄[,]π΅) β β) |
49 | 1, 2, 48 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ (π β (π΄[,]π΅) β β) |
50 | | fss 6735 |
. . . . . . . . . . . . . . . . 17
β’ ((πΉ:(π΄[,]π΅)βΆβ β§ β β
β) β πΉ:(π΄[,]π΅)βΆβ) |
51 | 31, 35, 50 | sylancl 587 |
. . . . . . . . . . . . . . . 16
β’ (π β πΉ:(π΄[,]π΅)βΆβ) |
52 | 51 | ffvelcdmda 7087 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π’ β (π΄[,]π΅)) β (πΉβπ’) β β) |
53 | 52 | negcld 11558 |
. . . . . . . . . . . . . 14
β’ ((π β§ π’ β (π΄[,]π΅)) β -(πΉβπ’) β β) |
54 | | eqid 2733 |
. . . . . . . . . . . . . . 15
β’
(TopOpenββfld) =
(TopOpenββfld) |
55 | 54 | tgioo2 24319 |
. . . . . . . . . . . . . 14
β’
(topGenβran (,)) = ((TopOpenββfld)
βΎt β) |
56 | | iccntr 24337 |
. . . . . . . . . . . . . . 15
β’ ((π΄ β β β§ π΅ β β) β
((intβ(topGenβran (,)))β(π΄[,]π΅)) = (π΄(,)π΅)) |
57 | 1, 2, 56 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ (π β
((intβ(topGenβran (,)))β(π΄[,]π΅)) = (π΄(,)π΅)) |
58 | 47, 49, 53, 55, 54, 57 | dvmptntr 25488 |
. . . . . . . . . . . . 13
β’ (π β (β D (π’ β (π΄[,]π΅) β¦ -(πΉβπ’))) = (β D (π’ β (π΄(,)π΅) β¦ -(πΉβπ’)))) |
59 | | reelprrecn 11202 |
. . . . . . . . . . . . . . 15
β’ β
β {β, β} |
60 | 59 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (π β β β {β,
β}) |
61 | | ioossicc 13410 |
. . . . . . . . . . . . . . . 16
β’ (π΄(,)π΅) β (π΄[,]π΅) |
62 | 61 | sseli 3979 |
. . . . . . . . . . . . . . 15
β’ (π’ β (π΄(,)π΅) β π’ β (π΄[,]π΅)) |
63 | 62, 52 | sylan2 594 |
. . . . . . . . . . . . . 14
β’ ((π β§ π’ β (π΄(,)π΅)) β (πΉβπ’) β β) |
64 | | fvexd 6907 |
. . . . . . . . . . . . . 14
β’ ((π β§ π’ β (π΄(,)π΅)) β ((β D πΉ)βπ’) β V) |
65 | 31 | feqmptd 6961 |
. . . . . . . . . . . . . . . 16
β’ (π β πΉ = (π’ β (π΄[,]π΅) β¦ (πΉβπ’))) |
66 | 65 | oveq2d 7425 |
. . . . . . . . . . . . . . 15
β’ (π β (β D πΉ) = (β D (π’ β (π΄[,]π΅) β¦ (πΉβπ’)))) |
67 | | dvf 25424 |
. . . . . . . . . . . . . . . . 17
β’ (β
D πΉ):dom (β D πΉ)βΆβ |
68 | 14 | feq2d 6704 |
. . . . . . . . . . . . . . . . 17
β’ (π β ((β D πΉ):dom (β D πΉ)βΆβ β (β
D πΉ):(π΄(,)π΅)βΆβ)) |
69 | 67, 68 | mpbii 232 |
. . . . . . . . . . . . . . . 16
β’ (π β (β D πΉ):(π΄(,)π΅)βΆβ) |
70 | 69 | feqmptd 6961 |
. . . . . . . . . . . . . . 15
β’ (π β (β D πΉ) = (π’ β (π΄(,)π΅) β¦ ((β D πΉ)βπ’))) |
71 | 47, 49, 52, 55, 54, 57 | dvmptntr 25488 |
. . . . . . . . . . . . . . 15
β’ (π β (β D (π’ β (π΄[,]π΅) β¦ (πΉβπ’))) = (β D (π’ β (π΄(,)π΅) β¦ (πΉβπ’)))) |
72 | 66, 70, 71 | 3eqtr3rd 2782 |
. . . . . . . . . . . . . 14
β’ (π β (β D (π’ β (π΄(,)π΅) β¦ (πΉβπ’))) = (π’ β (π΄(,)π΅) β¦ ((β D πΉ)βπ’))) |
73 | 60, 63, 64, 72 | dvmptneg 25483 |
. . . . . . . . . . . . 13
β’ (π β (β D (π’ β (π΄(,)π΅) β¦ -(πΉβπ’))) = (π’ β (π΄(,)π΅) β¦ -((β D πΉ)βπ’))) |
74 | 58, 73 | eqtrd 2773 |
. . . . . . . . . . . 12
β’ (π β (β D (π’ β (π΄[,]π΅) β¦ -(πΉβπ’))) = (π’ β (π΄(,)π΅) β¦ -((β D πΉ)βπ’))) |
75 | 74 | dmeqd 5906 |
. . . . . . . . . . 11
β’ (π β dom (β D (π’ β (π΄[,]π΅) β¦ -(πΉβπ’))) = dom (π’ β (π΄(,)π΅) β¦ -((β D πΉ)βπ’))) |
76 | | dmmptg 6242 |
. . . . . . . . . . . 12
β’
(βπ’ β
(π΄(,)π΅)-((β D πΉ)βπ’) β V β dom (π’ β (π΄(,)π΅) β¦ -((β D πΉ)βπ’)) = (π΄(,)π΅)) |
77 | | negex 11458 |
. . . . . . . . . . . . 13
β’
-((β D πΉ)βπ’) β V |
78 | 77 | a1i 11 |
. . . . . . . . . . . 12
β’ (π’ β (π΄(,)π΅) β -((β D πΉ)βπ’) β V) |
79 | 76, 78 | mprg 3068 |
. . . . . . . . . . 11
β’ dom
(π’ β (π΄(,)π΅) β¦ -((β D πΉ)βπ’)) = (π΄(,)π΅) |
80 | 75, 79 | eqtrdi 2789 |
. . . . . . . . . 10
β’ (π β dom (β D (π’ β (π΄[,]π΅) β¦ -(πΉβπ’))) = (π΄(,)π΅)) |
81 | 80 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ (π’ β (π΄[,]π΅) β§ π£ β (π΄[,]π΅))) β§ (βπ¦ β (π΄[,]π΅)((πΉβπ¦) β€ (πΉβπ’) β§ (πΉβπ£) β€ (πΉβπ¦)) β§ Β¬ π£ β {π΄, π΅})) β dom (β D (π’ β (π΄[,]π΅) β¦ -(πΉβπ’))) = (π΄(,)π΅)) |
82 | | simpr 486 |
. . . . . . . . . . . . . 14
β’ (((πΉβπ¦) β€ (πΉβπ’) β§ (πΉβπ£) β€ (πΉβπ¦)) β (πΉβπ£) β€ (πΉβπ¦)) |
83 | 31 | ad2antrr 725 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π’ β (π΄[,]π΅) β§ π£ β (π΄[,]π΅))) β§ π¦ β (π΄[,]π΅)) β πΉ:(π΄[,]π΅)βΆβ) |
84 | | simplrr 777 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π’ β (π΄[,]π΅) β§ π£ β (π΄[,]π΅))) β§ π¦ β (π΄[,]π΅)) β π£ β (π΄[,]π΅)) |
85 | 83, 84 | ffvelcdmd 7088 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π’ β (π΄[,]π΅) β§ π£ β (π΄[,]π΅))) β§ π¦ β (π΄[,]π΅)) β (πΉβπ£) β β) |
86 | 31 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ (π’ β (π΄[,]π΅) β§ π£ β (π΄[,]π΅))) β πΉ:(π΄[,]π΅)βΆβ) |
87 | 86 | ffvelcdmda 7087 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π’ β (π΄[,]π΅) β§ π£ β (π΄[,]π΅))) β§ π¦ β (π΄[,]π΅)) β (πΉβπ¦) β β) |
88 | 85, 87 | lenegd 11793 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π’ β (π΄[,]π΅) β§ π£ β (π΄[,]π΅))) β§ π¦ β (π΄[,]π΅)) β ((πΉβπ£) β€ (πΉβπ¦) β -(πΉβπ¦) β€ -(πΉβπ£))) |
89 | | fveq2 6892 |
. . . . . . . . . . . . . . . . . . 19
β’ (π’ = π¦ β (πΉβπ’) = (πΉβπ¦)) |
90 | 89 | negeqd 11454 |
. . . . . . . . . . . . . . . . . 18
β’ (π’ = π¦ β -(πΉβπ’) = -(πΉβπ¦)) |
91 | | negex 11458 |
. . . . . . . . . . . . . . . . . 18
β’ -(πΉβπ¦) β V |
92 | 90, 40, 91 | fvmpt 6999 |
. . . . . . . . . . . . . . . . 17
β’ (π¦ β (π΄[,]π΅) β ((π’ β (π΄[,]π΅) β¦ -(πΉβπ’))βπ¦) = -(πΉβπ¦)) |
93 | 92 | adantl 483 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π’ β (π΄[,]π΅) β§ π£ β (π΄[,]π΅))) β§ π¦ β (π΄[,]π΅)) β ((π’ β (π΄[,]π΅) β¦ -(πΉβπ’))βπ¦) = -(πΉβπ¦)) |
94 | | fveq2 6892 |
. . . . . . . . . . . . . . . . . . 19
β’ (π’ = π£ β (πΉβπ’) = (πΉβπ£)) |
95 | 94 | negeqd 11454 |
. . . . . . . . . . . . . . . . . 18
β’ (π’ = π£ β -(πΉβπ’) = -(πΉβπ£)) |
96 | | negex 11458 |
. . . . . . . . . . . . . . . . . 18
β’ -(πΉβπ£) β V |
97 | 95, 40, 96 | fvmpt 6999 |
. . . . . . . . . . . . . . . . 17
β’ (π£ β (π΄[,]π΅) β ((π’ β (π΄[,]π΅) β¦ -(πΉβπ’))βπ£) = -(πΉβπ£)) |
98 | 84, 97 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π’ β (π΄[,]π΅) β§ π£ β (π΄[,]π΅))) β§ π¦ β (π΄[,]π΅)) β ((π’ β (π΄[,]π΅) β¦ -(πΉβπ’))βπ£) = -(πΉβπ£)) |
99 | 93, 98 | breq12d 5162 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π’ β (π΄[,]π΅) β§ π£ β (π΄[,]π΅))) β§ π¦ β (π΄[,]π΅)) β (((π’ β (π΄[,]π΅) β¦ -(πΉβπ’))βπ¦) β€ ((π’ β (π΄[,]π΅) β¦ -(πΉβπ’))βπ£) β -(πΉβπ¦) β€ -(πΉβπ£))) |
100 | 88, 99 | bitr4d 282 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π’ β (π΄[,]π΅) β§ π£ β (π΄[,]π΅))) β§ π¦ β (π΄[,]π΅)) β ((πΉβπ£) β€ (πΉβπ¦) β ((π’ β (π΄[,]π΅) β¦ -(πΉβπ’))βπ¦) β€ ((π’ β (π΄[,]π΅) β¦ -(πΉβπ’))βπ£))) |
101 | 82, 100 | imbitrid 243 |
. . . . . . . . . . . . 13
β’ (((π β§ (π’ β (π΄[,]π΅) β§ π£ β (π΄[,]π΅))) β§ π¦ β (π΄[,]π΅)) β (((πΉβπ¦) β€ (πΉβπ’) β§ (πΉβπ£) β€ (πΉβπ¦)) β ((π’ β (π΄[,]π΅) β¦ -(πΉβπ’))βπ¦) β€ ((π’ β (π΄[,]π΅) β¦ -(πΉβπ’))βπ£))) |
102 | 101 | ralimdva 3168 |
. . . . . . . . . . . 12
β’ ((π β§ (π’ β (π΄[,]π΅) β§ π£ β (π΄[,]π΅))) β (βπ¦ β (π΄[,]π΅)((πΉβπ¦) β€ (πΉβπ’) β§ (πΉβπ£) β€ (πΉβπ¦)) β βπ¦ β (π΄[,]π΅)((π’ β (π΄[,]π΅) β¦ -(πΉβπ’))βπ¦) β€ ((π’ β (π΄[,]π΅) β¦ -(πΉβπ’))βπ£))) |
103 | 102 | imp 408 |
. . . . . . . . . . 11
β’ (((π β§ (π’ β (π΄[,]π΅) β§ π£ β (π΄[,]π΅))) β§ βπ¦ β (π΄[,]π΅)((πΉβπ¦) β€ (πΉβπ’) β§ (πΉβπ£) β€ (πΉβπ¦))) β βπ¦ β (π΄[,]π΅)((π’ β (π΄[,]π΅) β¦ -(πΉβπ’))βπ¦) β€ ((π’ β (π΄[,]π΅) β¦ -(πΉβπ’))βπ£)) |
104 | | fveq2 6892 |
. . . . . . . . . . . . 13
β’ (π¦ = π‘ β ((π’ β (π΄[,]π΅) β¦ -(πΉβπ’))βπ¦) = ((π’ β (π΄[,]π΅) β¦ -(πΉβπ’))βπ‘)) |
105 | 104 | breq1d 5159 |
. . . . . . . . . . . 12
β’ (π¦ = π‘ β (((π’ β (π΄[,]π΅) β¦ -(πΉβπ’))βπ¦) β€ ((π’ β (π΄[,]π΅) β¦ -(πΉβπ’))βπ£) β ((π’ β (π΄[,]π΅) β¦ -(πΉβπ’))βπ‘) β€ ((π’ β (π΄[,]π΅) β¦ -(πΉβπ’))βπ£))) |
106 | 105 | cbvralvw 3235 |
. . . . . . . . . . 11
β’
(βπ¦ β
(π΄[,]π΅)((π’ β (π΄[,]π΅) β¦ -(πΉβπ’))βπ¦) β€ ((π’ β (π΄[,]π΅) β¦ -(πΉβπ’))βπ£) β βπ‘ β (π΄[,]π΅)((π’ β (π΄[,]π΅) β¦ -(πΉβπ’))βπ‘) β€ ((π’ β (π΄[,]π΅) β¦ -(πΉβπ’))βπ£)) |
107 | 103, 106 | sylib 217 |
. . . . . . . . . 10
β’ (((π β§ (π’ β (π΄[,]π΅) β§ π£ β (π΄[,]π΅))) β§ βπ¦ β (π΄[,]π΅)((πΉβπ¦) β€ (πΉβπ’) β§ (πΉβπ£) β€ (πΉβπ¦))) β βπ‘ β (π΄[,]π΅)((π’ β (π΄[,]π΅) β¦ -(πΉβπ’))βπ‘) β€ ((π’ β (π΄[,]π΅) β¦ -(πΉβπ’))βπ£)) |
108 | 107 | adantrr 716 |
. . . . . . . . 9
β’ (((π β§ (π’ β (π΄[,]π΅) β§ π£ β (π΄[,]π΅))) β§ (βπ¦ β (π΄[,]π΅)((πΉβπ¦) β€ (πΉβπ’) β§ (πΉβπ£) β€ (πΉβπ¦)) β§ Β¬ π£ β {π΄, π΅})) β βπ‘ β (π΄[,]π΅)((π’ β (π΄[,]π΅) β¦ -(πΉβπ’))βπ‘) β€ ((π’ β (π΄[,]π΅) β¦ -(πΉβπ’))βπ£)) |
109 | | simplrr 777 |
. . . . . . . . 9
β’ (((π β§ (π’ β (π΄[,]π΅) β§ π£ β (π΄[,]π΅))) β§ (βπ¦ β (π΄[,]π΅)((πΉβπ¦) β€ (πΉβπ’) β§ (πΉβπ£) β€ (πΉβπ¦)) β§ Β¬ π£ β {π΄, π΅})) β π£ β (π΄[,]π΅)) |
110 | | simprr 772 |
. . . . . . . . 9
β’ (((π β§ (π’ β (π΄[,]π΅) β§ π£ β (π΄[,]π΅))) β§ (βπ¦ β (π΄[,]π΅)((πΉβπ¦) β€ (πΉβπ’) β§ (πΉβπ£) β€ (πΉβπ¦)) β§ Β¬ π£ β {π΄, π΅})) β Β¬ π£ β {π΄, π΅}) |
111 | 27, 28, 29, 46, 81, 108, 109, 110 | rollelem 25506 |
. . . . . . . 8
β’ (((π β§ (π’ β (π΄[,]π΅) β§ π£ β (π΄[,]π΅))) β§ (βπ¦ β (π΄[,]π΅)((πΉβπ¦) β€ (πΉβπ’) β§ (πΉβπ£) β€ (πΉβπ¦)) β§ Β¬ π£ β {π΄, π΅})) β βπ₯ β (π΄(,)π΅)((β D (π’ β (π΄[,]π΅) β¦ -(πΉβπ’)))βπ₯) = 0) |
112 | 74 | fveq1d 6894 |
. . . . . . . . . . . . 13
β’ (π β ((β D (π’ β (π΄[,]π΅) β¦ -(πΉβπ’)))βπ₯) = ((π’ β (π΄(,)π΅) β¦ -((β D πΉ)βπ’))βπ₯)) |
113 | | fveq2 6892 |
. . . . . . . . . . . . . . 15
β’ (π’ = π₯ β ((β D πΉ)βπ’) = ((β D πΉ)βπ₯)) |
114 | 113 | negeqd 11454 |
. . . . . . . . . . . . . 14
β’ (π’ = π₯ β -((β D πΉ)βπ’) = -((β D πΉ)βπ₯)) |
115 | | eqid 2733 |
. . . . . . . . . . . . . 14
β’ (π’ β (π΄(,)π΅) β¦ -((β D πΉ)βπ’)) = (π’ β (π΄(,)π΅) β¦ -((β D πΉ)βπ’)) |
116 | | negex 11458 |
. . . . . . . . . . . . . 14
β’
-((β D πΉ)βπ₯) β V |
117 | 114, 115,
116 | fvmpt 6999 |
. . . . . . . . . . . . 13
β’ (π₯ β (π΄(,)π΅) β ((π’ β (π΄(,)π΅) β¦ -((β D πΉ)βπ’))βπ₯) = -((β D πΉ)βπ₯)) |
118 | 112, 117 | sylan9eq 2793 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β (π΄(,)π΅)) β ((β D (π’ β (π΄[,]π΅) β¦ -(πΉβπ’)))βπ₯) = -((β D πΉ)βπ₯)) |
119 | 118 | eqeq1d 2735 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β (π΄(,)π΅)) β (((β D (π’ β (π΄[,]π΅) β¦ -(πΉβπ’)))βπ₯) = 0 β -((β D πΉ)βπ₯) = 0)) |
120 | 14 | eleq2d 2820 |
. . . . . . . . . . . . . 14
β’ (π β (π₯ β dom (β D πΉ) β π₯ β (π΄(,)π΅))) |
121 | 120 | biimpar 479 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β (π΄(,)π΅)) β π₯ β dom (β D πΉ)) |
122 | 67 | ffvelcdmi 7086 |
. . . . . . . . . . . . 13
β’ (π₯ β dom (β D πΉ) β ((β D πΉ)βπ₯) β β) |
123 | 121, 122 | syl 17 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β (π΄(,)π΅)) β ((β D πΉ)βπ₯) β β) |
124 | 123 | negeq0d 11563 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β (π΄(,)π΅)) β (((β D πΉ)βπ₯) = 0 β -((β D πΉ)βπ₯) = 0)) |
125 | 119, 124 | bitr4d 282 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (π΄(,)π΅)) β (((β D (π’ β (π΄[,]π΅) β¦ -(πΉβπ’)))βπ₯) = 0 β ((β D πΉ)βπ₯) = 0)) |
126 | 125 | rexbidva 3177 |
. . . . . . . . 9
β’ (π β (βπ₯ β (π΄(,)π΅)((β D (π’ β (π΄[,]π΅) β¦ -(πΉβπ’)))βπ₯) = 0 β βπ₯ β (π΄(,)π΅)((β D πΉ)βπ₯) = 0)) |
127 | 126 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ (π’ β (π΄[,]π΅) β§ π£ β (π΄[,]π΅))) β§ (βπ¦ β (π΄[,]π΅)((πΉβπ¦) β€ (πΉβπ’) β§ (πΉβπ£) β€ (πΉβπ¦)) β§ Β¬ π£ β {π΄, π΅})) β (βπ₯ β (π΄(,)π΅)((β D (π’ β (π΄[,]π΅) β¦ -(πΉβπ’)))βπ₯) = 0 β βπ₯ β (π΄(,)π΅)((β D πΉ)βπ₯) = 0)) |
128 | 111, 127 | mpbid 231 |
. . . . . . 7
β’ (((π β§ (π’ β (π΄[,]π΅) β§ π£ β (π΄[,]π΅))) β§ (βπ¦ β (π΄[,]π΅)((πΉβπ¦) β€ (πΉβπ’) β§ (πΉβπ£) β€ (πΉβπ¦)) β§ Β¬ π£ β {π΄, π΅})) β βπ₯ β (π΄(,)π΅)((β D πΉ)βπ₯) = 0) |
129 | 128 | expr 458 |
. . . . . 6
β’ (((π β§ (π’ β (π΄[,]π΅) β§ π£ β (π΄[,]π΅))) β§ βπ¦ β (π΄[,]π΅)((πΉβπ¦) β€ (πΉβπ’) β§ (πΉβπ£) β€ (πΉβπ¦))) β (Β¬ π£ β {π΄, π΅} β βπ₯ β (π΄(,)π΅)((β D πΉ)βπ₯) = 0)) |
130 | | vex 3479 |
. . . . . . . . . . 11
β’ π’ β V |
131 | 130 | elpr 4652 |
. . . . . . . . . 10
β’ (π’ β {π΄, π΅} β (π’ = π΄ β¨ π’ = π΅)) |
132 | | fveq2 6892 |
. . . . . . . . . . . 12
β’ (π’ = π΄ β (πΉβπ’) = (πΉβπ΄)) |
133 | 132 | a1i 11 |
. . . . . . . . . . 11
β’ (π β (π’ = π΄ β (πΉβπ’) = (πΉβπ΄))) |
134 | | rolle.e |
. . . . . . . . . . . . 13
β’ (π β (πΉβπ΄) = (πΉβπ΅)) |
135 | 134 | eqcomd 2739 |
. . . . . . . . . . . 12
β’ (π β (πΉβπ΅) = (πΉβπ΄)) |
136 | | fveqeq2 6901 |
. . . . . . . . . . . 12
β’ (π’ = π΅ β ((πΉβπ’) = (πΉβπ΄) β (πΉβπ΅) = (πΉβπ΄))) |
137 | 135, 136 | syl5ibrcom 246 |
. . . . . . . . . . 11
β’ (π β (π’ = π΅ β (πΉβπ’) = (πΉβπ΄))) |
138 | 133, 137 | jaod 858 |
. . . . . . . . . 10
β’ (π β ((π’ = π΄ β¨ π’ = π΅) β (πΉβπ’) = (πΉβπ΄))) |
139 | 131, 138 | biimtrid 241 |
. . . . . . . . 9
β’ (π β (π’ β {π΄, π΅} β (πΉβπ’) = (πΉβπ΄))) |
140 | | eleq1w 2817 |
. . . . . . . . . . . 12
β’ (π’ = π£ β (π’ β {π΄, π΅} β π£ β {π΄, π΅})) |
141 | | fveqeq2 6901 |
. . . . . . . . . . . 12
β’ (π’ = π£ β ((πΉβπ’) = (πΉβπ΄) β (πΉβπ£) = (πΉβπ΄))) |
142 | 140, 141 | imbi12d 345 |
. . . . . . . . . . 11
β’ (π’ = π£ β ((π’ β {π΄, π΅} β (πΉβπ’) = (πΉβπ΄)) β (π£ β {π΄, π΅} β (πΉβπ£) = (πΉβπ΄)))) |
143 | 142 | imbi2d 341 |
. . . . . . . . . 10
β’ (π’ = π£ β ((π β (π’ β {π΄, π΅} β (πΉβπ’) = (πΉβπ΄))) β (π β (π£ β {π΄, π΅} β (πΉβπ£) = (πΉβπ΄))))) |
144 | 143, 139 | chvarvv 2003 |
. . . . . . . . 9
β’ (π β (π£ β {π΄, π΅} β (πΉβπ£) = (πΉβπ΄))) |
145 | 139, 144 | anim12d 610 |
. . . . . . . 8
β’ (π β ((π’ β {π΄, π΅} β§ π£ β {π΄, π΅}) β ((πΉβπ’) = (πΉβπ΄) β§ (πΉβπ£) = (πΉβπ΄)))) |
146 | 145 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ (π’ β (π΄[,]π΅) β§ π£ β (π΄[,]π΅))) β§ βπ¦ β (π΄[,]π΅)((πΉβπ¦) β€ (πΉβπ’) β§ (πΉβπ£) β€ (πΉβπ¦))) β ((π’ β {π΄, π΅} β§ π£ β {π΄, π΅}) β ((πΉβπ’) = (πΉβπ΄) β§ (πΉβπ£) = (πΉβπ΄)))) |
147 | 1 | rexrd 11264 |
. . . . . . . . . . . . . . . . 17
β’ (π β π΄ β
β*) |
148 | 2 | rexrd 11264 |
. . . . . . . . . . . . . . . . 17
β’ (π β π΅ β
β*) |
149 | | lbicc2 13441 |
. . . . . . . . . . . . . . . . 17
β’ ((π΄ β β*
β§ π΅ β
β* β§ π΄
β€ π΅) β π΄ β (π΄[,]π΅)) |
150 | 147, 148,
4, 149 | syl3anc 1372 |
. . . . . . . . . . . . . . . 16
β’ (π β π΄ β (π΄[,]π΅)) |
151 | 31, 150 | ffvelcdmd 7088 |
. . . . . . . . . . . . . . 15
β’ (π β (πΉβπ΄) β β) |
152 | 151 | ad2antrr 725 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π’ β (π΄[,]π΅) β§ π£ β (π΄[,]π΅))) β§ π¦ β (π΄[,]π΅)) β (πΉβπ΄) β β) |
153 | 87, 152 | letri3d 11356 |
. . . . . . . . . . . . 13
β’ (((π β§ (π’ β (π΄[,]π΅) β§ π£ β (π΄[,]π΅))) β§ π¦ β (π΄[,]π΅)) β ((πΉβπ¦) = (πΉβπ΄) β ((πΉβπ¦) β€ (πΉβπ΄) β§ (πΉβπ΄) β€ (πΉβπ¦)))) |
154 | | breq2 5153 |
. . . . . . . . . . . . . . 15
β’ ((πΉβπ’) = (πΉβπ΄) β ((πΉβπ¦) β€ (πΉβπ’) β (πΉβπ¦) β€ (πΉβπ΄))) |
155 | | breq1 5152 |
. . . . . . . . . . . . . . 15
β’ ((πΉβπ£) = (πΉβπ΄) β ((πΉβπ£) β€ (πΉβπ¦) β (πΉβπ΄) β€ (πΉβπ¦))) |
156 | 154, 155 | bi2anan9 638 |
. . . . . . . . . . . . . 14
β’ (((πΉβπ’) = (πΉβπ΄) β§ (πΉβπ£) = (πΉβπ΄)) β (((πΉβπ¦) β€ (πΉβπ’) β§ (πΉβπ£) β€ (πΉβπ¦)) β ((πΉβπ¦) β€ (πΉβπ΄) β§ (πΉβπ΄) β€ (πΉβπ¦)))) |
157 | 156 | bibi2d 343 |
. . . . . . . . . . . . 13
β’ (((πΉβπ’) = (πΉβπ΄) β§ (πΉβπ£) = (πΉβπ΄)) β (((πΉβπ¦) = (πΉβπ΄) β ((πΉβπ¦) β€ (πΉβπ’) β§ (πΉβπ£) β€ (πΉβπ¦))) β ((πΉβπ¦) = (πΉβπ΄) β ((πΉβπ¦) β€ (πΉβπ΄) β§ (πΉβπ΄) β€ (πΉβπ¦))))) |
158 | 153, 157 | syl5ibrcom 246 |
. . . . . . . . . . . 12
β’ (((π β§ (π’ β (π΄[,]π΅) β§ π£ β (π΄[,]π΅))) β§ π¦ β (π΄[,]π΅)) β (((πΉβπ’) = (πΉβπ΄) β§ (πΉβπ£) = (πΉβπ΄)) β ((πΉβπ¦) = (πΉβπ΄) β ((πΉβπ¦) β€ (πΉβπ’) β§ (πΉβπ£) β€ (πΉβπ¦))))) |
159 | 158 | impancom 453 |
. . . . . . . . . . 11
β’ (((π β§ (π’ β (π΄[,]π΅) β§ π£ β (π΄[,]π΅))) β§ ((πΉβπ’) = (πΉβπ΄) β§ (πΉβπ£) = (πΉβπ΄))) β (π¦ β (π΄[,]π΅) β ((πΉβπ¦) = (πΉβπ΄) β ((πΉβπ¦) β€ (πΉβπ’) β§ (πΉβπ£) β€ (πΉβπ¦))))) |
160 | 159 | imp 408 |
. . . . . . . . . 10
β’ ((((π β§ (π’ β (π΄[,]π΅) β§ π£ β (π΄[,]π΅))) β§ ((πΉβπ’) = (πΉβπ΄) β§ (πΉβπ£) = (πΉβπ΄))) β§ π¦ β (π΄[,]π΅)) β ((πΉβπ¦) = (πΉβπ΄) β ((πΉβπ¦) β€ (πΉβπ’) β§ (πΉβπ£) β€ (πΉβπ¦)))) |
161 | 160 | ralbidva 3176 |
. . . . . . . . 9
β’ (((π β§ (π’ β (π΄[,]π΅) β§ π£ β (π΄[,]π΅))) β§ ((πΉβπ’) = (πΉβπ΄) β§ (πΉβπ£) = (πΉβπ΄))) β (βπ¦ β (π΄[,]π΅)(πΉβπ¦) = (πΉβπ΄) β βπ¦ β (π΄[,]π΅)((πΉβπ¦) β€ (πΉβπ’) β§ (πΉβπ£) β€ (πΉβπ¦)))) |
162 | 31 | ffnd 6719 |
. . . . . . . . . . . . 13
β’ (π β πΉ Fn (π΄[,]π΅)) |
163 | | fnconstg 6780 |
. . . . . . . . . . . . . 14
β’ ((πΉβπ΄) β β β ((π΄[,]π΅) Γ {(πΉβπ΄)}) Fn (π΄[,]π΅)) |
164 | 151, 163 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β ((π΄[,]π΅) Γ {(πΉβπ΄)}) Fn (π΄[,]π΅)) |
165 | | eqfnfv 7033 |
. . . . . . . . . . . . 13
β’ ((πΉ Fn (π΄[,]π΅) β§ ((π΄[,]π΅) Γ {(πΉβπ΄)}) Fn (π΄[,]π΅)) β (πΉ = ((π΄[,]π΅) Γ {(πΉβπ΄)}) β βπ¦ β (π΄[,]π΅)(πΉβπ¦) = (((π΄[,]π΅) Γ {(πΉβπ΄)})βπ¦))) |
166 | 162, 164,
165 | syl2anc 585 |
. . . . . . . . . . . 12
β’ (π β (πΉ = ((π΄[,]π΅) Γ {(πΉβπ΄)}) β βπ¦ β (π΄[,]π΅)(πΉβπ¦) = (((π΄[,]π΅) Γ {(πΉβπ΄)})βπ¦))) |
167 | | fvex 6905 |
. . . . . . . . . . . . . . 15
β’ (πΉβπ΄) β V |
168 | 167 | fvconst2 7205 |
. . . . . . . . . . . . . 14
β’ (π¦ β (π΄[,]π΅) β (((π΄[,]π΅) Γ {(πΉβπ΄)})βπ¦) = (πΉβπ΄)) |
169 | 168 | eqeq2d 2744 |
. . . . . . . . . . . . 13
β’ (π¦ β (π΄[,]π΅) β ((πΉβπ¦) = (((π΄[,]π΅) Γ {(πΉβπ΄)})βπ¦) β (πΉβπ¦) = (πΉβπ΄))) |
170 | 169 | ralbiia 3092 |
. . . . . . . . . . . 12
β’
(βπ¦ β
(π΄[,]π΅)(πΉβπ¦) = (((π΄[,]π΅) Γ {(πΉβπ΄)})βπ¦) β βπ¦ β (π΄[,]π΅)(πΉβπ¦) = (πΉβπ΄)) |
171 | 166, 170 | bitrdi 287 |
. . . . . . . . . . 11
β’ (π β (πΉ = ((π΄[,]π΅) Γ {(πΉβπ΄)}) β βπ¦ β (π΄[,]π΅)(πΉβπ¦) = (πΉβπ΄))) |
172 | | ioon0 13350 |
. . . . . . . . . . . . . . 15
β’ ((π΄ β β*
β§ π΅ β
β*) β ((π΄(,)π΅) β β
β π΄ < π΅)) |
173 | 147, 148,
172 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ (π β ((π΄(,)π΅) β β
β π΄ < π΅)) |
174 | 3, 173 | mpbird 257 |
. . . . . . . . . . . . 13
β’ (π β (π΄(,)π΅) β β
) |
175 | | fconstmpt 5739 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π΄[,]π΅) Γ {(πΉβπ΄)}) = (π’ β (π΄[,]π΅) β¦ (πΉβπ΄)) |
176 | 175 | eqeq2i 2746 |
. . . . . . . . . . . . . . . . . . 19
β’ (πΉ = ((π΄[,]π΅) Γ {(πΉβπ΄)}) β πΉ = (π’ β (π΄[,]π΅) β¦ (πΉβπ΄))) |
177 | 176 | biimpi 215 |
. . . . . . . . . . . . . . . . . 18
β’ (πΉ = ((π΄[,]π΅) Γ {(πΉβπ΄)}) β πΉ = (π’ β (π΄[,]π΅) β¦ (πΉβπ΄))) |
178 | 177 | oveq2d 7425 |
. . . . . . . . . . . . . . . . 17
β’ (πΉ = ((π΄[,]π΅) Γ {(πΉβπ΄)}) β (β D πΉ) = (β D (π’ β (π΄[,]π΅) β¦ (πΉβπ΄)))) |
179 | 151 | recnd 11242 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (πΉβπ΄) β β) |
180 | 179 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π’ β β) β (πΉβπ΄) β β) |
181 | | 0cnd 11207 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π’ β β) β 0 β
β) |
182 | 60, 179 | dvmptc 25475 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (β D (π’ β β β¦ (πΉβπ΄))) = (π’ β β β¦ 0)) |
183 | 60, 180, 181, 182, 49, 55, 54, 57 | dvmptres2 25479 |
. . . . . . . . . . . . . . . . 17
β’ (π β (β D (π’ β (π΄[,]π΅) β¦ (πΉβπ΄))) = (π’ β (π΄(,)π΅) β¦ 0)) |
184 | 178, 183 | sylan9eqr 2795 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ πΉ = ((π΄[,]π΅) Γ {(πΉβπ΄)})) β (β D πΉ) = (π’ β (π΄(,)π΅) β¦ 0)) |
185 | 184 | fveq1d 6894 |
. . . . . . . . . . . . . . 15
β’ ((π β§ πΉ = ((π΄[,]π΅) Γ {(πΉβπ΄)})) β ((β D πΉ)βπ₯) = ((π’ β (π΄(,)π΅) β¦ 0)βπ₯)) |
186 | | eqidd 2734 |
. . . . . . . . . . . . . . . 16
β’ (π’ = π₯ β 0 = 0) |
187 | | eqid 2733 |
. . . . . . . . . . . . . . . 16
β’ (π’ β (π΄(,)π΅) β¦ 0) = (π’ β (π΄(,)π΅) β¦ 0) |
188 | | c0ex 11208 |
. . . . . . . . . . . . . . . 16
β’ 0 β
V |
189 | 186, 187,
188 | fvmpt 6999 |
. . . . . . . . . . . . . . 15
β’ (π₯ β (π΄(,)π΅) β ((π’ β (π΄(,)π΅) β¦ 0)βπ₯) = 0) |
190 | 185, 189 | sylan9eq 2793 |
. . . . . . . . . . . . . 14
β’ (((π β§ πΉ = ((π΄[,]π΅) Γ {(πΉβπ΄)})) β§ π₯ β (π΄(,)π΅)) β ((β D πΉ)βπ₯) = 0) |
191 | 190 | ralrimiva 3147 |
. . . . . . . . . . . . 13
β’ ((π β§ πΉ = ((π΄[,]π΅) Γ {(πΉβπ΄)})) β βπ₯ β (π΄(,)π΅)((β D πΉ)βπ₯) = 0) |
192 | | r19.2z 4495 |
. . . . . . . . . . . . 13
β’ (((π΄(,)π΅) β β
β§ βπ₯ β (π΄(,)π΅)((β D πΉ)βπ₯) = 0) β βπ₯ β (π΄(,)π΅)((β D πΉ)βπ₯) = 0) |
193 | 174, 191,
192 | syl2an2r 684 |
. . . . . . . . . . . 12
β’ ((π β§ πΉ = ((π΄[,]π΅) Γ {(πΉβπ΄)})) β βπ₯ β (π΄(,)π΅)((β D πΉ)βπ₯) = 0) |
194 | 193 | ex 414 |
. . . . . . . . . . 11
β’ (π β (πΉ = ((π΄[,]π΅) Γ {(πΉβπ΄)}) β βπ₯ β (π΄(,)π΅)((β D πΉ)βπ₯) = 0)) |
195 | 171, 194 | sylbird 260 |
. . . . . . . . . 10
β’ (π β (βπ¦ β (π΄[,]π΅)(πΉβπ¦) = (πΉβπ΄) β βπ₯ β (π΄(,)π΅)((β D πΉ)βπ₯) = 0)) |
196 | 195 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ (π’ β (π΄[,]π΅) β§ π£ β (π΄[,]π΅))) β§ ((πΉβπ’) = (πΉβπ΄) β§ (πΉβπ£) = (πΉβπ΄))) β (βπ¦ β (π΄[,]π΅)(πΉβπ¦) = (πΉβπ΄) β βπ₯ β (π΄(,)π΅)((β D πΉ)βπ₯) = 0)) |
197 | 161, 196 | sylbird 260 |
. . . . . . . 8
β’ (((π β§ (π’ β (π΄[,]π΅) β§ π£ β (π΄[,]π΅))) β§ ((πΉβπ’) = (πΉβπ΄) β§ (πΉβπ£) = (πΉβπ΄))) β (βπ¦ β (π΄[,]π΅)((πΉβπ¦) β€ (πΉβπ’) β§ (πΉβπ£) β€ (πΉβπ¦)) β βπ₯ β (π΄(,)π΅)((β D πΉ)βπ₯) = 0)) |
198 | 197 | impancom 453 |
. . . . . . 7
β’ (((π β§ (π’ β (π΄[,]π΅) β§ π£ β (π΄[,]π΅))) β§ βπ¦ β (π΄[,]π΅)((πΉβπ¦) β€ (πΉβπ’) β§ (πΉβπ£) β€ (πΉβπ¦))) β (((πΉβπ’) = (πΉβπ΄) β§ (πΉβπ£) = (πΉβπ΄)) β βπ₯ β (π΄(,)π΅)((β D πΉ)βπ₯) = 0)) |
199 | 146, 198 | syld 47 |
. . . . . 6
β’ (((π β§ (π’ β (π΄[,]π΅) β§ π£ β (π΄[,]π΅))) β§ βπ¦ β (π΄[,]π΅)((πΉβπ¦) β€ (πΉβπ’) β§ (πΉβπ£) β€ (πΉβπ¦))) β ((π’ β {π΄, π΅} β§ π£ β {π΄, π΅}) β βπ₯ β (π΄(,)π΅)((β D πΉ)βπ₯) = 0)) |
200 | 26, 129, 199 | ecased 1034 |
. . . . 5
β’ (((π β§ (π’ β (π΄[,]π΅) β§ π£ β (π΄[,]π΅))) β§ βπ¦ β (π΄[,]π΅)((πΉβπ¦) β€ (πΉβπ’) β§ (πΉβπ£) β€ (πΉβπ¦))) β βπ₯ β (π΄(,)π΅)((β D πΉ)βπ₯) = 0) |
201 | 200 | ex 414 |
. . . 4
β’ ((π β§ (π’ β (π΄[,]π΅) β§ π£ β (π΄[,]π΅))) β (βπ¦ β (π΄[,]π΅)((πΉβπ¦) β€ (πΉβπ’) β§ (πΉβπ£) β€ (πΉβπ¦)) β βπ₯ β (π΄(,)π΅)((β D πΉ)βπ₯) = 0)) |
202 | 9, 201 | biimtrrid 242 |
. . 3
β’ ((π β§ (π’ β (π΄[,]π΅) β§ π£ β (π΄[,]π΅))) β ((βπ¦ β (π΄[,]π΅)(πΉβπ¦) β€ (πΉβπ’) β§ βπ¦ β (π΄[,]π΅)(πΉβπ£) β€ (πΉβπ¦)) β βπ₯ β (π΄(,)π΅)((β D πΉ)βπ₯) = 0)) |
203 | 202 | rexlimdvva 3212 |
. 2
β’ (π β (βπ’ β (π΄[,]π΅)βπ£ β (π΄[,]π΅)(βπ¦ β (π΄[,]π΅)(πΉβπ¦) β€ (πΉβπ’) β§ βπ¦ β (π΄[,]π΅)(πΉβπ£) β€ (πΉβπ¦)) β βπ₯ β (π΄(,)π΅)((β D πΉ)βπ₯) = 0)) |
204 | 8, 203 | mpd 15 |
1
β’ (π β βπ₯ β (π΄(,)π΅)((β D πΉ)βπ₯) = 0) |