Step | Hyp | Ref
| Expression |
1 | | vonn0icc2.i |
. . . . 5
β’ πΌ = Xπ β π (π΄[,]π΅) |
2 | 1 | a1i 11 |
. . . 4
β’ (π β πΌ = Xπ β π (π΄[,]π΅)) |
3 | | simpr 486 |
. . . . . . . 8
β’ ((π β§ π β π) β π β π) |
4 | | vonn0icc2.k |
. . . . . . . . . . 11
β’
β²ππ |
5 | | nfv 1918 |
. . . . . . . . . . 11
β’
β²π π β π |
6 | 4, 5 | nfan 1903 |
. . . . . . . . . 10
β’
β²π(π β§ π β π) |
7 | | nfcsb1v 3881 |
. . . . . . . . . . 11
β’
β²πβ¦π / πβ¦π΄ |
8 | | nfcv 2904 |
. . . . . . . . . . 11
β’
β²πβ |
9 | 7, 8 | nfel 2918 |
. . . . . . . . . 10
β’
β²πβ¦π / πβ¦π΄ β β |
10 | 6, 9 | nfim 1900 |
. . . . . . . . 9
β’
β²π((π β§ π β π) β β¦π / πβ¦π΄ β β) |
11 | | eleq1w 2817 |
. . . . . . . . . . 11
β’ (π = π β (π β π β π β π)) |
12 | 11 | anbi2d 630 |
. . . . . . . . . 10
β’ (π = π β ((π β§ π β π) β (π β§ π β π))) |
13 | | csbeq1a 3870 |
. . . . . . . . . . 11
β’ (π = π β π΄ = β¦π / πβ¦π΄) |
14 | 13 | eleq1d 2819 |
. . . . . . . . . 10
β’ (π = π β (π΄ β β β β¦π / πβ¦π΄ β β)) |
15 | 12, 14 | imbi12d 345 |
. . . . . . . . 9
β’ (π = π β (((π β§ π β π) β π΄ β β) β ((π β§ π β π) β β¦π / πβ¦π΄ β β))) |
16 | | vonn0icc2.a |
. . . . . . . . 9
β’ ((π β§ π β π) β π΄ β β) |
17 | 10, 15, 16 | chvarfv 2234 |
. . . . . . . 8
β’ ((π β§ π β π) β β¦π / πβ¦π΄ β β) |
18 | | eqid 2733 |
. . . . . . . . 9
β’ (π β π β¦ π΄) = (π β π β¦ π΄) |
19 | 18 | fvmpts 6952 |
. . . . . . . 8
β’ ((π β π β§ β¦π / πβ¦π΄ β β) β ((π β π β¦ π΄)βπ) = β¦π / πβ¦π΄) |
20 | 3, 17, 19 | syl2anc 585 |
. . . . . . 7
β’ ((π β§ π β π) β ((π β π β¦ π΄)βπ) = β¦π / πβ¦π΄) |
21 | | nfcsb1v 3881 |
. . . . . . . . . . 11
β’
β²πβ¦π / πβ¦π΅ |
22 | 21, 8 | nfel 2918 |
. . . . . . . . . 10
β’
β²πβ¦π / πβ¦π΅ β β |
23 | 6, 22 | nfim 1900 |
. . . . . . . . 9
β’
β²π((π β§ π β π) β β¦π / πβ¦π΅ β β) |
24 | | csbeq1a 3870 |
. . . . . . . . . . 11
β’ (π = π β π΅ = β¦π / πβ¦π΅) |
25 | 24 | eleq1d 2819 |
. . . . . . . . . 10
β’ (π = π β (π΅ β β β β¦π / πβ¦π΅ β β)) |
26 | 12, 25 | imbi12d 345 |
. . . . . . . . 9
β’ (π = π β (((π β§ π β π) β π΅ β β) β ((π β§ π β π) β β¦π / πβ¦π΅ β β))) |
27 | | vonn0icc2.b |
. . . . . . . . 9
β’ ((π β§ π β π) β π΅ β β) |
28 | 23, 26, 27 | chvarfv 2234 |
. . . . . . . 8
β’ ((π β§ π β π) β β¦π / πβ¦π΅ β β) |
29 | | eqid 2733 |
. . . . . . . . 9
β’ (π β π β¦ π΅) = (π β π β¦ π΅) |
30 | 29 | fvmpts 6952 |
. . . . . . . 8
β’ ((π β π β§ β¦π / πβ¦π΅ β β) β ((π β π β¦ π΅)βπ) = β¦π / πβ¦π΅) |
31 | 3, 28, 30 | syl2anc 585 |
. . . . . . 7
β’ ((π β§ π β π) β ((π β π β¦ π΅)βπ) = β¦π / πβ¦π΅) |
32 | 20, 31 | oveq12d 7376 |
. . . . . 6
β’ ((π β§ π β π) β (((π β π β¦ π΄)βπ)[,]((π β π β¦ π΅)βπ)) = (β¦π / πβ¦π΄[,]β¦π / πβ¦π΅)) |
33 | 32 | ixpeq2dva 8853 |
. . . . 5
β’ (π β Xπ β
π (((π β π β¦ π΄)βπ)[,]((π β π β¦ π΅)βπ)) = Xπ β π (β¦π / πβ¦π΄[,]β¦π / πβ¦π΅)) |
34 | | nfcv 2904 |
. . . . . . . 8
β’
β²π[,] |
35 | 7, 34, 21 | nfov 7388 |
. . . . . . 7
β’
β²π(β¦π / πβ¦π΄[,]β¦π / πβ¦π΅) |
36 | | nfcv 2904 |
. . . . . . 7
β’
β²π(π΄[,]π΅) |
37 | 13 | equcoms 2024 |
. . . . . . . . . 10
β’ (π = π β π΄ = β¦π / πβ¦π΄) |
38 | 37 | eqcomd 2739 |
. . . . . . . . 9
β’ (π = π β β¦π / πβ¦π΄ = π΄) |
39 | | eqidd 2734 |
. . . . . . . . 9
β’ (π = π β π΄ = π΄) |
40 | 38, 39 | eqtrd 2773 |
. . . . . . . 8
β’ (π = π β β¦π / πβ¦π΄ = π΄) |
41 | 24 | equcoms 2024 |
. . . . . . . . 9
β’ (π = π β π΅ = β¦π / πβ¦π΅) |
42 | 41 | eqcomd 2739 |
. . . . . . . 8
β’ (π = π β β¦π / πβ¦π΅ = π΅) |
43 | 40, 42 | oveq12d 7376 |
. . . . . . 7
β’ (π = π β (β¦π / πβ¦π΄[,]β¦π / πβ¦π΅) = (π΄[,]π΅)) |
44 | 35, 36, 43 | cbvixp 8855 |
. . . . . 6
β’ Xπ β
π (β¦π / πβ¦π΄[,]β¦π / πβ¦π΅) = Xπ β π (π΄[,]π΅) |
45 | 44 | a1i 11 |
. . . . 5
β’ (π β Xπ β
π (β¦π / πβ¦π΄[,]β¦π / πβ¦π΅) = Xπ β π (π΄[,]π΅)) |
46 | 33, 45 | eqtrd 2773 |
. . . 4
β’ (π β Xπ β
π (((π β π β¦ π΄)βπ)[,]((π β π β¦ π΅)βπ)) = Xπ β π (π΄[,]π΅)) |
47 | 2, 46 | eqtr4d 2776 |
. . 3
β’ (π β πΌ = Xπ β π (((π β π β¦ π΄)βπ)[,]((π β π β¦ π΅)βπ))) |
48 | 47 | fveq2d 6847 |
. 2
β’ (π β ((volnβπ)βπΌ) = ((volnβπ)βXπ β π (((π β π β¦ π΄)βπ)[,]((π β π β¦ π΅)βπ)))) |
49 | | vonn0icc2.x |
. . 3
β’ (π β π β Fin) |
50 | | vonn0icc2.n |
. . 3
β’ (π β π β β
) |
51 | 4, 16, 18 | fmptdf 7066 |
. . 3
β’ (π β (π β π β¦ π΄):πβΆβ) |
52 | 4, 27, 29 | fmptdf 7066 |
. . 3
β’ (π β (π β π β¦ π΅):πβΆβ) |
53 | | eqid 2733 |
. . 3
β’ Xπ β
π (((π β π β¦ π΄)βπ)[,]((π β π β¦ π΅)βπ)) = Xπ β π (((π β π β¦ π΄)βπ)[,]((π β π β¦ π΅)βπ)) |
54 | 49, 50, 51, 52, 53 | vonn0icc 45015 |
. 2
β’ (π β ((volnβπ)βXπ β
π (((π β π β¦ π΄)βπ)[,]((π β π β¦ π΅)βπ))) = βπ β π (volβ(((π β π β¦ π΄)βπ)[,]((π β π β¦ π΅)βπ)))) |
55 | 32 | fveq2d 6847 |
. . . 4
β’ ((π β§ π β π) β (volβ(((π β π β¦ π΄)βπ)[,]((π β π β¦ π΅)βπ))) = (volβ(β¦π / πβ¦π΄[,]β¦π / πβ¦π΅))) |
56 | 55 | prodeq2dv 15811 |
. . 3
β’ (π β βπ β π (volβ(((π β π β¦ π΄)βπ)[,]((π β π β¦ π΅)βπ))) = βπ β π (volβ(β¦π / πβ¦π΄[,]β¦π / πβ¦π΅))) |
57 | 43 | fveq2d 6847 |
. . . . 5
β’ (π = π β (volβ(β¦π / πβ¦π΄[,]β¦π / πβ¦π΅)) = (volβ(π΄[,]π΅))) |
58 | | nfcv 2904 |
. . . . 5
β’
β²ππ |
59 | | nfcv 2904 |
. . . . 5
β’
β²ππ |
60 | | nfcv 2904 |
. . . . . 6
β’
β²πvol |
61 | 60, 35 | nffv 6853 |
. . . . 5
β’
β²π(volβ(β¦π / πβ¦π΄[,]β¦π / πβ¦π΅)) |
62 | | nfcv 2904 |
. . . . 5
β’
β²π(volβ(π΄[,]π΅)) |
63 | 57, 58, 59, 61, 62 | cbvprod 15803 |
. . . 4
β’
βπ β
π
(volβ(β¦π / πβ¦π΄[,]β¦π / πβ¦π΅)) = βπ β π (volβ(π΄[,]π΅)) |
64 | 63 | a1i 11 |
. . 3
β’ (π β βπ β π (volβ(β¦π / πβ¦π΄[,]β¦π / πβ¦π΅)) = βπ β π (volβ(π΄[,]π΅))) |
65 | 56, 64 | eqtrd 2773 |
. 2
β’ (π β βπ β π (volβ(((π β π β¦ π΄)βπ)[,]((π β π β¦ π΅)βπ))) = βπ β π (volβ(π΄[,]π΅))) |
66 | 48, 54, 65 | 3eqtrd 2777 |
1
β’ (π β ((volnβπ)βπΌ) = βπ β π (volβ(π΄[,]π΅))) |