Step | Hyp | Ref
| Expression |
1 | | volioof 44318 |
. . . . 5
β’ (vol
β (,)):(β* Γ
β*)βΆ(0[,]+β) |
2 | 1 | a1i 11 |
. . . 4
β’ (π β (vol β
(,)):(β* Γ
β*)βΆ(0[,]+β)) |
3 | | rexpssxrxp 11208 |
. . . . 5
β’ (β
Γ β) β (β* Γ
β*) |
4 | 3 | a1i 11 |
. . . 4
β’ (π β (β Γ β)
β (β* Γ β*)) |
5 | | voliooicof.1 |
. . . 4
β’ (π β πΉ:π΄βΆ(β Γ
β)) |
6 | 2, 4, 5 | fcoss 43522 |
. . 3
β’ (π β ((vol β (,)) β
πΉ):π΄βΆ(0[,]+β)) |
7 | 6 | ffnd 6673 |
. 2
β’ (π β ((vol β (,)) β
πΉ) Fn π΄) |
8 | | volf 24916 |
. . . . . 6
β’ vol:dom
volβΆ(0[,]+β) |
9 | 8 | a1i 11 |
. . . . 5
β’ (π β vol:dom
volβΆ(0[,]+β)) |
10 | | icof 43531 |
. . . . . . . . . 10
β’
[,):(β* Γ β*)βΆπ«
β* |
11 | 10 | a1i 11 |
. . . . . . . . 9
β’ (π β [,):(β*
Γ β*)βΆπ«
β*) |
12 | 11, 4, 5 | fcoss 43522 |
. . . . . . . 8
β’ (π β ([,) β πΉ):π΄βΆπ«
β*) |
13 | 12 | ffnd 6673 |
. . . . . . 7
β’ (π β ([,) β πΉ) Fn π΄) |
14 | 5 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π₯ β π΄) β πΉ:π΄βΆ(β Γ
β)) |
15 | | simpr 486 |
. . . . . . . . . 10
β’ ((π β§ π₯ β π΄) β π₯ β π΄) |
16 | 14, 15 | fvovco 43505 |
. . . . . . . . 9
β’ ((π β§ π₯ β π΄) β (([,) β πΉ)βπ₯) = ((1st β(πΉβπ₯))[,)(2nd β(πΉβπ₯)))) |
17 | 5 | ffvelcdmda 7039 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β π΄) β (πΉβπ₯) β (β Γ
β)) |
18 | | xp1st 7957 |
. . . . . . . . . . 11
β’ ((πΉβπ₯) β (β Γ β) β
(1st β(πΉβπ₯)) β β) |
19 | 17, 18 | syl 17 |
. . . . . . . . . 10
β’ ((π β§ π₯ β π΄) β (1st β(πΉβπ₯)) β β) |
20 | | xp2nd 7958 |
. . . . . . . . . . . 12
β’ ((πΉβπ₯) β (β Γ β) β
(2nd β(πΉβπ₯)) β β) |
21 | 17, 20 | syl 17 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β π΄) β (2nd β(πΉβπ₯)) β β) |
22 | 21 | rexrd 11213 |
. . . . . . . . . 10
β’ ((π β§ π₯ β π΄) β (2nd β(πΉβπ₯)) β
β*) |
23 | | icombl 24951 |
. . . . . . . . . 10
β’
(((1st β(πΉβπ₯)) β β β§ (2nd
β(πΉβπ₯)) β β*)
β ((1st β(πΉβπ₯))[,)(2nd β(πΉβπ₯))) β dom vol) |
24 | 19, 22, 23 | syl2anc 585 |
. . . . . . . . 9
β’ ((π β§ π₯ β π΄) β ((1st β(πΉβπ₯))[,)(2nd β(πΉβπ₯))) β dom vol) |
25 | 16, 24 | eqeltrd 2834 |
. . . . . . . 8
β’ ((π β§ π₯ β π΄) β (([,) β πΉ)βπ₯) β dom vol) |
26 | 25 | ralrimiva 3140 |
. . . . . . 7
β’ (π β βπ₯ β π΄ (([,) β πΉ)βπ₯) β dom vol) |
27 | 13, 26 | jca 513 |
. . . . . 6
β’ (π β (([,) β πΉ) Fn π΄ β§ βπ₯ β π΄ (([,) β πΉ)βπ₯) β dom vol)) |
28 | | ffnfv 7070 |
. . . . . 6
β’ (([,)
β πΉ):π΄βΆdom vol β (([,)
β πΉ) Fn π΄ β§ βπ₯ β π΄ (([,) β πΉ)βπ₯) β dom vol)) |
29 | 27, 28 | sylibr 233 |
. . . . 5
β’ (π β ([,) β πΉ):π΄βΆdom vol) |
30 | | fco 6696 |
. . . . 5
β’ ((vol:dom
volβΆ(0[,]+β) β§ ([,) β πΉ):π΄βΆdom vol) β (vol β ([,)
β πΉ)):π΄βΆ(0[,]+β)) |
31 | 9, 29, 30 | syl2anc 585 |
. . . 4
β’ (π β (vol β ([,) β
πΉ)):π΄βΆ(0[,]+β)) |
32 | | coass 6221 |
. . . . . 6
β’ ((vol
β [,)) β πΉ) =
(vol β ([,) β πΉ)) |
33 | 32 | a1i 11 |
. . . . 5
β’ (π β ((vol β [,)) β
πΉ) = (vol β ([,)
β πΉ))) |
34 | 33 | feq1d 6657 |
. . . 4
β’ (π β (((vol β [,))
β πΉ):π΄βΆ(0[,]+β) β
(vol β ([,) β πΉ)):π΄βΆ(0[,]+β))) |
35 | 31, 34 | mpbird 257 |
. . 3
β’ (π β ((vol β [,)) β
πΉ):π΄βΆ(0[,]+β)) |
36 | 35 | ffnd 6673 |
. 2
β’ (π β ((vol β [,)) β
πΉ) Fn π΄) |
37 | 19, 21 | voliooico 44323 |
. . 3
β’ ((π β§ π₯ β π΄) β (volβ((1st
β(πΉβπ₯))(,)(2nd
β(πΉβπ₯)))) =
(volβ((1st β(πΉβπ₯))[,)(2nd β(πΉβπ₯))))) |
38 | 5, 4 | fssd 6690 |
. . . . 5
β’ (π β πΉ:π΄βΆ(β* Γ
β*)) |
39 | 38 | adantr 482 |
. . . 4
β’ ((π β§ π₯ β π΄) β πΉ:π΄βΆ(β* Γ
β*)) |
40 | 39, 15 | fvvolioof 44320 |
. . 3
β’ ((π β§ π₯ β π΄) β (((vol β (,)) β πΉ)βπ₯) = (volβ((1st β(πΉβπ₯))(,)(2nd β(πΉβπ₯))))) |
41 | 39, 15 | fvvolicof 44322 |
. . 3
β’ ((π β§ π₯ β π΄) β (((vol β [,)) β πΉ)βπ₯) = (volβ((1st β(πΉβπ₯))[,)(2nd β(πΉβπ₯))))) |
42 | 37, 40, 41 | 3eqtr4d 2783 |
. 2
β’ ((π β§ π₯ β π΄) β (((vol β (,)) β πΉ)βπ₯) = (((vol β [,)) β πΉ)βπ₯)) |
43 | 7, 36, 42 | eqfnfvd 6989 |
1
β’ (π β ((vol β (,)) β
πΉ) = ((vol β [,))
β πΉ)) |