Step | Hyp | Ref
| Expression |
1 | | fveq2 6862 |
. . . . . 6
β’ (π = β
β
(voln*βπ) =
(voln*ββ
)) |
2 | 1 | fveq1d 6864 |
. . . . 5
β’ (π = β
β
((voln*βπ)βπ΄) = ((voln*ββ
)βπ΄)) |
3 | 2 | adantl 482 |
. . . 4
β’ ((π β§ π = β
) β ((voln*βπ)βπ΄) = ((voln*ββ
)βπ΄)) |
4 | | ovnlecvr2.s |
. . . . . . 7
β’ (π β π΄ β βͺ
π β β Xπ β
π (((πΆβπ)βπ)[,)((π·βπ)βπ))) |
5 | 4 | adantr 481 |
. . . . . 6
β’ ((π β§ π = β
) β π΄ β βͺ
π β β Xπ β
π (((πΆβπ)βπ)[,)((π·βπ)βπ))) |
6 | | 1nn 12188 |
. . . . . . . . . . 11
β’ 1 β
β |
7 | | ne0i 4314 |
. . . . . . . . . . 11
β’ (1 β
β β β β β
) |
8 | 6, 7 | ax-mp 5 |
. . . . . . . . . 10
β’ β
β β
|
9 | 8 | a1i 11 |
. . . . . . . . 9
β’ (π β β β
β
) |
10 | | iunconst 4983 |
. . . . . . . . 9
β’ (β
β β
β βͺ π β β {β
} =
{β
}) |
11 | 9, 10 | syl 17 |
. . . . . . . 8
β’ (π β βͺ π β β {β
} =
{β
}) |
12 | 11 | adantr 481 |
. . . . . . 7
β’ ((π β§ π = β
) β βͺ π β β {β
} =
{β
}) |
13 | | ixpeq1 8868 |
. . . . . . . . . . 11
β’ (π = β
β Xπ β
π (((πΆβπ)βπ)[,)((π·βπ)βπ)) = Xπ β β
(((πΆβπ)βπ)[,)((π·βπ)βπ))) |
14 | | ixp0x 8886 |
. . . . . . . . . . . 12
β’ Xπ β
β
(((πΆβπ)βπ)[,)((π·βπ)βπ)) = {β
} |
15 | 14 | a1i 11 |
. . . . . . . . . . 11
β’ (π = β
β Xπ β
β
(((πΆβπ)βπ)[,)((π·βπ)βπ)) = {β
}) |
16 | 13, 15 | eqtrd 2771 |
. . . . . . . . . 10
β’ (π = β
β Xπ β
π (((πΆβπ)βπ)[,)((π·βπ)βπ)) = {β
}) |
17 | 16 | adantr 481 |
. . . . . . . . 9
β’ ((π = β
β§ π β β) β Xπ β
π (((πΆβπ)βπ)[,)((π·βπ)βπ)) = {β
}) |
18 | 17 | iuneq2dv 4998 |
. . . . . . . 8
β’ (π = β
β βͺ π β β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ)) = βͺ
π β β
{β
}) |
19 | 18 | adantl 482 |
. . . . . . 7
β’ ((π β§ π = β
) β βͺ π β β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ)) = βͺ
π β β
{β
}) |
20 | | reex 11166 |
. . . . . . . . 9
β’ β
β V |
21 | | mapdm0 8802 |
. . . . . . . . 9
β’ (β
β V β (β βm β
) =
{β
}) |
22 | 20, 21 | ax-mp 5 |
. . . . . . . 8
β’ (β
βm β
) = {β
} |
23 | 22 | a1i 11 |
. . . . . . 7
β’ ((π β§ π = β
) β (β
βm β
) = {β
}) |
24 | 12, 19, 23 | 3eqtr4d 2781 |
. . . . . 6
β’ ((π β§ π = β
) β βͺ π β β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ)) = (β βm
β
)) |
25 | 5, 24 | sseqtrd 4002 |
. . . . 5
β’ ((π β§ π = β
) β π΄ β (β βm
β
)) |
26 | 25 | ovn0val 44944 |
. . . 4
β’ ((π β§ π = β
) β
((voln*ββ
)βπ΄) = 0) |
27 | 3, 26 | eqtrd 2771 |
. . 3
β’ ((π β§ π = β
) β ((voln*βπ)βπ΄) = 0) |
28 | | nfv 1917 |
. . . . 5
β’
β²ππ |
29 | | nnex 12183 |
. . . . . 6
β’ β
β V |
30 | 29 | a1i 11 |
. . . . 5
β’ (π β β β
V) |
31 | | icossicc 13378 |
. . . . . 6
β’
(0[,)+β) β (0[,]+β) |
32 | | ovnlecvr2.l |
. . . . . . 7
β’ πΏ = (π₯ β Fin β¦ (π β (β βm π₯), π β (β βm π₯) β¦ if(π₯ = β
, 0, βπ β π₯ (volβ((πβπ)[,)(πβπ)))))) |
33 | | ovnlecvr2.x |
. . . . . . . 8
β’ (π β π β Fin) |
34 | 33 | adantr 481 |
. . . . . . 7
β’ ((π β§ π β β) β π β Fin) |
35 | | ovnlecvr2.c |
. . . . . . . . 9
β’ (π β πΆ:ββΆ(β βm
π)) |
36 | 35 | ffvelcdmda 7055 |
. . . . . . . 8
β’ ((π β§ π β β) β (πΆβπ) β (β βm π)) |
37 | | elmapi 8809 |
. . . . . . . 8
β’ ((πΆβπ) β (β βm π) β (πΆβπ):πβΆβ) |
38 | 36, 37 | syl 17 |
. . . . . . 7
β’ ((π β§ π β β) β (πΆβπ):πβΆβ) |
39 | | ovnlecvr2.d |
. . . . . . . . 9
β’ (π β π·:ββΆ(β βm
π)) |
40 | 39 | ffvelcdmda 7055 |
. . . . . . . 8
β’ ((π β§ π β β) β (π·βπ) β (β βm π)) |
41 | | elmapi 8809 |
. . . . . . . 8
β’ ((π·βπ) β (β βm π) β (π·βπ):πβΆβ) |
42 | 40, 41 | syl 17 |
. . . . . . 7
β’ ((π β§ π β β) β (π·βπ):πβΆβ) |
43 | 32, 34, 38, 42 | hoidmvcl 44976 |
. . . . . 6
β’ ((π β§ π β β) β ((πΆβπ)(πΏβπ)(π·βπ)) β (0[,)+β)) |
44 | 31, 43 | sselid 3960 |
. . . . 5
β’ ((π β§ π β β) β ((πΆβπ)(πΏβπ)(π·βπ)) β (0[,]+β)) |
45 | 28, 30, 44 | sge0ge0mpt 44832 |
. . . 4
β’ (π β 0 β€
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ))))) |
46 | 45 | adantr 481 |
. . 3
β’ ((π β§ π = β
) β 0 β€
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ))))) |
47 | 27, 46 | eqbrtrd 5147 |
. 2
β’ ((π β§ π = β
) β ((voln*βπ)βπ΄) β€
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ))))) |
48 | | simpl 483 |
. . 3
β’ ((π β§ Β¬ π = β
) β π) |
49 | | neqne 2947 |
. . . 4
β’ (Β¬
π = β
β π β β
) |
50 | 49 | adantl 482 |
. . 3
β’ ((π β§ Β¬ π = β
) β π β β
) |
51 | 33 | adantr 481 |
. . . . 5
β’ ((π β§ π β β
) β π β Fin) |
52 | | simpr 485 |
. . . . 5
β’ ((π β§ π β β
) β π β β
) |
53 | 38 | ffvelcdmda 7055 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β) β§ π β π) β ((πΆβπ)βπ) β β) |
54 | 42 | ffvelcdmda 7055 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β) β§ π β π) β ((π·βπ)βπ) β β) |
55 | 54 | rexrd 11229 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β) β§ π β π) β ((π·βπ)βπ) β
β*) |
56 | | icossre 13370 |
. . . . . . . . . . . . 13
β’ ((((πΆβπ)βπ) β β β§ ((π·βπ)βπ) β β*) β (((πΆβπ)βπ)[,)((π·βπ)βπ)) β β) |
57 | 53, 55, 56 | syl2anc 584 |
. . . . . . . . . . . 12
β’ (((π β§ π β β) β§ π β π) β (((πΆβπ)βπ)[,)((π·βπ)βπ)) β β) |
58 | 57 | ralrimiva 3145 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β βπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ)) β β) |
59 | | ss2ixp 8870 |
. . . . . . . . . . 11
β’
(βπ β
π (((πΆβπ)βπ)[,)((π·βπ)βπ)) β β β Xπ β
π (((πΆβπ)βπ)[,)((π·βπ)βπ)) β Xπ β π β) |
60 | 58, 59 | syl 17 |
. . . . . . . . . 10
β’ ((π β§ π β β) β Xπ β
π (((πΆβπ)βπ)[,)((π·βπ)βπ)) β Xπ β π β) |
61 | 20 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β β β
V) |
62 | | ixpconstg 8866 |
. . . . . . . . . . . 12
β’ ((π β Fin β§ β β
V) β Xπ β π β = (β βm π)) |
63 | 33, 61, 62 | syl2anc 584 |
. . . . . . . . . . 11
β’ (π β Xπ β
π β = (β
βm π)) |
64 | 63 | adantr 481 |
. . . . . . . . . 10
β’ ((π β§ π β β) β Xπ β
π β = (β
βm π)) |
65 | 60, 64 | sseqtrd 4002 |
. . . . . . . . 9
β’ ((π β§ π β β) β Xπ β
π (((πΆβπ)βπ)[,)((π·βπ)βπ)) β (β βm π)) |
66 | 65 | ralrimiva 3145 |
. . . . . . . 8
β’ (π β βπ β β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ)) β (β βm π)) |
67 | | iunss 5025 |
. . . . . . . 8
β’ (βͺ π β β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ)) β (β βm π) β βπ β β Xπ β
π (((πΆβπ)βπ)[,)((π·βπ)βπ)) β (β βm π)) |
68 | 66, 67 | sylibr 233 |
. . . . . . 7
β’ (π β βͺ π β β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ)) β (β βm π)) |
69 | 4, 68 | sstrd 3972 |
. . . . . 6
β’ (π β π΄ β (β βm π)) |
70 | 69 | adantr 481 |
. . . . 5
β’ ((π β§ π β β
) β π΄ β (β βm π)) |
71 | | eqid 2731 |
. . . . 5
β’ {π§ β β*
β£ βπ β
(((β Γ β) βm π) βm β)(π΄ β βͺ π β β Xπ β π (([,) β (πβπ))βπ) β§ π§ =
(Ξ£^β(π β β β¦ βπ β π (volβ(([,) β (πβπ))βπ)))))} = {π§ β β* β£
βπ β (((β
Γ β) βm π) βm β)(π΄ β βͺ π β β Xπ β π (([,) β (πβπ))βπ) β§ π§ =
(Ξ£^β(π β β β¦ βπ β π (volβ(([,) β (πβπ))βπ)))))} |
72 | 51, 52, 70, 71 | ovnn0val 44945 |
. . . 4
β’ ((π β§ π β β
) β ((voln*βπ)βπ΄) = inf({π§ β β* β£
βπ β (((β
Γ β) βm π) βm β)(π΄ β βͺ π β β Xπ β π (([,) β (πβπ))βπ) β§ π§ =
(Ξ£^β(π β β β¦ βπ β π (volβ(([,) β (πβπ))βπ)))))}, β*, <
)) |
73 | | ssrab2 4057 |
. . . . . 6
β’ {π§ β β*
β£ βπ β
(((β Γ β) βm π) βm β)(π΄ β βͺ π β β Xπ β π (([,) β (πβπ))βπ) β§ π§ =
(Ξ£^β(π β β β¦ βπ β π (volβ(([,) β (πβπ))βπ)))))} β
β* |
74 | 73 | a1i 11 |
. . . . 5
β’ ((π β§ π β β
) β {π§ β β* β£
βπ β (((β
Γ β) βm π) βm β)(π΄ β βͺ π β β Xπ β π (([,) β (πβπ))βπ) β§ π§ =
(Ξ£^β(π β β β¦ βπ β π (volβ(([,) β (πβπ))βπ)))))} β
β*) |
75 | 28, 30, 44 | sge0xrclmpt 44822 |
. . . . . . . 8
β’ (π β
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) β
β*) |
76 | 75 | adantr 481 |
. . . . . . 7
β’ ((π β§ π β β
) β
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) β
β*) |
77 | | opelxpi 5690 |
. . . . . . . . . . . . . 14
β’ ((((πΆβπ)βπ) β β β§ ((π·βπ)βπ) β β) β β¨((πΆβπ)βπ), ((π·βπ)βπ)β© β (β Γ
β)) |
78 | 53, 54, 77 | syl2anc 584 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β) β§ π β π) β β¨((πΆβπ)βπ), ((π·βπ)βπ)β© β (β Γ
β)) |
79 | 78 | fmpttd 7083 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β (π β π β¦ β¨((πΆβπ)βπ), ((π·βπ)βπ)β©):πβΆ(β Γ
β)) |
80 | 20, 20 | xpex 7707 |
. . . . . . . . . . . . . 14
β’ (β
Γ β) β V |
81 | 80 | a1i 11 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β (β Γ
β) β V) |
82 | | elmapg 8800 |
. . . . . . . . . . . . 13
β’
(((β Γ β) β V β§ π β Fin) β ((π β π β¦ β¨((πΆβπ)βπ), ((π·βπ)βπ)β©) β ((β Γ β)
βm π)
β (π β π β¦ β¨((πΆβπ)βπ), ((π·βπ)βπ)β©):πβΆ(β Γ
β))) |
83 | 81, 34, 82 | syl2anc 584 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β ((π β π β¦ β¨((πΆβπ)βπ), ((π·βπ)βπ)β©) β ((β Γ β)
βm π)
β (π β π β¦ β¨((πΆβπ)βπ), ((π·βπ)βπ)β©):πβΆ(β Γ
β))) |
84 | 79, 83 | mpbird 256 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β (π β π β¦ β¨((πΆβπ)βπ), ((π·βπ)βπ)β©) β ((β Γ β)
βm π)) |
85 | 84 | fmpttd 7083 |
. . . . . . . . . 10
β’ (π β (π β β β¦ (π β π β¦ β¨((πΆβπ)βπ), ((π·βπ)βπ)β©)):ββΆ((β Γ
β) βm π)) |
86 | | ovexd 7412 |
. . . . . . . . . . 11
β’ (π β ((β Γ β)
βm π)
β V) |
87 | | elmapg 8800 |
. . . . . . . . . . 11
β’
((((β Γ β) βm π) β V β§ β β V) β
((π β β β¦
(π β π β¦ β¨((πΆβπ)βπ), ((π·βπ)βπ)β©)) β (((β Γ β)
βm π)
βm β) β (π β β β¦ (π β π β¦ β¨((πΆβπ)βπ), ((π·βπ)βπ)β©)):ββΆ((β Γ
β) βm π))) |
88 | 86, 30, 87 | syl2anc 584 |
. . . . . . . . . 10
β’ (π β ((π β β β¦ (π β π β¦ β¨((πΆβπ)βπ), ((π·βπ)βπ)β©)) β (((β Γ β)
βm π)
βm β) β (π β β β¦ (π β π β¦ β¨((πΆβπ)βπ), ((π·βπ)βπ)β©)):ββΆ((β Γ
β) βm π))) |
89 | 85, 88 | mpbird 256 |
. . . . . . . . 9
β’ (π β (π β β β¦ (π β π β¦ β¨((πΆβπ)βπ), ((π·βπ)βπ)β©)) β (((β Γ β)
βm π)
βm β)) |
90 | 89 | adantr 481 |
. . . . . . . 8
β’ ((π β§ π β β
) β (π β β β¦ (π β π β¦ β¨((πΆβπ)βπ), ((π·βπ)βπ)β©)) β (((β Γ β)
βm π)
βm β)) |
91 | | simpr 485 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β β) β π β β) |
92 | | mptexg 7191 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β Fin β (π β π β¦ β¨((πΆβπ)βπ), ((π·βπ)βπ)β©) β V) |
93 | 33, 92 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (π β π β¦ β¨((πΆβπ)βπ), ((π·βπ)βπ)β©) β V) |
94 | 93 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β β) β (π β π β¦ β¨((πΆβπ)βπ), ((π·βπ)βπ)β©) β V) |
95 | | eqid 2731 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β β β¦ (π β π β¦ β¨((πΆβπ)βπ), ((π·βπ)βπ)β©)) = (π β β β¦ (π β π β¦ β¨((πΆβπ)βπ), ((π·βπ)βπ)β©)) |
96 | 95 | fvmpt2 6979 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β β β§ (π β π β¦ β¨((πΆβπ)βπ), ((π·βπ)βπ)β©) β V) β ((π β β β¦ (π β π β¦ β¨((πΆβπ)βπ), ((π·βπ)βπ)β©))βπ) = (π β π β¦ β¨((πΆβπ)βπ), ((π·βπ)βπ)β©)) |
97 | 91, 94, 96 | syl2anc 584 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β β) β ((π β β β¦ (π β π β¦ β¨((πΆβπ)βπ), ((π·βπ)βπ)β©))βπ) = (π β π β¦ β¨((πΆβπ)βπ), ((π·βπ)βπ)β©)) |
98 | 97 | coeq2d 5838 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β β) β ([,) β ((π β β β¦ (π β π β¦ β¨((πΆβπ)βπ), ((π·βπ)βπ)β©))βπ)) = ([,) β (π β π β¦ β¨((πΆβπ)βπ), ((π·βπ)βπ)β©))) |
99 | 98 | fveq1d 6864 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β) β (([,) β ((π β β β¦ (π β π β¦ β¨((πΆβπ)βπ), ((π·βπ)βπ)β©))βπ))βπ) = (([,) β (π β π β¦ β¨((πΆβπ)βπ), ((π·βπ)βπ)β©))βπ)) |
100 | 99 | adantr 481 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β) β§ π β π) β (([,) β ((π β β β¦ (π β π β¦ β¨((πΆβπ)βπ), ((π·βπ)βπ)β©))βπ))βπ) = (([,) β (π β π β¦ β¨((πΆβπ)βπ), ((π·βπ)βπ)β©))βπ)) |
101 | 79 | adantr 481 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β) β§ π β π) β (π β π β¦ β¨((πΆβπ)βπ), ((π·βπ)βπ)β©):πβΆ(β Γ
β)) |
102 | | simpr 485 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β) β§ π β π) β π β π) |
103 | 101, 102 | fvovco 43568 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β) β§ π β π) β (([,) β (π β π β¦ β¨((πΆβπ)βπ), ((π·βπ)βπ)β©))βπ) = ((1st β((π β π β¦ β¨((πΆβπ)βπ), ((π·βπ)βπ)β©)βπ))[,)(2nd β((π β π β¦ β¨((πΆβπ)βπ), ((π·βπ)βπ)β©)βπ)))) |
104 | | simpr 485 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β π) β π β π) |
105 | | opex 5441 |
. . . . . . . . . . . . . . . . . . . 20
β’
β¨((πΆβπ)βπ), ((π·βπ)βπ)β© β V |
106 | 105 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β π) β β¨((πΆβπ)βπ), ((π·βπ)βπ)β© β V) |
107 | | eqid 2731 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β π β¦ β¨((πΆβπ)βπ), ((π·βπ)βπ)β©) = (π β π β¦ β¨((πΆβπ)βπ), ((π·βπ)βπ)β©) |
108 | 107 | fvmpt2 6979 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β π β§ β¨((πΆβπ)βπ), ((π·βπ)βπ)β© β V) β ((π β π β¦ β¨((πΆβπ)βπ), ((π·βπ)βπ)β©)βπ) = β¨((πΆβπ)βπ), ((π·βπ)βπ)β©) |
109 | 104, 106,
108 | syl2anc 584 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β π) β ((π β π β¦ β¨((πΆβπ)βπ), ((π·βπ)βπ)β©)βπ) = β¨((πΆβπ)βπ), ((π·βπ)βπ)β©) |
110 | 109 | fveq2d 6866 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β π) β (1st β((π β π β¦ β¨((πΆβπ)βπ), ((π·βπ)βπ)β©)βπ)) = (1st ββ¨((πΆβπ)βπ), ((π·βπ)βπ)β©)) |
111 | | fvex 6875 |
. . . . . . . . . . . . . . . . . . 19
β’ ((πΆβπ)βπ) β V |
112 | | fvex 6875 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π·βπ)βπ) β V |
113 | | op1stg 7953 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((πΆβπ)βπ) β V β§ ((π·βπ)βπ) β V) β (1st
ββ¨((πΆβπ)βπ), ((π·βπ)βπ)β©) = ((πΆβπ)βπ)) |
114 | 111, 112,
113 | mp2an 690 |
. . . . . . . . . . . . . . . . . 18
β’
(1st ββ¨((πΆβπ)βπ), ((π·βπ)βπ)β©) = ((πΆβπ)βπ) |
115 | 114 | a1i 11 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β π) β (1st
ββ¨((πΆβπ)βπ), ((π·βπ)βπ)β©) = ((πΆβπ)βπ)) |
116 | 110, 115 | eqtrd 2771 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β π) β (1st β((π β π β¦ β¨((πΆβπ)βπ), ((π·βπ)βπ)β©)βπ)) = ((πΆβπ)βπ)) |
117 | 109 | fveq2d 6866 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β π) β (2nd β((π β π β¦ β¨((πΆβπ)βπ), ((π·βπ)βπ)β©)βπ)) = (2nd ββ¨((πΆβπ)βπ), ((π·βπ)βπ)β©)) |
118 | 111, 112 | op2nd 7950 |
. . . . . . . . . . . . . . . . . 18
β’
(2nd ββ¨((πΆβπ)βπ), ((π·βπ)βπ)β©) = ((π·βπ)βπ) |
119 | 118 | a1i 11 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β π) β (2nd
ββ¨((πΆβπ)βπ), ((π·βπ)βπ)β©) = ((π·βπ)βπ)) |
120 | 117, 119 | eqtrd 2771 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β π) β (2nd β((π β π β¦ β¨((πΆβπ)βπ), ((π·βπ)βπ)β©)βπ)) = ((π·βπ)βπ)) |
121 | 116, 120 | oveq12d 7395 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β π) β ((1st β((π β π β¦ β¨((πΆβπ)βπ), ((π·βπ)βπ)β©)βπ))[,)(2nd β((π β π β¦ β¨((πΆβπ)βπ), ((π·βπ)βπ)β©)βπ))) = (((πΆβπ)βπ)[,)((π·βπ)βπ))) |
122 | 121 | adantlr 713 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β) β§ π β π) β ((1st β((π β π β¦ β¨((πΆβπ)βπ), ((π·βπ)βπ)β©)βπ))[,)(2nd β((π β π β¦ β¨((πΆβπ)βπ), ((π·βπ)βπ)β©)βπ))) = (((πΆβπ)βπ)[,)((π·βπ)βπ))) |
123 | 100, 103,
122 | 3eqtrrd 2776 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β) β§ π β π) β (((πΆβπ)βπ)[,)((π·βπ)βπ)) = (([,) β ((π β β β¦ (π β π β¦ β¨((πΆβπ)βπ), ((π·βπ)βπ)β©))βπ))βπ)) |
124 | 123 | ixpeq2dva 8872 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β Xπ β
π (((πΆβπ)βπ)[,)((π·βπ)βπ)) = Xπ β π (([,) β ((π β β β¦ (π β π β¦ β¨((πΆβπ)βπ), ((π·βπ)βπ)β©))βπ))βπ)) |
125 | 124 | iuneq2dv 4998 |
. . . . . . . . . . 11
β’ (π β βͺ π β β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ)) = βͺ
π β β Xπ β
π (([,) β ((π β β β¦ (π β π β¦ β¨((πΆβπ)βπ), ((π·βπ)βπ)β©))βπ))βπ)) |
126 | 4, 125 | sseqtrd 4002 |
. . . . . . . . . 10
β’ (π β π΄ β βͺ
π β β Xπ β
π (([,) β ((π β β β¦ (π β π β¦ β¨((πΆβπ)βπ), ((π·βπ)βπ)β©))βπ))βπ)) |
127 | 126 | adantr 481 |
. . . . . . . . 9
β’ ((π β§ π β β
) β π΄ β βͺ
π β β Xπ β
π (([,) β ((π β β β¦ (π β π β¦ β¨((πΆβπ)βπ), ((π·βπ)βπ)β©))βπ))βπ)) |
128 | | eqidd 2732 |
. . . . . . . . . 10
β’ ((π β§ π β β
) β
(Ξ£^β(π β β β¦ βπ β π (volβ(((πΆβπ)βπ)[,)((π·βπ)βπ))))) =
(Ξ£^β(π β β β¦ βπ β π (volβ(((πΆβπ)βπ)[,)((π·βπ)βπ)))))) |
129 | 51 | adantr 481 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β
) β§ π β β) β π β Fin) |
130 | 52 | adantr 481 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β
) β§ π β β) β π β β
) |
131 | 38 | adantlr 713 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β
) β§ π β β) β (πΆβπ):πβΆβ) |
132 | 42 | adantlr 713 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β
) β§ π β β) β (π·βπ):πβΆβ) |
133 | 32, 129, 130, 131, 132 | hoidmvn0val 44978 |
. . . . . . . . . . . 12
β’ (((π β§ π β β
) β§ π β β) β ((πΆβπ)(πΏβπ)(π·βπ)) = βπ β π (volβ(((πΆβπ)βπ)[,)((π·βπ)βπ)))) |
134 | 133 | mpteq2dva 5225 |
. . . . . . . . . . 11
β’ ((π β§ π β β
) β (π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ))) = (π β β β¦ βπ β π (volβ(((πΆβπ)βπ)[,)((π·βπ)βπ))))) |
135 | 134 | fveq2d 6866 |
. . . . . . . . . 10
β’ ((π β§ π β β
) β
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) =
(Ξ£^β(π β β β¦ βπ β π (volβ(((πΆβπ)βπ)[,)((π·βπ)βπ)))))) |
136 | 123 | eqcomd 2737 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β) β§ π β π) β (([,) β ((π β β β¦ (π β π β¦ β¨((πΆβπ)βπ), ((π·βπ)βπ)β©))βπ))βπ) = (((πΆβπ)βπ)[,)((π·βπ)βπ))) |
137 | 136 | fveq2d 6866 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β) β§ π β π) β (volβ(([,) β ((π β β β¦ (π β π β¦ β¨((πΆβπ)βπ), ((π·βπ)βπ)β©))βπ))βπ)) = (volβ(((πΆβπ)βπ)[,)((π·βπ)βπ)))) |
138 | 137 | prodeq2dv 15832 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β βπ β π (volβ(([,) β ((π β β β¦ (π β π β¦ β¨((πΆβπ)βπ), ((π·βπ)βπ)β©))βπ))βπ)) = βπ β π (volβ(((πΆβπ)βπ)[,)((π·βπ)βπ)))) |
139 | 138 | mpteq2dva 5225 |
. . . . . . . . . . . 12
β’ (π β (π β β β¦ βπ β π (volβ(([,) β ((π β β β¦ (π β π β¦ β¨((πΆβπ)βπ), ((π·βπ)βπ)β©))βπ))βπ))) = (π β β β¦ βπ β π (volβ(((πΆβπ)βπ)[,)((π·βπ)βπ))))) |
140 | 139 | fveq2d 6866 |
. . . . . . . . . . 11
β’ (π β
(Ξ£^β(π β β β¦ βπ β π (volβ(([,) β ((π β β β¦ (π β π β¦ β¨((πΆβπ)βπ), ((π·βπ)βπ)β©))βπ))βπ)))) =
(Ξ£^β(π β β β¦ βπ β π (volβ(((πΆβπ)βπ)[,)((π·βπ)βπ)))))) |
141 | 140 | adantr 481 |
. . . . . . . . . 10
β’ ((π β§ π β β
) β
(Ξ£^β(π β β β¦ βπ β π (volβ(([,) β ((π β β β¦ (π β π β¦ β¨((πΆβπ)βπ), ((π·βπ)βπ)β©))βπ))βπ)))) =
(Ξ£^β(π β β β¦ βπ β π (volβ(((πΆβπ)βπ)[,)((π·βπ)βπ)))))) |
142 | 128, 135,
141 | 3eqtr4d 2781 |
. . . . . . . . 9
β’ ((π β§ π β β
) β
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) =
(Ξ£^β(π β β β¦ βπ β π (volβ(([,) β ((π β β β¦ (π β π β¦ β¨((πΆβπ)βπ), ((π·βπ)βπ)β©))βπ))βπ))))) |
143 | 127, 142 | jca 512 |
. . . . . . . 8
β’ ((π β§ π β β
) β (π΄ β βͺ
π β β Xπ β
π (([,) β ((π β β β¦ (π β π β¦ β¨((πΆβπ)βπ), ((π·βπ)βπ)β©))βπ))βπ) β§
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) =
(Ξ£^β(π β β β¦ βπ β π (volβ(([,) β ((π β β β¦ (π β π β¦ β¨((πΆβπ)βπ), ((π·βπ)βπ)β©))βπ))βπ)))))) |
144 | | nfcv 2902 |
. . . . . . . . . . . . 13
β’
β²ππ |
145 | | nfmpt1 5233 |
. . . . . . . . . . . . 13
β’
β²π(π β β β¦ (π β π β¦ β¨((πΆβπ)βπ), ((π·βπ)βπ)β©)) |
146 | 144, 145 | nfeq 2915 |
. . . . . . . . . . . 12
β’
β²π π = (π β β β¦ (π β π β¦ β¨((πΆβπ)βπ), ((π·βπ)βπ)β©)) |
147 | | nfcv 2902 |
. . . . . . . . . . . . . . 15
β’
β²ππ |
148 | | nfcv 2902 |
. . . . . . . . . . . . . . . 16
β’
β²πβ |
149 | | nfmpt1 5233 |
. . . . . . . . . . . . . . . 16
β’
β²π(π β π β¦ β¨((πΆβπ)βπ), ((π·βπ)βπ)β©) |
150 | 148, 149 | nfmpt 5232 |
. . . . . . . . . . . . . . 15
β’
β²π(π β β β¦ (π β π β¦ β¨((πΆβπ)βπ), ((π·βπ)βπ)β©)) |
151 | 147, 150 | nfeq 2915 |
. . . . . . . . . . . . . 14
β’
β²π π = (π β β β¦ (π β π β¦ β¨((πΆβπ)βπ), ((π·βπ)βπ)β©)) |
152 | | fveq1 6861 |
. . . . . . . . . . . . . . . . 17
β’ (π = (π β β β¦ (π β π β¦ β¨((πΆβπ)βπ), ((π·βπ)βπ)β©)) β (πβπ) = ((π β β β¦ (π β π β¦ β¨((πΆβπ)βπ), ((π·βπ)βπ)β©))βπ)) |
153 | 152 | coeq2d 5838 |
. . . . . . . . . . . . . . . 16
β’ (π = (π β β β¦ (π β π β¦ β¨((πΆβπ)βπ), ((π·βπ)βπ)β©)) β ([,) β (πβπ)) = ([,) β ((π β β β¦ (π β π β¦ β¨((πΆβπ)βπ), ((π·βπ)βπ)β©))βπ))) |
154 | 153 | fveq1d 6864 |
. . . . . . . . . . . . . . 15
β’ (π = (π β β β¦ (π β π β¦ β¨((πΆβπ)βπ), ((π·βπ)βπ)β©)) β (([,) β (πβπ))βπ) = (([,) β ((π β β β¦ (π β π β¦ β¨((πΆβπ)βπ), ((π·βπ)βπ)β©))βπ))βπ)) |
155 | 154 | adantr 481 |
. . . . . . . . . . . . . 14
β’ ((π = (π β β β¦ (π β π β¦ β¨((πΆβπ)βπ), ((π·βπ)βπ)β©)) β§ π β π) β (([,) β (πβπ))βπ) = (([,) β ((π β β β¦ (π β π β¦ β¨((πΆβπ)βπ), ((π·βπ)βπ)β©))βπ))βπ)) |
156 | 151, 155 | ixpeq2d 43431 |
. . . . . . . . . . . . 13
β’ (π = (π β β β¦ (π β π β¦ β¨((πΆβπ)βπ), ((π·βπ)βπ)β©)) β Xπ β
π (([,) β (πβπ))βπ) = Xπ β π (([,) β ((π β β β¦ (π β π β¦ β¨((πΆβπ)βπ), ((π·βπ)βπ)β©))βπ))βπ)) |
157 | 156 | adantr 481 |
. . . . . . . . . . . 12
β’ ((π = (π β β β¦ (π β π β¦ β¨((πΆβπ)βπ), ((π·βπ)βπ)β©)) β§ π β β) β Xπ β
π (([,) β (πβπ))βπ) = Xπ β π (([,) β ((π β β β¦ (π β π β¦ β¨((πΆβπ)βπ), ((π·βπ)βπ)β©))βπ))βπ)) |
158 | 146, 157 | iuneq2df 43409 |
. . . . . . . . . . 11
β’ (π = (π β β β¦ (π β π β¦ β¨((πΆβπ)βπ), ((π·βπ)βπ)β©)) β βͺ π β β Xπ β π (([,) β (πβπ))βπ) = βͺ π β β Xπ β
π (([,) β ((π β β β¦ (π β π β¦ β¨((πΆβπ)βπ), ((π·βπ)βπ)β©))βπ))βπ)) |
159 | 158 | sseq2d 3994 |
. . . . . . . . . 10
β’ (π = (π β β β¦ (π β π β¦ β¨((πΆβπ)βπ), ((π·βπ)βπ)β©)) β (π΄ β βͺ
π β β Xπ β
π (([,) β (πβπ))βπ) β π΄ β βͺ
π β β Xπ β
π (([,) β ((π β β β¦ (π β π β¦ β¨((πΆβπ)βπ), ((π·βπ)βπ)β©))βπ))βπ))) |
160 | | nfv 1917 |
. . . . . . . . . . . . . . . 16
β’
β²π π β β |
161 | 151, 160 | nfan 1902 |
. . . . . . . . . . . . . . 15
β’
β²π(π = (π β β β¦ (π β π β¦ β¨((πΆβπ)βπ), ((π·βπ)βπ)β©)) β§ π β β) |
162 | 154 | fveq2d 6866 |
. . . . . . . . . . . . . . . . 17
β’ (π = (π β β β¦ (π β π β¦ β¨((πΆβπ)βπ), ((π·βπ)βπ)β©)) β (volβ(([,) β
(πβπ))βπ)) = (volβ(([,) β ((π β β β¦ (π β π β¦ β¨((πΆβπ)βπ), ((π·βπ)βπ)β©))βπ))βπ))) |
163 | 162 | a1d 25 |
. . . . . . . . . . . . . . . 16
β’ (π = (π β β β¦ (π β π β¦ β¨((πΆβπ)βπ), ((π·βπ)βπ)β©)) β (π β π β (volβ(([,) β (πβπ))βπ)) = (volβ(([,) β ((π β β β¦ (π β π β¦ β¨((πΆβπ)βπ), ((π·βπ)βπ)β©))βπ))βπ)))) |
164 | 163 | adantr 481 |
. . . . . . . . . . . . . . 15
β’ ((π = (π β β β¦ (π β π β¦ β¨((πΆβπ)βπ), ((π·βπ)βπ)β©)) β§ π β β) β (π β π β (volβ(([,) β (πβπ))βπ)) = (volβ(([,) β ((π β β β¦ (π β π β¦ β¨((πΆβπ)βπ), ((π·βπ)βπ)β©))βπ))βπ)))) |
165 | 161, 164 | ralrimi 3251 |
. . . . . . . . . . . . . 14
β’ ((π = (π β β β¦ (π β π β¦ β¨((πΆβπ)βπ), ((π·βπ)βπ)β©)) β§ π β β) β βπ β π (volβ(([,) β (πβπ))βπ)) = (volβ(([,) β ((π β β β¦ (π β π β¦ β¨((πΆβπ)βπ), ((π·βπ)βπ)β©))βπ))βπ))) |
166 | 165 | prodeq2d 15831 |
. . . . . . . . . . . . 13
β’ ((π = (π β β β¦ (π β π β¦ β¨((πΆβπ)βπ), ((π·βπ)βπ)β©)) β§ π β β) β βπ β π (volβ(([,) β (πβπ))βπ)) = βπ β π (volβ(([,) β ((π β β β¦ (π β π β¦ β¨((πΆβπ)βπ), ((π·βπ)βπ)β©))βπ))βπ))) |
167 | 146, 166 | mpteq2da 5223 |
. . . . . . . . . . . 12
β’ (π = (π β β β¦ (π β π β¦ β¨((πΆβπ)βπ), ((π·βπ)βπ)β©)) β (π β β β¦ βπ β π (volβ(([,) β (πβπ))βπ))) = (π β β β¦ βπ β π (volβ(([,) β ((π β β β¦ (π β π β¦ β¨((πΆβπ)βπ), ((π·βπ)βπ)β©))βπ))βπ)))) |
168 | 167 | fveq2d 6866 |
. . . . . . . . . . 11
β’ (π = (π β β β¦ (π β π β¦ β¨((πΆβπ)βπ), ((π·βπ)βπ)β©)) β
(Ξ£^β(π β β β¦ βπ β π (volβ(([,) β (πβπ))βπ)))) =
(Ξ£^β(π β β β¦ βπ β π (volβ(([,) β ((π β β β¦ (π β π β¦ β¨((πΆβπ)βπ), ((π·βπ)βπ)β©))βπ))βπ))))) |
169 | 168 | eqeq2d 2742 |
. . . . . . . . . 10
β’ (π = (π β β β¦ (π β π β¦ β¨((πΆβπ)βπ), ((π·βπ)βπ)β©)) β
((Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) =
(Ξ£^β(π β β β¦ βπ β π (volβ(([,) β (πβπ))βπ)))) β
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) =
(Ξ£^β(π β β β¦ βπ β π (volβ(([,) β ((π β β β¦ (π β π β¦ β¨((πΆβπ)βπ), ((π·βπ)βπ)β©))βπ))βπ)))))) |
170 | 159, 169 | anbi12d 631 |
. . . . . . . . 9
β’ (π = (π β β β¦ (π β π β¦ β¨((πΆβπ)βπ), ((π·βπ)βπ)β©)) β ((π΄ β βͺ
π β β Xπ β
π (([,) β (πβπ))βπ) β§
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) =
(Ξ£^β(π β β β¦ βπ β π (volβ(([,) β (πβπ))βπ))))) β (π΄ β βͺ
π β β Xπ β
π (([,) β ((π β β β¦ (π β π β¦ β¨((πΆβπ)βπ), ((π·βπ)βπ)β©))βπ))βπ) β§
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) =
(Ξ£^β(π β β β¦ βπ β π (volβ(([,) β ((π β β β¦ (π β π β¦ β¨((πΆβπ)βπ), ((π·βπ)βπ)β©))βπ))βπ))))))) |
171 | 170 | rspcev 3595 |
. . . . . . . 8
β’ (((π β β β¦ (π β π β¦ β¨((πΆβπ)βπ), ((π·βπ)βπ)β©)) β (((β Γ β)
βm π)
βm β) β§ (π΄ β βͺ
π β β Xπ β
π (([,) β ((π β β β¦ (π β π β¦ β¨((πΆβπ)βπ), ((π·βπ)βπ)β©))βπ))βπ) β§
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) =
(Ξ£^β(π β β β¦ βπ β π (volβ(([,) β ((π β β β¦ (π β π β¦ β¨((πΆβπ)βπ), ((π·βπ)βπ)β©))βπ))βπ)))))) β βπ β (((β Γ β)
βm π)
βm β)(π΄ β βͺ
π β β Xπ β
π (([,) β (πβπ))βπ) β§
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) =
(Ξ£^β(π β β β¦ βπ β π (volβ(([,) β (πβπ))βπ)))))) |
172 | 90, 143, 171 | syl2anc 584 |
. . . . . . 7
β’ ((π β§ π β β
) β βπ β (((β Γ
β) βm π) βm β)(π΄ β βͺ π β β Xπ β π (([,) β (πβπ))βπ) β§
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) =
(Ξ£^β(π β β β¦ βπ β π (volβ(([,) β (πβπ))βπ)))))) |
173 | 76, 172 | jca 512 |
. . . . . 6
β’ ((π β§ π β β
) β
((Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) β β* β§
βπ β (((β
Γ β) βm π) βm β)(π΄ β βͺ π β β Xπ β π (([,) β (πβπ))βπ) β§
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) =
(Ξ£^β(π β β β¦ βπ β π (volβ(([,) β (πβπ))βπ))))))) |
174 | | eqeq1 2735 |
. . . . . . . . 9
β’ (π§ =
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) β (π§ =
(Ξ£^β(π β β β¦ βπ β π (volβ(([,) β (πβπ))βπ)))) β
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) =
(Ξ£^β(π β β β¦ βπ β π (volβ(([,) β (πβπ))βπ)))))) |
175 | 174 | anbi2d 629 |
. . . . . . . 8
β’ (π§ =
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) β ((π΄ β βͺ
π β β Xπ β
π (([,) β (πβπ))βπ) β§ π§ =
(Ξ£^β(π β β β¦ βπ β π (volβ(([,) β (πβπ))βπ))))) β (π΄ β βͺ
π β β Xπ β
π (([,) β (πβπ))βπ) β§
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) =
(Ξ£^β(π β β β¦ βπ β π (volβ(([,) β (πβπ))βπ))))))) |
176 | 175 | rexbidv 3177 |
. . . . . . 7
β’ (π§ =
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) β (βπ β (((β Γ β)
βm π)
βm β)(π΄ β βͺ
π β β Xπ β
π (([,) β (πβπ))βπ) β§ π§ =
(Ξ£^β(π β β β¦ βπ β π (volβ(([,) β (πβπ))βπ))))) β βπ β (((β Γ β)
βm π)
βm β)(π΄ β βͺ
π β β Xπ β
π (([,) β (πβπ))βπ) β§
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) =
(Ξ£^β(π β β β¦ βπ β π (volβ(([,) β (πβπ))βπ))))))) |
177 | 176 | elrab 3663 |
. . . . . 6
β’
((Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) β {π§ β β* β£
βπ β (((β
Γ β) βm π) βm β)(π΄ β βͺ π β β Xπ β π (([,) β (πβπ))βπ) β§ π§ =
(Ξ£^β(π β β β¦ βπ β π (volβ(([,) β (πβπ))βπ)))))} β
((Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) β β* β§
βπ β (((β
Γ β) βm π) βm β)(π΄ β βͺ π β β Xπ β π (([,) β (πβπ))βπ) β§
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) =
(Ξ£^β(π β β β¦ βπ β π (volβ(([,) β (πβπ))βπ))))))) |
178 | 173, 177 | sylibr 233 |
. . . . 5
β’ ((π β§ π β β
) β
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) β {π§ β β* β£
βπ β (((β
Γ β) βm π) βm β)(π΄ β βͺ π β β Xπ β π (([,) β (πβπ))βπ) β§ π§ =
(Ξ£^β(π β β β¦ βπ β π (volβ(([,) β (πβπ))βπ)))))}) |
179 | | infxrlb 13278 |
. . . . 5
β’ (({π§ β β*
β£ βπ β
(((β Γ β) βm π) βm β)(π΄ β βͺ π β β Xπ β π (([,) β (πβπ))βπ) β§ π§ =
(Ξ£^β(π β β β¦ βπ β π (volβ(([,) β (πβπ))βπ)))))} β β* β§
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) β {π§ β β* β£
βπ β (((β
Γ β) βm π) βm β)(π΄ β βͺ π β β Xπ β π (([,) β (πβπ))βπ) β§ π§ =
(Ξ£^β(π β β β¦ βπ β π (volβ(([,) β (πβπ))βπ)))))}) β inf({π§ β β* β£
βπ β (((β
Γ β) βm π) βm β)(π΄ β βͺ π β β Xπ β π (([,) β (πβπ))βπ) β§ π§ =
(Ξ£^β(π β β β¦ βπ β π (volβ(([,) β (πβπ))βπ)))))}, β*, < ) β€
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ))))) |
180 | 74, 178, 179 | syl2anc 584 |
. . . 4
β’ ((π β§ π β β
) β inf({π§ β β*
β£ βπ β
(((β Γ β) βm π) βm β)(π΄ β βͺ π β β Xπ β π (([,) β (πβπ))βπ) β§ π§ =
(Ξ£^β(π β β β¦ βπ β π (volβ(([,) β (πβπ))βπ)))))}, β*, < ) β€
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ))))) |
181 | 72, 180 | eqbrtrd 5147 |
. . 3
β’ ((π β§ π β β
) β ((voln*βπ)βπ΄) β€
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ))))) |
182 | 48, 50, 181 | syl2anc 584 |
. 2
β’ ((π β§ Β¬ π = β
) β ((voln*βπ)βπ΄) β€
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ))))) |
183 | 47, 182 | pm2.61dan 811 |
1
β’ (π β ((voln*βπ)βπ΄) β€
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ))))) |