Step | Hyp | Ref
| Expression |
1 | | fvvolicof.f |
. . . 4
β’ (π β πΉ:π΄βΆ(β* Γ
β*)) |
2 | 1 | ffund 6676 |
. . 3
β’ (π β Fun πΉ) |
3 | | fvvolicof.x |
. . . 4
β’ (π β π β π΄) |
4 | 1 | fdmd 6683 |
. . . . 5
β’ (π β dom πΉ = π΄) |
5 | 4 | eqcomd 2739 |
. . . 4
β’ (π β π΄ = dom πΉ) |
6 | 3, 5 | eleqtrd 2836 |
. . 3
β’ (π β π β dom πΉ) |
7 | | fvco 6943 |
. . 3
β’ ((Fun
πΉ β§ π β dom πΉ) β (((vol β [,)) β πΉ)βπ) = ((vol β [,))β(πΉβπ))) |
8 | 2, 6, 7 | syl2anc 585 |
. 2
β’ (π β (((vol β [,))
β πΉ)βπ) = ((vol β
[,))β(πΉβπ))) |
9 | | icof 43531 |
. . . . 5
β’
[,):(β* Γ β*)βΆπ«
β* |
10 | | ffun 6675 |
. . . . 5
β’
([,):(β* Γ β*)βΆπ«
β* β Fun [,)) |
11 | 9, 10 | ax-mp 5 |
. . . 4
β’ Fun
[,) |
12 | 11 | a1i 11 |
. . 3
β’ (π β Fun [,)) |
13 | 1, 3 | ffvelcdmd 7040 |
. . . 4
β’ (π β (πΉβπ) β (β* Γ
β*)) |
14 | 9 | fdmi 6684 |
. . . 4
β’ dom [,) =
(β* Γ β*) |
15 | 13, 14 | eleqtrrdi 2845 |
. . 3
β’ (π β (πΉβπ) β dom [,)) |
16 | | fvco 6943 |
. . 3
β’ ((Fun [,)
β§ (πΉβπ) β dom [,)) β ((vol
β [,))β(πΉβπ)) = (volβ([,)β(πΉβπ)))) |
17 | 12, 15, 16 | syl2anc 585 |
. 2
β’ (π β ((vol β
[,))β(πΉβπ)) =
(volβ([,)β(πΉβπ)))) |
18 | | df-ov 7364 |
. . . . 5
β’
((1st β(πΉβπ))[,)(2nd β(πΉβπ))) = ([,)ββ¨(1st
β(πΉβπ)), (2nd
β(πΉβπ))β©) |
19 | 18 | a1i 11 |
. . . 4
β’ (π β ((1st
β(πΉβπ))[,)(2nd
β(πΉβπ))) =
([,)ββ¨(1st β(πΉβπ)), (2nd β(πΉβπ))β©)) |
20 | | 1st2nd2 7964 |
. . . . . . 7
β’ ((πΉβπ) β (β* Γ
β*) β (πΉβπ) = β¨(1st β(πΉβπ)), (2nd β(πΉβπ))β©) |
21 | 13, 20 | syl 17 |
. . . . . 6
β’ (π β (πΉβπ) = β¨(1st β(πΉβπ)), (2nd β(πΉβπ))β©) |
22 | 21 | eqcomd 2739 |
. . . . 5
β’ (π β β¨(1st
β(πΉβπ)), (2nd
β(πΉβπ))β© = (πΉβπ)) |
23 | 22 | fveq2d 6850 |
. . . 4
β’ (π β
([,)ββ¨(1st β(πΉβπ)), (2nd β(πΉβπ))β©) = ([,)β(πΉβπ))) |
24 | 19, 23 | eqtr2d 2774 |
. . 3
β’ (π β ([,)β(πΉβπ)) = ((1st β(πΉβπ))[,)(2nd β(πΉβπ)))) |
25 | 24 | fveq2d 6850 |
. 2
β’ (π β
(volβ([,)β(πΉβπ))) = (volβ((1st
β(πΉβπ))[,)(2nd
β(πΉβπ))))) |
26 | 8, 17, 25 | 3eqtrd 2777 |
1
β’ (π β (((vol β [,))
β πΉ)βπ) = (volβ((1st
β(πΉβπ))[,)(2nd
β(πΉβπ))))) |