Step | Hyp | Ref
| Expression |
1 | | id 22 |
. 2
β’ (π β π) |
2 | | hoidmvval0.j |
. . 3
β’ (π β βπ β π (π΅βπ) β€ (π΄βπ)) |
3 | | fveq2 6888 |
. . . . . 6
β’ (π = π β (π΅βπ) = (π΅βπ)) |
4 | | fveq2 6888 |
. . . . . 6
β’ (π = π β (π΄βπ) = (π΄βπ)) |
5 | 3, 4 | breq12d 5160 |
. . . . 5
β’ (π = π β ((π΅βπ) β€ (π΄βπ) β (π΅βπ) β€ (π΄βπ))) |
6 | 5 | cbvrexvw 3236 |
. . . 4
β’
(βπ β
π (π΅βπ) β€ (π΄βπ) β βπ β π (π΅βπ) β€ (π΄βπ)) |
7 | | rexn0 4509 |
. . . 4
β’
(βπ β
π (π΅βπ) β€ (π΄βπ) β π β β
) |
8 | 6, 7 | sylbir 234 |
. . 3
β’
(βπ β
π (π΅βπ) β€ (π΄βπ) β π β β
) |
9 | 2, 8 | syl 17 |
. 2
β’ (π β π β β
) |
10 | | hoidmvval0.l |
. . . 4
β’ πΏ = (π₯ β Fin β¦ (π β (β βm π₯), π β (β βm π₯) β¦ if(π₯ = β
, 0, βπ β π₯ (volβ((πβπ)[,)(πβπ)))))) |
11 | | hoidmvval0.x |
. . . . 5
β’ (π β π β Fin) |
12 | 11 | adantr 482 |
. . . 4
β’ ((π β§ π β β
) β π β Fin) |
13 | | simpr 486 |
. . . 4
β’ ((π β§ π β β
) β π β β
) |
14 | | hoidmvval0.a |
. . . . 5
β’ (π β π΄:πβΆβ) |
15 | 14 | adantr 482 |
. . . 4
β’ ((π β§ π β β
) β π΄:πβΆβ) |
16 | | hoidmvval0.b |
. . . . 5
β’ (π β π΅:πβΆβ) |
17 | 16 | adantr 482 |
. . . 4
β’ ((π β§ π β β
) β π΅:πβΆβ) |
18 | 10, 12, 13, 15, 17 | hoidmvn0val 45235 |
. . 3
β’ ((π β§ π β β
) β (π΄(πΏβπ)π΅) = βπ β π (volβ((π΄βπ)[,)(π΅βπ)))) |
19 | 2 | adantr 482 |
. . . 4
β’ ((π β§ π β β
) β βπ β π (π΅βπ) β€ (π΄βπ)) |
20 | | hoidmvval0.p |
. . . . . 6
β’
β²ππ |
21 | | nfv 1918 |
. . . . . 6
β’
β²π π β β
|
22 | 20, 21 | nfan 1903 |
. . . . 5
β’
β²π(π β§ π β β
) |
23 | | nfv 1918 |
. . . . 5
β’
β²πβπ β π (volβ((π΄βπ)[,)(π΅βπ))) = 0 |
24 | | nfv 1918 |
. . . . . . . 8
β’
β²π(π β§ π β π β§ (π΅βπ) β€ (π΄βπ)) |
25 | | nfcv 2904 |
. . . . . . . 8
β’
β²π(volβ((π΄βπ)[,)(π΅βπ))) |
26 | 11 | 3ad2ant1 1134 |
. . . . . . . 8
β’ ((π β§ π β π β§ (π΅βπ) β€ (π΄βπ)) β π β Fin) |
27 | 14 | ffvelcdmda 7082 |
. . . . . . . . . . 11
β’ ((π β§ π β π) β (π΄βπ) β β) |
28 | 16 | ffvelcdmda 7082 |
. . . . . . . . . . 11
β’ ((π β§ π β π) β (π΅βπ) β β) |
29 | | volicore 45232 |
. . . . . . . . . . 11
β’ (((π΄βπ) β β β§ (π΅βπ) β β) β (volβ((π΄βπ)[,)(π΅βπ))) β β) |
30 | 27, 28, 29 | syl2anc 585 |
. . . . . . . . . 10
β’ ((π β§ π β π) β (volβ((π΄βπ)[,)(π΅βπ))) β β) |
31 | 30 | recnd 11238 |
. . . . . . . . 9
β’ ((π β§ π β π) β (volβ((π΄βπ)[,)(π΅βπ))) β β) |
32 | 31 | 3ad2antl1 1186 |
. . . . . . . 8
β’ (((π β§ π β π β§ (π΅βπ) β€ (π΄βπ)) β§ π β π) β (volβ((π΄βπ)[,)(π΅βπ))) β β) |
33 | 4, 3 | oveq12d 7422 |
. . . . . . . . 9
β’ (π = π β ((π΄βπ)[,)(π΅βπ)) = ((π΄βπ)[,)(π΅βπ))) |
34 | 33 | fveq2d 6892 |
. . . . . . . 8
β’ (π = π β (volβ((π΄βπ)[,)(π΅βπ))) = (volβ((π΄βπ)[,)(π΅βπ)))) |
35 | | simp2 1138 |
. . . . . . . 8
β’ ((π β§ π β π β§ (π΅βπ) β€ (π΄βπ)) β π β π) |
36 | 14 | ffvelcdmda 7082 |
. . . . . . . . . . 11
β’ ((π β§ π β π) β (π΄βπ) β β) |
37 | 36 | 3adant3 1133 |
. . . . . . . . . 10
β’ ((π β§ π β π β§ (π΅βπ) β€ (π΄βπ)) β (π΄βπ) β β) |
38 | 16 | ffvelcdmda 7082 |
. . . . . . . . . . 11
β’ ((π β§ π β π) β (π΅βπ) β β) |
39 | 38 | 3adant3 1133 |
. . . . . . . . . 10
β’ ((π β§ π β π β§ (π΅βπ) β€ (π΄βπ)) β (π΅βπ) β β) |
40 | | volico 44634 |
. . . . . . . . . 10
β’ (((π΄βπ) β β β§ (π΅βπ) β β) β (volβ((π΄βπ)[,)(π΅βπ))) = if((π΄βπ) < (π΅βπ), ((π΅βπ) β (π΄βπ)), 0)) |
41 | 37, 39, 40 | syl2anc 585 |
. . . . . . . . 9
β’ ((π β§ π β π β§ (π΅βπ) β€ (π΄βπ)) β (volβ((π΄βπ)[,)(π΅βπ))) = if((π΄βπ) < (π΅βπ), ((π΅βπ) β (π΄βπ)), 0)) |
42 | | simp3 1139 |
. . . . . . . . . . 11
β’ ((π β§ π β π β§ (π΅βπ) β€ (π΄βπ)) β (π΅βπ) β€ (π΄βπ)) |
43 | 39, 37 | lenltd 11356 |
. . . . . . . . . . 11
β’ ((π β§ π β π β§ (π΅βπ) β€ (π΄βπ)) β ((π΅βπ) β€ (π΄βπ) β Β¬ (π΄βπ) < (π΅βπ))) |
44 | 42, 43 | mpbid 231 |
. . . . . . . . . 10
β’ ((π β§ π β π β§ (π΅βπ) β€ (π΄βπ)) β Β¬ (π΄βπ) < (π΅βπ)) |
45 | 44 | iffalsed 4538 |
. . . . . . . . 9
β’ ((π β§ π β π β§ (π΅βπ) β€ (π΄βπ)) β if((π΄βπ) < (π΅βπ), ((π΅βπ) β (π΄βπ)), 0) = 0) |
46 | 41, 45 | eqtrd 2773 |
. . . . . . . 8
β’ ((π β§ π β π β§ (π΅βπ) β€ (π΄βπ)) β (volβ((π΄βπ)[,)(π΅βπ))) = 0) |
47 | 24, 25, 26, 32, 34, 35, 46 | fprod0 44247 |
. . . . . . 7
β’ ((π β§ π β π β§ (π΅βπ) β€ (π΄βπ)) β βπ β π (volβ((π΄βπ)[,)(π΅βπ))) = 0) |
48 | 47 | 3adant1r 1178 |
. . . . . 6
β’ (((π β§ π β β
) β§ π β π β§ (π΅βπ) β€ (π΄βπ)) β βπ β π (volβ((π΄βπ)[,)(π΅βπ))) = 0) |
49 | 48 | 3exp 1120 |
. . . . 5
β’ ((π β§ π β β
) β (π β π β ((π΅βπ) β€ (π΄βπ) β βπ β π (volβ((π΄βπ)[,)(π΅βπ))) = 0))) |
50 | 22, 23, 49 | rexlimd 3264 |
. . . 4
β’ ((π β§ π β β
) β (βπ β π (π΅βπ) β€ (π΄βπ) β βπ β π (volβ((π΄βπ)[,)(π΅βπ))) = 0)) |
51 | 19, 50 | mpd 15 |
. . 3
β’ ((π β§ π β β
) β βπ β π (volβ((π΄βπ)[,)(π΅βπ))) = 0) |
52 | | eqidd 2734 |
. . 3
β’ ((π β§ π β β
) β 0 =
0) |
53 | 18, 51, 52 | 3eqtrd 2777 |
. 2
β’ ((π β§ π β β
) β (π΄(πΏβπ)π΅) = 0) |
54 | 1, 9, 53 | syl2anc 585 |
1
β’ (π β (π΄(πΏβπ)π΅) = 0) |