Step | Hyp | Ref
| Expression |
1 | | hoidmvval.l |
. . 3
β’ πΏ = (π₯ β Fin β¦ (π β (β βm π₯), π β (β βm π₯) β¦ if(π₯ = β
, 0, βπ β π₯ (volβ((πβπ)[,)(πβπ)))))) |
2 | | oveq2 7359 |
. . . 4
β’ (π₯ = π β (β βm π₯) = (β βm
π)) |
3 | | eqeq1 2741 |
. . . . 5
β’ (π₯ = π β (π₯ = β
β π = β
)) |
4 | | prodeq1 15752 |
. . . . 5
β’ (π₯ = π β βπ β π₯ (volβ((πβπ)[,)(πβπ))) = βπ β π (volβ((πβπ)[,)(πβπ)))) |
5 | 3, 4 | ifbieq2d 4510 |
. . . 4
β’ (π₯ = π β if(π₯ = β
, 0, βπ β π₯ (volβ((πβπ)[,)(πβπ)))) = if(π = β
, 0, βπ β π (volβ((πβπ)[,)(πβπ))))) |
6 | 2, 2, 5 | mpoeq123dv 7426 |
. . 3
β’ (π₯ = π β (π β (β βm π₯), π β (β βm π₯) β¦ if(π₯ = β
, 0, βπ β π₯ (volβ((πβπ)[,)(πβπ))))) = (π β (β βm π), π β (β βm π) β¦ if(π = β
, 0, βπ β π (volβ((πβπ)[,)(πβπ)))))) |
7 | | hoidmvval.x |
. . 3
β’ (π β π β Fin) |
8 | | ovex 7384 |
. . . . 5
β’ (β
βm π)
β V |
9 | 8, 8 | mpoex 8004 |
. . . 4
β’ (π β (β
βm π),
π β (β
βm π)
β¦ if(π = β
, 0,
βπ β π (volβ((πβπ)[,)(πβπ))))) β V |
10 | 9 | a1i 11 |
. . 3
β’ (π β (π β (β βm π), π β (β βm π) β¦ if(π = β
, 0, βπ β π (volβ((πβπ)[,)(πβπ))))) β V) |
11 | 1, 6, 7, 10 | fvmptd3 6968 |
. 2
β’ (π β (πΏβπ) = (π β (β βm π), π β (β βm π) β¦ if(π = β
, 0, βπ β π (volβ((πβπ)[,)(πβπ)))))) |
12 | | fveq1 6838 |
. . . . . . . 8
β’ (π = π΄ β (πβπ) = (π΄βπ)) |
13 | 12 | adantr 481 |
. . . . . . 7
β’ ((π = π΄ β§ π = π΅) β (πβπ) = (π΄βπ)) |
14 | | fveq1 6838 |
. . . . . . . 8
β’ (π = π΅ β (πβπ) = (π΅βπ)) |
15 | 14 | adantl 482 |
. . . . . . 7
β’ ((π = π΄ β§ π = π΅) β (πβπ) = (π΅βπ)) |
16 | 13, 15 | oveq12d 7369 |
. . . . . 6
β’ ((π = π΄ β§ π = π΅) β ((πβπ)[,)(πβπ)) = ((π΄βπ)[,)(π΅βπ))) |
17 | 16 | fveq2d 6843 |
. . . . 5
β’ ((π = π΄ β§ π = π΅) β (volβ((πβπ)[,)(πβπ))) = (volβ((π΄βπ)[,)(π΅βπ)))) |
18 | 17 | prodeq2ad 43734 |
. . . 4
β’ ((π = π΄ β§ π = π΅) β βπ β π (volβ((πβπ)[,)(πβπ))) = βπ β π (volβ((π΄βπ)[,)(π΅βπ)))) |
19 | 18 | ifeq2d 4504 |
. . 3
β’ ((π = π΄ β§ π = π΅) β if(π = β
, 0, βπ β π (volβ((πβπ)[,)(πβπ)))) = if(π = β
, 0, βπ β π (volβ((π΄βπ)[,)(π΅βπ))))) |
20 | 19 | adantl 482 |
. 2
β’ ((π β§ (π = π΄ β§ π = π΅)) β if(π = β
, 0, βπ β π (volβ((πβπ)[,)(πβπ)))) = if(π = β
, 0, βπ β π (volβ((π΄βπ)[,)(π΅βπ))))) |
21 | | hoidmvval.a |
. . 3
β’ (π β π΄:πβΆβ) |
22 | | reex 11100 |
. . . . 5
β’ β
β V |
23 | 22 | a1i 11 |
. . . 4
β’ (π β β β
V) |
24 | | elmapg 8736 |
. . . 4
β’ ((β
β V β§ π β
Fin) β (π΄ β
(β βm π) β π΄:πβΆβ)) |
25 | 23, 7, 24 | syl2anc 584 |
. . 3
β’ (π β (π΄ β (β βm π) β π΄:πβΆβ)) |
26 | 21, 25 | mpbird 256 |
. 2
β’ (π β π΄ β (β βm π)) |
27 | | hoidmvval.b |
. . 3
β’ (π β π΅:πβΆβ) |
28 | | elmapg 8736 |
. . . 4
β’ ((β
β V β§ π β
Fin) β (π΅ β
(β βm π) β π΅:πβΆβ)) |
29 | 23, 7, 28 | syl2anc 584 |
. . 3
β’ (π β (π΅ β (β βm π) β π΅:πβΆβ)) |
30 | 27, 29 | mpbird 256 |
. 2
β’ (π β π΅ β (β βm π)) |
31 | | c0ex 11107 |
. . . 4
β’ 0 β
V |
32 | | prodex 15750 |
. . . 4
β’
βπ β
π (volβ((π΄βπ)[,)(π΅βπ))) β V |
33 | 31, 32 | ifex 4534 |
. . 3
β’ if(π = β
, 0, βπ β π (volβ((π΄βπ)[,)(π΅βπ)))) β V |
34 | 33 | a1i 11 |
. 2
β’ (π β if(π = β
, 0, βπ β π (volβ((π΄βπ)[,)(π΅βπ)))) β V) |
35 | 11, 20, 26, 30, 34 | ovmpod 7501 |
1
β’ (π β (π΄(πΏβπ)π΅) = if(π = β
, 0, βπ β π (volβ((π΄βπ)[,)(π΅βπ))))) |