Step | Hyp | Ref
| Expression |
1 | | hoiprodp1.l |
. . 3
β’ πΏ = (π₯ β Fin β¦ (π β (β βm π₯), π β (β βm π₯) β¦ if(π₯ = β
, 0, βπ β π₯ (volβ((πβπ)[,)(πβπ)))))) |
2 | | hoiprodp1.x |
. . . 4
β’ π = (π βͺ {π}) |
3 | | hoiprodp1.y |
. . . . 5
β’ (π β π β Fin) |
4 | | snfi 9044 |
. . . . . 6
β’ {π} β Fin |
5 | 4 | a1i 11 |
. . . . 5
β’ (π β {π} β Fin) |
6 | | unfi 9172 |
. . . . 5
β’ ((π β Fin β§ {π} β Fin) β (π βͺ {π}) β Fin) |
7 | 3, 5, 6 | syl2anc 585 |
. . . 4
β’ (π β (π βͺ {π}) β Fin) |
8 | 2, 7 | eqeltrid 2838 |
. . 3
β’ (π β π β Fin) |
9 | | hoiprodp1.3 |
. . . . . . 7
β’ (π β π β π) |
10 | | snidg 4663 |
. . . . . . 7
β’ (π β π β π β {π}) |
11 | 9, 10 | syl 17 |
. . . . . 6
β’ (π β π β {π}) |
12 | | elun2 4178 |
. . . . . 6
β’ (π β {π} β π β (π βͺ {π})) |
13 | 11, 12 | syl 17 |
. . . . 5
β’ (π β π β (π βͺ {π})) |
14 | 13, 2 | eleqtrrdi 2845 |
. . . 4
β’ (π β π β π) |
15 | 14 | ne0d 4336 |
. . 3
β’ (π β π β β
) |
16 | | hoiprodp1.a |
. . 3
β’ (π β π΄:πβΆβ) |
17 | | hoiprodp1.b |
. . 3
β’ (π β π΅:πβΆβ) |
18 | 1, 8, 15, 16, 17 | hoidmvn0val 45300 |
. 2
β’ (π β (π΄(πΏβπ)π΅) = βπ β π (volβ((π΄βπ)[,)(π΅βπ)))) |
19 | 16 | ffvelcdmda 7087 |
. . . . 5
β’ ((π β§ π β π) β (π΄βπ) β β) |
20 | 17 | ffvelcdmda 7087 |
. . . . 5
β’ ((π β§ π β π) β (π΅βπ) β β) |
21 | | volicore 45297 |
. . . . 5
β’ (((π΄βπ) β β β§ (π΅βπ) β β) β (volβ((π΄βπ)[,)(π΅βπ))) β β) |
22 | 19, 20, 21 | syl2anc 585 |
. . . 4
β’ ((π β§ π β π) β (volβ((π΄βπ)[,)(π΅βπ))) β β) |
23 | 22 | recnd 11242 |
. . 3
β’ ((π β§ π β π) β (volβ((π΄βπ)[,)(π΅βπ))) β β) |
24 | | fveq2 6892 |
. . . . . 6
β’ (π = π β (π΄βπ) = (π΄βπ)) |
25 | | fveq2 6892 |
. . . . . 6
β’ (π = π β (π΅βπ) = (π΅βπ)) |
26 | 24, 25 | oveq12d 7427 |
. . . . 5
β’ (π = π β ((π΄βπ)[,)(π΅βπ)) = ((π΄βπ)[,)(π΅βπ))) |
27 | 26 | fveq2d 6896 |
. . . 4
β’ (π = π β (volβ((π΄βπ)[,)(π΅βπ))) = (volβ((π΄βπ)[,)(π΅βπ)))) |
28 | 27 | adantl 483 |
. . 3
β’ ((π β§ π = π) β (volβ((π΄βπ)[,)(π΅βπ))) = (volβ((π΄βπ)[,)(π΅βπ)))) |
29 | 8, 23, 14, 28 | fprodsplit1 44309 |
. 2
β’ (π β βπ β π (volβ((π΄βπ)[,)(π΅βπ))) = ((volβ((π΄βπ)[,)(π΅βπ))) Β· βπ β (π β {π})(volβ((π΄βπ)[,)(π΅βπ))))) |
30 | 2 | difeq1i 4119 |
. . . . . . . 8
β’ (π β {π}) = ((π βͺ {π}) β {π}) |
31 | 30 | a1i 11 |
. . . . . . 7
β’ (π β (π β {π}) = ((π βͺ {π}) β {π})) |
32 | | difun2 4481 |
. . . . . . . 8
β’ ((π βͺ {π}) β {π}) = (π β {π}) |
33 | 32 | a1i 11 |
. . . . . . 7
β’ (π β ((π βͺ {π}) β {π}) = (π β {π})) |
34 | | hoiprodp1.z |
. . . . . . . 8
β’ (π β Β¬ π β π) |
35 | | difsn 4802 |
. . . . . . . 8
β’ (Β¬
π β π β (π β {π}) = π) |
36 | 34, 35 | syl 17 |
. . . . . . 7
β’ (π β (π β {π}) = π) |
37 | 31, 33, 36 | 3eqtrd 2777 |
. . . . . 6
β’ (π β (π β {π}) = π) |
38 | 37 | prodeq1d 15865 |
. . . . 5
β’ (π β βπ β (π β {π})(volβ((π΄βπ)[,)(π΅βπ))) = βπ β π (volβ((π΄βπ)[,)(π΅βπ)))) |
39 | | hoiprodp1.g |
. . . . . . 7
β’ πΊ = βπ β π (volβ((π΄βπ)[,)(π΅βπ))) |
40 | 39 | eqcomi 2742 |
. . . . . 6
β’
βπ β
π (volβ((π΄βπ)[,)(π΅βπ))) = πΊ |
41 | 40 | a1i 11 |
. . . . 5
β’ (π β βπ β π (volβ((π΄βπ)[,)(π΅βπ))) = πΊ) |
42 | 38, 41 | eqtrd 2773 |
. . . 4
β’ (π β βπ β (π β {π})(volβ((π΄βπ)[,)(π΅βπ))) = πΊ) |
43 | 42 | oveq2d 7425 |
. . 3
β’ (π β ((volβ((π΄βπ)[,)(π΅βπ))) Β· βπ β (π β {π})(volβ((π΄βπ)[,)(π΅βπ)))) = ((volβ((π΄βπ)[,)(π΅βπ))) Β· πΊ)) |
44 | 16, 14 | ffvelcdmd 7088 |
. . . . . 6
β’ (π β (π΄βπ) β β) |
45 | 17, 14 | ffvelcdmd 7088 |
. . . . . 6
β’ (π β (π΅βπ) β β) |
46 | | volicore 45297 |
. . . . . 6
β’ (((π΄βπ) β β β§ (π΅βπ) β β) β (volβ((π΄βπ)[,)(π΅βπ))) β β) |
47 | 44, 45, 46 | syl2anc 585 |
. . . . 5
β’ (π β (volβ((π΄βπ)[,)(π΅βπ))) β β) |
48 | 47 | recnd 11242 |
. . . 4
β’ (π β (volβ((π΄βπ)[,)(π΅βπ))) β β) |
49 | 16 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β π) β π΄:πβΆβ) |
50 | | ssun1 4173 |
. . . . . . . . . . . 12
β’ π β (π βͺ {π}) |
51 | 50, 2 | sseqtrri 4020 |
. . . . . . . . . . 11
β’ π β π |
52 | | id 22 |
. . . . . . . . . . 11
β’ (π β π β π β π) |
53 | 51, 52 | sselid 3981 |
. . . . . . . . . 10
β’ (π β π β π β π) |
54 | 53 | adantl 483 |
. . . . . . . . 9
β’ ((π β§ π β π) β π β π) |
55 | 49, 54 | ffvelcdmd 7088 |
. . . . . . . 8
β’ ((π β§ π β π) β (π΄βπ) β β) |
56 | 17 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β π) β π΅:πβΆβ) |
57 | 56, 54 | ffvelcdmd 7088 |
. . . . . . . 8
β’ ((π β§ π β π) β (π΅βπ) β β) |
58 | 55, 57, 21 | syl2anc 585 |
. . . . . . 7
β’ ((π β§ π β π) β (volβ((π΄βπ)[,)(π΅βπ))) β β) |
59 | 3, 58 | fprodrecl 15897 |
. . . . . 6
β’ (π β βπ β π (volβ((π΄βπ)[,)(π΅βπ))) β β) |
60 | 39, 59 | eqeltrid 2838 |
. . . . 5
β’ (π β πΊ β β) |
61 | 60 | recnd 11242 |
. . . 4
β’ (π β πΊ β β) |
62 | 48, 61 | mulcomd 11235 |
. . 3
β’ (π β ((volβ((π΄βπ)[,)(π΅βπ))) Β· πΊ) = (πΊ Β· (volβ((π΄βπ)[,)(π΅βπ))))) |
63 | 43, 62 | eqtrd 2773 |
. 2
β’ (π β ((volβ((π΄βπ)[,)(π΅βπ))) Β· βπ β (π β {π})(volβ((π΄βπ)[,)(π΅βπ)))) = (πΊ Β· (volβ((π΄βπ)[,)(π΅βπ))))) |
64 | 18, 29, 63 | 3eqtrd 2777 |
1
β’ (π β (π΄(πΏβπ)π΅) = (πΊ Β· (volβ((π΄βπ)[,)(π΅βπ))))) |