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 9046 |
. . . . . 6
β’ {π} β Fin |
5 | 4 | a1i 11 |
. . . . 5
β’ (π β {π} β Fin) |
6 | | unfi 9174 |
. . . . 5
β’ ((π β Fin β§ {π} β Fin) β (π βͺ {π}) β Fin) |
7 | 3, 5, 6 | syl2anc 582 |
. . . 4
β’ (π β (π βͺ {π}) β Fin) |
8 | 2, 7 | eqeltrid 2835 |
. . 3
β’ (π β π β Fin) |
9 | | hoiprodp1.3 |
. . . . . . 7
β’ (π β π β π) |
10 | | snidg 4661 |
. . . . . . 7
β’ (π β π β π β {π}) |
11 | 9, 10 | syl 17 |
. . . . . 6
β’ (π β π β {π}) |
12 | | elun2 4176 |
. . . . . 6
β’ (π β {π} β π β (π βͺ {π})) |
13 | 11, 12 | syl 17 |
. . . . 5
β’ (π β π β (π βͺ {π})) |
14 | 13, 2 | eleqtrrdi 2842 |
. . . 4
β’ (π β π β π) |
15 | 14 | ne0d 4334 |
. . 3
β’ (π β π β β
) |
16 | | hoiprodp1.a |
. . 3
β’ (π β π΄:πβΆβ) |
17 | | hoiprodp1.b |
. . 3
β’ (π β π΅:πβΆβ) |
18 | 1, 8, 15, 16, 17 | hoidmvn0val 45598 |
. 2
β’ (π β (π΄(πΏβπ)π΅) = βπ β π (volβ((π΄βπ)[,)(π΅βπ)))) |
19 | 16 | ffvelcdmda 7085 |
. . . . 5
β’ ((π β§ π β π) β (π΄βπ) β β) |
20 | 17 | ffvelcdmda 7085 |
. . . . 5
β’ ((π β§ π β π) β (π΅βπ) β β) |
21 | | volicore 45595 |
. . . . 5
β’ (((π΄βπ) β β β§ (π΅βπ) β β) β (volβ((π΄βπ)[,)(π΅βπ))) β β) |
22 | 19, 20, 21 | syl2anc 582 |
. . . 4
β’ ((π β§ π β π) β (volβ((π΄βπ)[,)(π΅βπ))) β β) |
23 | 22 | recnd 11246 |
. . 3
β’ ((π β§ π β π) β (volβ((π΄βπ)[,)(π΅βπ))) β β) |
24 | | fveq2 6890 |
. . . . . 6
β’ (π = π β (π΄βπ) = (π΄βπ)) |
25 | | fveq2 6890 |
. . . . . 6
β’ (π = π β (π΅βπ) = (π΅βπ)) |
26 | 24, 25 | oveq12d 7429 |
. . . . 5
β’ (π = π β ((π΄βπ)[,)(π΅βπ)) = ((π΄βπ)[,)(π΅βπ))) |
27 | 26 | fveq2d 6894 |
. . . 4
β’ (π = π β (volβ((π΄βπ)[,)(π΅βπ))) = (volβ((π΄βπ)[,)(π΅βπ)))) |
28 | 27 | adantl 480 |
. . 3
β’ ((π β§ π = π) β (volβ((π΄βπ)[,)(π΅βπ))) = (volβ((π΄βπ)[,)(π΅βπ)))) |
29 | 8, 23, 14, 28 | fprodsplit1 44607 |
. 2
β’ (π β βπ β π (volβ((π΄βπ)[,)(π΅βπ))) = ((volβ((π΄βπ)[,)(π΅βπ))) Β· βπ β (π β {π})(volβ((π΄βπ)[,)(π΅βπ))))) |
30 | 2 | difeq1i 4117 |
. . . . . . . 8
β’ (π β {π}) = ((π βͺ {π}) β {π}) |
31 | 30 | a1i 11 |
. . . . . . 7
β’ (π β (π β {π}) = ((π βͺ {π}) β {π})) |
32 | | difun2 4479 |
. . . . . . . 8
β’ ((π βͺ {π}) β {π}) = (π β {π}) |
33 | 32 | a1i 11 |
. . . . . . 7
β’ (π β ((π βͺ {π}) β {π}) = (π β {π})) |
34 | | hoiprodp1.z |
. . . . . . . 8
β’ (π β Β¬ π β π) |
35 | | difsn 4800 |
. . . . . . . 8
β’ (Β¬
π β π β (π β {π}) = π) |
36 | 34, 35 | syl 17 |
. . . . . . 7
β’ (π β (π β {π}) = π) |
37 | 31, 33, 36 | 3eqtrd 2774 |
. . . . . 6
β’ (π β (π β {π}) = π) |
38 | 37 | prodeq1d 15869 |
. . . . 5
β’ (π β βπ β (π β {π})(volβ((π΄βπ)[,)(π΅βπ))) = βπ β π (volβ((π΄βπ)[,)(π΅βπ)))) |
39 | | hoiprodp1.g |
. . . . . . 7
β’ πΊ = βπ β π (volβ((π΄βπ)[,)(π΅βπ))) |
40 | 39 | eqcomi 2739 |
. . . . . 6
β’
βπ β
π (volβ((π΄βπ)[,)(π΅βπ))) = πΊ |
41 | 40 | a1i 11 |
. . . . 5
β’ (π β βπ β π (volβ((π΄βπ)[,)(π΅βπ))) = πΊ) |
42 | 38, 41 | eqtrd 2770 |
. . . 4
β’ (π β βπ β (π β {π})(volβ((π΄βπ)[,)(π΅βπ))) = πΊ) |
43 | 42 | oveq2d 7427 |
. . 3
β’ (π β ((volβ((π΄βπ)[,)(π΅βπ))) Β· βπ β (π β {π})(volβ((π΄βπ)[,)(π΅βπ)))) = ((volβ((π΄βπ)[,)(π΅βπ))) Β· πΊ)) |
44 | 16, 14 | ffvelcdmd 7086 |
. . . . . 6
β’ (π β (π΄βπ) β β) |
45 | 17, 14 | ffvelcdmd 7086 |
. . . . . 6
β’ (π β (π΅βπ) β β) |
46 | | volicore 45595 |
. . . . . 6
β’ (((π΄βπ) β β β§ (π΅βπ) β β) β (volβ((π΄βπ)[,)(π΅βπ))) β β) |
47 | 44, 45, 46 | syl2anc 582 |
. . . . 5
β’ (π β (volβ((π΄βπ)[,)(π΅βπ))) β β) |
48 | 47 | recnd 11246 |
. . . 4
β’ (π β (volβ((π΄βπ)[,)(π΅βπ))) β β) |
49 | 16 | adantr 479 |
. . . . . . . . 9
β’ ((π β§ π β π) β π΄:πβΆβ) |
50 | | ssun1 4171 |
. . . . . . . . . . . 12
β’ π β (π βͺ {π}) |
51 | 50, 2 | sseqtrri 4018 |
. . . . . . . . . . 11
β’ π β π |
52 | | id 22 |
. . . . . . . . . . 11
β’ (π β π β π β π) |
53 | 51, 52 | sselid 3979 |
. . . . . . . . . 10
β’ (π β π β π β π) |
54 | 53 | adantl 480 |
. . . . . . . . 9
β’ ((π β§ π β π) β π β π) |
55 | 49, 54 | ffvelcdmd 7086 |
. . . . . . . 8
β’ ((π β§ π β π) β (π΄βπ) β β) |
56 | 17 | adantr 479 |
. . . . . . . . 9
β’ ((π β§ π β π) β π΅:πβΆβ) |
57 | 56, 54 | ffvelcdmd 7086 |
. . . . . . . 8
β’ ((π β§ π β π) β (π΅βπ) β β) |
58 | 55, 57, 21 | syl2anc 582 |
. . . . . . 7
β’ ((π β§ π β π) β (volβ((π΄βπ)[,)(π΅βπ))) β β) |
59 | 3, 58 | fprodrecl 15901 |
. . . . . 6
β’ (π β βπ β π (volβ((π΄βπ)[,)(π΅βπ))) β β) |
60 | 39, 59 | eqeltrid 2835 |
. . . . 5
β’ (π β πΊ β β) |
61 | 60 | recnd 11246 |
. . . 4
β’ (π β πΊ β β) |
62 | 48, 61 | mulcomd 11239 |
. . 3
β’ (π β ((volβ((π΄βπ)[,)(π΅βπ))) Β· πΊ) = (πΊ Β· (volβ((π΄βπ)[,)(π΅βπ))))) |
63 | 43, 62 | eqtrd 2770 |
. 2
β’ (π β ((volβ((π΄βπ)[,)(π΅βπ))) Β· βπ β (π β {π})(volβ((π΄βπ)[,)(π΅βπ)))) = (πΊ Β· (volβ((π΄βπ)[,)(π΅βπ))))) |
64 | 18, 29, 63 | 3eqtrd 2774 |
1
β’ (π β (π΄(πΏβπ)π΅) = (πΊ Β· (volβ((π΄βπ)[,)(π΅βπ))))) |