Step | Hyp | Ref
| Expression |
1 | | hspmbllem2.i |
. . 3
β’ (π β ((voln*βπ)β(π΄ β© (πΎ(π»βπ)π))) β β) |
2 | | hspmbllem2.f |
. . 3
β’ (π β ((voln*βπ)β(π΄ β (πΎ(π»βπ)π))) β β) |
3 | 1, 2 | readdcld 11142 |
. 2
β’ (π β (((voln*βπ)β(π΄ β© (πΎ(π»βπ)π))) + ((voln*βπ)β(π΄ β (πΎ(π»βπ)π)))) β β) |
4 | | hspmbllem2.r |
. . . 4
β’ (π β ((voln*βπ)βπ΄) β β) |
5 | | hspmbllem2.e |
. . . . 5
β’ (π β πΈ β
β+) |
6 | 5 | rpred 12911 |
. . . 4
β’ (π β πΈ β β) |
7 | 4, 6 | readdcld 11142 |
. . 3
β’ (π β (((voln*βπ)βπ΄) + πΈ) β β) |
8 | | nfv 1917 |
. . . 4
β’
β²ππ |
9 | | nnex 12117 |
. . . . 5
β’ β
β V |
10 | 9 | a1i 11 |
. . . 4
β’ (π β β β
V) |
11 | | icossicc 13307 |
. . . . 5
β’
(0[,)+β) β (0[,]+β) |
12 | | hspmbllem2.l |
. . . . . 6
β’ πΏ = (π₯ β Fin β¦ (π β (β βm π₯), π β (β βm π₯) β¦ if(π₯ = β
, 0, βπ β π₯ (volβ((πβπ)[,)(πβπ)))))) |
13 | | hspmbllem2.x |
. . . . . . 7
β’ (π β π β Fin) |
14 | 13 | adantr 481 |
. . . . . 6
β’ ((π β§ π β β) β π β Fin) |
15 | | hspmbllem2.c |
. . . . . . . 8
β’ (π β πΆ:ββΆ(β βm
π)) |
16 | 15 | ffvelcdmda 7031 |
. . . . . . 7
β’ ((π β§ π β β) β (πΆβπ) β (β βm π)) |
17 | | elmapi 8745 |
. . . . . . 7
β’ ((πΆβπ) β (β βm π) β (πΆβπ):πβΆβ) |
18 | 16, 17 | syl 17 |
. . . . . 6
β’ ((π β§ π β β) β (πΆβπ):πβΆβ) |
19 | | hspmbllem2.d |
. . . . . . . 8
β’ (π β π·:ββΆ(β βm
π)) |
20 | 19 | ffvelcdmda 7031 |
. . . . . . 7
β’ ((π β§ π β β) β (π·βπ) β (β βm π)) |
21 | | elmapi 8745 |
. . . . . . 7
β’ ((π·βπ) β (β βm π) β (π·βπ):πβΆβ) |
22 | 20, 21 | syl 17 |
. . . . . 6
β’ ((π β§ π β β) β (π·βπ):πβΆβ) |
23 | 12, 14, 18, 22 | hoidmvcl 44724 |
. . . . 5
β’ ((π β§ π β β) β ((πΆβπ)(πΏβπ)(π·βπ)) β (0[,)+β)) |
24 | 11, 23 | sselid 3940 |
. . . 4
β’ ((π β§ π β β) β ((πΆβπ)(πΏβπ)(π·βπ)) β (0[,]+β)) |
25 | 8, 10, 24 | sge0clmpt 44567 |
. . 3
β’ (π β
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) β (0[,]+β)) |
26 | | hspmbllem2.k |
. . . . . . . . 9
β’ (π β πΎ β π) |
27 | | ne0i 4292 |
. . . . . . . . 9
β’ (πΎ β π β π β β
) |
28 | 26, 27 | syl 17 |
. . . . . . . 8
β’ (π β π β β
) |
29 | 28 | adantr 481 |
. . . . . . 7
β’ ((π β§ π β β) β π β β
) |
30 | 12, 14, 29, 18, 22 | hoidmvn0val 44726 |
. . . . . 6
β’ ((π β§ π β β) β ((πΆβπ)(πΏβπ)(π·βπ)) = βπ β π (volβ(((πΆβπ)βπ)[,)((π·βπ)βπ)))) |
31 | 30 | mpteq2dva 5203 |
. . . . 5
β’ (π β (π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ))) = (π β β β¦ βπ β π (volβ(((πΆβπ)βπ)[,)((π·βπ)βπ))))) |
32 | 31 | fveq2d 6843 |
. . . 4
β’ (π β
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) =
(Ξ£^β(π β β β¦ βπ β π (volβ(((πΆβπ)βπ)[,)((π·βπ)βπ)))))) |
33 | | hspmbllem2.g |
. . . 4
β’ (π β
(Ξ£^β(π β β β¦ βπ β π (volβ(((πΆβπ)βπ)[,)((π·βπ)βπ))))) β€ (((voln*βπ)βπ΄) + πΈ)) |
34 | 32, 33 | eqbrtrd 5125 |
. . 3
β’ (π β
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) β€ (((voln*βπ)βπ΄) + πΈ)) |
35 | 7, 25, 34 | ge0lere 43671 |
. 2
β’ (π β
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) β β) |
36 | | hspmbllem2.t |
. . . . . . . . 9
β’ π = (π¦ β β β¦ (π β (β βm π) β¦ (β β π β¦ if(β β (π β {πΎ}), (πββ), if((πββ) β€ π¦, (πββ), π¦))))) |
37 | | hspmbllem2.y |
. . . . . . . . . 10
β’ (π β π β β) |
38 | 37 | adantr 481 |
. . . . . . . . 9
β’ ((π β§ π β β) β π β β) |
39 | 36, 38, 14, 22 | hsphoif 44718 |
. . . . . . . 8
β’ ((π β§ π β β) β ((πβπ)β(π·βπ)):πβΆβ) |
40 | 12, 14, 18, 39 | hoidmvcl 44724 |
. . . . . . 7
β’ ((π β§ π β β) β ((πΆβπ)(πΏβπ)((πβπ)β(π·βπ))) β (0[,)+β)) |
41 | 11, 40 | sselid 3940 |
. . . . . 6
β’ ((π β§ π β β) β ((πΆβπ)(πΏβπ)((πβπ)β(π·βπ))) β (0[,]+β)) |
42 | 8, 10, 41 | sge0clmpt 44567 |
. . . . 5
β’ (π β
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((πβπ)β(π·βπ))))) β (0[,]+β)) |
43 | | oveq2 7359 |
. . . . . . . . . . 11
β’ (π₯ = π¦ β (β βm π₯) = (β βm
π¦)) |
44 | | eqeq1 2741 |
. . . . . . . . . . . 12
β’ (π₯ = π¦ β (π₯ = β
β π¦ = β
)) |
45 | | prodeq1 15752 |
. . . . . . . . . . . 12
β’ (π₯ = π¦ β βπ β π₯ (volβ((πβπ)[,)(πβπ))) = βπ β π¦ (volβ((πβπ)[,)(πβπ)))) |
46 | 44, 45 | ifbieq2d 4510 |
. . . . . . . . . . 11
β’ (π₯ = π¦ β if(π₯ = β
, 0, βπ β π₯ (volβ((πβπ)[,)(πβπ)))) = if(π¦ = β
, 0, βπ β π¦ (volβ((πβπ)[,)(πβπ))))) |
47 | 43, 43, 46 | mpoeq123dv 7426 |
. . . . . . . . . 10
β’ (π₯ = π¦ β (π β (β βm π₯), π β (β βm π₯) β¦ if(π₯ = β
, 0, βπ β π₯ (volβ((πβπ)[,)(πβπ))))) = (π β (β βm π¦), π β (β βm π¦) β¦ if(π¦ = β
, 0, βπ β π¦ (volβ((πβπ)[,)(πβπ)))))) |
48 | 47 | cbvmptv 5216 |
. . . . . . . . 9
β’ (π₯ β Fin β¦ (π β (β
βm π₯),
π β (β
βm π₯)
β¦ if(π₯ = β
, 0,
βπ β π₯ (volβ((πβπ)[,)(πβπ)))))) = (π¦ β Fin β¦ (π β (β βm π¦), π β (β βm π¦) β¦ if(π¦ = β
, 0, βπ β π¦ (volβ((πβπ)[,)(πβπ)))))) |
49 | 12, 48 | eqtri 2765 |
. . . . . . . 8
β’ πΏ = (π¦ β Fin β¦ (π β (β βm π¦), π β (β βm π¦) β¦ if(π¦ = β
, 0, βπ β π¦ (volβ((πβπ)[,)(πβπ)))))) |
50 | | diffi 9081 |
. . . . . . . . . . 11
β’ (π β Fin β (π β {πΎ}) β Fin) |
51 | 13, 50 | syl 17 |
. . . . . . . . . 10
β’ (π β (π β {πΎ}) β Fin) |
52 | | snfi 8946 |
. . . . . . . . . . 11
β’ {πΎ} β Fin |
53 | 52 | a1i 11 |
. . . . . . . . . 10
β’ (π β {πΎ} β Fin) |
54 | | unfi 9074 |
. . . . . . . . . 10
β’ (((π β {πΎ}) β Fin β§ {πΎ} β Fin) β ((π β {πΎ}) βͺ {πΎ}) β Fin) |
55 | 51, 53, 54 | syl2anc 584 |
. . . . . . . . 9
β’ (π β ((π β {πΎ}) βͺ {πΎ}) β Fin) |
56 | 55 | adantr 481 |
. . . . . . . 8
β’ ((π β§ π β β) β ((π β {πΎ}) βͺ {πΎ}) β Fin) |
57 | | snidg 4618 |
. . . . . . . . . . . 12
β’ (πΎ β π β πΎ β {πΎ}) |
58 | 26, 57 | syl 17 |
. . . . . . . . . . 11
β’ (π β πΎ β {πΎ}) |
59 | | elun2 4135 |
. . . . . . . . . . 11
β’ (πΎ β {πΎ} β πΎ β ((π β {πΎ}) βͺ {πΎ})) |
60 | 58, 59 | syl 17 |
. . . . . . . . . 10
β’ (π β πΎ β ((π β {πΎ}) βͺ {πΎ})) |
61 | | neldifsnd 4751 |
. . . . . . . . . 10
β’ (π β Β¬ πΎ β (π β {πΎ})) |
62 | 60, 61 | eldifd 3919 |
. . . . . . . . 9
β’ (π β πΎ β (((π β {πΎ}) βͺ {πΎ}) β (π β {πΎ}))) |
63 | 62 | adantr 481 |
. . . . . . . 8
β’ ((π β§ π β β) β πΎ β (((π β {πΎ}) βͺ {πΎ}) β (π β {πΎ}))) |
64 | | eqid 2737 |
. . . . . . . 8
β’ ((π β {πΎ}) βͺ {πΎ}) = ((π β {πΎ}) βͺ {πΎ}) |
65 | | eqid 2737 |
. . . . . . . 8
β’ (π¦ β β β¦ (π β (β
βm ((π
β {πΎ}) βͺ {πΎ})) β¦ (β β ((π β {πΎ}) βͺ {πΎ}) β¦ if(β β (π β {πΎ}), (πββ), if((πββ) β€ π¦, (πββ), π¦))))) = (π¦ β β β¦ (π β (β βm ((π β {πΎ}) βͺ {πΎ})) β¦ (β β ((π β {πΎ}) βͺ {πΎ}) β¦ if(β β (π β {πΎ}), (πββ), if((πββ) β€ π¦, (πββ), π¦))))) |
66 | | uncom 4111 |
. . . . . . . . . . . . 13
β’ ((π β {πΎ}) βͺ {πΎ}) = ({πΎ} βͺ (π β {πΎ})) |
67 | 66 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β ((π β {πΎ}) βͺ {πΎ}) = ({πΎ} βͺ (π β {πΎ}))) |
68 | 26 | snssd 4767 |
. . . . . . . . . . . . 13
β’ (π β {πΎ} β π) |
69 | | undif 4439 |
. . . . . . . . . . . . 13
β’ ({πΎ} β π β ({πΎ} βͺ (π β {πΎ})) = π) |
70 | 68, 69 | sylib 217 |
. . . . . . . . . . . 12
β’ (π β ({πΎ} βͺ (π β {πΎ})) = π) |
71 | 67, 70 | eqtrd 2777 |
. . . . . . . . . . 11
β’ (π β ((π β {πΎ}) βͺ {πΎ}) = π) |
72 | 71 | adantr 481 |
. . . . . . . . . 10
β’ ((π β§ π β β) β ((π β {πΎ}) βͺ {πΎ}) = π) |
73 | 72 | feq2d 6651 |
. . . . . . . . 9
β’ ((π β§ π β β) β ((πΆβπ):((π β {πΎ}) βͺ {πΎ})βΆβ β (πΆβπ):πβΆβ)) |
74 | 18, 73 | mpbird 256 |
. . . . . . . 8
β’ ((π β§ π β β) β (πΆβπ):((π β {πΎ}) βͺ {πΎ})βΆβ) |
75 | 72 | feq2d 6651 |
. . . . . . . . 9
β’ ((π β§ π β β) β ((π·βπ):((π β {πΎ}) βͺ {πΎ})βΆβ β (π·βπ):πβΆβ)) |
76 | 22, 75 | mpbird 256 |
. . . . . . . 8
β’ ((π β§ π β β) β (π·βπ):((π β {πΎ}) βͺ {πΎ})βΆβ) |
77 | 49, 56, 63, 64, 38, 65, 74, 76 | hsphoidmvle 44728 |
. . . . . . 7
β’ ((π β§ π β β) β ((πΆβπ)(πΏβ((π β {πΎ}) βͺ {πΎ}))(((π¦ β β β¦ (π β (β βm ((π β {πΎ}) βͺ {πΎ})) β¦ (β β ((π β {πΎ}) βͺ {πΎ}) β¦ if(β β (π β {πΎ}), (πββ), if((πββ) β€ π¦, (πββ), π¦)))))βπ)β(π·βπ))) β€ ((πΆβπ)(πΏβ((π β {πΎ}) βͺ {πΎ}))(π·βπ))) |
78 | 71 | fveq2d 6843 |
. . . . . . . . . 10
β’ (π β (πΏβ((π β {πΎ}) βͺ {πΎ})) = (πΏβπ)) |
79 | | eqidd 2738 |
. . . . . . . . . 10
β’ (π β (πΆβπ) = (πΆβπ)) |
80 | 36 | a1i 11 |
. . . . . . . . . . . . 13
β’ (π β π = (π¦ β β β¦ (π β (β βm π) β¦ (β β π β¦ if(β β (π β {πΎ}), (πββ), if((πββ) β€ π¦, (πββ), π¦)))))) |
81 | 71 | oveq2d 7367 |
. . . . . . . . . . . . . . . 16
β’ (π β (β
βm ((π
β {πΎ}) βͺ {πΎ})) = (β
βm π)) |
82 | 71 | mpteq1d 5198 |
. . . . . . . . . . . . . . . 16
β’ (π β (β β ((π β {πΎ}) βͺ {πΎ}) β¦ if(β β (π β {πΎ}), (πββ), if((πββ) β€ π¦, (πββ), π¦))) = (β β π β¦ if(β β (π β {πΎ}), (πββ), if((πββ) β€ π¦, (πββ), π¦)))) |
83 | 81, 82 | mpteq12dv 5194 |
. . . . . . . . . . . . . . 15
β’ (π β (π β (β βm ((π β {πΎ}) βͺ {πΎ})) β¦ (β β ((π β {πΎ}) βͺ {πΎ}) β¦ if(β β (π β {πΎ}), (πββ), if((πββ) β€ π¦, (πββ), π¦)))) = (π β (β βm π) β¦ (β β π β¦ if(β β (π β {πΎ}), (πββ), if((πββ) β€ π¦, (πββ), π¦))))) |
84 | 83 | eqcomd 2743 |
. . . . . . . . . . . . . 14
β’ (π β (π β (β βm π) β¦ (β β π β¦ if(β β (π β {πΎ}), (πββ), if((πββ) β€ π¦, (πββ), π¦)))) = (π β (β βm ((π β {πΎ}) βͺ {πΎ})) β¦ (β β ((π β {πΎ}) βͺ {πΎ}) β¦ if(β β (π β {πΎ}), (πββ), if((πββ) β€ π¦, (πββ), π¦))))) |
85 | 84 | mpteq2dv 5205 |
. . . . . . . . . . . . 13
β’ (π β (π¦ β β β¦ (π β (β βm π) β¦ (β β π β¦ if(β β (π β {πΎ}), (πββ), if((πββ) β€ π¦, (πββ), π¦))))) = (π¦ β β β¦ (π β (β βm ((π β {πΎ}) βͺ {πΎ})) β¦ (β β ((π β {πΎ}) βͺ {πΎ}) β¦ if(β β (π β {πΎ}), (πββ), if((πββ) β€ π¦, (πββ), π¦)))))) |
86 | 80, 85 | eqtr2d 2778 |
. . . . . . . . . . . 12
β’ (π β (π¦ β β β¦ (π β (β βm ((π β {πΎ}) βͺ {πΎ})) β¦ (β β ((π β {πΎ}) βͺ {πΎ}) β¦ if(β β (π β {πΎ}), (πββ), if((πββ) β€ π¦, (πββ), π¦))))) = π) |
87 | 86 | fveq1d 6841 |
. . . . . . . . . . 11
β’ (π β ((π¦ β β β¦ (π β (β βm ((π β {πΎ}) βͺ {πΎ})) β¦ (β β ((π β {πΎ}) βͺ {πΎ}) β¦ if(β β (π β {πΎ}), (πββ), if((πββ) β€ π¦, (πββ), π¦)))))βπ) = (πβπ)) |
88 | 87 | fveq1d 6841 |
. . . . . . . . . 10
β’ (π β (((π¦ β β β¦ (π β (β βm ((π β {πΎ}) βͺ {πΎ})) β¦ (β β ((π β {πΎ}) βͺ {πΎ}) β¦ if(β β (π β {πΎ}), (πββ), if((πββ) β€ π¦, (πββ), π¦)))))βπ)β(π·βπ)) = ((πβπ)β(π·βπ))) |
89 | 78, 79, 88 | oveq123d 7372 |
. . . . . . . . 9
β’ (π β ((πΆβπ)(πΏβ((π β {πΎ}) βͺ {πΎ}))(((π¦ β β β¦ (π β (β βm ((π β {πΎ}) βͺ {πΎ})) β¦ (β β ((π β {πΎ}) βͺ {πΎ}) β¦ if(β β (π β {πΎ}), (πββ), if((πββ) β€ π¦, (πββ), π¦)))))βπ)β(π·βπ))) = ((πΆβπ)(πΏβπ)((πβπ)β(π·βπ)))) |
90 | 89 | adantr 481 |
. . . . . . . 8
β’ ((π β§ π β β) β ((πΆβπ)(πΏβ((π β {πΎ}) βͺ {πΎ}))(((π¦ β β β¦ (π β (β βm ((π β {πΎ}) βͺ {πΎ})) β¦ (β β ((π β {πΎ}) βͺ {πΎ}) β¦ if(β β (π β {πΎ}), (πββ), if((πββ) β€ π¦, (πββ), π¦)))))βπ)β(π·βπ))) = ((πΆβπ)(πΏβπ)((πβπ)β(π·βπ)))) |
91 | 78 | adantr 481 |
. . . . . . . . 9
β’ ((π β§ π β β) β (πΏβ((π β {πΎ}) βͺ {πΎ})) = (πΏβπ)) |
92 | 91 | oveqd 7368 |
. . . . . . . 8
β’ ((π β§ π β β) β ((πΆβπ)(πΏβ((π β {πΎ}) βͺ {πΎ}))(π·βπ)) = ((πΆβπ)(πΏβπ)(π·βπ))) |
93 | 90, 92 | breq12d 5116 |
. . . . . . 7
β’ ((π β§ π β β) β (((πΆβπ)(πΏβ((π β {πΎ}) βͺ {πΎ}))(((π¦ β β β¦ (π β (β βm ((π β {πΎ}) βͺ {πΎ})) β¦ (β β ((π β {πΎ}) βͺ {πΎ}) β¦ if(β β (π β {πΎ}), (πββ), if((πββ) β€ π¦, (πββ), π¦)))))βπ)β(π·βπ))) β€ ((πΆβπ)(πΏβ((π β {πΎ}) βͺ {πΎ}))(π·βπ)) β ((πΆβπ)(πΏβπ)((πβπ)β(π·βπ))) β€ ((πΆβπ)(πΏβπ)(π·βπ)))) |
94 | 77, 93 | mpbid 231 |
. . . . . 6
β’ ((π β§ π β β) β ((πΆβπ)(πΏβπ)((πβπ)β(π·βπ))) β€ ((πΆβπ)(πΏβπ)(π·βπ))) |
95 | 8, 10, 41, 24, 94 | sge0lempt 44552 |
. . . . 5
β’ (π β
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((πβπ)β(π·βπ))))) β€
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ))))) |
96 | 35, 42, 95 | ge0lere 43671 |
. . . 4
β’ (π β
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((πβπ)β(π·βπ))))) β β) |
97 | | hspmbllem2.s |
. . . . . . . . . 10
β’ π = (π₯ β β β¦ (π β (β βm π) β¦ (β β π β¦ if(β = πΎ, if(π₯ β€ (πββ), (πββ), π₯), (πββ))))) |
98 | 97, 38, 14, 18 | hoidifhspf 44760 |
. . . . . . . . 9
β’ ((π β§ π β β) β ((πβπ)β(πΆβπ)):πβΆβ) |
99 | 12, 14, 98, 22 | hoidmvcl 44724 |
. . . . . . . 8
β’ ((π β§ π β β) β (((πβπ)β(πΆβπ))(πΏβπ)(π·βπ)) β (0[,)+β)) |
100 | 99 | fmpttd 7059 |
. . . . . . 7
β’ (π β (π β β β¦ (((πβπ)β(πΆβπ))(πΏβπ)(π·βπ))):ββΆ(0[,)+β)) |
101 | 11 | a1i 11 |
. . . . . . 7
β’ (π β (0[,)+β) β
(0[,]+β)) |
102 | 100, 101 | fssd 6683 |
. . . . . 6
β’ (π β (π β β β¦ (((πβπ)β(πΆβπ))(πΏβπ)(π·βπ))):ββΆ(0[,]+β)) |
103 | 10, 102 | sge0cl 44523 |
. . . . 5
β’ (π β
(Ξ£^β(π β β β¦ (((πβπ)β(πΆβπ))(πΏβπ)(π·βπ)))) β (0[,]+β)) |
104 | 11, 99 | sselid 3940 |
. . . . . 6
β’ ((π β§ π β β) β (((πβπ)β(πΆβπ))(πΏβπ)(π·βπ)) β (0[,]+β)) |
105 | 26 | adantr 481 |
. . . . . . 7
β’ ((π β§ π β β) β πΎ β π) |
106 | 12, 14, 18, 22, 105, 97, 38 | hoidifhspdmvle 44762 |
. . . . . 6
β’ ((π β§ π β β) β (((πβπ)β(πΆβπ))(πΏβπ)(π·βπ)) β€ ((πΆβπ)(πΏβπ)(π·βπ))) |
107 | 8, 10, 104, 24, 106 | sge0lempt 44552 |
. . . . 5
β’ (π β
(Ξ£^β(π β β β¦ (((πβπ)β(πΆβπ))(πΏβπ)(π·βπ)))) β€
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ))))) |
108 | 35, 103, 107 | ge0lere 43671 |
. . . 4
β’ (π β
(Ξ£^β(π β β β¦ (((πβπ)β(πΆβπ))(πΏβπ)(π·βπ)))) β β) |
109 | 37 | adantr 481 |
. . . . . . . . 9
β’ ((π β§ π β β) β π β β) |
110 | 13 | adantr 481 |
. . . . . . . . 9
β’ ((π β§ π β β) β π β Fin) |
111 | | eleq1w 2820 |
. . . . . . . . . . . 12
β’ (π = π β (π β β β π β β)) |
112 | 111 | anbi2d 629 |
. . . . . . . . . . 11
β’ (π = π β ((π β§ π β β) β (π β§ π β β))) |
113 | | fveq2 6839 |
. . . . . . . . . . . 12
β’ (π = π β (π·βπ) = (π·βπ)) |
114 | 113 | feq1d 6650 |
. . . . . . . . . . 11
β’ (π = π β ((π·βπ):πβΆβ β (π·βπ):πβΆβ)) |
115 | 112, 114 | imbi12d 344 |
. . . . . . . . . 10
β’ (π = π β (((π β§ π β β) β (π·βπ):πβΆβ) β ((π β§ π β β) β (π·βπ):πβΆβ))) |
116 | 115, 22 | chvarvv 2002 |
. . . . . . . . 9
β’ ((π β§ π β β) β (π·βπ):πβΆβ) |
117 | 36, 109, 110, 116 | hsphoif 44718 |
. . . . . . . 8
β’ ((π β§ π β β) β ((πβπ)β(π·βπ)):πβΆβ) |
118 | | reex 11100 |
. . . . . . . . . . . 12
β’ β
β V |
119 | 118 | a1i 11 |
. . . . . . . . . . 11
β’ (π β β β
V) |
120 | 119, 13 | jca 512 |
. . . . . . . . . 10
β’ (π β (β β V β§
π β
Fin)) |
121 | 120 | adantr 481 |
. . . . . . . . 9
β’ ((π β§ π β β) β (β β V
β§ π β
Fin)) |
122 | | elmapg 8736 |
. . . . . . . . 9
β’ ((β
β V β§ π β
Fin) β (((πβπ)β(π·βπ)) β (β βm π) β ((πβπ)β(π·βπ)):πβΆβ)) |
123 | 121, 122 | syl 17 |
. . . . . . . 8
β’ ((π β§ π β β) β (((πβπ)β(π·βπ)) β (β βm π) β ((πβπ)β(π·βπ)):πβΆβ)) |
124 | 117, 123 | mpbird 256 |
. . . . . . 7
β’ ((π β§ π β β) β ((πβπ)β(π·βπ)) β (β βm π)) |
125 | 124 | fmpttd 7059 |
. . . . . 6
β’ (π β (π β β β¦ ((πβπ)β(π·βπ))):ββΆ(β
βm π)) |
126 | | simpl 483 |
. . . . . . . . . . . 12
β’ ((π β§ π β (π΄ β© (πΎ(π»βπ)π))) β π) |
127 | | elinel1 4153 |
. . . . . . . . . . . . 13
β’ (π β (π΄ β© (πΎ(π»βπ)π)) β π β π΄) |
128 | 127 | adantl 482 |
. . . . . . . . . . . 12
β’ ((π β§ π β (π΄ β© (πΎ(π»βπ)π))) β π β π΄) |
129 | | hspmbllem2.a |
. . . . . . . . . . . . . 14
β’ (π β π΄ β βͺ
π β β Xπ β
π (((πΆβπ)βπ)[,)((π·βπ)βπ))) |
130 | 129 | sselda 3942 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π΄) β π β βͺ
π β β Xπ β
π (((πΆβπ)βπ)[,)((π·βπ)βπ))) |
131 | | eliun 4956 |
. . . . . . . . . . . . 13
β’ (π β βͺ π β β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ)) β βπ β β π β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ))) |
132 | 130, 131 | sylib 217 |
. . . . . . . . . . . 12
β’ ((π β§ π β π΄) β βπ β β π β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ))) |
133 | 126, 128,
132 | syl2anc 584 |
. . . . . . . . . . 11
β’ ((π β§ π β (π΄ β© (πΎ(π»βπ)π))) β βπ β β π β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ))) |
134 | | simpll 765 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (π΄ β© (πΎ(π»βπ)π))) β§ π β β) β π) |
135 | | elinel2 4154 |
. . . . . . . . . . . . . . 15
β’ (π β (π΄ β© (πΎ(π»βπ)π)) β π β (πΎ(π»βπ)π)) |
136 | 135 | adantl 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (π΄ β© (πΎ(π»βπ)π))) β π β (πΎ(π»βπ)π)) |
137 | 136 | adantr 481 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (π΄ β© (πΎ(π»βπ)π))) β§ π β β) β π β (πΎ(π»βπ)π)) |
138 | | simpr 485 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (π΄ β© (πΎ(π»βπ)π))) β§ π β β) β π β β) |
139 | | ixpfn 8799 |
. . . . . . . . . . . . . . . . 17
β’ (π β Xπ β
π (((πΆβπ)βπ)[,)((π·βπ)βπ)) β π Fn π) |
140 | 139 | adantl 482 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π β (πΎ(π»βπ)π)) β§ π β β) β§ π β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ))) β π Fn π) |
141 | | nfv 1917 |
. . . . . . . . . . . . . . . . . 18
β’
β²π((π β§ π β (πΎ(π»βπ)π)) β§ π β β) |
142 | | nfcv 2905 |
. . . . . . . . . . . . . . . . . . 19
β’
β²ππ |
143 | | nfixp1 8814 |
. . . . . . . . . . . . . . . . . . 19
β’
β²πXπ β
π (((πΆβπ)βπ)[,)((π·βπ)βπ)) |
144 | 142, 143 | nfel 2919 |
. . . . . . . . . . . . . . . . . 18
β’
β²π π β Xπ β
π (((πΆβπ)βπ)[,)((π·βπ)βπ)) |
145 | 141, 144 | nfan 1902 |
. . . . . . . . . . . . . . . . 17
β’
β²π(((π β§ π β (πΎ(π»βπ)π)) β§ π β β) β§ π β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ))) |
146 | 18 | 3adant3 1132 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π β β β§ π β π) β (πΆβπ):πβΆβ) |
147 | | simp3 1138 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π β β β§ π β π) β π β π) |
148 | 146, 147 | ffvelcdmd 7032 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π β β β§ π β π) β ((πΆβπ)βπ) β β) |
149 | 148 | rexrd 11163 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π β β β§ π β π) β ((πΆβπ)βπ) β
β*) |
150 | 149 | ad5ant135 1368 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((π β§ π β (πΎ(π»βπ)π)) β§ π β β) β§ π β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ))) β§ π β π) β ((πΆβπ)βπ) β
β*) |
151 | 39 | 3adant3 1132 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π β β β§ π β π) β ((πβπ)β(π·βπ)):πβΆβ) |
152 | 151, 147 | ffvelcdmd 7032 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π β β β§ π β π) β (((πβπ)β(π·βπ))βπ) β β) |
153 | 152 | rexrd 11163 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π β β β§ π β π) β (((πβπ)β(π·βπ))βπ) β
β*) |
154 | 153 | ad5ant135 1368 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((π β§ π β (πΎ(π»βπ)π)) β§ π β β) β§ π β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ))) β§ π β π) β (((πβπ)β(π·βπ))βπ) β
β*) |
155 | | iftrue 4490 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π = πΎ β if(π = πΎ, (-β(,)π), β) = (-β(,)π)) |
156 | | ioossre 13279 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(-β(,)π)
β β |
157 | 156 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π = πΎ β (-β(,)π) β β) |
158 | 155, 157 | eqsstrd 3980 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π = πΎ β if(π = πΎ, (-β(,)π), β) β
β) |
159 | | iffalse 4493 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (Β¬
π = πΎ β if(π = πΎ, (-β(,)π), β) = β) |
160 | | ssid 3964 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ β
β β |
161 | 160 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (Β¬
π = πΎ β β β
β) |
162 | 159, 161 | eqsstrd 3980 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (Β¬
π = πΎ β if(π = πΎ, (-β(,)π), β) β
β) |
163 | 158, 162 | pm2.61i 182 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ if(π = πΎ, (-β(,)π), β) β β |
164 | | simpr 485 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β§ π β (πΎ(π»βπ)π)) β π β (πΎ(π»βπ)π)) |
165 | | hspmbllem2.h |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ π» = (π₯ β Fin β¦ (π β π₯, π¦ β β β¦ Xπ β
π₯ if(π = π, (-β(,)π¦), β))) |
166 | 165, 13, 26, 37 | hspval 44751 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β (πΎ(π»βπ)π) = Xπ β π if(π = πΎ, (-β(,)π), β)) |
167 | 166 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β§ π β (πΎ(π»βπ)π)) β (πΎ(π»βπ)π) = Xπ β π if(π = πΎ, (-β(,)π), β)) |
168 | 164, 167 | eleqtrd 2840 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ π β (πΎ(π»βπ)π)) β π β Xπ β π if(π = πΎ, (-β(,)π), β)) |
169 | 168 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β§ π β (πΎ(π»βπ)π)) β§ π β π) β π β Xπ β π if(π = πΎ, (-β(,)π), β)) |
170 | | simpr 485 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β§ π β (πΎ(π»βπ)π)) β§ π β π) β π β π) |
171 | | vex 3447 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ π β V |
172 | 171 | elixp 8800 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β Xπ β
π if(π = πΎ, (-β(,)π), β) β (π Fn π β§ βπ β π (πβπ) β if(π = πΎ, (-β(,)π), β))) |
173 | 172 | biimpi 215 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β Xπ β
π if(π = πΎ, (-β(,)π), β) β (π Fn π β§ βπ β π (πβπ) β if(π = πΎ, (-β(,)π), β))) |
174 | 173 | simprd 496 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β Xπ β
π if(π = πΎ, (-β(,)π), β) β βπ β π (πβπ) β if(π = πΎ, (-β(,)π), β)) |
175 | 174 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β Xπ β
π if(π = πΎ, (-β(,)π), β) β§ π β π) β βπ β π (πβπ) β if(π = πΎ, (-β(,)π), β)) |
176 | | simpr 485 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β Xπ β
π if(π = πΎ, (-β(,)π), β) β§ π β π) β π β π) |
177 | | rspa 3229 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
((βπ β
π (πβπ) β if(π = πΎ, (-β(,)π), β) β§ π β π) β (πβπ) β if(π = πΎ, (-β(,)π), β)) |
178 | 175, 176,
177 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β Xπ β
π if(π = πΎ, (-β(,)π), β) β§ π β π) β (πβπ) β if(π = πΎ, (-β(,)π), β)) |
179 | 169, 170,
178 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π β (πΎ(π»βπ)π)) β§ π β π) β (πβπ) β if(π = πΎ, (-β(,)π), β)) |
180 | 163, 179 | sselid 3940 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π β (πΎ(π»βπ)π)) β§ π β π) β (πβπ) β β) |
181 | 180 | rexrd 11163 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π β (πΎ(π»βπ)π)) β§ π β π) β (πβπ) β
β*) |
182 | 181 | ad4ant14 750 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((π β§ π β (πΎ(π»βπ)π)) β§ π β β) β§ π β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ))) β§ π β π) β (πβπ) β
β*) |
183 | 149 | ad4ant124 1173 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ π β β) β§ π β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ))) β§ π β π) β ((πΆβπ)βπ) β
β*) |
184 | 22 | 3adant3 1132 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ π β β β§ π β π) β (π·βπ):πβΆβ) |
185 | 184, 147 | ffvelcdmd 7032 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ π β β β§ π β π) β ((π·βπ)βπ) β β) |
186 | 185 | rexrd 11163 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π β β β§ π β π) β ((π·βπ)βπ) β
β*) |
187 | 186 | ad4ant124 1173 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ π β β) β§ π β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ))) β§ π β π) β ((π·βπ)βπ) β
β*) |
188 | 171 | elixp 8800 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β Xπ β
π (((πΆβπ)βπ)[,)((π·βπ)βπ)) β (π Fn π β§ βπ β π (πβπ) β (((πΆβπ)βπ)[,)((π·βπ)βπ)))) |
189 | 188 | biimpi 215 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β Xπ β
π (((πΆβπ)βπ)[,)((π·βπ)βπ)) β (π Fn π β§ βπ β π (πβπ) β (((πΆβπ)βπ)[,)((π·βπ)βπ)))) |
190 | 189 | simprd 496 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β Xπ β
π (((πΆβπ)βπ)[,)((π·βπ)βπ)) β βπ β π (πβπ) β (((πΆβπ)βπ)[,)((π·βπ)βπ))) |
191 | 190 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β Xπ β
π (((πΆβπ)βπ)[,)((π·βπ)βπ)) β§ π β π) β βπ β π (πβπ) β (((πΆβπ)βπ)[,)((π·βπ)βπ))) |
192 | | simpr 485 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β Xπ β
π (((πΆβπ)βπ)[,)((π·βπ)βπ)) β§ π β π) β π β π) |
193 | | rspa 3229 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
((βπ β
π (πβπ) β (((πΆβπ)βπ)[,)((π·βπ)βπ)) β§ π β π) β (πβπ) β (((πΆβπ)βπ)[,)((π·βπ)βπ))) |
194 | 191, 192,
193 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β Xπ β
π (((πΆβπ)βπ)[,)((π·βπ)βπ)) β§ π β π) β (πβπ) β (((πΆβπ)βπ)[,)((π·βπ)βπ))) |
195 | 194 | adantll 712 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ π β β) β§ π β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ))) β§ π β π) β (πβπ) β (((πΆβπ)βπ)[,)((π·βπ)βπ))) |
196 | | icogelb 13269 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((πΆβπ)βπ) β β* β§ ((π·βπ)βπ) β β* β§ (πβπ) β (((πΆβπ)βπ)[,)((π·βπ)βπ))) β ((πΆβπ)βπ) β€ (πβπ)) |
197 | 183, 187,
195, 196 | syl3anc 1371 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π β β) β§ π β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ))) β§ π β π) β ((πΆβπ)βπ) β€ (πβπ)) |
198 | 197 | adantl3r 748 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((π β§ π β (πΎ(π»βπ)π)) β§ π β β) β§ π β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ))) β§ π β π) β ((πΆβπ)βπ) β€ (πβπ)) |
199 | | icoltub 43647 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((πΆβπ)βπ) β β* β§ ((π·βπ)βπ) β β* β§ (πβπ) β (((πΆβπ)βπ)[,)((π·βπ)βπ))) β (πβπ) < ((π·βπ)βπ)) |
200 | 183, 187,
195, 199 | syl3anc 1371 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β§ π β β) β§ π β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ))) β§ π β π) β (πβπ) < ((π·βπ)βπ)) |
201 | 200 | adantl3r 748 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(((((π β§ π β (πΎ(π»βπ)π)) β§ π β β) β§ π β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ))) β§ π β π) β (πβπ) < ((π·βπ)βπ)) |
202 | 201 | ad2antrr 724 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((((((π β§ π β (πΎ(π»βπ)π)) β§ π β β) β§ π β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ))) β§ π β π) β§ π = πΎ) β§ ((π·βπ)βπ) β€ π) β (πβπ) < ((π·βπ)βπ)) |
203 | | simpll 765 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π β§ π β (πΎ(π»βπ)π)) β§ π β β) β π) |
204 | | simpr 485 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π β§ π β (πΎ(π»βπ)π)) β§ π β β) β π β β) |
205 | 203, 204 | jca 512 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β§ π β (πΎ(π»βπ)π)) β§ π β β) β (π β§ π β β)) |
206 | 205 | 3ad2ant1 1133 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β§ π β (πΎ(π»βπ)π)) β§ π β β) β§ π = πΎ β§ ((π·βπ)βπ) β€ π) β (π β§ π β β)) |
207 | | simp2 1137 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β§ π β (πΎ(π»βπ)π)) β§ π β β) β§ π = πΎ β§ ((π·βπ)βπ) β€ π) β π = πΎ) |
208 | | simp3 1138 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β§ π β (πΎ(π»βπ)π)) β§ π β β) β§ π = πΎ β§ ((π·βπ)βπ) β€ π) β ((π·βπ)βπ) β€ π) |
209 | | fveq2 6839 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π = πΎ β ((π·βπ)βπ) = ((π·βπ)βπΎ)) |
210 | 209 | breq1d 5113 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π = πΎ β (((π·βπ)βπ) β€ π β ((π·βπ)βπΎ) β€ π)) |
211 | 210 | biimpa 477 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π = πΎ β§ ((π·βπ)βπ) β€ π) β ((π·βπ)βπΎ) β€ π) |
212 | 211 | iftrued 4492 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π = πΎ β§ ((π·βπ)βπ) β€ π) β if(((π·βπ)βπΎ) β€ π, ((π·βπ)βπΎ), π) = ((π·βπ)βπΎ)) |
213 | 209 | eqcomd 2743 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π = πΎ β ((π·βπ)βπΎ) = ((π·βπ)βπ)) |
214 | 213 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π = πΎ β§ ((π·βπ)βπ) β€ π) β ((π·βπ)βπΎ) = ((π·βπ)βπ)) |
215 | 212, 214 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π = πΎ β§ ((π·βπ)βπ) β€ π) β if(((π·βπ)βπΎ) β€ π, ((π·βπ)βπΎ), π) = ((π·βπ)βπ)) |
216 | 215 | 3adant1 1130 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β§ π β β) β§ π = πΎ β§ ((π·βπ)βπ) β€ π) β if(((π·βπ)βπΎ) β€ π, ((π·βπ)βπΎ), π) = ((π·βπ)βπ)) |
217 | | breq2 5107 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ (π¦ = π β ((πββ) β€ π¦ β (πββ) β€ π)) |
218 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ (π¦ = π β π¦ = π) |
219 | 217, 218 | ifbieq2d 4510 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ (π¦ = π β if((πββ) β€ π¦, (πββ), π¦) = if((πββ) β€ π, (πββ), π)) |
220 | 219 | ifeq2d 4504 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ (π¦ = π β if(β β (π β {πΎ}), (πββ), if((πββ) β€ π¦, (πββ), π¦)) = if(β β (π β {πΎ}), (πββ), if((πββ) β€ π, (πββ), π))) |
221 | 220 | mpteq2dv 5205 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (π¦ = π β (β β π β¦ if(β β (π β {πΎ}), (πββ), if((πββ) β€ π¦, (πββ), π¦))) = (β β π β¦ if(β β (π β {πΎ}), (πββ), if((πββ) β€ π, (πββ), π)))) |
222 | 221 | mpteq2dv 5205 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (π¦ = π β (π β (β βm π) β¦ (β β π β¦ if(β β (π β {πΎ}), (πββ), if((πββ) β€ π¦, (πββ), π¦)))) = (π β (β βm π) β¦ (β β π β¦ if(β β (π β {πΎ}), (πββ), if((πββ) β€ π, (πββ), π))))) |
223 | | ovex 7384 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ (β
βm π)
β V |
224 | 223 | mptex 7169 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (π β (β
βm π)
β¦ (β β π β¦ if(β β (π β {πΎ}), (πββ), if((πββ) β€ π, (πββ), π)))) β V |
225 | 224 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (π β (π β (β βm π) β¦ (β β π β¦ if(β β (π β {πΎ}), (πββ), if((πββ) β€ π, (πββ), π)))) β V) |
226 | 36, 222, 37, 225 | fvmptd3 6968 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (π β (πβπ) = (π β (β βm π) β¦ (β β π β¦ if(β β (π β {πΎ}), (πββ), if((πββ) β€ π, (πββ), π))))) |
227 | 226 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((π β§ π β β) β (πβπ) = (π β (β βm π) β¦ (β β π β¦ if(β β (π β {πΎ}), (πββ), if((πββ) β€ π, (πββ), π))))) |
228 | | fveq1 6838 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (π = (π·βπ) β (πββ) = ((π·βπ)ββ)) |
229 | 228 | breq1d 5113 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ (π = (π·βπ) β ((πββ) β€ π β ((π·βπ)ββ) β€ π)) |
230 | 229, 228 | ifbieq1d 4508 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (π = (π·βπ) β if((πββ) β€ π, (πββ), π) = if(((π·βπ)ββ) β€ π, ((π·βπ)ββ), π)) |
231 | 228, 230 | ifeq12d 4505 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (π = (π·βπ) β if(β β (π β {πΎ}), (πββ), if((πββ) β€ π, (πββ), π)) = if(β β (π β {πΎ}), ((π·βπ)ββ), if(((π·βπ)ββ) β€ π, ((π·βπ)ββ), π))) |
232 | 231 | mpteq2dv 5205 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (π = (π·βπ) β (β β π β¦ if(β β (π β {πΎ}), (πββ), if((πββ) β€ π, (πββ), π))) = (β β π β¦ if(β β (π β {πΎ}), ((π·βπ)ββ), if(((π·βπ)ββ) β€ π, ((π·βπ)ββ), π)))) |
233 | 232 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (((π β§ π β β) β§ π = (π·βπ)) β (β β π β¦ if(β β (π β {πΎ}), (πββ), if((πββ) β€ π, (πββ), π))) = (β β π β¦ if(β β (π β {πΎ}), ((π·βπ)ββ), if(((π·βπ)ββ) β€ π, ((π·βπ)ββ), π)))) |
234 | | mptexg 7167 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (π β Fin β (β β π β¦ if(β β (π β {πΎ}), ((π·βπ)ββ), if(((π·βπ)ββ) β€ π, ((π·βπ)ββ), π))) β V) |
235 | 13, 234 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (π β (β β π β¦ if(β β (π β {πΎ}), ((π·βπ)ββ), if(((π·βπ)ββ) β€ π, ((π·βπ)ββ), π))) β V) |
236 | 235 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((π β§ π β β) β (β β π β¦ if(β β (π β {πΎ}), ((π·βπ)ββ), if(((π·βπ)ββ) β€ π, ((π·βπ)ββ), π))) β V) |
237 | 227, 233,
20, 236 | fvmptd 6952 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((π β§ π β β) β ((πβπ)β(π·βπ)) = (β β π β¦ if(β β (π β {πΎ}), ((π·βπ)ββ), if(((π·βπ)ββ) β€ π, ((π·βπ)ββ), π)))) |
238 | 237 | fveq1d 6841 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((π β§ π β β) β (((πβπ)β(π·βπ))βπ) = ((β β π β¦ if(β β (π β {πΎ}), ((π·βπ)ββ), if(((π·βπ)ββ) β€ π, ((π·βπ)ββ), π)))βπ)) |
239 | 238 | 3adant3 1132 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π β§ π β β β§ π = πΎ) β (((πβπ)β(π·βπ))βπ) = ((β β π β¦ if(β β (π β {πΎ}), ((π·βπ)ββ), if(((π·βπ)ββ) β€ π, ((π·βπ)ββ), π)))βπ)) |
240 | | simpl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((π β§ π = πΎ) β π) |
241 | | simpr 485 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((π β§ π = πΎ) β π = πΎ) |
242 | 240, 26 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((π β§ π = πΎ) β πΎ β π) |
243 | 241, 242 | eqeltrd 2838 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((π β§ π = πΎ) β π β π) |
244 | | eqidd 2738 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((π β§ π β π) β (β β π β¦ if(β β (π β {πΎ}), ((π·βπ)ββ), if(((π·βπ)ββ) β€ π, ((π·βπ)ββ), π))) = (β β π β¦ if(β β (π β {πΎ}), ((π·βπ)ββ), if(((π·βπ)ββ) β€ π, ((π·βπ)ββ), π)))) |
245 | | eleq1w 2820 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (β = π β (β β (π β {πΎ}) β π β (π β {πΎ}))) |
246 | | fveq2 6839 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (β = π β ((π·βπ)ββ) = ((π·βπ)βπ)) |
247 | 246 | breq1d 5113 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ (β = π β (((π·βπ)ββ) β€ π β ((π·βπ)βπ) β€ π)) |
248 | 247, 246 | ifbieq1d 4508 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (β = π β if(((π·βπ)ββ) β€ π, ((π·βπ)ββ), π) = if(((π·βπ)βπ) β€ π, ((π·βπ)βπ), π)) |
249 | 245, 246,
248 | ifbieq12d 4512 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (β = π β if(β β (π β {πΎ}), ((π·βπ)ββ), if(((π·βπ)ββ) β€ π, ((π·βπ)ββ), π)) = if(π β (π β {πΎ}), ((π·βπ)βπ), if(((π·βπ)βπ) β€ π, ((π·βπ)βπ), π))) |
250 | 249 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (((π β§ π β π) β§ β = π) β if(β β (π β {πΎ}), ((π·βπ)ββ), if(((π·βπ)ββ) β€ π, ((π·βπ)ββ), π)) = if(π β (π β {πΎ}), ((π·βπ)βπ), if(((π·βπ)βπ) β€ π, ((π·βπ)βπ), π))) |
251 | | simpr 485 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((π β§ π β π) β π β π) |
252 | | fvexd 6854 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (π β ((π·βπ)βπ) β V) |
253 | 252, 37 | ifexd 4532 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (π β if(((π·βπ)βπ) β€ π, ((π·βπ)βπ), π) β V) |
254 | 252, 253 | ifexd 4532 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (π β if(π β (π β {πΎ}), ((π·βπ)βπ), if(((π·βπ)βπ) β€ π, ((π·βπ)βπ), π)) β V) |
255 | 254 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((π β§ π β π) β if(π β (π β {πΎ}), ((π·βπ)βπ), if(((π·βπ)βπ) β€ π, ((π·βπ)βπ), π)) β V) |
256 | 244, 250,
251, 255 | fvmptd 6952 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((π β§ π β π) β ((β β π β¦ if(β β (π β {πΎ}), ((π·βπ)ββ), if(((π·βπ)ββ) β€ π, ((π·βπ)ββ), π)))βπ) = if(π β (π β {πΎ}), ((π·βπ)βπ), if(((π·βπ)βπ) β€ π, ((π·βπ)βπ), π))) |
257 | 240, 243,
256 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((π β§ π = πΎ) β ((β β π β¦ if(β β (π β {πΎ}), ((π·βπ)ββ), if(((π·βπ)ββ) β€ π, ((π·βπ)ββ), π)))βπ) = if(π β (π β {πΎ}), ((π·βπ)βπ), if(((π·βπ)βπ) β€ π, ((π·βπ)βπ), π))) |
258 | | eleq1 2825 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (π = πΎ β (π β (π β {πΎ}) β πΎ β (π β {πΎ}))) |
259 | 210, 209 | ifbieq1d 4508 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (π = πΎ β if(((π·βπ)βπ) β€ π, ((π·βπ)βπ), π) = if(((π·βπ)βπΎ) β€ π, ((π·βπ)βπΎ), π)) |
260 | 258, 209,
259 | ifbieq12d 4512 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (π = πΎ β if(π β (π β {πΎ}), ((π·βπ)βπ), if(((π·βπ)βπ) β€ π, ((π·βπ)βπ), π)) = if(πΎ β (π β {πΎ}), ((π·βπ)βπΎ), if(((π·βπ)βπΎ) β€ π, ((π·βπ)βπΎ), π))) |
261 | 260 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((π β§ π = πΎ) β if(π β (π β {πΎ}), ((π·βπ)βπ), if(((π·βπ)βπ) β€ π, ((π·βπ)βπ), π)) = if(πΎ β (π β {πΎ}), ((π·βπ)βπΎ), if(((π·βπ)βπΎ) β€ π, ((π·βπ)βπΎ), π))) |
262 | 257, 261 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((π β§ π = πΎ) β ((β β π β¦ if(β β (π β {πΎ}), ((π·βπ)ββ), if(((π·βπ)ββ) β€ π, ((π·βπ)ββ), π)))βπ) = if(πΎ β (π β {πΎ}), ((π·βπ)βπΎ), if(((π·βπ)βπΎ) β€ π, ((π·βπ)βπΎ), π))) |
263 | 262 | 3adant2 1131 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π β§ π β β β§ π = πΎ) β ((β β π β¦ if(β β (π β {πΎ}), ((π·βπ)ββ), if(((π·βπ)ββ) β€ π, ((π·βπ)ββ), π)))βπ) = if(πΎ β (π β {πΎ}), ((π·βπ)βπΎ), if(((π·βπ)βπΎ) β€ π, ((π·βπ)βπΎ), π))) |
264 | | neldifsnd 4751 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π = πΎ β Β¬ πΎ β (π β {πΎ})) |
265 | 264 | iffalsed 4495 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π = πΎ β if(πΎ β (π β {πΎ}), ((π·βπ)βπΎ), if(((π·βπ)βπΎ) β€ π, ((π·βπ)βπΎ), π)) = if(((π·βπ)βπΎ) β€ π, ((π·βπ)βπΎ), π)) |
266 | 265 | 3ad2ant3 1135 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π β§ π β β β§ π = πΎ) β if(πΎ β (π β {πΎ}), ((π·βπ)βπΎ), if(((π·βπ)βπΎ) β€ π, ((π·βπ)βπΎ), π)) = if(((π·βπ)βπΎ) β€ π, ((π·βπ)βπΎ), π)) |
267 | 239, 263,
266 | 3eqtrrd 2782 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β§ π β β β§ π = πΎ) β if(((π·βπ)βπΎ) β€ π, ((π·βπ)βπΎ), π) = (((πβπ)β(π·βπ))βπ)) |
268 | 267 | 3expa 1118 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π β§ π β β) β§ π = πΎ) β if(((π·βπ)βπΎ) β€ π, ((π·βπ)βπΎ), π) = (((πβπ)β(π·βπ))βπ)) |
269 | 268 | 3adant3 1132 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β§ π β β) β§ π = πΎ β§ ((π·βπ)βπ) β€ π) β if(((π·βπ)βπΎ) β€ π, ((π·βπ)βπΎ), π) = (((πβπ)β(π·βπ))βπ)) |
270 | 216, 269 | eqtr3d 2779 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β§ π β β) β§ π = πΎ β§ ((π·βπ)βπ) β€ π) β ((π·βπ)βπ) = (((πβπ)β(π·βπ))βπ)) |
271 | 206, 207,
208, 270 | syl3anc 1371 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ π β (πΎ(π»βπ)π)) β§ π β β) β§ π = πΎ β§ ((π·βπ)βπ) β€ π) β ((π·βπ)βπ) = (((πβπ)β(π·βπ))βπ)) |
272 | 271 | ad5ant145 1369 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((((((π β§ π β (πΎ(π»βπ)π)) β§ π β β) β§ π β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ))) β§ π β π) β§ π = πΎ) β§ ((π·βπ)βπ) β€ π) β ((π·βπ)βπ) = (((πβπ)β(π·βπ))βπ)) |
273 | 202, 272 | breqtrd 5129 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((((π β§ π β (πΎ(π»βπ)π)) β§ π β β) β§ π β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ))) β§ π β π) β§ π = πΎ) β§ ((π·βπ)βπ) β€ π) β (πβπ) < (((πβπ)β(π·βπ))βπ)) |
274 | | mnfxr 11170 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ -β
β β* |
275 | 274 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π β§ π β (πΎ(π»βπ)π)) β§ π β π β§ π = πΎ) β -β β
β*) |
276 | 37 | rexrd 11163 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π β π β
β*) |
277 | 276 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β§ π β (πΎ(π»βπ)π)) β π β
β*) |
278 | 277 | 3ad2ant1 1133 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π β§ π β (πΎ(π»βπ)π)) β§ π β π β§ π = πΎ) β π β
β*) |
279 | 179 | 3adant3 1132 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (((π β§ π β (πΎ(π»βπ)π)) β§ π β π β§ π = πΎ) β (πβπ) β if(π = πΎ, (-β(,)π), β)) |
280 | 155 | 3ad2ant3 1135 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (((π β§ π β (πΎ(π»βπ)π)) β§ π β π β§ π = πΎ) β if(π = πΎ, (-β(,)π), β) = (-β(,)π)) |
281 | 279, 280 | eleqtrd 2840 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π β§ π β (πΎ(π»βπ)π)) β§ π β π β§ π = πΎ) β (πβπ) β (-β(,)π)) |
282 | | iooltub 43649 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
((-β β β* β§ π β β* β§ (πβπ) β (-β(,)π)) β (πβπ) < π) |
283 | 275, 278,
281, 282 | syl3anc 1371 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β§ π β (πΎ(π»βπ)π)) β§ π β π β§ π = πΎ) β (πβπ) < π) |
284 | 283 | 3adant1r 1177 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β§ π β (πΎ(π»βπ)π)) β§ π β β) β§ π β π β§ π = πΎ) β (πβπ) < π) |
285 | 284 | ad4ant123 1172 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
((((((π β§ π β (πΎ(π»βπ)π)) β§ π β β) β§ π β π) β§ π = πΎ) β§ Β¬ ((π·βπ)βπ) β€ π) β (πβπ) < π) |
286 | | simpr 485 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π = πΎ β§ Β¬ ((π·βπ)βπ) β€ π) β Β¬ ((π·βπ)βπ) β€ π) |
287 | 210 | notbid 317 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π = πΎ β (Β¬ ((π·βπ)βπ) β€ π β Β¬ ((π·βπ)βπΎ) β€ π)) |
288 | 287 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π = πΎ β§ Β¬ ((π·βπ)βπ) β€ π) β (Β¬ ((π·βπ)βπ) β€ π β Β¬ ((π·βπ)βπΎ) β€ π)) |
289 | 286, 288 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π = πΎ β§ Β¬ ((π·βπ)βπ) β€ π) β Β¬ ((π·βπ)βπΎ) β€ π) |
290 | 289 | iffalsed 4495 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π = πΎ β§ Β¬ ((π·βπ)βπ) β€ π) β if(((π·βπ)βπΎ) β€ π, ((π·βπ)βπΎ), π) = π) |
291 | | eqidd 2738 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π = πΎ β§ Β¬ ((π·βπ)βπ) β€ π) β π = π) |
292 | 290, 291 | eqtr2d 2778 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π = πΎ β§ Β¬ ((π·βπ)βπ) β€ π) β π = if(((π·βπ)βπΎ) β€ π, ((π·βπ)βπΎ), π)) |
293 | 292 | adantll 712 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
((((((π β§ π β (πΎ(π»βπ)π)) β§ π β β) β§ π β π) β§ π = πΎ) β§ Β¬ ((π·βπ)βπ) β€ π) β π = if(((π·βπ)βπΎ) β€ π, ((π·βπ)βπΎ), π)) |
294 | 268 | adantlr 713 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((((π β§ π β β) β§ π β π) β§ π = πΎ) β if(((π·βπ)βπΎ) β€ π, ((π·βπ)βπΎ), π) = (((πβπ)β(π·βπ))βπ)) |
295 | 294 | adantl3r 748 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(((((π β§ π β (πΎ(π»βπ)π)) β§ π β β) β§ π β π) β§ π = πΎ) β if(((π·βπ)βπΎ) β€ π, ((π·βπ)βπΎ), π) = (((πβπ)β(π·βπ))βπ)) |
296 | 295 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
((((((π β§ π β (πΎ(π»βπ)π)) β§ π β β) β§ π β π) β§ π = πΎ) β§ Β¬ ((π·βπ)βπ) β€ π) β if(((π·βπ)βπΎ) β€ π, ((π·βπ)βπΎ), π) = (((πβπ)β(π·βπ))βπ)) |
297 | 293, 296 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
((((((π β§ π β (πΎ(π»βπ)π)) β§ π β β) β§ π β π) β§ π = πΎ) β§ Β¬ ((π·βπ)βπ) β€ π) β π = (((πβπ)β(π·βπ))βπ)) |
298 | 285, 297 | breqtrd 5129 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
((((((π β§ π β (πΎ(π»βπ)π)) β§ π β β) β§ π β π) β§ π = πΎ) β§ Β¬ ((π·βπ)βπ) β€ π) β (πβπ) < (((πβπ)β(π·βπ))βπ)) |
299 | 298 | adantl3r 748 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((((π β§ π β (πΎ(π»βπ)π)) β§ π β β) β§ π β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ))) β§ π β π) β§ π = πΎ) β§ Β¬ ((π·βπ)βπ) β€ π) β (πβπ) < (((πβπ)β(π·βπ))βπ)) |
300 | 273, 299 | pm2.61dan 811 |
. . . . . . . . . . . . . . . . . . . 20
β’
((((((π β§ π β (πΎ(π»βπ)π)) β§ π β β) β§ π β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ))) β§ π β π) β§ π = πΎ) β (πβπ) < (((πβπ)β(π·βπ))βπ)) |
301 | 201 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((((((π β§ π β (πΎ(π»βπ)π)) β§ π β β) β§ π β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ))) β§ π β π) β§ Β¬ π = πΎ) β (πβπ) < ((π·βπ)βπ)) |
302 | 237 | 3adant3 1132 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β§ π β β β§ π β π) β ((πβπ)β(π·βπ)) = (β β π β¦ if(β β (π β {πΎ}), ((π·βπ)ββ), if(((π·βπ)ββ) β€ π, ((π·βπ)ββ), π)))) |
303 | 249 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π β§ π β β β§ π β π) β§ β = π) β if(β β (π β {πΎ}), ((π·βπ)ββ), if(((π·βπ)ββ) β€ π, ((π·βπ)ββ), π)) = if(π β (π β {πΎ}), ((π·βπ)βπ), if(((π·βπ)βπ) β€ π, ((π·βπ)βπ), π))) |
304 | 255 | 3adant2 1131 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β§ π β β β§ π β π) β if(π β (π β {πΎ}), ((π·βπ)βπ), if(((π·βπ)βπ) β€ π, ((π·βπ)βπ), π)) β V) |
305 | 302, 303,
147, 304 | fvmptd 6952 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β§ π β β β§ π β π) β (((πβπ)β(π·βπ))βπ) = if(π β (π β {πΎ}), ((π·βπ)βπ), if(((π·βπ)βπ) β€ π, ((π·βπ)βπ), π))) |
306 | 305 | 3expa 1118 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β§ π β β) β§ π β π) β (((πβπ)β(π·βπ))βπ) = if(π β (π β {πΎ}), ((π·βπ)βπ), if(((π·βπ)βπ) β€ π, ((π·βπ)βπ), π))) |
307 | 306 | adantllr 717 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ π β (πΎ(π»βπ)π)) β§ π β β) β§ π β π) β (((πβπ)β(π·βπ))βπ) = if(π β (π β {πΎ}), ((π·βπ)βπ), if(((π·βπ)βπ) β€ π, ((π·βπ)βπ), π))) |
308 | 307 | ad4ant13 749 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
((((((π β§ π β (πΎ(π»βπ)π)) β§ π β β) β§ π β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ))) β§ π β π) β§ Β¬ π = πΎ) β (((πβπ)β(π·βπ))βπ) = if(π β (π β {πΎ}), ((π·βπ)βπ), if(((π·βπ)βπ) β€ π, ((π·βπ)βπ), π))) |
309 | | simpl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β π β§ Β¬ π = πΎ) β π β π) |
310 | | neqne 2949 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (Β¬
π = πΎ β π β πΎ) |
311 | | nelsn 4624 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β πΎ β Β¬ π β {πΎ}) |
312 | 310, 311 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (Β¬
π = πΎ β Β¬ π β {πΎ}) |
313 | 312 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β π β§ Β¬ π = πΎ) β Β¬ π β {πΎ}) |
314 | 309, 313 | eldifd 3919 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β π β§ Β¬ π = πΎ) β π β (π β {πΎ})) |
315 | 314 | iftrued 4492 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β π β§ Β¬ π = πΎ) β if(π β (π β {πΎ}), ((π·βπ)βπ), if(((π·βπ)βπ) β€ π, ((π·βπ)βπ), π)) = ((π·βπ)βπ)) |
316 | 315 | adantll 712 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
((((((π β§ π β (πΎ(π»βπ)π)) β§ π β β) β§ π β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ))) β§ π β π) β§ Β¬ π = πΎ) β if(π β (π β {πΎ}), ((π·βπ)βπ), if(((π·βπ)βπ) β€ π, ((π·βπ)βπ), π)) = ((π·βπ)βπ)) |
317 | 308, 316 | eqtr2d 2778 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((((((π β§ π β (πΎ(π»βπ)π)) β§ π β β) β§ π β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ))) β§ π β π) β§ Β¬ π = πΎ) β ((π·βπ)βπ) = (((πβπ)β(π·βπ))βπ)) |
318 | 301, 317 | breqtrd 5129 |
. . . . . . . . . . . . . . . . . . . 20
β’
((((((π β§ π β (πΎ(π»βπ)π)) β§ π β β) β§ π β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ))) β§ π β π) β§ Β¬ π = πΎ) β (πβπ) < (((πβπ)β(π·βπ))βπ)) |
319 | 300, 318 | pm2.61dan 811 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((π β§ π β (πΎ(π»βπ)π)) β§ π β β) β§ π β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ))) β§ π β π) β (πβπ) < (((πβπ)β(π·βπ))βπ)) |
320 | 150, 154,
182, 198, 319 | elicod 13268 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π β§ π β (πΎ(π»βπ)π)) β§ π β β) β§ π β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ))) β§ π β π) β (πβπ) β (((πΆβπ)βπ)[,)(((πβπ)β(π·βπ))βπ))) |
321 | 320 | ex 413 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π β (πΎ(π»βπ)π)) β§ π β β) β§ π β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ))) β (π β π β (πβπ) β (((πΆβπ)βπ)[,)(((πβπ)β(π·βπ))βπ)))) |
322 | 145, 321 | ralrimi 3238 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π β (πΎ(π»βπ)π)) β§ π β β) β§ π β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ))) β βπ β π (πβπ) β (((πΆβπ)βπ)[,)(((πβπ)β(π·βπ))βπ))) |
323 | 140, 322 | jca 512 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π β (πΎ(π»βπ)π)) β§ π β β) β§ π β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ))) β (π Fn π β§ βπ β π (πβπ) β (((πΆβπ)βπ)[,)(((πβπ)β(π·βπ))βπ)))) |
324 | 171 | elixp 8800 |
. . . . . . . . . . . . . . 15
β’ (π β Xπ β
π (((πΆβπ)βπ)[,)(((πβπ)β(π·βπ))βπ)) β (π Fn π β§ βπ β π (πβπ) β (((πΆβπ)βπ)[,)(((πβπ)β(π·βπ))βπ)))) |
325 | 323, 324 | sylibr 233 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π β (πΎ(π»βπ)π)) β§ π β β) β§ π β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ))) β π β Xπ β π (((πΆβπ)βπ)[,)(((πβπ)β(π·βπ))βπ))) |
326 | 325 | ex 413 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (πΎ(π»βπ)π)) β§ π β β) β (π β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ)) β π β Xπ β π (((πΆβπ)βπ)[,)(((πβπ)β(π·βπ))βπ)))) |
327 | 134, 137,
138, 326 | syl21anc 836 |
. . . . . . . . . . . 12
β’ (((π β§ π β (π΄ β© (πΎ(π»βπ)π))) β§ π β β) β (π β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ)) β π β Xπ β π (((πΆβπ)βπ)[,)(((πβπ)β(π·βπ))βπ)))) |
328 | 327 | reximdva 3163 |
. . . . . . . . . . 11
β’ ((π β§ π β (π΄ β© (πΎ(π»βπ)π))) β (βπ β β π β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ)) β βπ β β π β Xπ β π (((πΆβπ)βπ)[,)(((πβπ)β(π·βπ))βπ)))) |
329 | 133, 328 | mpd 15 |
. . . . . . . . . 10
β’ ((π β§ π β (π΄ β© (πΎ(π»βπ)π))) β βπ β β π β Xπ β π (((πΆβπ)βπ)[,)(((πβπ)β(π·βπ))βπ))) |
330 | | eliun 4956 |
. . . . . . . . . 10
β’ (π β βͺ π β β Xπ β π (((πΆβπ)βπ)[,)(((πβπ)β(π·βπ))βπ)) β βπ β β π β Xπ β π (((πΆβπ)βπ)[,)(((πβπ)β(π·βπ))βπ))) |
331 | 329, 330 | sylibr 233 |
. . . . . . . . 9
β’ ((π β§ π β (π΄ β© (πΎ(π»βπ)π))) β π β βͺ
π β β Xπ β
π (((πΆβπ)βπ)[,)(((πβπ)β(π·βπ))βπ))) |
332 | 331 | ralrimiva 3141 |
. . . . . . . 8
β’ (π β βπ β (π΄ β© (πΎ(π»βπ)π))π β βͺ
π β β Xπ β
π (((πΆβπ)βπ)[,)(((πβπ)β(π·βπ))βπ))) |
333 | | dfss3 3930 |
. . . . . . . 8
β’ ((π΄ β© (πΎ(π»βπ)π)) β βͺ π β β Xπ β π (((πΆβπ)βπ)[,)(((πβπ)β(π·βπ))βπ)) β βπ β (π΄ β© (πΎ(π»βπ)π))π β βͺ
π β β Xπ β
π (((πΆβπ)βπ)[,)(((πβπ)β(π·βπ))βπ))) |
334 | 332, 333 | sylibr 233 |
. . . . . . 7
β’ (π β (π΄ β© (πΎ(π»βπ)π)) β βͺ π β β Xπ β π (((πΆβπ)βπ)[,)(((πβπ)β(π·βπ))βπ))) |
335 | | eqidd 2738 |
. . . . . . . . . . . 12
β’ (π β β β (π β β β¦ ((πβπ)β(π·βπ))) = (π β β β¦ ((πβπ)β(π·βπ)))) |
336 | | 2fveq3 6844 |
. . . . . . . . . . . . 13
β’ (π = π β ((πβπ)β(π·βπ)) = ((πβπ)β(π·βπ))) |
337 | 336 | adantl 482 |
. . . . . . . . . . . 12
β’ ((π β β β§ π = π) β ((πβπ)β(π·βπ)) = ((πβπ)β(π·βπ))) |
338 | | id 22 |
. . . . . . . . . . . 12
β’ (π β β β π β
β) |
339 | | fvexd 6854 |
. . . . . . . . . . . 12
β’ (π β β β ((πβπ)β(π·βπ)) β V) |
340 | 335, 337,
338, 339 | fvmptd 6952 |
. . . . . . . . . . 11
β’ (π β β β ((π β β β¦ ((πβπ)β(π·βπ)))βπ) = ((πβπ)β(π·βπ))) |
341 | 340 | fveq1d 6841 |
. . . . . . . . . 10
β’ (π β β β (((π β β β¦ ((πβπ)β(π·βπ)))βπ)βπ) = (((πβπ)β(π·βπ))βπ)) |
342 | 341 | oveq2d 7367 |
. . . . . . . . 9
β’ (π β β β (((πΆβπ)βπ)[,)(((π β β β¦ ((πβπ)β(π·βπ)))βπ)βπ)) = (((πΆβπ)βπ)[,)(((πβπ)β(π·βπ))βπ))) |
343 | 342 | ixpeq2dv 8809 |
. . . . . . . 8
β’ (π β β β Xπ β
π (((πΆβπ)βπ)[,)(((π β β β¦ ((πβπ)β(π·βπ)))βπ)βπ)) = Xπ β π (((πΆβπ)βπ)[,)(((πβπ)β(π·βπ))βπ))) |
344 | 343 | iuneq2i 4973 |
. . . . . . 7
β’ βͺ π β β Xπ β π (((πΆβπ)βπ)[,)(((π β β β¦ ((πβπ)β(π·βπ)))βπ)βπ)) = βͺ
π β β Xπ β
π (((πΆβπ)βπ)[,)(((πβπ)β(π·βπ))βπ)) |
345 | 334, 344 | sseqtrrdi 3993 |
. . . . . 6
β’ (π β (π΄ β© (πΎ(π»βπ)π)) β βͺ π β β Xπ β π (((πΆβπ)βπ)[,)(((π β β β¦ ((πβπ)β(π·βπ)))βπ)βπ))) |
346 | 13, 15, 125, 345, 12 | ovnlecvr2 44752 |
. . . . 5
β’ (π β ((voln*βπ)β(π΄ β© (πΎ(π»βπ)π))) β€
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π β β β¦ ((πβπ)β(π·βπ)))βπ))))) |
347 | 340 | oveq2d 7367 |
. . . . . . . 8
β’ (π β β β ((πΆβπ)(πΏβπ)((π β β β¦ ((πβπ)β(π·βπ)))βπ)) = ((πΆβπ)(πΏβπ)((πβπ)β(π·βπ)))) |
348 | 347 | mpteq2ia 5206 |
. . . . . . 7
β’ (π β β β¦ ((πΆβπ)(πΏβπ)((π β β β¦ ((πβπ)β(π·βπ)))βπ))) = (π β β β¦ ((πΆβπ)(πΏβπ)((πβπ)β(π·βπ)))) |
349 | 348 | fveq2i 6842 |
. . . . . 6
β’
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π β β β¦ ((πβπ)β(π·βπ)))βπ)))) =
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((πβπ)β(π·βπ))))) |
350 | 349 | a1i 11 |
. . . . 5
β’ (π β
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π β β β¦ ((πβπ)β(π·βπ)))βπ)))) =
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((πβπ)β(π·βπ)))))) |
351 | 346, 350 | breqtrd 5129 |
. . . 4
β’ (π β ((voln*βπ)β(π΄ β© (πΎ(π»βπ)π))) β€
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((πβπ)β(π·βπ)))))) |
352 | 15 | ffvelcdmda 7031 |
. . . . . . . . . 10
β’ ((π β§ π β β) β (πΆβπ) β (β βm π)) |
353 | | elmapi 8745 |
. . . . . . . . . 10
β’ ((πΆβπ) β (β βm π) β (πΆβπ):πβΆβ) |
354 | 352, 353 | syl 17 |
. . . . . . . . 9
β’ ((π β§ π β β) β (πΆβπ):πβΆβ) |
355 | 97, 109, 110, 354 | hoidifhspf 44760 |
. . . . . . . 8
β’ ((π β§ π β β) β ((πβπ)β(πΆβπ)):πβΆβ) |
356 | | elmapg 8736 |
. . . . . . . . . 10
β’ ((β
β V β§ π β
Fin) β (((πβπ)β(πΆβπ)) β (β βm π) β ((πβπ)β(πΆβπ)):πβΆβ)) |
357 | 120, 356 | syl 17 |
. . . . . . . . 9
β’ (π β (((πβπ)β(πΆβπ)) β (β βm π) β ((πβπ)β(πΆβπ)):πβΆβ)) |
358 | 357 | adantr 481 |
. . . . . . . 8
β’ ((π β§ π β β) β (((πβπ)β(πΆβπ)) β (β βm π) β ((πβπ)β(πΆβπ)):πβΆβ)) |
359 | 355, 358 | mpbird 256 |
. . . . . . 7
β’ ((π β§ π β β) β ((πβπ)β(πΆβπ)) β (β βm π)) |
360 | 359 | fmpttd 7059 |
. . . . . 6
β’ (π β (π β β β¦ ((πβπ)β(πΆβπ))):ββΆ(β
βm π)) |
361 | | simpl 483 |
. . . . . . . . . . 11
β’ ((π β§ π β (π΄ β (πΎ(π»βπ)π))) β π) |
362 | | eldifi 4084 |
. . . . . . . . . . . 12
β’ (π β (π΄ β (πΎ(π»βπ)π)) β π β π΄) |
363 | 362 | adantl 482 |
. . . . . . . . . . 11
β’ ((π β§ π β (π΄ β (πΎ(π»βπ)π))) β π β π΄) |
364 | 361, 363,
132 | syl2anc 584 |
. . . . . . . . . 10
β’ ((π β§ π β (π΄ β (πΎ(π»βπ)π))) β βπ β β π β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ))) |
365 | 139 | adantl 482 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π β (π΄ β (πΎ(π»βπ)π))) β§ π β β) β§ π β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ))) β π Fn π) |
366 | | nfv 1917 |
. . . . . . . . . . . . . . . . 17
β’
β²π((π β§ π β (π΄ β (πΎ(π»βπ)π))) β§ π β β) |
367 | 366, 144 | nfan 1902 |
. . . . . . . . . . . . . . . 16
β’
β²π(((π β§ π β (π΄ β (πΎ(π»βπ)π))) β§ π β β) β§ π β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ))) |
368 | 98 | 3adant3 1132 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π β β β§ π β π) β ((πβπ)β(πΆβπ)):πβΆβ) |
369 | 368, 147 | ffvelcdmd 7032 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π β β β§ π β π) β (((πβπ)β(πΆβπ))βπ) β β) |
370 | 369 | rexrd 11163 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β β β§ π β π) β (((πβπ)β(πΆβπ))βπ) β
β*) |
371 | 370 | ad5ant135 1368 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π β§ π β (π΄ β (πΎ(π»βπ)π))) β§ π β β) β§ π β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ))) β§ π β π) β (((πβπ)β(πΆβπ))βπ) β
β*) |
372 | 187 | adantl3r 748 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π β§ π β (π΄ β (πΎ(π»βπ)π))) β§ π β β) β§ π β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ))) β§ π β π) β ((π·βπ)βπ) β
β*) |
373 | 148 | 3expa 1118 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β§ π β β) β§ π β π) β ((πΆβπ)βπ) β β) |
374 | 186 | 3expa 1118 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β§ π β β) β§ π β π) β ((π·βπ)βπ) β
β*) |
375 | | icossre 13299 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((πΆβπ)βπ) β β β§ ((π·βπ)βπ) β β*) β (((πΆβπ)βπ)[,)((π·βπ)βπ)) β β) |
376 | 373, 374,
375 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π β β) β§ π β π) β (((πΆβπ)βπ)[,)((π·βπ)βπ)) β β) |
377 | 376 | adantlr 713 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ π β β) β§ π β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ))) β§ π β π) β (((πΆβπ)βπ)[,)((π·βπ)βπ)) β β) |
378 | 377, 195 | sseldd 3943 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π β β) β§ π β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ))) β§ π β π) β (πβπ) β β) |
379 | 378 | rexrd 11163 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π β β) β§ π β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ))) β§ π β π) β (πβπ) β
β*) |
380 | 379 | adantl3r 748 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π β§ π β (π΄ β (πΎ(π»βπ)π))) β§ π β β) β§ π β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ))) β§ π β π) β (πβπ) β
β*) |
381 | 38 | 3adant3 1132 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ π β β β§ π β π) β π β β) |
382 | 14 | 3adant3 1132 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ π β β β§ π β π) β π β Fin) |
383 | 97, 381, 382, 146, 147 | hoidifhspval3 44761 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ π β β β§ π β π) β (((πβπ)β(πΆβπ))βπ) = if(π = πΎ, if(π β€ ((πΆβπ)βπ), ((πΆβπ)βπ), π), ((πΆβπ)βπ))) |
384 | 383 | ad5ant134 1367 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((((π β§ π β (π΄ β (πΎ(π»βπ)π))) β§ π β β) β§ π β π) β§ π = πΎ) β (((πβπ)β(πΆβπ))βπ) = if(π = πΎ, if(π β€ ((πΆβπ)βπ), ((πΆβπ)βπ), π), ((πΆβπ)βπ))) |
385 | | iftrue 4490 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π = πΎ β if(π = πΎ, if(π β€ ((πΆβπ)βπ), ((πΆβπ)βπ), π), ((πΆβπ)βπ)) = if(π β€ ((πΆβπ)βπ), ((πΆβπ)βπ), π)) |
386 | 385 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((((π β§ π β (π΄ β (πΎ(π»βπ)π))) β§ π β β) β§ π β π) β§ π = πΎ) β if(π = πΎ, if(π β€ ((πΆβπ)βπ), ((πΆβπ)βπ), π), ((πΆβπ)βπ)) = if(π β€ ((πΆβπ)βπ), ((πΆβπ)βπ), π)) |
387 | 384, 386 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((π β§ π β (π΄ β (πΎ(π»βπ)π))) β§ π β β) β§ π β π) β§ π = πΎ) β (((πβπ)β(πΆβπ))βπ) = if(π β€ ((πΆβπ)βπ), ((πΆβπ)βπ), π)) |
388 | 387 | adantllr 717 |
. . . . . . . . . . . . . . . . . . . 20
β’
((((((π β§ π β (π΄ β (πΎ(π»βπ)π))) β§ π β β) β§ π β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ))) β§ π β π) β§ π = πΎ) β (((πβπ)β(πΆβπ))βπ) = if(π β€ ((πΆβπ)βπ), ((πΆβπ)βπ), π)) |
389 | | iftrue 4490 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β€ ((πΆβπ)βπ) β if(π β€ ((πΆβπ)βπ), ((πΆβπ)βπ), π) = ((πΆβπ)βπ)) |
390 | 389 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((((((π β§ π β (π΄ β (πΎ(π»βπ)π))) β§ π β β) β§ π β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ))) β§ π β π) β§ π = πΎ) β§ π β€ ((πΆβπ)βπ)) β if(π β€ ((πΆβπ)βπ), ((πΆβπ)βπ), π) = ((πΆβπ)βπ)) |
391 | 197 | adantl3r 748 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(((((π β§ π β (π΄ β (πΎ(π»βπ)π))) β§ π β β) β§ π β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ))) β§ π β π) β ((πΆβπ)βπ) β€ (πβπ)) |
392 | 391 | ad2antrr 724 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((((((π β§ π β (π΄ β (πΎ(π»βπ)π))) β§ π β β) β§ π β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ))) β§ π β π) β§ π = πΎ) β§ π β€ ((πΆβπ)βπ)) β ((πΆβπ)βπ) β€ (πβπ)) |
393 | 390, 392 | eqbrtrd 5125 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((((π β§ π β (π΄ β (πΎ(π»βπ)π))) β§ π β β) β§ π β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ))) β§ π β π) β§ π = πΎ) β§ π β€ ((πΆβπ)βπ)) β if(π β€ ((πΆβπ)βπ), ((πΆβπ)βπ), π) β€ (πβπ)) |
394 | | iffalse 4493 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (Β¬
π β€ ((πΆβπ)βπ) β if(π β€ ((πΆβπ)βπ), ((πΆβπ)βπ), π) = π) |
395 | 394 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((((((π β§ π β (π΄ β (πΎ(π»βπ)π))) β§ π β β) β§ π β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ))) β§ π β π) β§ π = πΎ) β§ Β¬ π β€ ((πΆβπ)βπ)) β if(π β€ ((πΆβπ)βπ), ((πΆβπ)βπ), π) = π) |
396 | | simpl1 1191 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((((π β§ π β (π΄ β (πΎ(π»βπ)π))) β§ π β π β§ π = πΎ) β§ Β¬ π β€ (πβπ)) β (π β§ π β (π΄ β (πΎ(π»βπ)π)))) |
397 | | simpr 485 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((π = πΎ β§ Β¬ π β€ (πβπ)) β Β¬ π β€ (πβπ)) |
398 | | fveq2 6839 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (π = πΎ β (πβπ) = (πβπΎ)) |
399 | 398 | breq2d 5115 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (π = πΎ β (π β€ (πβπ) β π β€ (πβπΎ))) |
400 | 399 | notbid 317 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (π = πΎ β (Β¬ π β€ (πβπ) β Β¬ π β€ (πβπΎ))) |
401 | 400 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((π = πΎ β§ Β¬ π β€ (πβπ)) β (Β¬ π β€ (πβπ) β Β¬ π β€ (πβπΎ))) |
402 | 397, 401 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((π = πΎ β§ Β¬ π β€ (πβπ)) β Β¬ π β€ (πβπΎ)) |
403 | 402 | 3ad2antl3 1187 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((((π β§ π β (π΄ β (πΎ(π»βπ)π))) β§ π β π β§ π = πΎ) β§ Β¬ π β€ (πβπ)) β Β¬ π β€ (πβπΎ)) |
404 | 398 | eqcomd 2743 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (π = πΎ β (πβπΎ) = (πβπ)) |
405 | 404 | 3ad2ant3 1135 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (((π β§ π β (π΄ β (πΎ(π»βπ)π))) β§ π β π β§ π = πΎ) β (πβπΎ) = (πβπ)) |
406 | 364 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (((π β§ π β (π΄ β (πΎ(π»βπ)π))) β§ π β π) β βπ β β π β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ))) |
407 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’ ((π β§ π β β) β (π β§ π β β)) |
408 | 407 | ad4ant13 749 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ ((((π β§ π β π) β§ π β β) β§ π β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ))) β (π β§ π β β)) |
409 | | simpr 485 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ ((((π β§ π β π) β§ π β β) β§ π β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ))) β π β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ))) |
410 | 251 | ad2antrr 724 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ ((((π β§ π β π) β§ π β β) β§ π β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ))) β π β π) |
411 | 408, 409,
410, 378 | syl21anc 836 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ ((((π β§ π β π) β§ π β β) β§ π β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ))) β (πβπ) β β) |
412 | 411 | rexlimdva2 3152 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ ((π β§ π β π) β (βπ β β π β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ)) β (πβπ) β β)) |
413 | 412 | adantlr 713 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (((π β§ π β (π΄ β (πΎ(π»βπ)π))) β§ π β π) β (βπ β β π β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ)) β (πβπ) β β)) |
414 | 406, 413 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (((π β§ π β (π΄ β (πΎ(π»βπ)π))) β§ π β π) β (πβπ) β β) |
415 | 414 | 3adant3 1132 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (((π β§ π β (π΄ β (πΎ(π»βπ)π))) β§ π β π β§ π = πΎ) β (πβπ) β β) |
416 | 405, 415 | eqeltrd 2838 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (((π β§ π β (π΄ β (πΎ(π»βπ)π))) β§ π β π β§ π = πΎ) β (πβπΎ) β β) |
417 | 416 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((((π β§ π β (π΄ β (πΎ(π»βπ)π))) β§ π β π β§ π = πΎ) β§ Β¬ π β€ (πβπ)) β (πβπΎ) β β) |
418 | 396, 361,
37 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((((π β§ π β (π΄ β (πΎ(π»βπ)π))) β§ π β π β§ π = πΎ) β§ Β¬ π β€ (πβπ)) β π β β) |
419 | 417, 418 | ltnled 11260 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((((π β§ π β (π΄ β (πΎ(π»βπ)π))) β§ π β π β§ π = πΎ) β§ Β¬ π β€ (πβπ)) β ((πβπΎ) < π β Β¬ π β€ (πβπΎ))) |
420 | 403, 419 | mpbird 256 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((((π β§ π β (π΄ β (πΎ(π»βπ)π))) β§ π β π β§ π = πΎ) β§ Β¬ π β€ (πβπ)) β (πβπΎ) < π) |
421 | 365, 364 | r19.29a 3157 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((π β§ π β (π΄ β (πΎ(π»βπ)π))) β π Fn π) |
422 | 421 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (((π β§ π β (π΄ β (πΎ(π»βπ)π))) β§ (πβπΎ) < π) β π Fn π) |
423 | 274 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’
(((((π β§ π β (π΄ β (πΎ(π»βπ)π))) β§ (πβπΎ) < π) β§ π β π) β§ π = πΎ) β -β β
β*) |
424 | 276 | ad4antr 730 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’
(((((π β§ π β (π΄ β (πΎ(π»βπ)π))) β§ (πβπΎ) < π) β§ π β π) β§ π = πΎ) β π β
β*) |
425 | 414 | ad4ant13 749 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’
(((((π β§ π β (π΄ β (πΎ(π»βπ)π))) β§ (πβπΎ) < π) β§ π β π) β§ π = πΎ) β (πβπ) β β) |
426 | 425 | mnfltd 12999 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’
(((((π β§ π β (π΄ β (πΎ(π»βπ)π))) β§ (πβπΎ) < π) β§ π β π) β§ π = πΎ) β -β < (πβπ)) |
427 | 398 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ (((πβπΎ) < π β§ π = πΎ) β (πβπ) = (πβπΎ)) |
428 | | simpl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ (((πβπΎ) < π β§ π = πΎ) β (πβπΎ) < π) |
429 | 427, 428 | eqbrtrd 5125 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (((πβπΎ) < π β§ π = πΎ) β (πβπ) < π) |
430 | 429 | ad4ant24 752 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’
(((((π β§ π β (π΄ β (πΎ(π»βπ)π))) β§ (πβπΎ) < π) β§ π β π) β§ π = πΎ) β (πβπ) < π) |
431 | 423, 424,
425, 426, 430 | eliood 43637 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’
(((((π β§ π β (π΄ β (πΎ(π»βπ)π))) β§ (πβπΎ) < π) β§ π β π) β§ π = πΎ) β (πβπ) β (-β(,)π)) |
432 | 155 | eqcomd 2743 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (π = πΎ β (-β(,)π) = if(π = πΎ, (-β(,)π), β)) |
433 | 432 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’
(((((π β§ π β (π΄ β (πΎ(π»βπ)π))) β§ (πβπΎ) < π) β§ π β π) β§ π = πΎ) β (-β(,)π) = if(π = πΎ, (-β(,)π), β)) |
434 | 431, 433 | eleqtrd 2840 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’
(((((π β§ π β (π΄ β (πΎ(π»βπ)π))) β§ (πβπΎ) < π) β§ π β π) β§ π = πΎ) β (πβπ) β if(π = πΎ, (-β(,)π), β)) |
435 | 414 | ad4ant13 749 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’
(((((π β§ π β (π΄ β (πΎ(π»βπ)π))) β§ (πβπΎ) < π) β§ π β π) β§ Β¬ π = πΎ) β (πβπ) β β) |
436 | 159 | eqcomd 2743 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (Β¬
π = πΎ β β = if(π = πΎ, (-β(,)π), β)) |
437 | 436 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’
(((((π β§ π β (π΄ β (πΎ(π»βπ)π))) β§ (πβπΎ) < π) β§ π β π) β§ Β¬ π = πΎ) β β = if(π = πΎ, (-β(,)π), β)) |
438 | 435, 437 | eleqtrd 2840 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’
(((((π β§ π β (π΄ β (πΎ(π»βπ)π))) β§ (πβπΎ) < π) β§ π β π) β§ Β¬ π = πΎ) β (πβπ) β if(π = πΎ, (-β(,)π), β)) |
439 | 434, 438 | pm2.61dan 811 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((((π β§ π β (π΄ β (πΎ(π»βπ)π))) β§ (πβπΎ) < π) β§ π β π) β (πβπ) β if(π = πΎ, (-β(,)π), β)) |
440 | 439 | ralrimiva 3141 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (((π β§ π β (π΄ β (πΎ(π»βπ)π))) β§ (πβπΎ) < π) β βπ β π (πβπ) β if(π = πΎ, (-β(,)π), β)) |
441 | 422, 440 | jca 512 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (((π β§ π β (π΄ β (πΎ(π»βπ)π))) β§ (πβπΎ) < π) β (π Fn π β§ βπ β π (πβπ) β if(π = πΎ, (-β(,)π), β))) |
442 | 396, 420,
441 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((((π β§ π β (π΄ β (πΎ(π»βπ)π))) β§ π β π β§ π = πΎ) β§ Β¬ π β€ (πβπ)) β (π Fn π β§ βπ β π (πβπ) β if(π = πΎ, (-β(,)π), β))) |
443 | 442, 172 | sylibr 233 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((((π β§ π β (π΄ β (πΎ(π»βπ)π))) β§ π β π β§ π = πΎ) β§ Β¬ π β€ (πβπ)) β π β Xπ β π if(π = πΎ, (-β(,)π), β)) |
444 | 166 | eqcomd 2743 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π β Xπ β
π if(π = πΎ, (-β(,)π), β) = (πΎ(π»βπ)π)) |
445 | 444 | ad2antrr 724 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (((π β§ π β (π΄ β (πΎ(π»βπ)π))) β§ Β¬ π β€ (πβπ)) β Xπ β π if(π = πΎ, (-β(,)π), β) = (πΎ(π»βπ)π)) |
446 | 445 | 3ad2antl1 1185 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((((π β§ π β (π΄ β (πΎ(π»βπ)π))) β§ π β π β§ π = πΎ) β§ Β¬ π β€ (πβπ)) β Xπ β π if(π = πΎ, (-β(,)π), β) = (πΎ(π»βπ)π)) |
447 | 443, 446 | eleqtrd 2840 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π β§ π β (π΄ β (πΎ(π»βπ)π))) β§ π β π β§ π = πΎ) β§ Β¬ π β€ (πβπ)) β π β (πΎ(π»βπ)π)) |
448 | | eldifn 4085 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π β (π΄ β (πΎ(π»βπ)π)) β Β¬ π β (πΎ(π»βπ)π)) |
449 | 448 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β§ π β (π΄ β (πΎ(π»βπ)π))) β Β¬ π β (πΎ(π»βπ)π)) |
450 | 449 | 3ad2ant1 1133 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π β§ π β (π΄ β (πΎ(π»βπ)π))) β§ π β π β§ π = πΎ) β Β¬ π β (πΎ(π»βπ)π)) |
451 | 450 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π β§ π β (π΄ β (πΎ(π»βπ)π))) β§ π β π β§ π = πΎ) β§ Β¬ π β€ (πβπ)) β Β¬ π β (πΎ(π»βπ)π)) |
452 | 447, 451 | condan 816 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β§ π β (π΄ β (πΎ(π»βπ)π))) β§ π β π β§ π = πΎ) β π β€ (πβπ)) |
453 | 452 | ad5ant145 1369 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
((((((π β§ π β (π΄ β (πΎ(π»βπ)π))) β§ π β β) β§ π β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ))) β§ π β π) β§ π = πΎ) β π β€ (πβπ)) |
454 | 453 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((((((π β§ π β (π΄ β (πΎ(π»βπ)π))) β§ π β β) β§ π β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ))) β§ π β π) β§ π = πΎ) β§ Β¬ π β€ ((πΆβπ)βπ)) β π β€ (πβπ)) |
455 | 395, 454 | eqbrtrd 5125 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((((π β§ π β (π΄ β (πΎ(π»βπ)π))) β§ π β β) β§ π β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ))) β§ π β π) β§ π = πΎ) β§ Β¬ π β€ ((πΆβπ)βπ)) β if(π β€ ((πΆβπ)βπ), ((πΆβπ)βπ), π) β€ (πβπ)) |
456 | 393, 455 | pm2.61dan 811 |
. . . . . . . . . . . . . . . . . . . 20
β’
((((((π β§ π β (π΄ β (πΎ(π»βπ)π))) β§ π β β) β§ π β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ))) β§ π β π) β§ π = πΎ) β if(π β€ ((πΆβπ)βπ), ((πΆβπ)βπ), π) β€ (πβπ)) |
457 | 388, 456 | eqbrtrd 5125 |
. . . . . . . . . . . . . . . . . . 19
β’
((((((π β§ π β (π΄ β (πΎ(π»βπ)π))) β§ π β β) β§ π β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ))) β§ π β π) β§ π = πΎ) β (((πβπ)β(πΆβπ))βπ) β€ (πβπ)) |
458 | 383 | ad5ant124 1365 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((((π β§ π β β) β§ π β Xπ β
π (((πΆβπ)βπ)[,)((π·βπ)βπ))) β§ π β π) β§ Β¬ π = πΎ) β (((πβπ)β(πΆβπ))βπ) = if(π = πΎ, if(π β€ ((πΆβπ)βπ), ((πΆβπ)βπ), π), ((πΆβπ)βπ))) |
459 | | iffalse 4493 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (Β¬
π = πΎ β if(π = πΎ, if(π β€ ((πΆβπ)βπ), ((πΆβπ)βπ), π), ((πΆβπ)βπ)) = ((πΆβπ)βπ)) |
460 | 459 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((((π β§ π β β) β§ π β Xπ β
π (((πΆβπ)βπ)[,)((π·βπ)βπ))) β§ π β π) β§ Β¬ π = πΎ) β if(π = πΎ, if(π β€ ((πΆβπ)βπ), ((πΆβπ)βπ), π), ((πΆβπ)βπ)) = ((πΆβπ)βπ)) |
461 | 458, 460 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((π β§ π β β) β§ π β Xπ β
π (((πΆβπ)βπ)[,)((π·βπ)βπ))) β§ π β π) β§ Β¬ π = πΎ) β (((πβπ)β(πΆβπ))βπ) = ((πΆβπ)βπ)) |
462 | 197 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((π β§ π β β) β§ π β Xπ β
π (((πΆβπ)βπ)[,)((π·βπ)βπ))) β§ π β π) β§ Β¬ π = πΎ) β ((πΆβπ)βπ) β€ (πβπ)) |
463 | 461, 462 | eqbrtrd 5125 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((π β§ π β β) β§ π β Xπ β
π (((πΆβπ)βπ)[,)((π·βπ)βπ))) β§ π β π) β§ Β¬ π = πΎ) β (((πβπ)β(πΆβπ))βπ) β€ (πβπ)) |
464 | 463 | adantl4r 753 |
. . . . . . . . . . . . . . . . . . 19
β’
((((((π β§ π β (π΄ β (πΎ(π»βπ)π))) β§ π β β) β§ π β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ))) β§ π β π) β§ Β¬ π = πΎ) β (((πβπ)β(πΆβπ))βπ) β€ (πβπ)) |
465 | 457, 464 | pm2.61dan 811 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π β§ π β (π΄ β (πΎ(π»βπ)π))) β§ π β β) β§ π β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ))) β§ π β π) β (((πβπ)β(πΆβπ))βπ) β€ (πβπ)) |
466 | 200 | adantl3r 748 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π β§ π β (π΄ β (πΎ(π»βπ)π))) β§ π β β) β§ π β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ))) β§ π β π) β (πβπ) < ((π·βπ)βπ)) |
467 | 371, 372,
380, 465, 466 | elicod 13268 |
. . . . . . . . . . . . . . . . 17
β’
(((((π β§ π β (π΄ β (πΎ(π»βπ)π))) β§ π β β) β§ π β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ))) β§ π β π) β (πβπ) β ((((πβπ)β(πΆβπ))βπ)[,)((π·βπ)βπ))) |
468 | 467 | ex 413 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π β (π΄ β (πΎ(π»βπ)π))) β§ π β β) β§ π β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ))) β (π β π β (πβπ) β ((((πβπ)β(πΆβπ))βπ)[,)((π·βπ)βπ)))) |
469 | 367, 468 | ralrimi 3238 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π β (π΄ β (πΎ(π»βπ)π))) β§ π β β) β§ π β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ))) β βπ β π (πβπ) β ((((πβπ)β(πΆβπ))βπ)[,)((π·βπ)βπ))) |
470 | 365, 469 | jca 512 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π β (π΄ β (πΎ(π»βπ)π))) β§ π β β) β§ π β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ))) β (π Fn π β§ βπ β π (πβπ) β ((((πβπ)β(πΆβπ))βπ)[,)((π·βπ)βπ)))) |
471 | 171 | elixp 8800 |
. . . . . . . . . . . . . 14
β’ (π β Xπ β
π ((((πβπ)β(πΆβπ))βπ)[,)((π·βπ)βπ)) β (π Fn π β§ βπ β π (πβπ) β ((((πβπ)β(πΆβπ))βπ)[,)((π·βπ)βπ)))) |
472 | 470, 471 | sylibr 233 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β (π΄ β (πΎ(π»βπ)π))) β§ π β β) β§ π β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ))) β π β Xπ β π ((((πβπ)β(πΆβπ))βπ)[,)((π·βπ)βπ))) |
473 | | eqidd 2738 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β β β (π β β β¦ ((πβπ)β(πΆβπ))) = (π β β β¦ ((πβπ)β(πΆβπ)))) |
474 | | 2fveq3 6844 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = π β ((πβπ)β(πΆβπ)) = ((πβπ)β(πΆβπ))) |
475 | 474 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β β β§ π = π) β ((πβπ)β(πΆβπ)) = ((πβπ)β(πΆβπ))) |
476 | | fvexd 6854 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β β β ((πβπ)β(πΆβπ)) β V) |
477 | 473, 475,
338, 476 | fvmptd 6952 |
. . . . . . . . . . . . . . . . . 18
β’ (π β β β ((π β β β¦ ((πβπ)β(πΆβπ)))βπ) = ((πβπ)β(πΆβπ))) |
478 | 477 | fveq1d 6841 |
. . . . . . . . . . . . . . . . 17
β’ (π β β β (((π β β β¦ ((πβπ)β(πΆβπ)))βπ)βπ) = (((πβπ)β(πΆβπ))βπ)) |
479 | 478 | oveq1d 7366 |
. . . . . . . . . . . . . . . 16
β’ (π β β β ((((π β β β¦ ((πβπ)β(πΆβπ)))βπ)βπ)[,)((π·βπ)βπ)) = ((((πβπ)β(πΆβπ))βπ)[,)((π·βπ)βπ))) |
480 | 479 | ixpeq2dv 8809 |
. . . . . . . . . . . . . . 15
β’ (π β β β Xπ β
π ((((π β β β¦ ((πβπ)β(πΆβπ)))βπ)βπ)[,)((π·βπ)βπ)) = Xπ β π ((((πβπ)β(πΆβπ))βπ)[,)((π·βπ)βπ))) |
481 | 480 | ad2antlr 725 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π β (π΄ β (πΎ(π»βπ)π))) β§ π β β) β§ π β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ))) β Xπ β π ((((π β β β¦ ((πβπ)β(πΆβπ)))βπ)βπ)[,)((π·βπ)βπ)) = Xπ β π ((((πβπ)β(πΆβπ))βπ)[,)((π·βπ)βπ))) |
482 | 481 | eleq2d 2823 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β (π΄ β (πΎ(π»βπ)π))) β§ π β β) β§ π β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ))) β (π β Xπ β π ((((π β β β¦ ((πβπ)β(πΆβπ)))βπ)βπ)[,)((π·βπ)βπ)) β π β Xπ β π ((((πβπ)β(πΆβπ))βπ)[,)((π·βπ)βπ)))) |
483 | 472, 482 | mpbird 256 |
. . . . . . . . . . . 12
β’ ((((π β§ π β (π΄ β (πΎ(π»βπ)π))) β§ π β β) β§ π β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ))) β π β Xπ β π ((((π β β β¦ ((πβπ)β(πΆβπ)))βπ)βπ)[,)((π·βπ)βπ))) |
484 | 483 | ex 413 |
. . . . . . . . . . 11
β’ (((π β§ π β (π΄ β (πΎ(π»βπ)π))) β§ π β β) β (π β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ)) β π β Xπ β π ((((π β β β¦ ((πβπ)β(πΆβπ)))βπ)βπ)[,)((π·βπ)βπ)))) |
485 | 484 | reximdva 3163 |
. . . . . . . . . 10
β’ ((π β§ π β (π΄ β (πΎ(π»βπ)π))) β (βπ β β π β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ)) β βπ β β π β Xπ β π ((((π β β β¦ ((πβπ)β(πΆβπ)))βπ)βπ)[,)((π·βπ)βπ)))) |
486 | 364, 485 | mpd 15 |
. . . . . . . . 9
β’ ((π β§ π β (π΄ β (πΎ(π»βπ)π))) β βπ β β π β Xπ β π ((((π β β β¦ ((πβπ)β(πΆβπ)))βπ)βπ)[,)((π·βπ)βπ))) |
487 | | eliun 4956 |
. . . . . . . . 9
β’ (π β βͺ π β β Xπ β π ((((π β β β¦ ((πβπ)β(πΆβπ)))βπ)βπ)[,)((π·βπ)βπ)) β βπ β β π β Xπ β π ((((π β β β¦ ((πβπ)β(πΆβπ)))βπ)βπ)[,)((π·βπ)βπ))) |
488 | 486, 487 | sylibr 233 |
. . . . . . . 8
β’ ((π β§ π β (π΄ β (πΎ(π»βπ)π))) β π β βͺ
π β β Xπ β
π ((((π β β β¦ ((πβπ)β(πΆβπ)))βπ)βπ)[,)((π·βπ)βπ))) |
489 | 488 | ralrimiva 3141 |
. . . . . . 7
β’ (π β βπ β (π΄ β (πΎ(π»βπ)π))π β βͺ
π β β Xπ β
π ((((π β β β¦ ((πβπ)β(πΆβπ)))βπ)βπ)[,)((π·βπ)βπ))) |
490 | | dfss3 3930 |
. . . . . . 7
β’ ((π΄ β (πΎ(π»βπ)π)) β βͺ π β β Xπ β π ((((π β β β¦ ((πβπ)β(πΆβπ)))βπ)βπ)[,)((π·βπ)βπ)) β βπ β (π΄ β (πΎ(π»βπ)π))π β βͺ
π β β Xπ β
π ((((π β β β¦ ((πβπ)β(πΆβπ)))βπ)βπ)[,)((π·βπ)βπ))) |
491 | 489, 490 | sylibr 233 |
. . . . . 6
β’ (π β (π΄ β (πΎ(π»βπ)π)) β βͺ π β β Xπ β π ((((π β β β¦ ((πβπ)β(πΆβπ)))βπ)βπ)[,)((π·βπ)βπ))) |
492 | 13, 360, 19, 491, 12 | ovnlecvr2 44752 |
. . . . 5
β’ (π β ((voln*βπ)β(π΄ β (πΎ(π»βπ)π))) β€
(Ξ£^β(π β β β¦ (((π β β β¦ ((πβπ)β(πΆβπ)))βπ)(πΏβπ)(π·βπ))))) |
493 | 477 | oveq1d 7366 |
. . . . . . . 8
β’ (π β β β (((π β β β¦ ((πβπ)β(πΆβπ)))βπ)(πΏβπ)(π·βπ)) = (((πβπ)β(πΆβπ))(πΏβπ)(π·βπ))) |
494 | 493 | mpteq2ia 5206 |
. . . . . . 7
β’ (π β β β¦ (((π β β β¦ ((πβπ)β(πΆβπ)))βπ)(πΏβπ)(π·βπ))) = (π β β β¦ (((πβπ)β(πΆβπ))(πΏβπ)(π·βπ))) |
495 | 494 | fveq2i 6842 |
. . . . . 6
β’
(Ξ£^β(π β β β¦ (((π β β β¦ ((πβπ)β(πΆβπ)))βπ)(πΏβπ)(π·βπ)))) =
(Ξ£^β(π β β β¦ (((πβπ)β(πΆβπ))(πΏβπ)(π·βπ)))) |
496 | 495 | a1i 11 |
. . . . 5
β’ (π β
(Ξ£^β(π β β β¦ (((π β β β¦ ((πβπ)β(πΆβπ)))βπ)(πΏβπ)(π·βπ)))) =
(Ξ£^β(π β β β¦ (((πβπ)β(πΆβπ))(πΏβπ)(π·βπ))))) |
497 | 492, 496 | breqtrd 5129 |
. . . 4
β’ (π β ((voln*βπ)β(π΄ β (πΎ(π»βπ)π))) β€
(Ξ£^β(π β β β¦ (((πβπ)β(πΆβπ))(πΏβπ)(π·βπ))))) |
498 | 1, 2, 96, 108, 351, 497 | leadd12dd 43455 |
. . 3
β’ (π β (((voln*βπ)β(π΄ β© (πΎ(π»βπ)π))) + ((voln*βπ)β(π΄ β (πΎ(π»βπ)π)))) β€
((Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((πβπ)β(π·βπ))))) +
(Ξ£^β(π β β β¦ (((πβπ)β(πΆβπ))(πΏβπ)(π·βπ)))))) |
499 | 14, 105, 38, 18, 22, 12, 36, 97 | hspmbllem1 44768 |
. . . . . 6
β’ ((π β§ π β β) β ((πΆβπ)(πΏβπ)(π·βπ)) = (((πΆβπ)(πΏβπ)((πβπ)β(π·βπ))) +π (((πβπ)β(πΆβπ))(πΏβπ)(π·βπ)))) |
500 | 499 | mpteq2dva 5203 |
. . . . 5
β’ (π β (π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ))) = (π β β β¦ (((πΆβπ)(πΏβπ)((πβπ)β(π·βπ))) +π (((πβπ)β(πΆβπ))(πΏβπ)(π·βπ))))) |
501 | 500 | fveq2d 6843 |
. . . 4
β’ (π β
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) =
(Ξ£^β(π β β β¦ (((πΆβπ)(πΏβπ)((πβπ)β(π·βπ))) +π (((πβπ)β(πΆβπ))(πΏβπ)(π·βπ)))))) |
502 | 8, 10, 41, 104 | sge0xadd 44577 |
. . . 4
β’ (π β
(Ξ£^β(π β β β¦ (((πΆβπ)(πΏβπ)((πβπ)β(π·βπ))) +π (((πβπ)β(πΆβπ))(πΏβπ)(π·βπ))))) =
((Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((πβπ)β(π·βπ))))) +π
(Ξ£^β(π β β β¦ (((πβπ)β(πΆβπ))(πΏβπ)(π·βπ)))))) |
503 | 96, 108 | rexaddd 13107 |
. . . 4
β’ (π β
((Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((πβπ)β(π·βπ))))) +π
(Ξ£^β(π β β β¦ (((πβπ)β(πΆβπ))(πΏβπ)(π·βπ))))) =
((Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((πβπ)β(π·βπ))))) +
(Ξ£^β(π β β β¦ (((πβπ)β(πΆβπ))(πΏβπ)(π·βπ)))))) |
504 | 501, 502,
503 | 3eqtrrd 2782 |
. . 3
β’ (π β
((Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((πβπ)β(π·βπ))))) +
(Ξ£^β(π β β β¦ (((πβπ)β(πΆβπ))(πΏβπ)(π·βπ))))) =
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ))))) |
505 | 498, 504 | breqtrd 5129 |
. 2
β’ (π β (((voln*βπ)β(π΄ β© (πΎ(π»βπ)π))) + ((voln*βπ)β(π΄ β (πΎ(π»βπ)π)))) β€
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ))))) |
506 | 3, 35, 7, 505, 34 | letrd 11270 |
1
β’ (π β (((voln*βπ)β(π΄ β© (πΎ(π»βπ)π))) + ((voln*βπ)β(π΄ β (πΎ(π»βπ)π)))) β€ (((voln*βπ)βπ΄) + πΈ)) |