Step | Hyp | Ref
| Expression |
1 | | ovnhoilem2.m |
. . . . . . . . . 10
β’ π = {π§ β β* β£
βπ β (((β
Γ β) βm π) βm β)(πΌ β βͺ π β β Xπ β π (([,) β (πβπ))βπ) β§ π§ =
(Ξ£^β(π β β β¦ βπ β π (volβ(([,) β (πβπ))βπ)))))} |
2 | 1 | eleq2i 2826 |
. . . . . . . . 9
β’ (π§ β π β π§ β {π§ β β* β£
βπ β (((β
Γ β) βm π) βm β)(πΌ β βͺ π β β Xπ β π (([,) β (πβπ))βπ) β§ π§ =
(Ξ£^β(π β β β¦ βπ β π (volβ(([,) β (πβπ))βπ)))))}) |
3 | | rabid 3453 |
. . . . . . . . 9
β’ (π§ β {π§ β β* β£
βπ β (((β
Γ β) βm π) βm β)(πΌ β βͺ π β β Xπ β π (([,) β (πβπ))βπ) β§ π§ =
(Ξ£^β(π β β β¦ βπ β π (volβ(([,) β (πβπ))βπ)))))} β (π§ β β* β§
βπ β (((β
Γ β) βm π) βm β)(πΌ β βͺ π β β Xπ β π (([,) β (πβπ))βπ) β§ π§ =
(Ξ£^β(π β β β¦ βπ β π (volβ(([,) β (πβπ))βπ))))))) |
4 | 2, 3 | bitri 275 |
. . . . . . . 8
β’ (π§ β π β (π§ β β* β§
βπ β (((β
Γ β) βm π) βm β)(πΌ β βͺ π β β Xπ β π (([,) β (πβπ))βπ) β§ π§ =
(Ξ£^β(π β β β¦ βπ β π (volβ(([,) β (πβπ))βπ))))))) |
5 | 4 | biimpi 215 |
. . . . . . 7
β’ (π§ β π β (π§ β β* β§
βπ β (((β
Γ β) βm π) βm β)(πΌ β βͺ π β β Xπ β π (([,) β (πβπ))βπ) β§ π§ =
(Ξ£^β(π β β β¦ βπ β π (volβ(([,) β (πβπ))βπ))))))) |
6 | 5 | simprd 497 |
. . . . . 6
β’ (π§ β π β βπ β (((β Γ β)
βm π)
βm β)(πΌ β βͺ
π β β Xπ β
π (([,) β (πβπ))βπ) β§ π§ =
(Ξ£^β(π β β β¦ βπ β π (volβ(([,) β (πβπ))βπ)))))) |
7 | 6 | adantl 483 |
. . . . 5
β’ ((π β§ π§ β π) β βπ β (((β Γ β)
βm π)
βm β)(πΌ β βͺ
π β β Xπ β
π (([,) β (πβπ))βπ) β§ π§ =
(Ξ£^β(π β β β¦ βπ β π (volβ(([,) β (πβπ))βπ)))))) |
8 | | ovnhoilem2.l |
. . . . . . . . . 10
β’ πΏ = (π₯ β Fin β¦ (π β (β βm π₯), π β (β βm π₯) β¦ if(π₯ = β
, 0, βπ β π₯ (volβ((πβπ)[,)(πβπ)))))) |
9 | | ovnhoilem2.x |
. . . . . . . . . . 11
β’ (π β π β Fin) |
10 | 9 | 3ad2ant1 1134 |
. . . . . . . . . 10
β’ ((π β§ π β (((β Γ β)
βm π)
βm β) β§ (πΌ β βͺ
π β β Xπ β
π (([,) β (πβπ))βπ) β§ π§ =
(Ξ£^β(π β β β¦ βπ β π (volβ(([,) β (πβπ))βπ)))))) β π β Fin) |
11 | | ovnhoilem2.a |
. . . . . . . . . . 11
β’ (π β π΄:πβΆβ) |
12 | 11 | 3ad2ant1 1134 |
. . . . . . . . . 10
β’ ((π β§ π β (((β Γ β)
βm π)
βm β) β§ (πΌ β βͺ
π β β Xπ β
π (([,) β (πβπ))βπ) β§ π§ =
(Ξ£^β(π β β β¦ βπ β π (volβ(([,) β (πβπ))βπ)))))) β π΄:πβΆβ) |
13 | | ovnhoilem2.b |
. . . . . . . . . . 11
β’ (π β π΅:πβΆβ) |
14 | 13 | 3ad2ant1 1134 |
. . . . . . . . . 10
β’ ((π β§ π β (((β Γ β)
βm π)
βm β) β§ (πΌ β βͺ
π β β Xπ β
π (([,) β (πβπ))βπ) β§ π§ =
(Ξ£^β(π β β β¦ βπ β π (volβ(([,) β (πβπ))βπ)))))) β π΅:πβΆβ) |
15 | | elmapi 8843 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (((β Γ
β) βm π) βm β) β π:ββΆ((β
Γ β) βm π)) |
16 | 15 | ffvelcdmda 7087 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β (((β Γ
β) βm π) βm β) β§ π β β) β (πβπ) β ((β Γ β)
βm π)) |
17 | | elmapi 8843 |
. . . . . . . . . . . . . . . . . 18
β’ ((πβπ) β ((β Γ β)
βm π)
β (πβπ):πβΆ(β Γ
β)) |
18 | 16, 17 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ ((π β (((β Γ
β) βm π) βm β) β§ π β β) β (πβπ):πβΆ(β Γ
β)) |
19 | 18 | ffvelcdmda 7087 |
. . . . . . . . . . . . . . . 16
β’ (((π β (((β Γ
β) βm π) βm β) β§ π β β) β§ π β π) β ((πβπ)βπ) β (β Γ
β)) |
20 | | xp1st 8007 |
. . . . . . . . . . . . . . . 16
β’ (((πβπ)βπ) β (β Γ β) β
(1st β((πβπ)βπ)) β β) |
21 | 19, 20 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (((π β (((β Γ
β) βm π) βm β) β§ π β β) β§ π β π) β (1st β((πβπ)βπ)) β β) |
22 | 21 | fmpttd 7115 |
. . . . . . . . . . . . . 14
β’ ((π β (((β Γ
β) βm π) βm β) β§ π β β) β (π β π β¦ (1st β((πβπ)βπ))):πβΆβ) |
23 | | reex 11201 |
. . . . . . . . . . . . . . . 16
β’ β
β V |
24 | 23 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ ((π β (((β Γ
β) βm π) βm β) β§ π β β) β β
β V) |
25 | | 1nn 12223 |
. . . . . . . . . . . . . . . . . . 19
β’ 1 β
β |
26 | 25 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (((β Γ
β) βm π) βm β) β 1
β β) |
27 | 15, 26 | ffvelcdmd 7088 |
. . . . . . . . . . . . . . . . 17
β’ (π β (((β Γ
β) βm π) βm β) β (πβ1) β ((β
Γ β) βm π)) |
28 | | elmapex 8842 |
. . . . . . . . . . . . . . . . . 18
β’ ((πβ1) β ((β
Γ β) βm π) β ((β Γ β) β V
β§ π β
V)) |
29 | 28 | simprd 497 |
. . . . . . . . . . . . . . . . 17
β’ ((πβ1) β ((β
Γ β) βm π) β π β V) |
30 | 27, 29 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (π β (((β Γ
β) βm π) βm β) β π β V) |
31 | 30 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β (((β Γ
β) βm π) βm β) β§ π β β) β π β V) |
32 | | elmapg 8833 |
. . . . . . . . . . . . . . 15
β’ ((β
β V β§ π β V)
β ((π β π β¦ (1st
β((πβπ)βπ))) β (β βm π) β (π β π β¦ (1st β((πβπ)βπ))):πβΆβ)) |
33 | 24, 31, 32 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ ((π β (((β Γ
β) βm π) βm β) β§ π β β) β ((π β π β¦ (1st β((πβπ)βπ))) β (β βm π) β (π β π β¦ (1st β((πβπ)βπ))):πβΆβ)) |
34 | 22, 33 | mpbird 257 |
. . . . . . . . . . . . 13
β’ ((π β (((β Γ
β) βm π) βm β) β§ π β β) β (π β π β¦ (1st β((πβπ)βπ))) β (β βm π)) |
35 | 34 | fmpttd 7115 |
. . . . . . . . . . . 12
β’ (π β (((β Γ
β) βm π) βm β) β (π β β β¦ (π β π β¦ (1st β((πβπ)βπ)))):ββΆ(β
βm π)) |
36 | | id 22 |
. . . . . . . . . . . . . 14
β’ (π β (((β Γ
β) βm π) βm β) β π β (((β Γ
β) βm π) βm
β)) |
37 | | nnex 12218 |
. . . . . . . . . . . . . . . 16
β’ β
β V |
38 | 37 | mptex 7225 |
. . . . . . . . . . . . . . 15
β’ (π β β β¦ (π β π β¦ (1st β((πβπ)βπ)))) β V |
39 | 38 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (π β (((β Γ
β) βm π) βm β) β (π β β β¦ (π β π β¦ (1st β((πβπ)βπ)))) β V) |
40 | | ovnhoilem2.f |
. . . . . . . . . . . . . . 15
β’ πΉ = (π β (((β Γ β)
βm π)
βm β) β¦ (π β β β¦ (π β π β¦ (1st β((πβπ)βπ))))) |
41 | 40 | fvmpt2 7010 |
. . . . . . . . . . . . . 14
β’ ((π β (((β Γ
β) βm π) βm β) β§ (π β β β¦ (π β π β¦ (1st β((πβπ)βπ)))) β V) β (πΉβπ) = (π β β β¦ (π β π β¦ (1st β((πβπ)βπ))))) |
42 | 36, 39, 41 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ (π β (((β Γ
β) βm π) βm β) β (πΉβπ) = (π β β β¦ (π β π β¦ (1st β((πβπ)βπ))))) |
43 | 42 | feq1d 6703 |
. . . . . . . . . . . 12
β’ (π β (((β Γ
β) βm π) βm β) β ((πΉβπ):ββΆ(β βm
π) β (π β β β¦ (π β π β¦ (1st β((πβπ)βπ)))):ββΆ(β
βm π))) |
44 | 35, 43 | mpbird 257 |
. . . . . . . . . . 11
β’ (π β (((β Γ
β) βm π) βm β) β (πΉβπ):ββΆ(β βm
π)) |
45 | 44 | 3ad2ant2 1135 |
. . . . . . . . . 10
β’ ((π β§ π β (((β Γ β)
βm π)
βm β) β§ (πΌ β βͺ
π β β Xπ β
π (([,) β (πβπ))βπ) β§ π§ =
(Ξ£^β(π β β β¦ βπ β π (volβ(([,) β (πβπ))βπ)))))) β (πΉβπ):ββΆ(β βm
π)) |
46 | | xp2nd 8008 |
. . . . . . . . . . . . . . . 16
β’ (((πβπ)βπ) β (β Γ β) β
(2nd β((πβπ)βπ)) β β) |
47 | 19, 46 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (((π β (((β Γ
β) βm π) βm β) β§ π β β) β§ π β π) β (2nd β((πβπ)βπ)) β β) |
48 | 47 | fmpttd 7115 |
. . . . . . . . . . . . . 14
β’ ((π β (((β Γ
β) βm π) βm β) β§ π β β) β (π β π β¦ (2nd β((πβπ)βπ))):πβΆβ) |
49 | | elmapg 8833 |
. . . . . . . . . . . . . . 15
β’ ((β
β V β§ π β V)
β ((π β π β¦ (2nd
β((πβπ)βπ))) β (β βm π) β (π β π β¦ (2nd β((πβπ)βπ))):πβΆβ)) |
50 | 24, 31, 49 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ ((π β (((β Γ
β) βm π) βm β) β§ π β β) β ((π β π β¦ (2nd β((πβπ)βπ))) β (β βm π) β (π β π β¦ (2nd β((πβπ)βπ))):πβΆβ)) |
51 | 48, 50 | mpbird 257 |
. . . . . . . . . . . . 13
β’ ((π β (((β Γ
β) βm π) βm β) β§ π β β) β (π β π β¦ (2nd β((πβπ)βπ))) β (β βm π)) |
52 | 51 | fmpttd 7115 |
. . . . . . . . . . . 12
β’ (π β (((β Γ
β) βm π) βm β) β (π β β β¦ (π β π β¦ (2nd β((πβπ)βπ)))):ββΆ(β
βm π)) |
53 | 37 | mptex 7225 |
. . . . . . . . . . . . . . 15
β’ (π β β β¦ (π β π β¦ (2nd β((πβπ)βπ)))) β V |
54 | 53 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (π β (((β Γ
β) βm π) βm β) β (π β β β¦ (π β π β¦ (2nd β((πβπ)βπ)))) β V) |
55 | | ovnhoilem2.s |
. . . . . . . . . . . . . . 15
β’ π = (π β (((β Γ β)
βm π)
βm β) β¦ (π β β β¦ (π β π β¦ (2nd β((πβπ)βπ))))) |
56 | 55 | fvmpt2 7010 |
. . . . . . . . . . . . . 14
β’ ((π β (((β Γ
β) βm π) βm β) β§ (π β β β¦ (π β π β¦ (2nd β((πβπ)βπ)))) β V) β (πβπ) = (π β β β¦ (π β π β¦ (2nd β((πβπ)βπ))))) |
57 | 36, 54, 56 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ (π β (((β Γ
β) βm π) βm β) β (πβπ) = (π β β β¦ (π β π β¦ (2nd β((πβπ)βπ))))) |
58 | 57 | feq1d 6703 |
. . . . . . . . . . . 12
β’ (π β (((β Γ
β) βm π) βm β) β ((πβπ):ββΆ(β βm
π) β (π β β β¦ (π β π β¦ (2nd β((πβπ)βπ)))):ββΆ(β
βm π))) |
59 | 52, 58 | mpbird 257 |
. . . . . . . . . . 11
β’ (π β (((β Γ
β) βm π) βm β) β (πβπ):ββΆ(β βm
π)) |
60 | 59 | 3ad2ant2 1135 |
. . . . . . . . . 10
β’ ((π β§ π β (((β Γ β)
βm π)
βm β) β§ (πΌ β βͺ
π β β Xπ β
π (([,) β (πβπ))βπ) β§ π§ =
(Ξ£^β(π β β β¦ βπ β π (volβ(([,) β (πβπ))βπ)))))) β (πβπ):ββΆ(β βm
π)) |
61 | | simp3 1139 |
. . . . . . . . . . . 12
β’ ((π β§ π β (((β Γ β)
βm π)
βm β) β§ πΌ β βͺ
π β β Xπ β
π (([,) β (πβπ))βπ)) β πΌ β βͺ
π β β Xπ β
π (([,) β (πβπ))βπ)) |
62 | | ovnhoilem2.i |
. . . . . . . . . . . . . 14
β’ πΌ = Xπ β π ((π΄βπ)[,)(π΅βπ)) |
63 | 62 | a1i 11 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (((β Γ β)
βm π)
βm β) β§ πΌ β βͺ
π β β Xπ β
π (([,) β (πβπ))βπ)) β πΌ = Xπ β π ((π΄βπ)[,)(π΅βπ))) |
64 | | fveq2 6892 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = π β (πβπ) = (πβπ)) |
65 | 64 | fveq1d 6894 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = π β ((πβπ)βπ) = ((πβπ)βπ)) |
66 | 65 | fveq2d 6896 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = π β (1st β((πβπ)βπ)) = (1st β((πβπ)βπ))) |
67 | 65 | fveq2d 6896 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = π β (2nd β((πβπ)βπ)) = (2nd β((πβπ)βπ))) |
68 | 66, 67 | oveq12d 7427 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = π β ((1st β((πβπ)βπ))[,)(2nd β((πβπ)βπ))) = ((1st β((πβπ)βπ))[,)(2nd β((πβπ)βπ)))) |
69 | 68 | ixpeq2dv 8907 |
. . . . . . . . . . . . . . . . . 18
β’ (π = π β Xπ β π ((1st β((πβπ)βπ))[,)(2nd β((πβπ)βπ))) = Xπ β π ((1st β((πβπ)βπ))[,)(2nd β((πβπ)βπ)))) |
70 | 69 | cbviunv 5044 |
. . . . . . . . . . . . . . . . 17
β’ βͺ π β β Xπ β π ((1st β((πβπ)βπ))[,)(2nd β((πβπ)βπ))) = βͺ
π β β Xπ β
π ((1st
β((πβπ)βπ))[,)(2nd β((πβπ)βπ))) |
71 | 70 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ (π β (((β Γ
β) βm π) βm β) β
βͺ π β β Xπ β π ((1st β((πβπ)βπ))[,)(2nd β((πβπ)βπ))) = βͺ
π β β Xπ β
π ((1st
β((πβπ)βπ))[,)(2nd β((πβπ)βπ)))) |
72 | 15 | ffvelcdmda 7087 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β (((β Γ
β) βm π) βm β) β§ π β β) β (πβπ) β ((β Γ β)
βm π)) |
73 | | elmapi 8843 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((πβπ) β ((β Γ β)
βm π)
β (πβπ):πβΆ(β Γ
β)) |
74 | 72, 73 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β (((β Γ
β) βm π) βm β) β§ π β β) β (πβπ):πβΆ(β Γ
β)) |
75 | 74 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β (((β Γ
β) βm π) βm β) β§ π β β) β§ π β π) β (πβπ):πβΆ(β Γ
β)) |
76 | | simpr 486 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β (((β Γ
β) βm π) βm β) β§ π β β) β§ π β π) β π β π) |
77 | 75, 76 | fvovco 43892 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β (((β Γ
β) βm π) βm β) β§ π β β) β§ π β π) β (([,) β (πβπ))βπ) = ((1st β((πβπ)βπ))[,)(2nd β((πβπ)βπ)))) |
78 | 77 | ixpeq2dva 8906 |
. . . . . . . . . . . . . . . . 17
β’ ((π β (((β Γ
β) βm π) βm β) β§ π β β) β Xπ β
π (([,) β (πβπ))βπ) = Xπ β π ((1st β((πβπ)βπ))[,)(2nd β((πβπ)βπ)))) |
79 | 78 | iuneq2dv 5022 |
. . . . . . . . . . . . . . . 16
β’ (π β (((β Γ
β) βm π) βm β) β
βͺ π β β Xπ β π (([,) β (πβπ))βπ) = βͺ π β β Xπ β
π ((1st
β((πβπ)βπ))[,)(2nd β((πβπ)βπ)))) |
80 | | simpl 484 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β (((β Γ
β) βm π) βm β) β§ π β β) β π β (((β Γ
β) βm π) βm
β)) |
81 | 38 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β (((β Γ
β) βm π) βm β) β§ π β β) β (π β β β¦ (π β π β¦ (1st β((πβπ)βπ)))) β V) |
82 | 80, 81, 41 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β (((β Γ
β) βm π) βm β) β§ π β β) β (πΉβπ) = (π β β β¦ (π β π β¦ (1st β((πβπ)βπ))))) |
83 | 82 | fveq1d 6894 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β (((β Γ
β) βm π) βm β) β§ π β β) β ((πΉβπ)βπ) = ((π β β β¦ (π β π β¦ (1st β((πβπ)βπ))))βπ)) |
84 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β (((β Γ
β) βm π) βm β) β§ π β β) β π β
β) |
85 | | mptexg 7223 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β V β (π β π β¦ (1st β((πβπ)βπ))) β V) |
86 | 30, 85 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β (((β Γ
β) βm π) βm β) β (π β π β¦ (1st β((πβπ)βπ))) β V) |
87 | 86 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β (((β Γ
β) βm π) βm β) β§ π β β) β (π β π β¦ (1st β((πβπ)βπ))) β V) |
88 | | eqid 2733 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β β β¦ (π β π β¦ (1st β((πβπ)βπ)))) = (π β β β¦ (π β π β¦ (1st β((πβπ)βπ)))) |
89 | 88 | fvmpt2 7010 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β β β§ (π β π β¦ (1st β((πβπ)βπ))) β V) β ((π β β β¦ (π β π β¦ (1st β((πβπ)βπ))))βπ) = (π β π β¦ (1st β((πβπ)βπ)))) |
90 | 84, 87, 89 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β (((β Γ
β) βm π) βm β) β§ π β β) β ((π β β β¦ (π β π β¦ (1st β((πβπ)βπ))))βπ) = (π β π β¦ (1st β((πβπ)βπ)))) |
91 | 83, 90 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β (((β Γ
β) βm π) βm β) β§ π β β) β ((πΉβπ)βπ) = (π β π β¦ (1st β((πβπ)βπ)))) |
92 | 91 | fveq1d 6894 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β (((β Γ
β) βm π) βm β) β§ π β β) β (((πΉβπ)βπ)βπ) = ((π β π β¦ (1st β((πβπ)βπ)))βπ)) |
93 | 92 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β (((β Γ
β) βm π) βm β) β§ π β β) β§ π β π) β (((πΉβπ)βπ)βπ) = ((π β π β¦ (1st β((πβπ)βπ)))βπ)) |
94 | | eqidd 2734 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β (((β Γ
β) βm π) βm β) β§ π β π) β (π β π β¦ (1st β((πβπ)βπ))) = (π β π β¦ (1st β((πβπ)βπ)))) |
95 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β (((β Γ
β) βm π) βm β) β§ π β π) β§ π = π) β π = π) |
96 | 95 | fveq2d 6896 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β (((β Γ
β) βm π) βm β) β§ π β π) β§ π = π) β ((πβπ)βπ) = ((πβπ)βπ)) |
97 | 96 | fveq2d 6896 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β (((β Γ
β) βm π) βm β) β§ π β π) β§ π = π) β (1st β((πβπ)βπ)) = (1st β((πβπ)βπ))) |
98 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β (((β Γ
β) βm π) βm β) β§ π β π) β π β π) |
99 | | fvexd 6907 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β (((β Γ
β) βm π) βm β) β§ π β π) β (1st β((πβπ)βπ)) β V) |
100 | 94, 97, 98, 99 | fvmptd 7006 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β (((β Γ
β) βm π) βm β) β§ π β π) β ((π β π β¦ (1st β((πβπ)βπ)))βπ) = (1st β((πβπ)βπ))) |
101 | 100 | adantlr 714 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β (((β Γ
β) βm π) βm β) β§ π β β) β§ π β π) β ((π β π β¦ (1st β((πβπ)βπ)))βπ) = (1st β((πβπ)βπ))) |
102 | 93, 101 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β (((β Γ
β) βm π) βm β) β§ π β β) β§ π β π) β (((πΉβπ)βπ)βπ) = (1st β((πβπ)βπ))) |
103 | 57 | fveq1d 6894 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β (((β Γ
β) βm π) βm β) β ((πβπ)βπ) = ((π β β β¦ (π β π β¦ (2nd β((πβπ)βπ))))βπ)) |
104 | 103 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β (((β Γ
β) βm π) βm β) β§ π β β) β ((πβπ)βπ) = ((π β β β¦ (π β π β¦ (2nd β((πβπ)βπ))))βπ)) |
105 | | mptexg 7223 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β V β (π β π β¦ (2nd β((πβπ)βπ))) β V) |
106 | 30, 105 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β (((β Γ
β) βm π) βm β) β (π β π β¦ (2nd β((πβπ)βπ))) β V) |
107 | 106 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β (((β Γ
β) βm π) βm β) β§ π β β) β (π β π β¦ (2nd β((πβπ)βπ))) β V) |
108 | | eqid 2733 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β β β¦ (π β π β¦ (2nd β((πβπ)βπ)))) = (π β β β¦ (π β π β¦ (2nd β((πβπ)βπ)))) |
109 | 108 | fvmpt2 7010 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β β β§ (π β π β¦ (2nd β((πβπ)βπ))) β V) β ((π β β β¦ (π β π β¦ (2nd β((πβπ)βπ))))βπ) = (π β π β¦ (2nd β((πβπ)βπ)))) |
110 | 84, 107, 109 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β (((β Γ
β) βm π) βm β) β§ π β β) β ((π β β β¦ (π β π β¦ (2nd β((πβπ)βπ))))βπ) = (π β π β¦ (2nd β((πβπ)βπ)))) |
111 | 104, 110 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β (((β Γ
β) βm π) βm β) β§ π β β) β ((πβπ)βπ) = (π β π β¦ (2nd β((πβπ)βπ)))) |
112 | 111 | fveq1d 6894 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β (((β Γ
β) βm π) βm β) β§ π β β) β (((πβπ)βπ)βπ) = ((π β π β¦ (2nd β((πβπ)βπ)))βπ)) |
113 | 112 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β (((β Γ
β) βm π) βm β) β§ π β β) β§ π β π) β (((πβπ)βπ)βπ) = ((π β π β¦ (2nd β((πβπ)βπ)))βπ)) |
114 | | eqidd 2734 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β (((β Γ
β) βm π) βm β) β§ π β π) β (π β π β¦ (2nd β((πβπ)βπ))) = (π β π β¦ (2nd β((πβπ)βπ)))) |
115 | | 2fveq3 6897 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π = π β (2nd β((πβπ)βπ)) = (2nd β((πβπ)βπ))) |
116 | 115 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β (((β Γ
β) βm π) βm β) β§ π β π) β§ π = π) β (2nd β((πβπ)βπ)) = (2nd β((πβπ)βπ))) |
117 | | fvexd 6907 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β (((β Γ
β) βm π) βm β) β§ π β π) β (2nd β((πβπ)βπ)) β V) |
118 | 114, 116,
98, 117 | fvmptd 7006 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β (((β Γ
β) βm π) βm β) β§ π β π) β ((π β π β¦ (2nd β((πβπ)βπ)))βπ) = (2nd β((πβπ)βπ))) |
119 | 118 | adantlr 714 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β (((β Γ
β) βm π) βm β) β§ π β β) β§ π β π) β ((π β π β¦ (2nd β((πβπ)βπ)))βπ) = (2nd β((πβπ)βπ))) |
120 | 113, 119 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β (((β Γ
β) βm π) βm β) β§ π β β) β§ π β π) β (((πβπ)βπ)βπ) = (2nd β((πβπ)βπ))) |
121 | 102, 120 | oveq12d 7427 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β (((β Γ
β) βm π) βm β) β§ π β β) β§ π β π) β ((((πΉβπ)βπ)βπ)[,)(((πβπ)βπ)βπ)) = ((1st β((πβπ)βπ))[,)(2nd β((πβπ)βπ)))) |
122 | 121 | ixpeq2dva 8906 |
. . . . . . . . . . . . . . . . 17
β’ ((π β (((β Γ
β) βm π) βm β) β§ π β β) β Xπ β
π ((((πΉβπ)βπ)βπ)[,)(((πβπ)βπ)βπ)) = Xπ β π ((1st β((πβπ)βπ))[,)(2nd β((πβπ)βπ)))) |
123 | 122 | iuneq2dv 5022 |
. . . . . . . . . . . . . . . 16
β’ (π β (((β Γ
β) βm π) βm β) β
βͺ π β β Xπ β π ((((πΉβπ)βπ)βπ)[,)(((πβπ)βπ)βπ)) = βͺ
π β β Xπ β
π ((1st
β((πβπ)βπ))[,)(2nd β((πβπ)βπ)))) |
124 | 71, 79, 123 | 3eqtr4d 2783 |
. . . . . . . . . . . . . . 15
β’ (π β (((β Γ
β) βm π) βm β) β
βͺ π β β Xπ β π (([,) β (πβπ))βπ) = βͺ π β β Xπ β
π ((((πΉβπ)βπ)βπ)[,)(((πβπ)βπ)βπ))) |
125 | 124 | adantl 483 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (((β Γ β)
βm π)
βm β)) β βͺ π β β Xπ β
π (([,) β (πβπ))βπ) = βͺ π β β Xπ β
π ((((πΉβπ)βπ)βπ)[,)(((πβπ)βπ)βπ))) |
126 | 125 | 3adant3 1133 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (((β Γ β)
βm π)
βm β) β§ πΌ β βͺ
π β β Xπ β
π (([,) β (πβπ))βπ)) β βͺ
π β β Xπ β
π (([,) β (πβπ))βπ) = βͺ π β β Xπ β
π ((((πΉβπ)βπ)βπ)[,)(((πβπ)βπ)βπ))) |
127 | 63, 126 | sseq12d 4016 |
. . . . . . . . . . . 12
β’ ((π β§ π β (((β Γ β)
βm π)
βm β) β§ πΌ β βͺ
π β β Xπ β
π (([,) β (πβπ))βπ)) β (πΌ β βͺ
π β β Xπ β
π (([,) β (πβπ))βπ) β Xπ β π ((π΄βπ)[,)(π΅βπ)) β βͺ π β β Xπ β π ((((πΉβπ)βπ)βπ)[,)(((πβπ)βπ)βπ)))) |
128 | 61, 127 | mpbid 231 |
. . . . . . . . . . 11
β’ ((π β§ π β (((β Γ β)
βm π)
βm β) β§ πΌ β βͺ
π β β Xπ β
π (([,) β (πβπ))βπ)) β Xπ β π ((π΄βπ)[,)(π΅βπ)) β βͺ π β β Xπ β π ((((πΉβπ)βπ)βπ)[,)(((πβπ)βπ)βπ))) |
129 | 128 | 3adant3r 1182 |
. . . . . . . . . 10
β’ ((π β§ π β (((β Γ β)
βm π)
βm β) β§ (πΌ β βͺ
π β β Xπ β
π (([,) β (πβπ))βπ) β§ π§ =
(Ξ£^β(π β β β¦ βπ β π (volβ(([,) β (πβπ))βπ)))))) β Xπ β π ((π΄βπ)[,)(π΅βπ)) β βͺ π β β Xπ β π ((((πΉβπ)βπ)βπ)[,)(((πβπ)βπ)βπ))) |
130 | 8, 10, 12, 14, 45, 60, 129 | hoidmvle 45316 |
. . . . . . . . 9
β’ ((π β§ π β (((β Γ β)
βm π)
βm β) β§ (πΌ β βͺ
π β β Xπ β
π (([,) β (πβπ))βπ) β§ π§ =
(Ξ£^β(π β β β¦ βπ β π (volβ(([,) β (πβπ))βπ)))))) β (π΄(πΏβπ)π΅) β€
(Ξ£^β(π β β β¦ (((πΉβπ)βπ)(πΏβπ)((πβπ)βπ))))) |
131 | | simpl 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π = π β§ π β π) β π = π) |
132 | 131 | fveq2d 6896 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π = π β§ π β π) β (πβπ) = (πβπ)) |
133 | 132 | fveq1d 6894 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π = π β§ π β π) β ((πβπ)βπ) = ((πβπ)βπ)) |
134 | 133 | fveq2d 6896 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π = π β§ π β π) β (1st β((πβπ)βπ)) = (1st β((πβπ)βπ))) |
135 | 134 | mpteq2dva 5249 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = π β (π β π β¦ (1st β((πβπ)βπ))) = (π β π β¦ (1st β((πβπ)βπ)))) |
136 | 135 | fveq1d 6894 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = π β ((π β π β¦ (1st β((πβπ)βπ)))βπ) = ((π β π β¦ (1st β((πβπ)βπ)))βπ)) |
137 | 136 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π = π β§ π β π) β ((π β π β¦ (1st β((πβπ)βπ)))βπ) = ((π β π β¦ (1st β((πβπ)βπ)))βπ)) |
138 | | eqidd 2734 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β π β (π β π β¦ (1st β((πβπ)βπ))) = (π β π β¦ (1st β((πβπ)βπ)))) |
139 | | 2fveq3 6897 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π = π β (1st β((πβπ)βπ)) = (1st β((πβπ)βπ))) |
140 | 139 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β π β§ π = π) β (1st β((πβπ)βπ)) = (1st β((πβπ)βπ))) |
141 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β π β π β π) |
142 | | fvexd 6907 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β π β (1st β((πβπ)βπ)) β V) |
143 | 138, 140,
141, 142 | fvmptd 7006 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β π β ((π β π β¦ (1st β((πβπ)βπ)))βπ) = (1st β((πβπ)βπ))) |
144 | 143 | adantl 483 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π = π β§ π β π) β ((π β π β¦ (1st β((πβπ)βπ)))βπ) = (1st β((πβπ)βπ))) |
145 | 137, 144 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π = π β§ π β π) β ((π β π β¦ (1st β((πβπ)βπ)))βπ) = (1st β((πβπ)βπ))) |
146 | 133 | fveq2d 6896 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π = π β§ π β π) β (2nd β((πβπ)βπ)) = (2nd β((πβπ)βπ))) |
147 | 146 | mpteq2dva 5249 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = π β (π β π β¦ (2nd β((πβπ)βπ))) = (π β π β¦ (2nd β((πβπ)βπ)))) |
148 | 147 | fveq1d 6894 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = π β ((π β π β¦ (2nd β((πβπ)βπ)))βπ) = ((π β π β¦ (2nd β((πβπ)βπ)))βπ)) |
149 | 148 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π = π β§ π β π) β ((π β π β¦ (2nd β((πβπ)βπ)))βπ) = ((π β π β¦ (2nd β((πβπ)βπ)))βπ)) |
150 | | eqidd 2734 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β π β (π β π β¦ (2nd β((πβπ)βπ))) = (π β π β¦ (2nd β((πβπ)βπ)))) |
151 | | 2fveq3 6897 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π = π β (2nd β((πβπ)βπ)) = (2nd β((πβπ)βπ))) |
152 | 151 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β π β§ π = π) β (2nd β((πβπ)βπ)) = (2nd β((πβπ)βπ))) |
153 | | fvexd 6907 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β π β (2nd β((πβπ)βπ)) β V) |
154 | 150, 152,
141, 153 | fvmptd 7006 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β π β ((π β π β¦ (2nd β((πβπ)βπ)))βπ) = (2nd β((πβπ)βπ))) |
155 | 154 | adantl 483 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π = π β§ π β π) β ((π β π β¦ (2nd β((πβπ)βπ)))βπ) = (2nd β((πβπ)βπ))) |
156 | 149, 155 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π = π β§ π β π) β ((π β π β¦ (2nd β((πβπ)βπ)))βπ) = (2nd β((πβπ)βπ))) |
157 | 145, 156 | oveq12d 7427 |
. . . . . . . . . . . . . . . . . 18
β’ ((π = π β§ π β π) β (((π β π β¦ (1st β((πβπ)βπ)))βπ)[,)((π β π β¦ (2nd β((πβπ)βπ)))βπ)) = ((1st β((πβπ)βπ))[,)(2nd β((πβπ)βπ)))) |
158 | 157 | fveq2d 6896 |
. . . . . . . . . . . . . . . . 17
β’ ((π = π β§ π β π) β (volβ(((π β π β¦ (1st β((πβπ)βπ)))βπ)[,)((π β π β¦ (2nd β((πβπ)βπ)))βπ))) = (volβ((1st
β((πβπ)βπ))[,)(2nd β((πβπ)βπ))))) |
159 | 158 | prodeq2dv 15867 |
. . . . . . . . . . . . . . . 16
β’ (π = π β βπ β π (volβ(((π β π β¦ (1st β((πβπ)βπ)))βπ)[,)((π β π β¦ (2nd β((πβπ)βπ)))βπ))) = βπ β π (volβ((1st β((πβπ)βπ))[,)(2nd β((πβπ)βπ))))) |
160 | 159 | cbvmptv 5262 |
. . . . . . . . . . . . . . 15
β’ (π β β β¦
βπ β π (volβ(((π β π β¦ (1st β((πβπ)βπ)))βπ)[,)((π β π β¦ (2nd β((πβπ)βπ)))βπ)))) = (π β β β¦ βπ β π (volβ((1st β((πβπ)βπ))[,)(2nd β((πβπ)βπ))))) |
161 | 160 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (π β (((β Γ
β) βm π) βm β) β (π β β β¦
βπ β π (volβ(((π β π β¦ (1st β((πβπ)βπ)))βπ)[,)((π β π β¦ (2nd β((πβπ)βπ)))βπ)))) = (π β β β¦ βπ β π (volβ((1st β((πβπ)βπ))[,)(2nd β((πβπ)βπ)))))) |
162 | 77 | eqcomd 2739 |
. . . . . . . . . . . . . . . . 17
β’ (((π β (((β Γ
β) βm π) βm β) β§ π β β) β§ π β π) β ((1st β((πβπ)βπ))[,)(2nd β((πβπ)βπ))) = (([,) β (πβπ))βπ)) |
163 | 162 | fveq2d 6896 |
. . . . . . . . . . . . . . . 16
β’ (((π β (((β Γ
β) βm π) βm β) β§ π β β) β§ π β π) β (volβ((1st
β((πβπ)βπ))[,)(2nd β((πβπ)βπ)))) = (volβ(([,) β (πβπ))βπ))) |
164 | 163 | prodeq2dv 15867 |
. . . . . . . . . . . . . . 15
β’ ((π β (((β Γ
β) βm π) βm β) β§ π β β) β
βπ β π (volβ((1st
β((πβπ)βπ))[,)(2nd β((πβπ)βπ)))) = βπ β π (volβ(([,) β (πβπ))βπ))) |
165 | 164 | mpteq2dva 5249 |
. . . . . . . . . . . . . 14
β’ (π β (((β Γ
β) βm π) βm β) β (π β β β¦
βπ β π (volβ((1st
β((πβπ)βπ))[,)(2nd β((πβπ)βπ))))) = (π β β β¦ βπ β π (volβ(([,) β (πβπ))βπ)))) |
166 | 161, 165 | eqtrd 2773 |
. . . . . . . . . . . . 13
β’ (π β (((β Γ
β) βm π) βm β) β (π β β β¦
βπ β π (volβ(((π β π β¦ (1st β((πβπ)βπ)))βπ)[,)((π β π β¦ (2nd β((πβπ)βπ)))βπ)))) = (π β β β¦ βπ β π (volβ(([,) β (πβπ))βπ)))) |
167 | 166 | fveq2d 6896 |
. . . . . . . . . . . 12
β’ (π β (((β Γ
β) βm π) βm β) β
(Ξ£^β(π β β β¦ βπ β π (volβ(((π β π β¦ (1st β((πβπ)βπ)))βπ)[,)((π β π β¦ (2nd β((πβπ)βπ)))βπ))))) =
(Ξ£^β(π β β β¦ βπ β π (volβ(([,) β (πβπ))βπ))))) |
168 | 167 | 3ad2ant2 1135 |
. . . . . . . . . . 11
β’ ((π β§ π β (((β Γ β)
βm π)
βm β) β§ π§ =
(Ξ£^β(π β β β¦ βπ β π (volβ(([,) β (πβπ))βπ))))) β
(Ξ£^β(π β β β¦ βπ β π (volβ(((π β π β¦ (1st β((πβπ)βπ)))βπ)[,)((π β π β¦ (2nd β((πβπ)βπ)))βπ))))) =
(Ξ£^β(π β β β¦ βπ β π (volβ(([,) β (πβπ))βπ))))) |
169 | 91 | adantll 713 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (((β Γ β)
βm π)
βm β)) β§ π β β) β ((πΉβπ)βπ) = (π β π β¦ (1st β((πβπ)βπ)))) |
170 | 111 | adantll 713 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (((β Γ β)
βm π)
βm β)) β§ π β β) β ((πβπ)βπ) = (π β π β¦ (2nd β((πβπ)βπ)))) |
171 | 169, 170 | oveq12d 7427 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (((β Γ β)
βm π)
βm β)) β§ π β β) β (((πΉβπ)βπ)(πΏβπ)((πβπ)βπ)) = ((π β π β¦ (1st β((πβπ)βπ)))(πΏβπ)(π β π β¦ (2nd β((πβπ)βπ))))) |
172 | 9 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (((β Γ β)
βm π)
βm β)) β§ π β β) β π β Fin) |
173 | | ovnhoilem2.n |
. . . . . . . . . . . . . . . . 17
β’ (π β π β β
) |
174 | 173 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (((β Γ β)
βm π)
βm β)) β§ π β β) β π β β
) |
175 | 19 | adantlll 717 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π β (((β Γ β)
βm π)
βm β)) β§ π β β) β§ π β π) β ((πβπ)βπ) β (β Γ
β)) |
176 | 175, 20 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π β (((β Γ β)
βm π)
βm β)) β§ π β β) β§ π β π) β (1st β((πβπ)βπ)) β β) |
177 | 176 | fmpttd 7115 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (((β Γ β)
βm π)
βm β)) β§ π β β) β (π β π β¦ (1st β((πβπ)βπ))):πβΆβ) |
178 | 175, 46 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π β (((β Γ β)
βm π)
βm β)) β§ π β β) β§ π β π) β (2nd β((πβπ)βπ)) β β) |
179 | 178 | fmpttd 7115 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (((β Γ β)
βm π)
βm β)) β§ π β β) β (π β π β¦ (2nd β((πβπ)βπ))):πβΆβ) |
180 | 8, 172, 174, 177, 179 | hoidmvn0val 45300 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (((β Γ β)
βm π)
βm β)) β§ π β β) β ((π β π β¦ (1st β((πβπ)βπ)))(πΏβπ)(π β π β¦ (2nd β((πβπ)βπ)))) = βπ β π (volβ(((π β π β¦ (1st β((πβπ)βπ)))βπ)[,)((π β π β¦ (2nd β((πβπ)βπ)))βπ)))) |
181 | 171, 180 | eqtrd 2773 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β (((β Γ β)
βm π)
βm β)) β§ π β β) β (((πΉβπ)βπ)(πΏβπ)((πβπ)βπ)) = βπ β π (volβ(((π β π β¦ (1st β((πβπ)βπ)))βπ)[,)((π β π β¦ (2nd β((πβπ)βπ)))βπ)))) |
182 | 181 | mpteq2dva 5249 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (((β Γ β)
βm π)
βm β)) β (π β β β¦ (((πΉβπ)βπ)(πΏβπ)((πβπ)βπ))) = (π β β β¦ βπ β π (volβ(((π β π β¦ (1st β((πβπ)βπ)))βπ)[,)((π β π β¦ (2nd β((πβπ)βπ)))βπ))))) |
183 | 182 | fveq2d 6896 |
. . . . . . . . . . . 12
β’ ((π β§ π β (((β Γ β)
βm π)
βm β)) β
(Ξ£^β(π β β β¦ (((πΉβπ)βπ)(πΏβπ)((πβπ)βπ)))) =
(Ξ£^β(π β β β¦ βπ β π (volβ(((π β π β¦ (1st β((πβπ)βπ)))βπ)[,)((π β π β¦ (2nd β((πβπ)βπ)))βπ)))))) |
184 | 183 | 3adant3 1133 |
. . . . . . . . . . 11
β’ ((π β§ π β (((β Γ β)
βm π)
βm β) β§ π§ =
(Ξ£^β(π β β β¦ βπ β π (volβ(([,) β (πβπ))βπ))))) β
(Ξ£^β(π β β β¦ (((πΉβπ)βπ)(πΏβπ)((πβπ)βπ)))) =
(Ξ£^β(π β β β¦ βπ β π (volβ(((π β π β¦ (1st β((πβπ)βπ)))βπ)[,)((π β π β¦ (2nd β((πβπ)βπ)))βπ)))))) |
185 | | simp3 1139 |
. . . . . . . . . . 11
β’ ((π β§ π β (((β Γ β)
βm π)
βm β) β§ π§ =
(Ξ£^β(π β β β¦ βπ β π (volβ(([,) β (πβπ))βπ))))) β π§ =
(Ξ£^β(π β β β¦ βπ β π (volβ(([,) β (πβπ))βπ))))) |
186 | 168, 184,
185 | 3eqtr4d 2783 |
. . . . . . . . . 10
β’ ((π β§ π β (((β Γ β)
βm π)
βm β) β§ π§ =
(Ξ£^β(π β β β¦ βπ β π (volβ(([,) β (πβπ))βπ))))) β
(Ξ£^β(π β β β¦ (((πΉβπ)βπ)(πΏβπ)((πβπ)βπ)))) = π§) |
187 | 186 | 3adant3l 1181 |
. . . . . . . . 9
β’ ((π β§ π β (((β Γ β)
βm π)
βm β) β§ (πΌ β βͺ
π β β Xπ β
π (([,) β (πβπ))βπ) β§ π§ =
(Ξ£^β(π β β β¦ βπ β π (volβ(([,) β (πβπ))βπ)))))) β
(Ξ£^β(π β β β¦ (((πΉβπ)βπ)(πΏβπ)((πβπ)βπ)))) = π§) |
188 | 130, 187 | breqtrd 5175 |
. . . . . . . 8
β’ ((π β§ π β (((β Γ β)
βm π)
βm β) β§ (πΌ β βͺ
π β β Xπ β
π (([,) β (πβπ))βπ) β§ π§ =
(Ξ£^β(π β β β¦ βπ β π (volβ(([,) β (πβπ))βπ)))))) β (π΄(πΏβπ)π΅) β€ π§) |
189 | 188 | 3exp 1120 |
. . . . . . 7
β’ (π β (π β (((β Γ β)
βm π)
βm β) β ((πΌ β βͺ
π β β Xπ β
π (([,) β (πβπ))βπ) β§ π§ =
(Ξ£^β(π β β β¦ βπ β π (volβ(([,) β (πβπ))βπ))))) β (π΄(πΏβπ)π΅) β€ π§))) |
190 | 189 | adantr 482 |
. . . . . 6
β’ ((π β§ π§ β π) β (π β (((β Γ β)
βm π)
βm β) β ((πΌ β βͺ
π β β Xπ β
π (([,) β (πβπ))βπ) β§ π§ =
(Ξ£^β(π β β β¦ βπ β π (volβ(([,) β (πβπ))βπ))))) β (π΄(πΏβπ)π΅) β€ π§))) |
191 | 190 | rexlimdv 3154 |
. . . . 5
β’ ((π β§ π§ β π) β (βπ β (((β Γ β)
βm π)
βm β)(πΌ β βͺ
π β β Xπ β
π (([,) β (πβπ))βπ) β§ π§ =
(Ξ£^β(π β β β¦ βπ β π (volβ(([,) β (πβπ))βπ))))) β (π΄(πΏβπ)π΅) β€ π§)) |
192 | 7, 191 | mpd 15 |
. . . 4
β’ ((π β§ π§ β π) β (π΄(πΏβπ)π΅) β€ π§) |
193 | 192 | ralrimiva 3147 |
. . 3
β’ (π β βπ§ β π (π΄(πΏβπ)π΅) β€ π§) |
194 | | ssrab2 4078 |
. . . . . 6
β’ {π§ β β*
β£ βπ β
(((β Γ β) βm π) βm β)(πΌ β βͺ π β β Xπ β π (([,) β (πβπ))βπ) β§ π§ =
(Ξ£^β(π β β β¦ βπ β π (volβ(([,) β (πβπ))βπ)))))} β
β* |
195 | 1, 194 | eqsstri 4017 |
. . . . 5
β’ π β
β* |
196 | 195 | a1i 11 |
. . . 4
β’ (π β π β
β*) |
197 | | icossxr 13409 |
. . . . 5
β’
(0[,)+β) β β* |
198 | 8, 9, 11, 13 | hoidmvcl 45298 |
. . . . 5
β’ (π β (π΄(πΏβπ)π΅) β (0[,)+β)) |
199 | 197, 198 | sselid 3981 |
. . . 4
β’ (π β (π΄(πΏβπ)π΅) β
β*) |
200 | | infxrgelb 13314 |
. . . 4
β’ ((π β β*
β§ (π΄(πΏβπ)π΅) β β*) β ((π΄(πΏβπ)π΅) β€ inf(π, β*, < ) β
βπ§ β π (π΄(πΏβπ)π΅) β€ π§)) |
201 | 196, 199,
200 | syl2anc 585 |
. . 3
β’ (π β ((π΄(πΏβπ)π΅) β€ inf(π, β*, < ) β
βπ§ β π (π΄(πΏβπ)π΅) β€ π§)) |
202 | 193, 201 | mpbird 257 |
. 2
β’ (π β (π΄(πΏβπ)π΅) β€ inf(π, β*, <
)) |
203 | 62 | a1i 11 |
. . . . 5
β’ (π β πΌ = Xπ β π ((π΄βπ)[,)(π΅βπ))) |
204 | | nfv 1918 |
. . . . . 6
β’
β²ππ |
205 | 11 | ffvelcdmda 7087 |
. . . . . 6
β’ ((π β§ π β π) β (π΄βπ) β β) |
206 | 13 | ffvelcdmda 7087 |
. . . . . . 7
β’ ((π β§ π β π) β (π΅βπ) β β) |
207 | 206 | rexrd 11264 |
. . . . . 6
β’ ((π β§ π β π) β (π΅βπ) β
β*) |
208 | 204, 205,
207 | hoissrrn2 45294 |
. . . . 5
β’ (π β Xπ β
π ((π΄βπ)[,)(π΅βπ)) β (β βm π)) |
209 | 203, 208 | eqsstrd 4021 |
. . . 4
β’ (π β πΌ β (β βm π)) |
210 | 9, 173, 209, 1 | ovnn0val 45267 |
. . 3
β’ (π β ((voln*βπ)βπΌ) = inf(π, β*, <
)) |
211 | 210 | eqcomd 2739 |
. 2
β’ (π β inf(π, β*, < ) =
((voln*βπ)βπΌ)) |
212 | 202, 211 | breqtrd 5175 |
1
β’ (π β (π΄(πΏβπ)π΅) β€ ((voln*βπ)βπΌ)) |