Step | Hyp | Ref
| Expression |
1 | | uniioombl.k |
. . 3
β’ πΎ = βͺ
(((,) β πΊ) β
(1...π)) |
2 | | ioof 13423 |
. . . . . 6
β’
(,):(β* Γ β*)βΆπ«
β |
3 | | uniioombl.g |
. . . . . . 7
β’ (π β πΊ:ββΆ( β€ β© (β
Γ β))) |
4 | | inss2 4229 |
. . . . . . . 8
β’ ( β€
β© (β Γ β)) β (β Γ
β) |
5 | | rexpssxrxp 11258 |
. . . . . . . 8
β’ (β
Γ β) β (β* Γ
β*) |
6 | 4, 5 | sstri 3991 |
. . . . . . 7
β’ ( β€
β© (β Γ β)) β (β* Γ
β*) |
7 | | fss 6734 |
. . . . . . 7
β’ ((πΊ:ββΆ( β€ β©
(β Γ β)) β§ ( β€ β© (β Γ β))
β (β* Γ β*)) β πΊ:ββΆ(β* Γ
β*)) |
8 | 3, 6, 7 | sylancl 586 |
. . . . . 6
β’ (π β πΊ:ββΆ(β* Γ
β*)) |
9 | | fco 6741 |
. . . . . 6
β’
(((,):(β* Γ β*)βΆπ«
β β§ πΊ:ββΆ(β* Γ
β*)) β ((,) β πΊ):ββΆπ«
β) |
10 | 2, 8, 9 | sylancr 587 |
. . . . 5
β’ (π β ((,) β πΊ):ββΆπ«
β) |
11 | | ffun 6720 |
. . . . 5
β’ (((,)
β πΊ):ββΆπ« β β
Fun ((,) β πΊ)) |
12 | | funiunfv 7246 |
. . . . 5
β’ (Fun ((,)
β πΊ) β βͺ π β (1...π)(((,) β πΊ)βπ) = βͺ (((,)
β πΊ) β
(1...π))) |
13 | 10, 11, 12 | 3syl 18 |
. . . 4
β’ (π β βͺ π β (1...π)(((,) β πΊ)βπ) = βͺ (((,)
β πΊ) β
(1...π))) |
14 | | elfznn 13529 |
. . . . . 6
β’ (π β (1...π) β π β β) |
15 | | fvco3 6990 |
. . . . . 6
β’ ((πΊ:ββΆ( β€ β©
(β Γ β)) β§ π β β) β (((,) β πΊ)βπ) = ((,)β(πΊβπ))) |
16 | 3, 14, 15 | syl2an 596 |
. . . . 5
β’ ((π β§ π β (1...π)) β (((,) β πΊ)βπ) = ((,)β(πΊβπ))) |
17 | 16 | iuneq2dv 5021 |
. . . 4
β’ (π β βͺ π β (1...π)(((,) β πΊ)βπ) = βͺ π β (1...π)((,)β(πΊβπ))) |
18 | 13, 17 | eqtr3d 2774 |
. . 3
β’ (π β βͺ (((,) β πΊ) β (1...π)) = βͺ
π β (1...π)((,)β(πΊβπ))) |
19 | 1, 18 | eqtrid 2784 |
. 2
β’ (π β πΎ = βͺ π β (1...π)((,)β(πΊβπ))) |
20 | | ffvelcdm 7083 |
. . . . . . . . . . . 12
β’ ((πΊ:ββΆ( β€ β©
(β Γ β)) β§ π β β) β (πΊβπ) β ( β€ β© (β Γ
β))) |
21 | 3, 14, 20 | syl2an 596 |
. . . . . . . . . . 11
β’ ((π β§ π β (1...π)) β (πΊβπ) β ( β€ β© (β Γ
β))) |
22 | 21 | elin2d 4199 |
. . . . . . . . . 10
β’ ((π β§ π β (1...π)) β (πΊβπ) β (β Γ
β)) |
23 | | 1st2nd2 8013 |
. . . . . . . . . 10
β’ ((πΊβπ) β (β Γ β) β
(πΊβπ) = β¨(1st β(πΊβπ)), (2nd β(πΊβπ))β©) |
24 | 22, 23 | syl 17 |
. . . . . . . . 9
β’ ((π β§ π β (1...π)) β (πΊβπ) = β¨(1st β(πΊβπ)), (2nd β(πΊβπ))β©) |
25 | 24 | fveq2d 6895 |
. . . . . . . 8
β’ ((π β§ π β (1...π)) β ((,)β(πΊβπ)) = ((,)ββ¨(1st
β(πΊβπ)), (2nd
β(πΊβπ))β©)) |
26 | | df-ov 7411 |
. . . . . . . 8
β’
((1st β(πΊβπ))(,)(2nd β(πΊβπ))) = ((,)ββ¨(1st
β(πΊβπ)), (2nd
β(πΊβπ))β©) |
27 | 25, 26 | eqtr4di 2790 |
. . . . . . 7
β’ ((π β§ π β (1...π)) β ((,)β(πΊβπ)) = ((1st β(πΊβπ))(,)(2nd β(πΊβπ)))) |
28 | | ioossre 13384 |
. . . . . . 7
β’
((1st β(πΊβπ))(,)(2nd β(πΊβπ))) β β |
29 | 27, 28 | eqsstrdi 4036 |
. . . . . 6
β’ ((π β§ π β (1...π)) β ((,)β(πΊβπ)) β β) |
30 | 29 | ralrimiva 3146 |
. . . . 5
β’ (π β βπ β (1...π)((,)β(πΊβπ)) β β) |
31 | | iunss 5048 |
. . . . 5
β’ (βͺ π β (1...π)((,)β(πΊβπ)) β β β βπ β (1...π)((,)β(πΊβπ)) β β) |
32 | 30, 31 | sylibr 233 |
. . . 4
β’ (π β βͺ π β (1...π)((,)β(πΊβπ)) β β) |
33 | 19, 32 | eqsstrd 4020 |
. . 3
β’ (π β πΎ β β) |
34 | | fzfid 13937 |
. . . 4
β’ (π β (1...π) β Fin) |
35 | 27 | fveq2d 6895 |
. . . . . 6
β’ ((π β§ π β (1...π)) β (vol*β((,)β(πΊβπ))) = (vol*β((1st
β(πΊβπ))(,)(2nd
β(πΊβπ))))) |
36 | | ovolfcl 24982 |
. . . . . . . 8
β’ ((πΊ:ββΆ( β€ β©
(β Γ β)) β§ π β β) β ((1st
β(πΊβπ)) β β β§
(2nd β(πΊβπ)) β β β§ (1st
β(πΊβπ)) β€ (2nd
β(πΊβπ)))) |
37 | 3, 14, 36 | syl2an 596 |
. . . . . . 7
β’ ((π β§ π β (1...π)) β ((1st β(πΊβπ)) β β β§ (2nd
β(πΊβπ)) β β β§
(1st β(πΊβπ)) β€ (2nd β(πΊβπ)))) |
38 | | ovolioo 25084 |
. . . . . . 7
β’
(((1st β(πΊβπ)) β β β§ (2nd
β(πΊβπ)) β β β§
(1st β(πΊβπ)) β€ (2nd β(πΊβπ))) β (vol*β((1st
β(πΊβπ))(,)(2nd
β(πΊβπ)))) = ((2nd
β(πΊβπ)) β (1st
β(πΊβπ)))) |
39 | 37, 38 | syl 17 |
. . . . . 6
β’ ((π β§ π β (1...π)) β (vol*β((1st
β(πΊβπ))(,)(2nd
β(πΊβπ)))) = ((2nd
β(πΊβπ)) β (1st
β(πΊβπ)))) |
40 | 35, 39 | eqtrd 2772 |
. . . . 5
β’ ((π β§ π β (1...π)) β (vol*β((,)β(πΊβπ))) = ((2nd β(πΊβπ)) β (1st β(πΊβπ)))) |
41 | 37 | simp2d 1143 |
. . . . . 6
β’ ((π β§ π β (1...π)) β (2nd β(πΊβπ)) β β) |
42 | 37 | simp1d 1142 |
. . . . . 6
β’ ((π β§ π β (1...π)) β (1st β(πΊβπ)) β β) |
43 | 41, 42 | resubcld 11641 |
. . . . 5
β’ ((π β§ π β (1...π)) β ((2nd β(πΊβπ)) β (1st β(πΊβπ))) β β) |
44 | 40, 43 | eqeltrd 2833 |
. . . 4
β’ ((π β§ π β (1...π)) β (vol*β((,)β(πΊβπ))) β β) |
45 | 34, 44 | fsumrecl 15679 |
. . 3
β’ (π β Ξ£π β (1...π)(vol*β((,)β(πΊβπ))) β β) |
46 | 19 | fveq2d 6895 |
. . . 4
β’ (π β (vol*βπΎ) = (vol*ββͺ π β (1...π)((,)β(πΊβπ)))) |
47 | 29, 44 | jca 512 |
. . . . . 6
β’ ((π β§ π β (1...π)) β (((,)β(πΊβπ)) β β β§
(vol*β((,)β(πΊβπ))) β β)) |
48 | 47 | ralrimiva 3146 |
. . . . 5
β’ (π β βπ β (1...π)(((,)β(πΊβπ)) β β β§
(vol*β((,)β(πΊβπ))) β β)) |
49 | | ovolfiniun 25017 |
. . . . 5
β’
(((1...π) β Fin
β§ βπ β
(1...π)(((,)β(πΊβπ)) β β β§
(vol*β((,)β(πΊβπ))) β β)) β
(vol*ββͺ π β (1...π)((,)β(πΊβπ))) β€ Ξ£π β (1...π)(vol*β((,)β(πΊβπ)))) |
50 | 34, 48, 49 | syl2anc 584 |
. . . 4
β’ (π β (vol*ββͺ π β (1...π)((,)β(πΊβπ))) β€ Ξ£π β (1...π)(vol*β((,)β(πΊβπ)))) |
51 | 46, 50 | eqbrtrd 5170 |
. . 3
β’ (π β (vol*βπΎ) β€ Ξ£π β (1...π)(vol*β((,)β(πΊβπ)))) |
52 | | ovollecl 24999 |
. . 3
β’ ((πΎ β β β§
Ξ£π β (1...π)(vol*β((,)β(πΊβπ))) β β β§ (vol*βπΎ) β€ Ξ£π β (1...π)(vol*β((,)β(πΊβπ)))) β (vol*βπΎ) β β) |
53 | 33, 45, 51, 52 | syl3anc 1371 |
. 2
β’ (π β (vol*βπΎ) β
β) |
54 | 19, 53 | jca 512 |
1
β’ (π β (πΎ = βͺ π β (1...π)((,)β(πΊβπ)) β§ (vol*βπΎ) β β)) |