Step | Hyp | Ref
| Expression |
1 | | id 22 |
. 2
β’ (π β π) |
2 | | hoidmvval0.j |
. . 3
β’ (π β βπ β π (π΅βπ) β€ (π΄βπ)) |
3 | | fveq2 6891 |
. . . . . 6
β’ (π = π β (π΅βπ) = (π΅βπ)) |
4 | | fveq2 6891 |
. . . . . 6
β’ (π = π β (π΄βπ) = (π΄βπ)) |
5 | 3, 4 | breq12d 5161 |
. . . . 5
β’ (π = π β ((π΅βπ) β€ (π΄βπ) β (π΅βπ) β€ (π΄βπ))) |
6 | 5 | cbvrexvw 3235 |
. . . 4
β’
(βπ β
π (π΅βπ) β€ (π΄βπ) β βπ β π (π΅βπ) β€ (π΄βπ)) |
7 | | rexn0 4510 |
. . . 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 481 |
. . . 4
β’ ((π β§ π β β
) β π β Fin) |
13 | | simpr 485 |
. . . 4
β’ ((π β§ π β β
) β π β β
) |
14 | | hoidmvval0.a |
. . . . 5
β’ (π β π΄:πβΆβ) |
15 | 14 | adantr 481 |
. . . 4
β’ ((π β§ π β β
) β π΄:πβΆβ) |
16 | | hoidmvval0.b |
. . . . 5
β’ (π β π΅:πβΆβ) |
17 | 16 | adantr 481 |
. . . 4
β’ ((π β§ π β β
) β π΅:πβΆβ) |
18 | 10, 12, 13, 15, 17 | hoidmvn0val 45379 |
. . 3
β’ ((π β§ π β β
) β (π΄(πΏβπ)π΅) = βπ β π (volβ((π΄βπ)[,)(π΅βπ)))) |
19 | 2 | adantr 481 |
. . . 4
β’ ((π β§ π β β
) β βπ β π (π΅βπ) β€ (π΄βπ)) |
20 | | hoidmvval0.p |
. . . . . 6
β’
β²ππ |
21 | | nfv 1917 |
. . . . . 6
β’
β²π π β β
|
22 | 20, 21 | nfan 1902 |
. . . . 5
β’
β²π(π β§ π β β
) |
23 | | nfv 1917 |
. . . . 5
β’
β²πβπ β π (volβ((π΄βπ)[,)(π΅βπ))) = 0 |
24 | | nfv 1917 |
. . . . . . . 8
β’
β²π(π β§ π β π β§ (π΅βπ) β€ (π΄βπ)) |
25 | | nfcv 2903 |
. . . . . . . 8
β’
β²π(volβ((π΄βπ)[,)(π΅βπ))) |
26 | 11 | 3ad2ant1 1133 |
. . . . . . . 8
β’ ((π β§ π β π β§ (π΅βπ) β€ (π΄βπ)) β π β Fin) |
27 | 14 | ffvelcdmda 7086 |
. . . . . . . . . . 11
β’ ((π β§ π β π) β (π΄βπ) β β) |
28 | 16 | ffvelcdmda 7086 |
. . . . . . . . . . 11
β’ ((π β§ π β π) β (π΅βπ) β β) |
29 | | volicore 45376 |
. . . . . . . . . . 11
β’ (((π΄βπ) β β β§ (π΅βπ) β β) β (volβ((π΄βπ)[,)(π΅βπ))) β β) |
30 | 27, 28, 29 | syl2anc 584 |
. . . . . . . . . 10
β’ ((π β§ π β π) β (volβ((π΄βπ)[,)(π΅βπ))) β β) |
31 | 30 | recnd 11244 |
. . . . . . . . 9
β’ ((π β§ π β π) β (volβ((π΄βπ)[,)(π΅βπ))) β β) |
32 | 31 | 3ad2antl1 1185 |
. . . . . . . 8
β’ (((π β§ π β π β§ (π΅βπ) β€ (π΄βπ)) β§ π β π) β (volβ((π΄βπ)[,)(π΅βπ))) β β) |
33 | 4, 3 | oveq12d 7429 |
. . . . . . . . 9
β’ (π = π β ((π΄βπ)[,)(π΅βπ)) = ((π΄βπ)[,)(π΅βπ))) |
34 | 33 | fveq2d 6895 |
. . . . . . . 8
β’ (π = π β (volβ((π΄βπ)[,)(π΅βπ))) = (volβ((π΄βπ)[,)(π΅βπ)))) |
35 | | simp2 1137 |
. . . . . . . 8
β’ ((π β§ π β π β§ (π΅βπ) β€ (π΄βπ)) β π β π) |
36 | 14 | ffvelcdmda 7086 |
. . . . . . . . . . 11
β’ ((π β§ π β π) β (π΄βπ) β β) |
37 | 36 | 3adant3 1132 |
. . . . . . . . . 10
β’ ((π β§ π β π β§ (π΅βπ) β€ (π΄βπ)) β (π΄βπ) β β) |
38 | 16 | ffvelcdmda 7086 |
. . . . . . . . . . 11
β’ ((π β§ π β π) β (π΅βπ) β β) |
39 | 38 | 3adant3 1132 |
. . . . . . . . . 10
β’ ((π β§ π β π β§ (π΅βπ) β€ (π΄βπ)) β (π΅βπ) β β) |
40 | | volico 44778 |
. . . . . . . . . 10
β’ (((π΄βπ) β β β§ (π΅βπ) β β) β (volβ((π΄βπ)[,)(π΅βπ))) = if((π΄βπ) < (π΅βπ), ((π΅βπ) β (π΄βπ)), 0)) |
41 | 37, 39, 40 | syl2anc 584 |
. . . . . . . . 9
β’ ((π β§ π β π β§ (π΅βπ) β€ (π΄βπ)) β (volβ((π΄βπ)[,)(π΅βπ))) = if((π΄βπ) < (π΅βπ), ((π΅βπ) β (π΄βπ)), 0)) |
42 | | simp3 1138 |
. . . . . . . . . . 11
β’ ((π β§ π β π β§ (π΅βπ) β€ (π΄βπ)) β (π΅βπ) β€ (π΄βπ)) |
43 | 39, 37 | lenltd 11362 |
. . . . . . . . . . 11
β’ ((π β§ π β π β§ (π΅βπ) β€ (π΄βπ)) β ((π΅βπ) β€ (π΄βπ) β Β¬ (π΄βπ) < (π΅βπ))) |
44 | 42, 43 | mpbid 231 |
. . . . . . . . . 10
β’ ((π β§ π β π β§ (π΅βπ) β€ (π΄βπ)) β Β¬ (π΄βπ) < (π΅βπ)) |
45 | 44 | iffalsed 4539 |
. . . . . . . . 9
β’ ((π β§ π β π β§ (π΅βπ) β€ (π΄βπ)) β if((π΄βπ) < (π΅βπ), ((π΅βπ) β (π΄βπ)), 0) = 0) |
46 | 41, 45 | eqtrd 2772 |
. . . . . . . 8
β’ ((π β§ π β π β§ (π΅βπ) β€ (π΄βπ)) β (volβ((π΄βπ)[,)(π΅βπ))) = 0) |
47 | 24, 25, 26, 32, 34, 35, 46 | fprod0 44391 |
. . . . . . 7
β’ ((π β§ π β π β§ (π΅βπ) β€ (π΄βπ)) β βπ β π (volβ((π΄βπ)[,)(π΅βπ))) = 0) |
48 | 47 | 3adant1r 1177 |
. . . . . 6
β’ (((π β§ π β β
) β§ π β π β§ (π΅βπ) β€ (π΄βπ)) β βπ β π (volβ((π΄βπ)[,)(π΅βπ))) = 0) |
49 | 48 | 3exp 1119 |
. . . . 5
β’ ((π β§ π β β
) β (π β π β ((π΅βπ) β€ (π΄βπ) β βπ β π (volβ((π΄βπ)[,)(π΅βπ))) = 0))) |
50 | 22, 23, 49 | rexlimd 3263 |
. . . 4
β’ ((π β§ π β β
) β (βπ β π (π΅βπ) β€ (π΄βπ) β βπ β π (volβ((π΄βπ)[,)(π΅βπ))) = 0)) |
51 | 19, 50 | mpd 15 |
. . 3
β’ ((π β§ π β β
) β βπ β π (volβ((π΄βπ)[,)(π΅βπ))) = 0) |
52 | | eqidd 2733 |
. . 3
β’ ((π β§ π β β
) β 0 =
0) |
53 | 18, 51, 52 | 3eqtrd 2776 |
. 2
β’ ((π β§ π β β
) β (π΄(πΏβπ)π΅) = 0) |
54 | 1, 9, 53 | syl2anc 584 |
1
β’ (π β (π΄(πΏβπ)π΅) = 0) |