Step | Hyp | Ref
| Expression |
1 | | uniioombl.k |
. . 3
β’ πΎ = βͺ
(((,) β πΊ) β
(1...π)) |
2 | | ioof 13373 |
. . . . . 6
β’
(,):(β* Γ β*)βΆπ«
β |
3 | | uniioombl.g |
. . . . . . 7
β’ (π β πΊ:ββΆ( β€ β© (β
Γ β))) |
4 | | inss2 4193 |
. . . . . . . 8
β’ ( β€
β© (β Γ β)) β (β Γ
β) |
5 | | rexpssxrxp 11208 |
. . . . . . . 8
β’ (β
Γ β) β (β* Γ
β*) |
6 | 4, 5 | sstri 3957 |
. . . . . . 7
β’ ( β€
β© (β Γ β)) β (β* Γ
β*) |
7 | | fss 6689 |
. . . . . . 7
β’ ((πΊ:ββΆ( β€ β©
(β Γ β)) β§ ( β€ β© (β Γ β))
β (β* Γ β*)) β πΊ:ββΆ(β* Γ
β*)) |
8 | 3, 6, 7 | sylancl 587 |
. . . . . 6
β’ (π β πΊ:ββΆ(β* Γ
β*)) |
9 | | fco 6696 |
. . . . . 6
β’
(((,):(β* Γ β*)βΆπ«
β β§ πΊ:ββΆ(β* Γ
β*)) β ((,) β πΊ):ββΆπ«
β) |
10 | 2, 8, 9 | sylancr 588 |
. . . . 5
β’ (π β ((,) β πΊ):ββΆπ«
β) |
11 | | ffun 6675 |
. . . . 5
β’ (((,)
β πΊ):ββΆπ« β β
Fun ((,) β πΊ)) |
12 | | funiunfv 7199 |
. . . . 5
β’ (Fun ((,)
β πΊ) β βͺ π β (1...π)(((,) β πΊ)βπ) = βͺ (((,)
β πΊ) β
(1...π))) |
13 | 10, 11, 12 | 3syl 18 |
. . . 4
β’ (π β βͺ π β (1...π)(((,) β πΊ)βπ) = βͺ (((,)
β πΊ) β
(1...π))) |
14 | | elfznn 13479 |
. . . . . 6
β’ (π β (1...π) β π β β) |
15 | | fvco3 6944 |
. . . . . 6
β’ ((πΊ:ββΆ( β€ β©
(β Γ β)) β§ π β β) β (((,) β πΊ)βπ) = ((,)β(πΊβπ))) |
16 | 3, 14, 15 | syl2an 597 |
. . . . 5
β’ ((π β§ π β (1...π)) β (((,) β πΊ)βπ) = ((,)β(πΊβπ))) |
17 | 16 | iuneq2dv 4982 |
. . . 4
β’ (π β βͺ π β (1...π)(((,) β πΊ)βπ) = βͺ π β (1...π)((,)β(πΊβπ))) |
18 | 13, 17 | eqtr3d 2775 |
. . 3
β’ (π β βͺ (((,) β πΊ) β (1...π)) = βͺ
π β (1...π)((,)β(πΊβπ))) |
19 | 1, 18 | eqtrid 2785 |
. 2
β’ (π β πΎ = βͺ π β (1...π)((,)β(πΊβπ))) |
20 | | ffvelcdm 7036 |
. . . . . . . . . . . 12
β’ ((πΊ:ββΆ( β€ β©
(β Γ β)) β§ π β β) β (πΊβπ) β ( β€ β© (β Γ
β))) |
21 | 3, 14, 20 | syl2an 597 |
. . . . . . . . . . 11
β’ ((π β§ π β (1...π)) β (πΊβπ) β ( β€ β© (β Γ
β))) |
22 | 21 | elin2d 4163 |
. . . . . . . . . 10
β’ ((π β§ π β (1...π)) β (πΊβπ) β (β Γ
β)) |
23 | | 1st2nd2 7964 |
. . . . . . . . . 10
β’ ((πΊβπ) β (β Γ β) β
(πΊβπ) = β¨(1st β(πΊβπ)), (2nd β(πΊβπ))β©) |
24 | 22, 23 | syl 17 |
. . . . . . . . 9
β’ ((π β§ π β (1...π)) β (πΊβπ) = β¨(1st β(πΊβπ)), (2nd β(πΊβπ))β©) |
25 | 24 | fveq2d 6850 |
. . . . . . . 8
β’ ((π β§ π β (1...π)) β ((,)β(πΊβπ)) = ((,)ββ¨(1st
β(πΊβπ)), (2nd
β(πΊβπ))β©)) |
26 | | df-ov 7364 |
. . . . . . . 8
β’
((1st β(πΊβπ))(,)(2nd β(πΊβπ))) = ((,)ββ¨(1st
β(πΊβπ)), (2nd
β(πΊβπ))β©) |
27 | 25, 26 | eqtr4di 2791 |
. . . . . . 7
β’ ((π β§ π β (1...π)) β ((,)β(πΊβπ)) = ((1st β(πΊβπ))(,)(2nd β(πΊβπ)))) |
28 | | ioossre 13334 |
. . . . . . 7
β’
((1st β(πΊβπ))(,)(2nd β(πΊβπ))) β β |
29 | 27, 28 | eqsstrdi 4002 |
. . . . . 6
β’ ((π β§ π β (1...π)) β ((,)β(πΊβπ)) β β) |
30 | 29 | ralrimiva 3140 |
. . . . 5
β’ (π β βπ β (1...π)((,)β(πΊβπ)) β β) |
31 | | iunss 5009 |
. . . . 5
β’ (βͺ π β (1...π)((,)β(πΊβπ)) β β β βπ β (1...π)((,)β(πΊβπ)) β β) |
32 | 30, 31 | sylibr 233 |
. . . 4
β’ (π β βͺ π β (1...π)((,)β(πΊβπ)) β β) |
33 | 19, 32 | eqsstrd 3986 |
. . 3
β’ (π β πΎ β β) |
34 | | fzfid 13887 |
. . . 4
β’ (π β (1...π) β Fin) |
35 | 27 | fveq2d 6850 |
. . . . . 6
β’ ((π β§ π β (1...π)) β (vol*β((,)β(πΊβπ))) = (vol*β((1st
β(πΊβπ))(,)(2nd
β(πΊβπ))))) |
36 | | ovolfcl 24853 |
. . . . . . . 8
β’ ((πΊ:ββΆ( β€ β©
(β Γ β)) β§ π β β) β ((1st
β(πΊβπ)) β β β§
(2nd β(πΊβπ)) β β β§ (1st
β(πΊβπ)) β€ (2nd
β(πΊβπ)))) |
37 | 3, 14, 36 | syl2an 597 |
. . . . . . 7
β’ ((π β§ π β (1...π)) β ((1st β(πΊβπ)) β β β§ (2nd
β(πΊβπ)) β β β§
(1st β(πΊβπ)) β€ (2nd β(πΊβπ)))) |
38 | | ovolioo 24955 |
. . . . . . 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 2773 |
. . . . 5
β’ ((π β§ π β (1...π)) β (vol*β((,)β(πΊβπ))) = ((2nd β(πΊβπ)) β (1st β(πΊβπ)))) |
41 | 37 | simp2d 1144 |
. . . . . 6
β’ ((π β§ π β (1...π)) β (2nd β(πΊβπ)) β β) |
42 | 37 | simp1d 1143 |
. . . . . 6
β’ ((π β§ π β (1...π)) β (1st β(πΊβπ)) β β) |
43 | 41, 42 | resubcld 11591 |
. . . . 5
β’ ((π β§ π β (1...π)) β ((2nd β(πΊβπ)) β (1st β(πΊβπ))) β β) |
44 | 40, 43 | eqeltrd 2834 |
. . . 4
β’ ((π β§ π β (1...π)) β (vol*β((,)β(πΊβπ))) β β) |
45 | 34, 44 | fsumrecl 15627 |
. . 3
β’ (π β Ξ£π β (1...π)(vol*β((,)β(πΊβπ))) β β) |
46 | 19 | fveq2d 6850 |
. . . 4
β’ (π β (vol*βπΎ) = (vol*ββͺ π β (1...π)((,)β(πΊβπ)))) |
47 | 29, 44 | jca 513 |
. . . . . 6
β’ ((π β§ π β (1...π)) β (((,)β(πΊβπ)) β β β§
(vol*β((,)β(πΊβπ))) β β)) |
48 | 47 | ralrimiva 3140 |
. . . . 5
β’ (π β βπ β (1...π)(((,)β(πΊβπ)) β β β§
(vol*β((,)β(πΊβπ))) β β)) |
49 | | ovolfiniun 24888 |
. . . . 5
β’
(((1...π) β Fin
β§ βπ β
(1...π)(((,)β(πΊβπ)) β β β§
(vol*β((,)β(πΊβπ))) β β)) β
(vol*ββͺ π β (1...π)((,)β(πΊβπ))) β€ Ξ£π β (1...π)(vol*β((,)β(πΊβπ)))) |
50 | 34, 48, 49 | syl2anc 585 |
. . . 4
β’ (π β (vol*ββͺ π β (1...π)((,)β(πΊβπ))) β€ Ξ£π β (1...π)(vol*β((,)β(πΊβπ)))) |
51 | 46, 50 | eqbrtrd 5131 |
. . 3
β’ (π β (vol*βπΎ) β€ Ξ£π β (1...π)(vol*β((,)β(πΊβπ)))) |
52 | | ovollecl 24870 |
. . 3
β’ ((πΎ β β β§
Ξ£π β (1...π)(vol*β((,)β(πΊβπ))) β β β§ (vol*βπΎ) β€ Ξ£π β (1...π)(vol*β((,)β(πΊβπ)))) β (vol*βπΎ) β β) |
53 | 33, 45, 51, 52 | syl3anc 1372 |
. 2
β’ (π β (vol*βπΎ) β
β) |
54 | 19, 53 | jca 513 |
1
β’ (π β (πΎ = βͺ π β (1...π)((,)β(πΊβπ)) β§ (vol*βπΎ) β β)) |