Step | Hyp | Ref
| Expression |
1 | | ovnhoi.x |
. . 3
β’ (π β π β Fin) |
2 | | ovnhoi.c |
. . . . 5
β’ πΌ = Xπ β π ((π΄βπ)[,)(π΅βπ)) |
3 | 2 | a1i 11 |
. . . 4
β’ (π β πΌ = Xπ β π ((π΄βπ)[,)(π΅βπ))) |
4 | | nfv 1917 |
. . . . 5
β’
β²ππ |
5 | | ovnhoi.a |
. . . . . 6
β’ (π β π΄:πβΆβ) |
6 | 5 | ffvelcdmda 7031 |
. . . . 5
β’ ((π β§ π β π) β (π΄βπ) β β) |
7 | | ovnhoi.b |
. . . . . . 7
β’ (π β π΅:πβΆβ) |
8 | 7 | ffvelcdmda 7031 |
. . . . . 6
β’ ((π β§ π β π) β (π΅βπ) β β) |
9 | 8 | rexrd 11163 |
. . . . 5
β’ ((π β§ π β π) β (π΅βπ) β
β*) |
10 | 4, 6, 9 | hoissrrn2 44720 |
. . . 4
β’ (π β Xπ β
π ((π΄βπ)[,)(π΅βπ)) β (β βm π)) |
11 | 3, 10 | eqsstrd 3980 |
. . 3
β’ (π β πΌ β (β βm π)) |
12 | 1, 11 | ovnxrcl 44711 |
. 2
β’ (π β ((voln*βπ)βπΌ) β
β*) |
13 | | icossxr 13303 |
. . 3
β’
(0[,)+β) β β* |
14 | | ovnhoi.l |
. . . 4
β’ πΏ = (π₯ β Fin β¦ (π β (β βm π₯), π β (β βm π₯) β¦ if(π₯ = β
, 0, βπ β π₯ (volβ((πβπ)[,)(πβπ)))))) |
15 | 14, 1, 5, 7 | hoidmvcl 44724 |
. . 3
β’ (π β (π΄(πΏβπ)π΅) β (0[,)+β)) |
16 | 13, 15 | sselid 3940 |
. 2
β’ (π β (π΄(πΏβπ)π΅) β
β*) |
17 | | fveq2 6839 |
. . . . . . . 8
β’ (π = β
β
(voln*βπ) =
(voln*ββ
)) |
18 | 17 | fveq1d 6841 |
. . . . . . 7
β’ (π = β
β
((voln*βπ)βπΌ) = ((voln*ββ
)βπΌ)) |
19 | 18 | adantl 482 |
. . . . . 6
β’ ((π β§ π = β
) β ((voln*βπ)βπΌ) = ((voln*ββ
)βπΌ)) |
20 | | ixpeq1 8804 |
. . . . . . . . . . 11
β’ (π = β
β Xπ β
π ((π΄βπ)[,)(π΅βπ)) = Xπ β β
((π΄βπ)[,)(π΅βπ))) |
21 | | ixp0x 8822 |
. . . . . . . . . . . 12
β’ Xπ β
β
((π΄βπ)[,)(π΅βπ)) = {β
} |
22 | 21 | a1i 11 |
. . . . . . . . . . 11
β’ (π = β
β Xπ β
β
((π΄βπ)[,)(π΅βπ)) = {β
}) |
23 | 20, 22 | eqtrd 2777 |
. . . . . . . . . 10
β’ (π = β
β Xπ β
π ((π΄βπ)[,)(π΅βπ)) = {β
}) |
24 | 23 | adantl 482 |
. . . . . . . . 9
β’ ((π β§ π = β
) β Xπ β
π ((π΄βπ)[,)(π΅βπ)) = {β
}) |
25 | 2 | a1i 11 |
. . . . . . . . 9
β’ ((π β§ π = β
) β πΌ = Xπ β π ((π΄βπ)[,)(π΅βπ))) |
26 | | reex 11100 |
. . . . . . . . . . 11
β’ β
β V |
27 | | mapdm0 8738 |
. . . . . . . . . . 11
β’ (β
β V β (β βm β
) =
{β
}) |
28 | 26, 27 | ax-mp 5 |
. . . . . . . . . 10
β’ (β
βm β
) = {β
} |
29 | 28 | a1i 11 |
. . . . . . . . 9
β’ ((π β§ π = β
) β (β
βm β
) = {β
}) |
30 | 24, 25, 29 | 3eqtr4d 2787 |
. . . . . . . 8
β’ ((π β§ π = β
) β πΌ = (β βm
β
)) |
31 | | eqimss 3998 |
. . . . . . . 8
β’ (πΌ = (β βm
β
) β πΌ β
(β βm β
)) |
32 | 30, 31 | syl 17 |
. . . . . . 7
β’ ((π β§ π = β
) β πΌ β (β βm
β
)) |
33 | 32 | ovn0val 44692 |
. . . . . 6
β’ ((π β§ π = β
) β
((voln*ββ
)βπΌ) = 0) |
34 | 19, 33 | eqtrd 2777 |
. . . . 5
β’ ((π β§ π = β
) β ((voln*βπ)βπΌ) = 0) |
35 | | 0red 11116 |
. . . . 5
β’ ((π β§ π = β
) β 0 β
β) |
36 | 34, 35 | eqeltrd 2838 |
. . . 4
β’ ((π β§ π = β
) β ((voln*βπ)βπΌ) β β) |
37 | | eqidd 2738 |
. . . . 5
β’ ((π β§ π = β
) β 0 = 0) |
38 | | fveq2 6839 |
. . . . . . . 8
β’ (π = β
β (πΏβπ) = (πΏββ
)) |
39 | 38 | oveqd 7368 |
. . . . . . 7
β’ (π = β
β (π΄(πΏβπ)π΅) = (π΄(πΏββ
)π΅)) |
40 | 39 | adantl 482 |
. . . . . 6
β’ ((π β§ π = β
) β (π΄(πΏβπ)π΅) = (π΄(πΏββ
)π΅)) |
41 | 5 | adantr 481 |
. . . . . . . 8
β’ ((π β§ π = β
) β π΄:πβΆβ) |
42 | | simpr 485 |
. . . . . . . . 9
β’ ((π β§ π = β
) β π = β
) |
43 | 42 | feq2d 6651 |
. . . . . . . 8
β’ ((π β§ π = β
) β (π΄:πβΆβ β π΄:β
βΆβ)) |
44 | 41, 43 | mpbid 231 |
. . . . . . 7
β’ ((π β§ π = β
) β π΄:β
βΆβ) |
45 | 7 | adantr 481 |
. . . . . . . 8
β’ ((π β§ π = β
) β π΅:πβΆβ) |
46 | 42 | feq2d 6651 |
. . . . . . . 8
β’ ((π β§ π = β
) β (π΅:πβΆβ β π΅:β
βΆβ)) |
47 | 45, 46 | mpbid 231 |
. . . . . . 7
β’ ((π β§ π = β
) β π΅:β
βΆβ) |
48 | 14, 44, 47 | hoidmv0val 44725 |
. . . . . 6
β’ ((π β§ π = β
) β (π΄(πΏββ
)π΅) = 0) |
49 | 40, 48 | eqtrd 2777 |
. . . . 5
β’ ((π β§ π = β
) β (π΄(πΏβπ)π΅) = 0) |
50 | 37, 34, 49 | 3eqtr4d 2787 |
. . . 4
β’ ((π β§ π = β
) β ((voln*βπ)βπΌ) = (π΄(πΏβπ)π΅)) |
51 | 36, 50 | eqled 11216 |
. . 3
β’ ((π β§ π = β
) β ((voln*βπ)βπΌ) β€ (π΄(πΏβπ)π΅)) |
52 | | eqid 2737 |
. . . . . 6
β’ {π§ β β*
β£ βπ β
(((β Γ β) βm π) βm β)(πΌ β βͺ π β β Xπ β π (([,) β (πβπ))βπ) β§ π§ =
(Ξ£^β(π β β β¦ βπ β π (volβ(([,) β (πβπ))βπ)))))} = {π§ β β* β£
βπ β (((β
Γ β) βm π) βm β)(πΌ β βͺ π β β Xπ β π (([,) β (πβπ))βπ) β§ π§ =
(Ξ£^β(π β β β¦ βπ β π (volβ(([,) β (πβπ))βπ)))))} |
53 | | eqeq1 2741 |
. . . . . . . . 9
β’ (π = π β (π = 1 β π = 1)) |
54 | 53 | ifbid 4507 |
. . . . . . . 8
β’ (π = π β if(π = 1, β¨(π΄βπ), (π΅βπ)β©, β¨0, 0β©) = if(π = 1, β¨(π΄βπ), (π΅βπ)β©, β¨0, 0β©)) |
55 | 54 | mpteq2dv 5205 |
. . . . . . 7
β’ (π = π β (π β π β¦ if(π = 1, β¨(π΄βπ), (π΅βπ)β©, β¨0, 0β©)) = (π β π β¦ if(π = 1, β¨(π΄βπ), (π΅βπ)β©, β¨0, 0β©))) |
56 | 55 | cbvmptv 5216 |
. . . . . 6
β’ (π β β β¦ (π β π β¦ if(π = 1, β¨(π΄βπ), (π΅βπ)β©, β¨0, 0β©))) = (π β β β¦ (π β π β¦ if(π = 1, β¨(π΄βπ), (π΅βπ)β©, β¨0, 0β©))) |
57 | 1, 5, 7, 2, 52, 56 | ovnhoilem1 44743 |
. . . . 5
β’ (π β ((voln*βπ)βπΌ) β€ βπ β π (volβ((π΄βπ)[,)(π΅βπ)))) |
58 | 57 | adantr 481 |
. . . 4
β’ ((π β§ Β¬ π = β
) β ((voln*βπ)βπΌ) β€ βπ β π (volβ((π΄βπ)[,)(π΅βπ)))) |
59 | 1 | adantr 481 |
. . . . . 6
β’ ((π β§ Β¬ π = β
) β π β Fin) |
60 | | neqne 2949 |
. . . . . . 7
β’ (Β¬
π = β
β π β β
) |
61 | 60 | adantl 482 |
. . . . . 6
β’ ((π β§ Β¬ π = β
) β π β β
) |
62 | 5 | adantr 481 |
. . . . . 6
β’ ((π β§ Β¬ π = β
) β π΄:πβΆβ) |
63 | 7 | adantr 481 |
. . . . . 6
β’ ((π β§ Β¬ π = β
) β π΅:πβΆβ) |
64 | 14, 59, 61, 62, 63 | hoidmvn0val 44726 |
. . . . 5
β’ ((π β§ Β¬ π = β
) β (π΄(πΏβπ)π΅) = βπ β π (volβ((π΄βπ)[,)(π΅βπ)))) |
65 | 64 | eqcomd 2743 |
. . . 4
β’ ((π β§ Β¬ π = β
) β βπ β π (volβ((π΄βπ)[,)(π΅βπ))) = (π΄(πΏβπ)π΅)) |
66 | 58, 65 | breqtrd 5129 |
. . 3
β’ ((π β§ Β¬ π = β
) β ((voln*βπ)βπΌ) β€ (π΄(πΏβπ)π΅)) |
67 | 51, 66 | pm2.61dan 811 |
. 2
β’ (π β ((voln*βπ)βπΌ) β€ (π΄(πΏβπ)π΅)) |
68 | 49, 35 | eqeltrd 2838 |
. . . 4
β’ ((π β§ π = β
) β (π΄(πΏβπ)π΅) β β) |
69 | 50 | eqcomd 2743 |
. . . 4
β’ ((π β§ π = β
) β (π΄(πΏβπ)π΅) = ((voln*βπ)βπΌ)) |
70 | 68, 69 | eqled 11216 |
. . 3
β’ ((π β§ π = β
) β (π΄(πΏβπ)π΅) β€ ((voln*βπ)βπΌ)) |
71 | | fveq1 6838 |
. . . . . . . . . . . 12
β’ (π = π β (πβπ) = (πβπ)) |
72 | 71 | fvoveq1d 7373 |
. . . . . . . . . . 11
β’ (π = π β (volβ((πβπ)[,)(πβπ))) = (volβ((πβπ)[,)(πβπ)))) |
73 | 72 | prodeq2ad 43734 |
. . . . . . . . . 10
β’ (π = π β βπ β π₯ (volβ((πβπ)[,)(πβπ))) = βπ β π₯ (volβ((πβπ)[,)(πβπ)))) |
74 | 73 | ifeq2d 4504 |
. . . . . . . . 9
β’ (π = π β if(π₯ = β
, 0, βπ β π₯ (volβ((πβπ)[,)(πβπ)))) = if(π₯ = β
, 0, βπ β π₯ (volβ((πβπ)[,)(πβπ))))) |
75 | | fveq1 6838 |
. . . . . . . . . . . . 13
β’ (π = π β (πβπ) = (πβπ)) |
76 | 75 | oveq2d 7367 |
. . . . . . . . . . . 12
β’ (π = π β ((πβπ)[,)(πβπ)) = ((πβπ)[,)(πβπ))) |
77 | 76 | fveq2d 6843 |
. . . . . . . . . . 11
β’ (π = π β (volβ((πβπ)[,)(πβπ))) = (volβ((πβπ)[,)(πβπ)))) |
78 | 77 | prodeq2ad 43734 |
. . . . . . . . . 10
β’ (π = π β βπ β π₯ (volβ((πβπ)[,)(πβπ))) = βπ β π₯ (volβ((πβπ)[,)(πβπ)))) |
79 | 78 | ifeq2d 4504 |
. . . . . . . . 9
β’ (π = π β if(π₯ = β
, 0, βπ β π₯ (volβ((πβπ)[,)(πβπ)))) = if(π₯ = β
, 0, βπ β π₯ (volβ((πβπ)[,)(πβπ))))) |
80 | 74, 79 | cbvmpov 7446 |
. . . . . . . 8
β’ (π β (β
βm π₯),
π β (β
βm π₯)
β¦ if(π₯ = β
, 0,
βπ β π₯ (volβ((πβπ)[,)(πβπ))))) = (π β (β βm π₯), π β (β βm π₯) β¦ if(π₯ = β
, 0, βπ β π₯ (volβ((πβπ)[,)(πβπ))))) |
81 | 80 | a1i 11 |
. . . . . . 7
β’ (π₯ = π¦ β (π β (β βm π₯), π β (β βm π₯) β¦ if(π₯ = β
, 0, βπ β π₯ (volβ((πβπ)[,)(πβπ))))) = (π β (β βm π₯), π β (β βm π₯) β¦ if(π₯ = β
, 0, βπ β π₯ (volβ((πβπ)[,)(πβπ)))))) |
82 | | oveq2 7359 |
. . . . . . . 8
β’ (π₯ = π¦ β (β βm π₯) = (β βm
π¦)) |
83 | | eqeq1 2741 |
. . . . . . . . 9
β’ (π₯ = π¦ β (π₯ = β
β π¦ = β
)) |
84 | | prodeq1 15752 |
. . . . . . . . 9
β’ (π₯ = π¦ β βπ β π₯ (volβ((πβπ)[,)(πβπ))) = βπ β π¦ (volβ((πβπ)[,)(πβπ)))) |
85 | 83, 84 | ifbieq2d 4510 |
. . . . . . . 8
β’ (π₯ = π¦ β if(π₯ = β
, 0, βπ β π₯ (volβ((πβπ)[,)(πβπ)))) = if(π¦ = β
, 0, βπ β π¦ (volβ((πβπ)[,)(πβπ))))) |
86 | 82, 82, 85 | mpoeq123dv 7426 |
. . . . . . 7
β’ (π₯ = π¦ β (π β (β βm π₯), π β (β βm π₯) β¦ if(π₯ = β
, 0, βπ β π₯ (volβ((πβπ)[,)(πβπ))))) = (π β (β βm π¦), π β (β βm π¦) β¦ if(π¦ = β
, 0, βπ β π¦ (volβ((πβπ)[,)(πβπ)))))) |
87 | 81, 86 | eqtrd 2777 |
. . . . . 6
β’ (π₯ = π¦ β (π β (β βm π₯), π β (β βm π₯) β¦ if(π₯ = β
, 0, βπ β π₯ (volβ((πβπ)[,)(πβπ))))) = (π β (β βm π¦), π β (β βm π¦) β¦ if(π¦ = β
, 0, βπ β π¦ (volβ((πβπ)[,)(πβπ)))))) |
88 | 87 | cbvmptv 5216 |
. . . . 5
β’ (π₯ β Fin β¦ (π β (β
βm π₯),
π β (β
βm π₯)
β¦ if(π₯ = β
, 0,
βπ β π₯ (volβ((πβπ)[,)(πβπ)))))) = (π¦ β Fin β¦ (π β (β βm π¦), π β (β βm π¦) β¦ if(π¦ = β
, 0, βπ β π¦ (volβ((πβπ)[,)(πβπ)))))) |
89 | 14, 88 | eqtri 2765 |
. . . 4
β’ πΏ = (π¦ β Fin β¦ (π β (β βm π¦), π β (β βm π¦) β¦ if(π¦ = β
, 0, βπ β π¦ (volβ((πβπ)[,)(πβπ)))))) |
90 | | eqeq1 2741 |
. . . . . . . 8
β’ (π€ = π§ β (π€ =
(Ξ£^β(π β β β¦ βπ β π (volβ(([,) β (ββπ))βπ)))) β π§ =
(Ξ£^β(π β β β¦ βπ β π (volβ(([,) β (ββπ))βπ)))))) |
91 | 90 | anbi2d 629 |
. . . . . . 7
β’ (π€ = π§ β ((πΌ β βͺ
π β β Xπ β
π (([,) β (ββπ))βπ) β§ π€ =
(Ξ£^β(π β β β¦ βπ β π (volβ(([,) β (ββπ))βπ))))) β (πΌ β βͺ
π β β Xπ β
π (([,) β (ββπ))βπ) β§ π§ =
(Ξ£^β(π β β β¦ βπ β π (volβ(([,) β (ββπ))βπ))))))) |
92 | 91 | rexbidv 3173 |
. . . . . 6
β’ (π€ = π§ β (ββ β (((β Γ β)
βm π)
βm β)(πΌ β βͺ
π β β Xπ β
π (([,) β (ββπ))βπ) β§ π€ =
(Ξ£^β(π β β β¦ βπ β π (volβ(([,) β (ββπ))βπ))))) β ββ β (((β Γ β)
βm π)
βm β)(πΌ β βͺ
π β β Xπ β
π (([,) β (ββπ))βπ) β§ π§ =
(Ξ£^β(π β β β¦ βπ β π (volβ(([,) β (ββπ))βπ))))))) |
93 | | simpl 483 |
. . . . . . . . . . . . . . 15
β’ ((β = π β§ π β β) β β = π) |
94 | 93 | fveq1d 6841 |
. . . . . . . . . . . . . 14
β’ ((β = π β§ π β β) β (ββπ) = (πβπ)) |
95 | 94 | coeq2d 5816 |
. . . . . . . . . . . . 13
β’ ((β = π β§ π β β) β ([,) β (ββπ)) = ([,) β (πβπ))) |
96 | 95 | fveq1d 6841 |
. . . . . . . . . . . 12
β’ ((β = π β§ π β β) β (([,) β (ββπ))βπ) = (([,) β (πβπ))βπ)) |
97 | 96 | ixpeq2dv 8809 |
. . . . . . . . . . 11
β’ ((β = π β§ π β β) β Xπ β
π (([,) β (ββπ))βπ) = Xπ β π (([,) β (πβπ))βπ)) |
98 | 97 | iuneq2dv 4976 |
. . . . . . . . . 10
β’ (β = π β βͺ
π β β Xπ β
π (([,) β (ββπ))βπ) = βͺ π β β Xπ β
π (([,) β (πβπ))βπ)) |
99 | 98 | sseq2d 3974 |
. . . . . . . . 9
β’ (β = π β (πΌ β βͺ
π β β Xπ β
π (([,) β (ββπ))βπ) β πΌ β βͺ
π β β Xπ β
π (([,) β (πβπ))βπ))) |
100 | | simpl 483 |
. . . . . . . . . . . . . . . . 17
β’ ((β = π β§ π β π) β β = π) |
101 | 100 | fveq1d 6841 |
. . . . . . . . . . . . . . . 16
β’ ((β = π β§ π β π) β (ββπ) = (πβπ)) |
102 | 101 | coeq2d 5816 |
. . . . . . . . . . . . . . 15
β’ ((β = π β§ π β π) β ([,) β (ββπ)) = ([,) β (πβπ))) |
103 | 102 | fveq1d 6841 |
. . . . . . . . . . . . . 14
β’ ((β = π β§ π β π) β (([,) β (ββπ))βπ) = (([,) β (πβπ))βπ)) |
104 | 103 | fveq2d 6843 |
. . . . . . . . . . . . 13
β’ ((β = π β§ π β π) β (volβ(([,) β (ββπ))βπ)) = (volβ(([,) β (πβπ))βπ))) |
105 | 104 | prodeq2dv 15766 |
. . . . . . . . . . . 12
β’ (β = π β βπ β π (volβ(([,) β (ββπ))βπ)) = βπ β π (volβ(([,) β (πβπ))βπ))) |
106 | 105 | mpteq2dv 5205 |
. . . . . . . . . . 11
β’ (β = π β (π β β β¦ βπ β π (volβ(([,) β (ββπ))βπ))) = (π β β β¦ βπ β π (volβ(([,) β (πβπ))βπ)))) |
107 | 106 | fveq2d 6843 |
. . . . . . . . . 10
β’ (β = π β
(Ξ£^β(π β β β¦ βπ β π (volβ(([,) β (ββπ))βπ)))) =
(Ξ£^β(π β β β¦ βπ β π (volβ(([,) β (πβπ))βπ))))) |
108 | 107 | eqeq2d 2748 |
. . . . . . . . 9
β’ (β = π β (π§ =
(Ξ£^β(π β β β¦ βπ β π (volβ(([,) β (ββπ))βπ)))) β π§ =
(Ξ£^β(π β β β¦ βπ β π (volβ(([,) β (πβπ))βπ)))))) |
109 | 99, 108 | anbi12d 631 |
. . . . . . . 8
β’ (β = π β ((πΌ β βͺ
π β β Xπ β
π (([,) β (ββπ))βπ) β§ π§ =
(Ξ£^β(π β β β¦ βπ β π (volβ(([,) β (ββπ))βπ))))) β (πΌ β βͺ
π β β Xπ β
π (([,) β (πβπ))βπ) β§ π§ =
(Ξ£^β(π β β β¦ βπ β π (volβ(([,) β (πβπ))βπ))))))) |
110 | 109 | cbvrexvw 3224 |
. . . . . . 7
β’
(ββ β
(((β Γ β) βm π) βm β)(πΌ β βͺ π β β Xπ β π (([,) β (ββπ))βπ) β§ π§ =
(Ξ£^β(π β β β¦ βπ β π (volβ(([,) β (ββπ))βπ))))) β βπ β (((β Γ β)
βm π)
βm β)(πΌ β βͺ
π β β Xπ β
π (([,) β (πβπ))βπ) β§ π§ =
(Ξ£^β(π β β β¦ βπ β π (volβ(([,) β (πβπ))βπ)))))) |
111 | 110 | a1i 11 |
. . . . . 6
β’ (π€ = π§ β (ββ β (((β Γ β)
βm π)
βm β)(πΌ β βͺ
π β β Xπ β
π (([,) β (ββπ))βπ) β§ π§ =
(Ξ£^β(π β β β¦ βπ β π (volβ(([,) β (ββπ))βπ))))) β βπ β (((β Γ β)
βm π)
βm β)(πΌ β βͺ
π β β Xπ β
π (([,) β (πβπ))βπ) β§ π§ =
(Ξ£^β(π β β β¦ βπ β π (volβ(([,) β (πβπ))βπ))))))) |
112 | 92, 111 | bitrd 278 |
. . . . 5
β’ (π€ = π§ β (ββ β (((β Γ β)
βm π)
βm β)(πΌ β βͺ
π β β Xπ β
π (([,) β (ββπ))βπ) β§ π€ =
(Ξ£^β(π β β β¦ βπ β π (volβ(([,) β (ββπ))βπ))))) β βπ β (((β Γ β)
βm π)
βm β)(πΌ β βͺ
π β β Xπ β
π (([,) β (πβπ))βπ) β§ π§ =
(Ξ£^β(π β β β¦ βπ β π (volβ(([,) β (πβπ))βπ))))))) |
113 | 112 | cbvrabv 3415 |
. . . 4
β’ {π€ β β*
β£ ββ β
(((β Γ β) βm π) βm β)(πΌ β βͺ π β β Xπ β π (([,) β (ββπ))βπ) β§ π€ =
(Ξ£^β(π β β β¦ βπ β π (volβ(([,) β (ββπ))βπ)))))} = {π§ β β* β£
βπ β (((β
Γ β) βm π) βm β)(πΌ β βͺ π β β Xπ β π (([,) β (πβπ))βπ) β§ π§ =
(Ξ£^β(π β β β¦ βπ β π (volβ(([,) β (πβπ))βπ)))))} |
114 | | simpl 483 |
. . . . . . . . . 10
β’ ((π = π β§ π β π) β π = π) |
115 | 114 | fveq2d 6843 |
. . . . . . . . 9
β’ ((π = π β§ π β π) β (πβπ) = (πβπ)) |
116 | 115 | fveq1d 6841 |
. . . . . . . 8
β’ ((π = π β§ π β π) β ((πβπ)βπ) = ((πβπ)βπ)) |
117 | 116 | fveq2d 6843 |
. . . . . . 7
β’ ((π = π β§ π β π) β (1st β((πβπ)βπ)) = (1st β((πβπ)βπ))) |
118 | 117 | mpteq2dva 5203 |
. . . . . 6
β’ (π = π β (π β π β¦ (1st β((πβπ)βπ))) = (π β π β¦ (1st β((πβπ)βπ)))) |
119 | 118 | cbvmptv 5216 |
. . . . 5
β’ (π β β β¦ (π β π β¦ (1st β((πβπ)βπ)))) = (π β β β¦ (π β π β¦ (1st β((πβπ)βπ)))) |
120 | 119 | mpteq2i 5208 |
. . . 4
β’ (π β (((β Γ
β) βm π) βm β) β¦ (π β β β¦ (π β π β¦ (1st β((πβπ)βπ))))) = (π β (((β Γ β)
βm π)
βm β) β¦ (π β β β¦ (π β π β¦ (1st β((πβπ)βπ))))) |
121 | 116 | fveq2d 6843 |
. . . . . . 7
β’ ((π = π β§ π β π) β (2nd β((πβπ)βπ)) = (2nd β((πβπ)βπ))) |
122 | 121 | mpteq2dva 5203 |
. . . . . 6
β’ (π = π β (π β π β¦ (2nd β((πβπ)βπ))) = (π β π β¦ (2nd β((πβπ)βπ)))) |
123 | 122 | cbvmptv 5216 |
. . . . 5
β’ (π β β β¦ (π β π β¦ (2nd β((πβπ)βπ)))) = (π β β β¦ (π β π β¦ (2nd β((πβπ)βπ)))) |
124 | 123 | mpteq2i 5208 |
. . . 4
β’ (π β (((β Γ
β) βm π) βm β) β¦ (π β β β¦ (π β π β¦ (2nd β((πβπ)βπ))))) = (π β (((β Γ β)
βm π)
βm β) β¦ (π β β β¦ (π β π β¦ (2nd β((πβπ)βπ))))) |
125 | 59, 61, 62, 63, 2, 89, 113, 120, 124 | ovnhoilem2 44744 |
. . 3
β’ ((π β§ Β¬ π = β
) β (π΄(πΏβπ)π΅) β€ ((voln*βπ)βπΌ)) |
126 | 70, 125 | pm2.61dan 811 |
. 2
β’ (π β (π΄(πΏβπ)π΅) β€ ((voln*βπ)βπΌ)) |
127 | 12, 16, 67, 126 | xrletrid 13028 |
1
β’ (π β ((voln*βπ)βπΌ) = (π΄(πΏβπ)π΅)) |