Step | Hyp | Ref
| Expression |
1 | | ovolfcl 24853 |
. . . . 5
β’ ((πΉ:ββΆ( β€ β©
(β Γ β)) β§ π β β) β ((1st
β(πΉβπ)) β β β§
(2nd β(πΉβπ)) β β β§ (1st
β(πΉβπ)) β€ (2nd
β(πΉβπ)))) |
2 | | ovolioo 24955 |
. . . . 5
β’
(((1st β(πΉβπ)) β β β§ (2nd
β(πΉβπ)) β β β§
(1st β(πΉβπ)) β€ (2nd β(πΉβπ))) β (vol*β((1st
β(πΉβπ))(,)(2nd
β(πΉβπ)))) = ((2nd
β(πΉβπ)) β (1st
β(πΉβπ)))) |
3 | 1, 2 | syl 17 |
. . . 4
β’ ((πΉ:ββΆ( β€ β©
(β Γ β)) β§ π β β) β
(vol*β((1st β(πΉβπ))(,)(2nd β(πΉβπ)))) = ((2nd β(πΉβπ)) β (1st β(πΉβπ)))) |
4 | | inss2 4193 |
. . . . . . . . . 10
β’ ( β€
β© (β Γ β)) β (β Γ
β) |
5 | | rexpssxrxp 11208 |
. . . . . . . . . 10
β’ (β
Γ β) β (β* Γ
β*) |
6 | 4, 5 | sstri 3957 |
. . . . . . . . 9
β’ ( β€
β© (β Γ β)) β (β* Γ
β*) |
7 | | ffvelcdm 7036 |
. . . . . . . . 9
β’ ((πΉ:ββΆ( β€ β©
(β Γ β)) β§ π β β) β (πΉβπ) β ( β€ β© (β Γ
β))) |
8 | 6, 7 | sselid 3946 |
. . . . . . . 8
β’ ((πΉ:ββΆ( β€ β©
(β Γ β)) β§ π β β) β (πΉβπ) β (β* Γ
β*)) |
9 | | 1st2nd2 7964 |
. . . . . . . 8
β’ ((πΉβπ) β (β* Γ
β*) β (πΉβπ) = β¨(1st β(πΉβπ)), (2nd β(πΉβπ))β©) |
10 | 8, 9 | syl 17 |
. . . . . . 7
β’ ((πΉ:ββΆ( β€ β©
(β Γ β)) β§ π β β) β (πΉβπ) = β¨(1st β(πΉβπ)), (2nd β(πΉβπ))β©) |
11 | 10 | fveq2d 6850 |
. . . . . 6
β’ ((πΉ:ββΆ( β€ β©
(β Γ β)) β§ π β β) β ((,)β(πΉβπ)) = ((,)ββ¨(1st
β(πΉβπ)), (2nd
β(πΉβπ))β©)) |
12 | | df-ov 7364 |
. . . . . 6
β’
((1st β(πΉβπ))(,)(2nd β(πΉβπ))) = ((,)ββ¨(1st
β(πΉβπ)), (2nd
β(πΉβπ))β©) |
13 | 11, 12 | eqtr4di 2791 |
. . . . 5
β’ ((πΉ:ββΆ( β€ β©
(β Γ β)) β§ π β β) β ((,)β(πΉβπ)) = ((1st β(πΉβπ))(,)(2nd β(πΉβπ)))) |
14 | 13 | fveq2d 6850 |
. . . 4
β’ ((πΉ:ββΆ( β€ β©
(β Γ β)) β§ π β β) β
(vol*β((,)β(πΉβπ))) = (vol*β((1st
β(πΉβπ))(,)(2nd
β(πΉβπ))))) |
15 | | ovolfs2.1 |
. . . . 5
β’ πΊ = ((abs β β )
β πΉ) |
16 | 15 | ovolfsval 24857 |
. . . 4
β’ ((πΉ:ββΆ( β€ β©
(β Γ β)) β§ π β β) β (πΊβπ) = ((2nd β(πΉβπ)) β (1st β(πΉβπ)))) |
17 | 3, 14, 16 | 3eqtr4rd 2784 |
. . 3
β’ ((πΉ:ββΆ( β€ β©
(β Γ β)) β§ π β β) β (πΊβπ) = (vol*β((,)β(πΉβπ)))) |
18 | 17 | mpteq2dva 5209 |
. 2
β’ (πΉ:ββΆ( β€ β©
(β Γ β)) β (π β β β¦ (πΊβπ)) = (π β β β¦
(vol*β((,)β(πΉβπ))))) |
19 | 15 | ovolfsf 24858 |
. . 3
β’ (πΉ:ββΆ( β€ β©
(β Γ β)) β πΊ:ββΆ(0[,)+β)) |
20 | 19 | feqmptd 6914 |
. 2
β’ (πΉ:ββΆ( β€ β©
(β Γ β)) β πΊ = (π β β β¦ (πΊβπ))) |
21 | | id 22 |
. . . 4
β’ (πΉ:ββΆ( β€ β©
(β Γ β)) β πΉ:ββΆ( β€ β© (β
Γ β))) |
22 | 21 | feqmptd 6914 |
. . 3
β’ (πΉ:ββΆ( β€ β©
(β Γ β)) β πΉ = (π β β β¦ (πΉβπ))) |
23 | | ioof 13373 |
. . . . . 6
β’
(,):(β* Γ β*)βΆπ«
β |
24 | 23 | a1i 11 |
. . . . 5
β’ (πΉ:ββΆ( β€ β©
(β Γ β)) β (,):(β* Γ
β*)βΆπ« β) |
25 | 24 | ffvelcdmda 7039 |
. . . 4
β’ ((πΉ:ββΆ( β€ β©
(β Γ β)) β§ π₯ β (β* Γ
β*)) β ((,)βπ₯) β π« β) |
26 | 24 | feqmptd 6914 |
. . . 4
β’ (πΉ:ββΆ( β€ β©
(β Γ β)) β (,) = (π₯ β (β* Γ
β*) β¦ ((,)βπ₯))) |
27 | | ovolf 24869 |
. . . . . 6
β’
vol*:π« ββΆ(0[,]+β) |
28 | 27 | a1i 11 |
. . . . 5
β’ (πΉ:ββΆ( β€ β©
(β Γ β)) β vol*:π«
ββΆ(0[,]+β)) |
29 | 28 | feqmptd 6914 |
. . . 4
β’ (πΉ:ββΆ( β€ β©
(β Γ β)) β vol* = (π¦ β π« β β¦
(vol*βπ¦))) |
30 | | fveq2 6846 |
. . . 4
β’ (π¦ = ((,)βπ₯) β (vol*βπ¦) = (vol*β((,)βπ₯))) |
31 | 25, 26, 29, 30 | fmptco 7079 |
. . 3
β’ (πΉ:ββΆ( β€ β©
(β Γ β)) β (vol* β (,)) = (π₯ β (β* Γ
β*) β¦ (vol*β((,)βπ₯)))) |
32 | | 2fveq3 6851 |
. . 3
β’ (π₯ = (πΉβπ) β (vol*β((,)βπ₯)) =
(vol*β((,)β(πΉβπ)))) |
33 | 8, 22, 31, 32 | fmptco 7079 |
. 2
β’ (πΉ:ββΆ( β€ β©
(β Γ β)) β ((vol* β (,)) β πΉ) = (π β β β¦
(vol*β((,)β(πΉβπ))))) |
34 | 18, 20, 33 | 3eqtr4d 2783 |
1
β’ (πΉ:ββΆ( β€ β©
(β Γ β)) β πΊ = ((vol* β (,)) β πΉ)) |