Metamath Proof Explorer

Theorem itg1climres

Description: Restricting the simple function F to the increasing sequence A ( n ) of measurable sets whose union is RR yields a sequence of simple functions whose integrals approach the integral of F . (Contributed by Mario Carneiro, 15-Aug-2014)

Ref Expression
Hypotheses itg1climres.1 
|- ( ph -> A : NN --> dom vol )
itg1climres.2 
|- ( ( ph /\ n e. NN ) -> ( A ` n ) C_ ( A ` ( n + 1 ) ) )
itg1climres.3 
|- ( ph -> U. ran A = RR )
itg1climres.4 
|- ( ph -> F e. dom S.1 )
itg1climres.5 
|- G = ( x e. RR |-> if ( x e. ( A ` n ) , ( F ` x ) , 0 ) )
Assertion itg1climres 
|- ( ph -> ( n e. NN |-> ( S.1 ` G ) ) ~~> ( S.1 ` F ) )

Proof

Step Hyp Ref Expression
1 itg1climres.1 
 |-  ( ph -> A : NN --> dom vol )
2 itg1climres.2 
 |-  ( ( ph /\ n e. NN ) -> ( A ` n ) C_ ( A ` ( n + 1 ) ) )
3 itg1climres.3 
 |-  ( ph -> U. ran A = RR )
4 itg1climres.4 
 |-  ( ph -> F e. dom S.1 )
5 itg1climres.5 
 |-  G = ( x e. RR |-> if ( x e. ( A ` n ) , ( F ` x ) , 0 ) )
6 nnuz 
 |-  NN = ( ZZ>= ` 1 )
7 1zzd 
 |-  ( ph -> 1 e. ZZ )
8 i1frn 
 |-  ( F e. dom S.1 -> ran F e. Fin )
9 4 8 syl 
 |-  ( ph -> ran F e. Fin )
10 difss 
 |-  ( ran F \ { 0 } ) C_ ran F
11 ssfi 
 |-  ( ( ran F e. Fin /\ ( ran F \ { 0 } ) C_ ran F ) -> ( ran F \ { 0 } ) e. Fin )
12 9 10 11 sylancl 
 |-  ( ph -> ( ran F \ { 0 } ) e. Fin )
13 1zzd 
 |-  ( ( ph /\ k e. ( ran F \ { 0 } ) ) -> 1 e. ZZ )
14 i1fima 
 |-  ( F e. dom S.1 -> ( `' F " { k } ) e. dom vol )
15 4 14 syl 
 |-  ( ph -> ( `' F " { k } ) e. dom vol )
16 15 ad2antrr 
 |-  ( ( ( ph /\ k e. ( ran F \ { 0 } ) ) /\ n e. NN ) -> ( `' F " { k } ) e. dom vol )
17 1 ffvelcdmda 
 |-  ( ( ph /\ n e. NN ) -> ( A ` n ) e. dom vol )
18 17 adantlr 
 |-  ( ( ( ph /\ k e. ( ran F \ { 0 } ) ) /\ n e. NN ) -> ( A ` n ) e. dom vol )
19 inmbl 
 |-  ( ( ( `' F " { k } ) e. dom vol /\ ( A ` n ) e. dom vol ) -> ( ( `' F " { k } ) i^i ( A ` n ) ) e. dom vol )
20 16 18 19 syl2anc 
 |-  ( ( ( ph /\ k e. ( ran F \ { 0 } ) ) /\ n e. NN ) -> ( ( `' F " { k } ) i^i ( A ` n ) ) e. dom vol )
21 mblvol 
 |-  ( ( ( `' F " { k } ) i^i ( A ` n ) ) e. dom vol -> ( vol ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) = ( vol* ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) )
22 20 21 syl 
 |-  ( ( ( ph /\ k e. ( ran F \ { 0 } ) ) /\ n e. NN ) -> ( vol ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) = ( vol* ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) )
23 inss1 
 |-  ( ( `' F " { k } ) i^i ( A ` n ) ) C_ ( `' F " { k } )
24 23 a1i 
 |-  ( ( ( ph /\ k e. ( ran F \ { 0 } ) ) /\ n e. NN ) -> ( ( `' F " { k } ) i^i ( A ` n ) ) C_ ( `' F " { k } ) )
25 mblss 
 |-  ( ( `' F " { k } ) e. dom vol -> ( `' F " { k } ) C_ RR )
26 16 25 syl 
 |-  ( ( ( ph /\ k e. ( ran F \ { 0 } ) ) /\ n e. NN ) -> ( `' F " { k } ) C_ RR )
27 mblvol 
 |-  ( ( `' F " { k } ) e. dom vol -> ( vol ` ( `' F " { k } ) ) = ( vol* ` ( `' F " { k } ) ) )
28 16 27 syl 
 |-  ( ( ( ph /\ k e. ( ran F \ { 0 } ) ) /\ n e. NN ) -> ( vol ` ( `' F " { k } ) ) = ( vol* ` ( `' F " { k } ) ) )
29 i1fima2sn 
 |-  ( ( F e. dom S.1 /\ k e. ( ran F \ { 0 } ) ) -> ( vol ` ( `' F " { k } ) ) e. RR )
30 4 29 sylan 
 |-  ( ( ph /\ k e. ( ran F \ { 0 } ) ) -> ( vol ` ( `' F " { k } ) ) e. RR )
31 30 adantr 
 |-  ( ( ( ph /\ k e. ( ran F \ { 0 } ) ) /\ n e. NN ) -> ( vol ` ( `' F " { k } ) ) e. RR )
32 28 31 eqeltrrd 
 |-  ( ( ( ph /\ k e. ( ran F \ { 0 } ) ) /\ n e. NN ) -> ( vol* ` ( `' F " { k } ) ) e. RR )
33 ovolsscl 
 |-  ( ( ( ( `' F " { k } ) i^i ( A ` n ) ) C_ ( `' F " { k } ) /\ ( `' F " { k } ) C_ RR /\ ( vol* ` ( `' F " { k } ) ) e. RR ) -> ( vol* ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) e. RR )
34 24 26 32 33 syl3anc 
 |-  ( ( ( ph /\ k e. ( ran F \ { 0 } ) ) /\ n e. NN ) -> ( vol* ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) e. RR )
35 22 34 eqeltrd 
 |-  ( ( ( ph /\ k e. ( ran F \ { 0 } ) ) /\ n e. NN ) -> ( vol ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) e. RR )
36 35 fmpttd 
 |-  ( ( ph /\ k e. ( ran F \ { 0 } ) ) -> ( n e. NN |-> ( vol ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) ) : NN --> RR )
37 2 adantlr 
 |-  ( ( ( ph /\ k e. ( ran F \ { 0 } ) ) /\ n e. NN ) -> ( A ` n ) C_ ( A ` ( n + 1 ) ) )
38 sslin 
 |-  ( ( A ` n ) C_ ( A ` ( n + 1 ) ) -> ( ( `' F " { k } ) i^i ( A ` n ) ) C_ ( ( `' F " { k } ) i^i ( A ` ( n + 1 ) ) ) )
39 37 38 syl 
 |-  ( ( ( ph /\ k e. ( ran F \ { 0 } ) ) /\ n e. NN ) -> ( ( `' F " { k } ) i^i ( A ` n ) ) C_ ( ( `' F " { k } ) i^i ( A ` ( n + 1 ) ) ) )
40 1 adantr 
 |-  ( ( ph /\ k e. ( ran F \ { 0 } ) ) -> A : NN --> dom vol )
41 peano2nn 
 |-  ( n e. NN -> ( n + 1 ) e. NN )
42 ffvelcdm 
 |-  ( ( A : NN --> dom vol /\ ( n + 1 ) e. NN ) -> ( A ` ( n + 1 ) ) e. dom vol )
43 40 41 42 syl2an 
 |-  ( ( ( ph /\ k e. ( ran F \ { 0 } ) ) /\ n e. NN ) -> ( A ` ( n + 1 ) ) e. dom vol )
44 inmbl 
 |-  ( ( ( `' F " { k } ) e. dom vol /\ ( A ` ( n + 1 ) ) e. dom vol ) -> ( ( `' F " { k } ) i^i ( A ` ( n + 1 ) ) ) e. dom vol )
45 16 43 44 syl2anc 
 |-  ( ( ( ph /\ k e. ( ran F \ { 0 } ) ) /\ n e. NN ) -> ( ( `' F " { k } ) i^i ( A ` ( n + 1 ) ) ) e. dom vol )
46 mblss 
 |-  ( ( ( `' F " { k } ) i^i ( A ` ( n + 1 ) ) ) e. dom vol -> ( ( `' F " { k } ) i^i ( A ` ( n + 1 ) ) ) C_ RR )
47 45 46 syl 
 |-  ( ( ( ph /\ k e. ( ran F \ { 0 } ) ) /\ n e. NN ) -> ( ( `' F " { k } ) i^i ( A ` ( n + 1 ) ) ) C_ RR )
48 ovolss 
 |-  ( ( ( ( `' F " { k } ) i^i ( A ` n ) ) C_ ( ( `' F " { k } ) i^i ( A ` ( n + 1 ) ) ) /\ ( ( `' F " { k } ) i^i ( A ` ( n + 1 ) ) ) C_ RR ) -> ( vol* ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) <_ ( vol* ` ( ( `' F " { k } ) i^i ( A ` ( n + 1 ) ) ) ) )
49 39 47 48 syl2anc 
 |-  ( ( ( ph /\ k e. ( ran F \ { 0 } ) ) /\ n e. NN ) -> ( vol* ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) <_ ( vol* ` ( ( `' F " { k } ) i^i ( A ` ( n + 1 ) ) ) ) )
50 mblvol 
 |-  ( ( ( `' F " { k } ) i^i ( A ` ( n + 1 ) ) ) e. dom vol -> ( vol ` ( ( `' F " { k } ) i^i ( A ` ( n + 1 ) ) ) ) = ( vol* ` ( ( `' F " { k } ) i^i ( A ` ( n + 1 ) ) ) ) )
51 45 50 syl 
 |-  ( ( ( ph /\ k e. ( ran F \ { 0 } ) ) /\ n e. NN ) -> ( vol ` ( ( `' F " { k } ) i^i ( A ` ( n + 1 ) ) ) ) = ( vol* ` ( ( `' F " { k } ) i^i ( A ` ( n + 1 ) ) ) ) )
52 49 22 51 3brtr4d 
 |-  ( ( ( ph /\ k e. ( ran F \ { 0 } ) ) /\ n e. NN ) -> ( vol ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) <_ ( vol ` ( ( `' F " { k } ) i^i ( A ` ( n + 1 ) ) ) ) )
53 52 ralrimiva 
 |-  ( ( ph /\ k e. ( ran F \ { 0 } ) ) -> A. n e. NN ( vol ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) <_ ( vol ` ( ( `' F " { k } ) i^i ( A ` ( n + 1 ) ) ) ) )
54 fveq2 
 |-  ( n = j -> ( A ` n ) = ( A ` j ) )
55 54 ineq2d 
 |-  ( n = j -> ( ( `' F " { k } ) i^i ( A ` n ) ) = ( ( `' F " { k } ) i^i ( A ` j ) ) )
56 55 fveq2d 
 |-  ( n = j -> ( vol ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) = ( vol ` ( ( `' F " { k } ) i^i ( A ` j ) ) ) )
57 eqid 
 |-  ( n e. NN |-> ( vol ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) ) = ( n e. NN |-> ( vol ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) )
58 fvex 
 |-  ( vol ` ( ( `' F " { k } ) i^i ( A ` j ) ) ) e. _V
59 56 57 58 fvmpt 
 |-  ( j e. NN -> ( ( n e. NN |-> ( vol ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) ) ` j ) = ( vol ` ( ( `' F " { k } ) i^i ( A ` j ) ) ) )
60 peano2nn 
 |-  ( j e. NN -> ( j + 1 ) e. NN )
61 fveq2 
 |-  ( n = ( j + 1 ) -> ( A ` n ) = ( A ` ( j + 1 ) ) )
62 61 ineq2d 
 |-  ( n = ( j + 1 ) -> ( ( `' F " { k } ) i^i ( A ` n ) ) = ( ( `' F " { k } ) i^i ( A ` ( j + 1 ) ) ) )
63 62 fveq2d 
 |-  ( n = ( j + 1 ) -> ( vol ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) = ( vol ` ( ( `' F " { k } ) i^i ( A ` ( j + 1 ) ) ) ) )
64 fvex 
 |-  ( vol ` ( ( `' F " { k } ) i^i ( A ` ( j + 1 ) ) ) ) e. _V
65 63 57 64 fvmpt 
 |-  ( ( j + 1 ) e. NN -> ( ( n e. NN |-> ( vol ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) ) ` ( j + 1 ) ) = ( vol ` ( ( `' F " { k } ) i^i ( A ` ( j + 1 ) ) ) ) )
66 60 65 syl 
 |-  ( j e. NN -> ( ( n e. NN |-> ( vol ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) ) ` ( j + 1 ) ) = ( vol ` ( ( `' F " { k } ) i^i ( A ` ( j + 1 ) ) ) ) )
67 59 66 breq12d 
 |-  ( j e. NN -> ( ( ( n e. NN |-> ( vol ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) ) ` j ) <_ ( ( n e. NN |-> ( vol ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) ) ` ( j + 1 ) ) <-> ( vol ` ( ( `' F " { k } ) i^i ( A ` j ) ) ) <_ ( vol ` ( ( `' F " { k } ) i^i ( A ` ( j + 1 ) ) ) ) ) )
68 67 ralbiia 
 |-  ( A. j e. NN ( ( n e. NN |-> ( vol ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) ) ` j ) <_ ( ( n e. NN |-> ( vol ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) ) ` ( j + 1 ) ) <-> A. j e. NN ( vol ` ( ( `' F " { k } ) i^i ( A ` j ) ) ) <_ ( vol ` ( ( `' F " { k } ) i^i ( A ` ( j + 1 ) ) ) ) )
69 fvoveq1 
 |-  ( n = j -> ( A ` ( n + 1 ) ) = ( A ` ( j + 1 ) ) )
70 69 ineq2d 
 |-  ( n = j -> ( ( `' F " { k } ) i^i ( A ` ( n + 1 ) ) ) = ( ( `' F " { k } ) i^i ( A ` ( j + 1 ) ) ) )
71 70 fveq2d 
 |-  ( n = j -> ( vol ` ( ( `' F " { k } ) i^i ( A ` ( n + 1 ) ) ) ) = ( vol ` ( ( `' F " { k } ) i^i ( A ` ( j + 1 ) ) ) ) )
72 56 71 breq12d 
 |-  ( n = j -> ( ( vol ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) <_ ( vol ` ( ( `' F " { k } ) i^i ( A ` ( n + 1 ) ) ) ) <-> ( vol ` ( ( `' F " { k } ) i^i ( A ` j ) ) ) <_ ( vol ` ( ( `' F " { k } ) i^i ( A ` ( j + 1 ) ) ) ) ) )
73 72 cbvralvw 
 |-  ( A. n e. NN ( vol ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) <_ ( vol ` ( ( `' F " { k } ) i^i ( A ` ( n + 1 ) ) ) ) <-> A. j e. NN ( vol ` ( ( `' F " { k } ) i^i ( A ` j ) ) ) <_ ( vol ` ( ( `' F " { k } ) i^i ( A ` ( j + 1 ) ) ) ) )
74 68 73 bitr4i 
 |-  ( A. j e. NN ( ( n e. NN |-> ( vol ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) ) ` j ) <_ ( ( n e. NN |-> ( vol ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) ) ` ( j + 1 ) ) <-> A. n e. NN ( vol ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) <_ ( vol ` ( ( `' F " { k } ) i^i ( A ` ( n + 1 ) ) ) ) )
75 53 74 sylibr 
 |-  ( ( ph /\ k e. ( ran F \ { 0 } ) ) -> A. j e. NN ( ( n e. NN |-> ( vol ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) ) ` j ) <_ ( ( n e. NN |-> ( vol ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) ) ` ( j + 1 ) ) )
76 75 r19.21bi 
 |-  ( ( ( ph /\ k e. ( ran F \ { 0 } ) ) /\ j e. NN ) -> ( ( n e. NN |-> ( vol ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) ) ` j ) <_ ( ( n e. NN |-> ( vol ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) ) ` ( j + 1 ) ) )
77 ovolss 
 |-  ( ( ( ( `' F " { k } ) i^i ( A ` n ) ) C_ ( `' F " { k } ) /\ ( `' F " { k } ) C_ RR ) -> ( vol* ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) <_ ( vol* ` ( `' F " { k } ) ) )
78 23 26 77 sylancr 
 |-  ( ( ( ph /\ k e. ( ran F \ { 0 } ) ) /\ n e. NN ) -> ( vol* ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) <_ ( vol* ` ( `' F " { k } ) ) )
79 78 22 28 3brtr4d 
 |-  ( ( ( ph /\ k e. ( ran F \ { 0 } ) ) /\ n e. NN ) -> ( vol ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) <_ ( vol ` ( `' F " { k } ) ) )
80 79 ralrimiva 
 |-  ( ( ph /\ k e. ( ran F \ { 0 } ) ) -> A. n e. NN ( vol ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) <_ ( vol ` ( `' F " { k } ) ) )
81 59 breq1d 
 |-  ( j e. NN -> ( ( ( n e. NN |-> ( vol ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) ) ` j ) <_ ( vol ` ( `' F " { k } ) ) <-> ( vol ` ( ( `' F " { k } ) i^i ( A ` j ) ) ) <_ ( vol ` ( `' F " { k } ) ) ) )
82 81 ralbiia 
 |-  ( A. j e. NN ( ( n e. NN |-> ( vol ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) ) ` j ) <_ ( vol ` ( `' F " { k } ) ) <-> A. j e. NN ( vol ` ( ( `' F " { k } ) i^i ( A ` j ) ) ) <_ ( vol ` ( `' F " { k } ) ) )
83 56 breq1d 
 |-  ( n = j -> ( ( vol ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) <_ ( vol ` ( `' F " { k } ) ) <-> ( vol ` ( ( `' F " { k } ) i^i ( A ` j ) ) ) <_ ( vol ` ( `' F " { k } ) ) ) )
84 83 cbvralvw 
 |-  ( A. n e. NN ( vol ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) <_ ( vol ` ( `' F " { k } ) ) <-> A. j e. NN ( vol ` ( ( `' F " { k } ) i^i ( A ` j ) ) ) <_ ( vol ` ( `' F " { k } ) ) )
85 82 84 bitr4i 
 |-  ( A. j e. NN ( ( n e. NN |-> ( vol ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) ) ` j ) <_ ( vol ` ( `' F " { k } ) ) <-> A. n e. NN ( vol ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) <_ ( vol ` ( `' F " { k } ) ) )
86 80 85 sylibr 
 |-  ( ( ph /\ k e. ( ran F \ { 0 } ) ) -> A. j e. NN ( ( n e. NN |-> ( vol ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) ) ` j ) <_ ( vol ` ( `' F " { k } ) ) )
87 brralrspcev 
 |-  ( ( ( vol ` ( `' F " { k } ) ) e. RR /\ A. j e. NN ( ( n e. NN |-> ( vol ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) ) ` j ) <_ ( vol ` ( `' F " { k } ) ) ) -> E. x e. RR A. j e. NN ( ( n e. NN |-> ( vol ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) ) ` j ) <_ x )
88 30 86 87 syl2anc 
 |-  ( ( ph /\ k e. ( ran F \ { 0 } ) ) -> E. x e. RR A. j e. NN ( ( n e. NN |-> ( vol ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) ) ` j ) <_ x )
89 6 13 36 76 88 climsup 
 |-  ( ( ph /\ k e. ( ran F \ { 0 } ) ) -> ( n e. NN |-> ( vol ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) ) ~~> sup ( ran ( n e. NN |-> ( vol ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) ) , RR , < ) )
90 20 fmpttd 
 |-  ( ( ph /\ k e. ( ran F \ { 0 } ) ) -> ( n e. NN |-> ( ( `' F " { k } ) i^i ( A ` n ) ) ) : NN --> dom vol )
91 39 ralrimiva 
 |-  ( ( ph /\ k e. ( ran F \ { 0 } ) ) -> A. n e. NN ( ( `' F " { k } ) i^i ( A ` n ) ) C_ ( ( `' F " { k } ) i^i ( A ` ( n + 1 ) ) ) )
92 eqid 
 |-  ( n e. NN |-> ( ( `' F " { k } ) i^i ( A ` n ) ) ) = ( n e. NN |-> ( ( `' F " { k } ) i^i ( A ` n ) ) )
93 fvex 
 |-  ( A ` j ) e. _V
94 93 inex2 
 |-  ( ( `' F " { k } ) i^i ( A ` j ) ) e. _V
95 55 92 94 fvmpt 
 |-  ( j e. NN -> ( ( n e. NN |-> ( ( `' F " { k } ) i^i ( A ` n ) ) ) ` j ) = ( ( `' F " { k } ) i^i ( A ` j ) ) )
96 fvex 
 |-  ( A ` ( j + 1 ) ) e. _V
97 96 inex2 
 |-  ( ( `' F " { k } ) i^i ( A ` ( j + 1 ) ) ) e. _V
98 62 92 97 fvmpt 
 |-  ( ( j + 1 ) e. NN -> ( ( n e. NN |-> ( ( `' F " { k } ) i^i ( A ` n ) ) ) ` ( j + 1 ) ) = ( ( `' F " { k } ) i^i ( A ` ( j + 1 ) ) ) )
99 60 98 syl 
 |-  ( j e. NN -> ( ( n e. NN |-> ( ( `' F " { k } ) i^i ( A ` n ) ) ) ` ( j + 1 ) ) = ( ( `' F " { k } ) i^i ( A ` ( j + 1 ) ) ) )
100 95 99 sseq12d 
 |-  ( j e. NN -> ( ( ( n e. NN |-> ( ( `' F " { k } ) i^i ( A ` n ) ) ) ` j ) C_ ( ( n e. NN |-> ( ( `' F " { k } ) i^i ( A ` n ) ) ) ` ( j + 1 ) ) <-> ( ( `' F " { k } ) i^i ( A ` j ) ) C_ ( ( `' F " { k } ) i^i ( A ` ( j + 1 ) ) ) ) )
101 100 ralbiia 
 |-  ( A. j e. NN ( ( n e. NN |-> ( ( `' F " { k } ) i^i ( A ` n ) ) ) ` j ) C_ ( ( n e. NN |-> ( ( `' F " { k } ) i^i ( A ` n ) ) ) ` ( j + 1 ) ) <-> A. j e. NN ( ( `' F " { k } ) i^i ( A ` j ) ) C_ ( ( `' F " { k } ) i^i ( A ` ( j + 1 ) ) ) )
102 55 70 sseq12d 
 |-  ( n = j -> ( ( ( `' F " { k } ) i^i ( A ` n ) ) C_ ( ( `' F " { k } ) i^i ( A ` ( n + 1 ) ) ) <-> ( ( `' F " { k } ) i^i ( A ` j ) ) C_ ( ( `' F " { k } ) i^i ( A ` ( j + 1 ) ) ) ) )
103 102 cbvralvw 
 |-  ( A. n e. NN ( ( `' F " { k } ) i^i ( A ` n ) ) C_ ( ( `' F " { k } ) i^i ( A ` ( n + 1 ) ) ) <-> A. j e. NN ( ( `' F " { k } ) i^i ( A ` j ) ) C_ ( ( `' F " { k } ) i^i ( A ` ( j + 1 ) ) ) )
104 101 103 bitr4i 
 |-  ( A. j e. NN ( ( n e. NN |-> ( ( `' F " { k } ) i^i ( A ` n ) ) ) ` j ) C_ ( ( n e. NN |-> ( ( `' F " { k } ) i^i ( A ` n ) ) ) ` ( j + 1 ) ) <-> A. n e. NN ( ( `' F " { k } ) i^i ( A ` n ) ) C_ ( ( `' F " { k } ) i^i ( A ` ( n + 1 ) ) ) )
105 91 104 sylibr 
 |-  ( ( ph /\ k e. ( ran F \ { 0 } ) ) -> A. j e. NN ( ( n e. NN |-> ( ( `' F " { k } ) i^i ( A ` n ) ) ) ` j ) C_ ( ( n e. NN |-> ( ( `' F " { k } ) i^i ( A ` n ) ) ) ` ( j + 1 ) ) )
106 volsup 
 |-  ( ( ( n e. NN |-> ( ( `' F " { k } ) i^i ( A ` n ) ) ) : NN --> dom vol /\ A. j e. NN ( ( n e. NN |-> ( ( `' F " { k } ) i^i ( A ` n ) ) ) ` j ) C_ ( ( n e. NN |-> ( ( `' F " { k } ) i^i ( A ` n ) ) ) ` ( j + 1 ) ) ) -> ( vol ` U. ran ( n e. NN |-> ( ( `' F " { k } ) i^i ( A ` n ) ) ) ) = sup ( ( vol " ran ( n e. NN |-> ( ( `' F " { k } ) i^i ( A ` n ) ) ) ) , RR* , < ) )
107 90 105 106 syl2anc 
 |-  ( ( ph /\ k e. ( ran F \ { 0 } ) ) -> ( vol ` U. ran ( n e. NN |-> ( ( `' F " { k } ) i^i ( A ` n ) ) ) ) = sup ( ( vol " ran ( n e. NN |-> ( ( `' F " { k } ) i^i ( A ` n ) ) ) ) , RR* , < ) )
108 95 iuneq2i 
 |-  U_ j e. NN ( ( n e. NN |-> ( ( `' F " { k } ) i^i ( A ` n ) ) ) ` j ) = U_ j e. NN ( ( `' F " { k } ) i^i ( A ` j ) )
109 55 cbviunv 
 |-  U_ n e. NN ( ( `' F " { k } ) i^i ( A ` n ) ) = U_ j e. NN ( ( `' F " { k } ) i^i ( A ` j ) )
110 iunin2 
 |-  U_ n e. NN ( ( `' F " { k } ) i^i ( A ` n ) ) = ( ( `' F " { k } ) i^i U_ n e. NN ( A ` n ) )
111 108 109 110 3eqtr2i 
 |-  U_ j e. NN ( ( n e. NN |-> ( ( `' F " { k } ) i^i ( A ` n ) ) ) ` j ) = ( ( `' F " { k } ) i^i U_ n e. NN ( A ` n ) )
112 ffn 
 |-  ( A : NN --> dom vol -> A Fn NN )
113 fniunfv 
 |-  ( A Fn NN -> U_ n e. NN ( A ` n ) = U. ran A )
114 1 112 113 3syl 
 |-  ( ph -> U_ n e. NN ( A ` n ) = U. ran A )
115 114 3 eqtrd 
 |-  ( ph -> U_ n e. NN ( A ` n ) = RR )
116 115 adantr 
 |-  ( ( ph /\ k e. ( ran F \ { 0 } ) ) -> U_ n e. NN ( A ` n ) = RR )
117 116 ineq2d 
 |-  ( ( ph /\ k e. ( ran F \ { 0 } ) ) -> ( ( `' F " { k } ) i^i U_ n e. NN ( A ` n ) ) = ( ( `' F " { k } ) i^i RR ) )
118 15 adantr 
 |-  ( ( ph /\ k e. ( ran F \ { 0 } ) ) -> ( `' F " { k } ) e. dom vol )
119 118 25 syl 
 |-  ( ( ph /\ k e. ( ran F \ { 0 } ) ) -> ( `' F " { k } ) C_ RR )
120 dfss2 
 |-  ( ( `' F " { k } ) C_ RR <-> ( ( `' F " { k } ) i^i RR ) = ( `' F " { k } ) )
121 119 120 sylib 
 |-  ( ( ph /\ k e. ( ran F \ { 0 } ) ) -> ( ( `' F " { k } ) i^i RR ) = ( `' F " { k } ) )
122 117 121 eqtrd 
 |-  ( ( ph /\ k e. ( ran F \ { 0 } ) ) -> ( ( `' F " { k } ) i^i U_ n e. NN ( A ` n ) ) = ( `' F " { k } ) )
123 111 122 eqtrid 
 |-  ( ( ph /\ k e. ( ran F \ { 0 } ) ) -> U_ j e. NN ( ( n e. NN |-> ( ( `' F " { k } ) i^i ( A ` n ) ) ) ` j ) = ( `' F " { k } ) )
124 ffn 
 |-  ( ( n e. NN |-> ( ( `' F " { k } ) i^i ( A ` n ) ) ) : NN --> dom vol -> ( n e. NN |-> ( ( `' F " { k } ) i^i ( A ` n ) ) ) Fn NN )
125 fniunfv 
 |-  ( ( n e. NN |-> ( ( `' F " { k } ) i^i ( A ` n ) ) ) Fn NN -> U_ j e. NN ( ( n e. NN |-> ( ( `' F " { k } ) i^i ( A ` n ) ) ) ` j ) = U. ran ( n e. NN |-> ( ( `' F " { k } ) i^i ( A ` n ) ) ) )
126 90 124 125 3syl 
 |-  ( ( ph /\ k e. ( ran F \ { 0 } ) ) -> U_ j e. NN ( ( n e. NN |-> ( ( `' F " { k } ) i^i ( A ` n ) ) ) ` j ) = U. ran ( n e. NN |-> ( ( `' F " { k } ) i^i ( A ` n ) ) ) )
127 123 126 eqtr3d 
 |-  ( ( ph /\ k e. ( ran F \ { 0 } ) ) -> ( `' F " { k } ) = U. ran ( n e. NN |-> ( ( `' F " { k } ) i^i ( A ` n ) ) ) )
128 127 fveq2d 
 |-  ( ( ph /\ k e. ( ran F \ { 0 } ) ) -> ( vol ` ( `' F " { k } ) ) = ( vol ` U. ran ( n e. NN |-> ( ( `' F " { k } ) i^i ( A ` n ) ) ) ) )
129 36 frnd 
 |-  ( ( ph /\ k e. ( ran F \ { 0 } ) ) -> ran ( n e. NN |-> ( vol ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) ) C_ RR )
130 36 fdmd 
 |-  ( ( ph /\ k e. ( ran F \ { 0 } ) ) -> dom ( n e. NN |-> ( vol ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) ) = NN )
131 1nn 
 |-  1 e. NN
132 ne0i 
 |-  ( 1 e. NN -> NN =/= (/) )
133 131 132 mp1i 
 |-  ( ( ph /\ k e. ( ran F \ { 0 } ) ) -> NN =/= (/) )
134 130 133 eqnetrd 
 |-  ( ( ph /\ k e. ( ran F \ { 0 } ) ) -> dom ( n e. NN |-> ( vol ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) ) =/= (/) )
135 dm0rn0 
 |-  ( dom ( n e. NN |-> ( vol ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) ) = (/) <-> ran ( n e. NN |-> ( vol ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) ) = (/) )
136 135 necon3bii 
 |-  ( dom ( n e. NN |-> ( vol ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) ) =/= (/) <-> ran ( n e. NN |-> ( vol ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) ) =/= (/) )
137 134 136 sylib 
 |-  ( ( ph /\ k e. ( ran F \ { 0 } ) ) -> ran ( n e. NN |-> ( vol ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) ) =/= (/) )
138 ffn 
 |-  ( ( n e. NN |-> ( vol ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) ) : NN --> RR -> ( n e. NN |-> ( vol ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) ) Fn NN )
139 breq1 
 |-  ( z = ( ( n e. NN |-> ( vol ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) ) ` j ) -> ( z <_ x <-> ( ( n e. NN |-> ( vol ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) ) ` j ) <_ x ) )
140 139 ralrn 
 |-  ( ( n e. NN |-> ( vol ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) ) Fn NN -> ( A. z e. ran ( n e. NN |-> ( vol ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) ) z <_ x <-> A. j e. NN ( ( n e. NN |-> ( vol ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) ) ` j ) <_ x ) )
141 36 138 140 3syl 
 |-  ( ( ph /\ k e. ( ran F \ { 0 } ) ) -> ( A. z e. ran ( n e. NN |-> ( vol ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) ) z <_ x <-> A. j e. NN ( ( n e. NN |-> ( vol ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) ) ` j ) <_ x ) )
142 141 rexbidv 
 |-  ( ( ph /\ k e. ( ran F \ { 0 } ) ) -> ( E. x e. RR A. z e. ran ( n e. NN |-> ( vol ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) ) z <_ x <-> E. x e. RR A. j e. NN ( ( n e. NN |-> ( vol ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) ) ` j ) <_ x ) )
143 88 142 mpbird 
 |-  ( ( ph /\ k e. ( ran F \ { 0 } ) ) -> E. x e. RR A. z e. ran ( n e. NN |-> ( vol ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) ) z <_ x )
144 supxrre 
 |-  ( ( ran ( n e. NN |-> ( vol ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) ) C_ RR /\ ran ( n e. NN |-> ( vol ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) ) =/= (/) /\ E. x e. RR A. z e. ran ( n e. NN |-> ( vol ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) ) z <_ x ) -> sup ( ran ( n e. NN |-> ( vol ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) ) , RR* , < ) = sup ( ran ( n e. NN |-> ( vol ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) ) , RR , < ) )
145 129 137 143 144 syl3anc 
 |-  ( ( ph /\ k e. ( ran F \ { 0 } ) ) -> sup ( ran ( n e. NN |-> ( vol ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) ) , RR* , < ) = sup ( ran ( n e. NN |-> ( vol ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) ) , RR , < ) )
146 volf 
 |-  vol : dom vol --> ( 0 [,] +oo )
147 146 a1i 
 |-  ( ( ph /\ k e. ( ran F \ { 0 } ) ) -> vol : dom vol --> ( 0 [,] +oo ) )
148 147 20 cofmpt 
 |-  ( ( ph /\ k e. ( ran F \ { 0 } ) ) -> ( vol o. ( n e. NN |-> ( ( `' F " { k } ) i^i ( A ` n ) ) ) ) = ( n e. NN |-> ( vol ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) ) )
149 148 rneqd 
 |-  ( ( ph /\ k e. ( ran F \ { 0 } ) ) -> ran ( vol o. ( n e. NN |-> ( ( `' F " { k } ) i^i ( A ` n ) ) ) ) = ran ( n e. NN |-> ( vol ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) ) )
150 rnco2 
 |-  ran ( vol o. ( n e. NN |-> ( ( `' F " { k } ) i^i ( A ` n ) ) ) ) = ( vol " ran ( n e. NN |-> ( ( `' F " { k } ) i^i ( A ` n ) ) ) )
151 149 150 eqtr3di 
 |-  ( ( ph /\ k e. ( ran F \ { 0 } ) ) -> ran ( n e. NN |-> ( vol ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) ) = ( vol " ran ( n e. NN |-> ( ( `' F " { k } ) i^i ( A ` n ) ) ) ) )
152 151 supeq1d 
 |-  ( ( ph /\ k e. ( ran F \ { 0 } ) ) -> sup ( ran ( n e. NN |-> ( vol ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) ) , RR* , < ) = sup ( ( vol " ran ( n e. NN |-> ( ( `' F " { k } ) i^i ( A ` n ) ) ) ) , RR* , < ) )
153 145 152 eqtr3d 
 |-  ( ( ph /\ k e. ( ran F \ { 0 } ) ) -> sup ( ran ( n e. NN |-> ( vol ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) ) , RR , < ) = sup ( ( vol " ran ( n e. NN |-> ( ( `' F " { k } ) i^i ( A ` n ) ) ) ) , RR* , < ) )
154 107 128 153 3eqtr4d 
 |-  ( ( ph /\ k e. ( ran F \ { 0 } ) ) -> ( vol ` ( `' F " { k } ) ) = sup ( ran ( n e. NN |-> ( vol ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) ) , RR , < ) )
155 89 154 breqtrrd 
 |-  ( ( ph /\ k e. ( ran F \ { 0 } ) ) -> ( n e. NN |-> ( vol ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) ) ~~> ( vol ` ( `' F " { k } ) ) )
156 i1ff 
 |-  ( F e. dom S.1 -> F : RR --> RR )
157 frn 
 |-  ( F : RR --> RR -> ran F C_ RR )
158 4 156 157 3syl 
 |-  ( ph -> ran F C_ RR )
159 158 ssdifssd 
 |-  ( ph -> ( ran F \ { 0 } ) C_ RR )
160 159 sselda 
 |-  ( ( ph /\ k e. ( ran F \ { 0 } ) ) -> k e. RR )
161 160 recnd 
 |-  ( ( ph /\ k e. ( ran F \ { 0 } ) ) -> k e. CC )
162 nnex 
 |-  NN e. _V
163 162 mptex 
 |-  ( n e. NN |-> ( k x. ( vol ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) ) ) e. _V
164 163 a1i 
 |-  ( ( ph /\ k e. ( ran F \ { 0 } ) ) -> ( n e. NN |-> ( k x. ( vol ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) ) ) e. _V )
165 36 ffvelcdmda 
 |-  ( ( ( ph /\ k e. ( ran F \ { 0 } ) ) /\ j e. NN ) -> ( ( n e. NN |-> ( vol ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) ) ` j ) e. RR )
166 165 recnd 
 |-  ( ( ( ph /\ k e. ( ran F \ { 0 } ) ) /\ j e. NN ) -> ( ( n e. NN |-> ( vol ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) ) ` j ) e. CC )
167 56 oveq2d 
 |-  ( n = j -> ( k x. ( vol ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) ) = ( k x. ( vol ` ( ( `' F " { k } ) i^i ( A ` j ) ) ) ) )
168 eqid 
 |-  ( n e. NN |-> ( k x. ( vol ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) ) ) = ( n e. NN |-> ( k x. ( vol ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) ) )
169 ovex 
 |-  ( k x. ( vol ` ( ( `' F " { k } ) i^i ( A ` j ) ) ) ) e. _V
170 167 168 169 fvmpt 
 |-  ( j e. NN -> ( ( n e. NN |-> ( k x. ( vol ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) ) ) ` j ) = ( k x. ( vol ` ( ( `' F " { k } ) i^i ( A ` j ) ) ) ) )
171 59 oveq2d 
 |-  ( j e. NN -> ( k x. ( ( n e. NN |-> ( vol ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) ) ` j ) ) = ( k x. ( vol ` ( ( `' F " { k } ) i^i ( A ` j ) ) ) ) )
172 170 171 eqtr4d 
 |-  ( j e. NN -> ( ( n e. NN |-> ( k x. ( vol ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) ) ) ` j ) = ( k x. ( ( n e. NN |-> ( vol ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) ) ` j ) ) )
173 172 adantl 
 |-  ( ( ( ph /\ k e. ( ran F \ { 0 } ) ) /\ j e. NN ) -> ( ( n e. NN |-> ( k x. ( vol ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) ) ) ` j ) = ( k x. ( ( n e. NN |-> ( vol ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) ) ` j ) ) )
174 6 13 155 161 164 166 173 climmulc2 
 |-  ( ( ph /\ k e. ( ran F \ { 0 } ) ) -> ( n e. NN |-> ( k x. ( vol ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) ) ) ~~> ( k x. ( vol ` ( `' F " { k } ) ) ) )
175 162 mptex 
 |-  ( n e. NN |-> ( S.1 ` G ) ) e. _V
176 175 a1i 
 |-  ( ph -> ( n e. NN |-> ( S.1 ` G ) ) e. _V )
177 160 adantr 
 |-  ( ( ( ph /\ k e. ( ran F \ { 0 } ) ) /\ n e. NN ) -> k e. RR )
178 177 35 remulcld 
 |-  ( ( ( ph /\ k e. ( ran F \ { 0 } ) ) /\ n e. NN ) -> ( k x. ( vol ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) ) e. RR )
179 178 fmpttd 
 |-  ( ( ph /\ k e. ( ran F \ { 0 } ) ) -> ( n e. NN |-> ( k x. ( vol ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) ) ) : NN --> RR )
180 179 ffvelcdmda 
 |-  ( ( ( ph /\ k e. ( ran F \ { 0 } ) ) /\ j e. NN ) -> ( ( n e. NN |-> ( k x. ( vol ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) ) ) ` j ) e. RR )
181 180 recnd 
 |-  ( ( ( ph /\ k e. ( ran F \ { 0 } ) ) /\ j e. NN ) -> ( ( n e. NN |-> ( k x. ( vol ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) ) ) ` j ) e. CC )
182 181 anasss 
 |-  ( ( ph /\ ( k e. ( ran F \ { 0 } ) /\ j e. NN ) ) -> ( ( n e. NN |-> ( k x. ( vol ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) ) ) ` j ) e. CC )
183 4 adantr 
 |-  ( ( ph /\ n e. NN ) -> F e. dom S.1 )
184 5 i1fres 
 |-  ( ( F e. dom S.1 /\ ( A ` n ) e. dom vol ) -> G e. dom S.1 )
185 183 17 184 syl2anc 
 |-  ( ( ph /\ n e. NN ) -> G e. dom S.1 )
186 12 adantr 
 |-  ( ( ph /\ n e. NN ) -> ( ran F \ { 0 } ) e. Fin )
187 ffn 
 |-  ( F : RR --> RR -> F Fn RR )
188 4 156 187 3syl 
 |-  ( ph -> F Fn RR )
189 188 adantr 
 |-  ( ( ph /\ n e. NN ) -> F Fn RR )
190 fnfvelrn 
 |-  ( ( F Fn RR /\ x e. RR ) -> ( F ` x ) e. ran F )
191 189 190 sylan 
 |-  ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( F ` x ) e. ran F )
192 i1f0rn 
 |-  ( F e. dom S.1 -> 0 e. ran F )
193 4 192 syl 
 |-  ( ph -> 0 e. ran F )
194 193 ad2antrr 
 |-  ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> 0 e. ran F )
195 191 194 ifcld 
 |-  ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> if ( x e. ( A ` n ) , ( F ` x ) , 0 ) e. ran F )
196 195 5 fmptd 
 |-  ( ( ph /\ n e. NN ) -> G : RR --> ran F )
197 frn 
 |-  ( G : RR --> ran F -> ran G C_ ran F )
198 ssdif 
 |-  ( ran G C_ ran F -> ( ran G \ { 0 } ) C_ ( ran F \ { 0 } ) )
199 196 197 198 3syl 
 |-  ( ( ph /\ n e. NN ) -> ( ran G \ { 0 } ) C_ ( ran F \ { 0 } ) )
200 158 adantr 
 |-  ( ( ph /\ n e. NN ) -> ran F C_ RR )
201 200 ssdifd 
 |-  ( ( ph /\ n e. NN ) -> ( ran F \ { 0 } ) C_ ( RR \ { 0 } ) )
202 itg1val2 
 |-  ( ( G e. dom S.1 /\ ( ( ran F \ { 0 } ) e. Fin /\ ( ran G \ { 0 } ) C_ ( ran F \ { 0 } ) /\ ( ran F \ { 0 } ) C_ ( RR \ { 0 } ) ) ) -> ( S.1 ` G ) = sum_ k e. ( ran F \ { 0 } ) ( k x. ( vol ` ( `' G " { k } ) ) ) )
203 185 186 199 201 202 syl13anc 
 |-  ( ( ph /\ n e. NN ) -> ( S.1 ` G ) = sum_ k e. ( ran F \ { 0 } ) ( k x. ( vol ` ( `' G " { k } ) ) ) )
204 fvex 
 |-  ( F ` x ) e. _V
205 c0ex 
 |-  0 e. _V
206 204 205 ifex 
 |-  if ( x e. ( A ` n ) , ( F ` x ) , 0 ) e. _V
207 5 fvmpt2 
 |-  ( ( x e. RR /\ if ( x e. ( A ` n ) , ( F ` x ) , 0 ) e. _V ) -> ( G ` x ) = if ( x e. ( A ` n ) , ( F ` x ) , 0 ) )
208 206 207 mpan2 
 |-  ( x e. RR -> ( G ` x ) = if ( x e. ( A ` n ) , ( F ` x ) , 0 ) )
209 208 adantl 
 |-  ( ( ( ( ph /\ n e. NN ) /\ k e. ( ran F \ { 0 } ) ) /\ x e. RR ) -> ( G ` x ) = if ( x e. ( A ` n ) , ( F ` x ) , 0 ) )
210 209 eqeq1d 
 |-  ( ( ( ( ph /\ n e. NN ) /\ k e. ( ran F \ { 0 } ) ) /\ x e. RR ) -> ( ( G ` x ) = k <-> if ( x e. ( A ` n ) , ( F ` x ) , 0 ) = k ) )
211 eldifsni 
 |-  ( k e. ( ran F \ { 0 } ) -> k =/= 0 )
212 211 ad2antlr 
 |-  ( ( ( ( ph /\ n e. NN ) /\ k e. ( ran F \ { 0 } ) ) /\ x e. RR ) -> k =/= 0 )
213 neeq1 
 |-  ( if ( x e. ( A ` n ) , ( F ` x ) , 0 ) = k -> ( if ( x e. ( A ` n ) , ( F ` x ) , 0 ) =/= 0 <-> k =/= 0 ) )
214 212 213 syl5ibrcom 
 |-  ( ( ( ( ph /\ n e. NN ) /\ k e. ( ran F \ { 0 } ) ) /\ x e. RR ) -> ( if ( x e. ( A ` n ) , ( F ` x ) , 0 ) = k -> if ( x e. ( A ` n ) , ( F ` x ) , 0 ) =/= 0 ) )
215 iffalse 
 |-  ( -. x e. ( A ` n ) -> if ( x e. ( A ` n ) , ( F ` x ) , 0 ) = 0 )
216 215 necon1ai 
 |-  ( if ( x e. ( A ` n ) , ( F ` x ) , 0 ) =/= 0 -> x e. ( A ` n ) )
217 214 216 syl6 
 |-  ( ( ( ( ph /\ n e. NN ) /\ k e. ( ran F \ { 0 } ) ) /\ x e. RR ) -> ( if ( x e. ( A ` n ) , ( F ` x ) , 0 ) = k -> x e. ( A ` n ) ) )
218 217 pm4.71rd 
 |-  ( ( ( ( ph /\ n e. NN ) /\ k e. ( ran F \ { 0 } ) ) /\ x e. RR ) -> ( if ( x e. ( A ` n ) , ( F ` x ) , 0 ) = k <-> ( x e. ( A ` n ) /\ if ( x e. ( A ` n ) , ( F ` x ) , 0 ) = k ) ) )
219 210 218 bitrd 
 |-  ( ( ( ( ph /\ n e. NN ) /\ k e. ( ran F \ { 0 } ) ) /\ x e. RR ) -> ( ( G ` x ) = k <-> ( x e. ( A ` n ) /\ if ( x e. ( A ` n ) , ( F ` x ) , 0 ) = k ) ) )
220 iftrue 
 |-  ( x e. ( A ` n ) -> if ( x e. ( A ` n ) , ( F ` x ) , 0 ) = ( F ` x ) )
221 220 eqeq1d 
 |-  ( x e. ( A ` n ) -> ( if ( x e. ( A ` n ) , ( F ` x ) , 0 ) = k <-> ( F ` x ) = k ) )
222 221 pm5.32i 
 |-  ( ( x e. ( A ` n ) /\ if ( x e. ( A ` n ) , ( F ` x ) , 0 ) = k ) <-> ( x e. ( A ` n ) /\ ( F ` x ) = k ) )
223 222 biancomi 
 |-  ( ( x e. ( A ` n ) /\ if ( x e. ( A ` n ) , ( F ` x ) , 0 ) = k ) <-> ( ( F ` x ) = k /\ x e. ( A ` n ) ) )
224 219 223 bitrdi 
 |-  ( ( ( ( ph /\ n e. NN ) /\ k e. ( ran F \ { 0 } ) ) /\ x e. RR ) -> ( ( G ` x ) = k <-> ( ( F ` x ) = k /\ x e. ( A ` n ) ) ) )
225 224 pm5.32da 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( ran F \ { 0 } ) ) -> ( ( x e. RR /\ ( G ` x ) = k ) <-> ( x e. RR /\ ( ( F ` x ) = k /\ x e. ( A ` n ) ) ) ) )
226 anass 
 |-  ( ( ( x e. RR /\ ( F ` x ) = k ) /\ x e. ( A ` n ) ) <-> ( x e. RR /\ ( ( F ` x ) = k /\ x e. ( A ` n ) ) ) )
227 225 226 bitr4di 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( ran F \ { 0 } ) ) -> ( ( x e. RR /\ ( G ` x ) = k ) <-> ( ( x e. RR /\ ( F ` x ) = k ) /\ x e. ( A ` n ) ) ) )
228 i1ff 
 |-  ( G e. dom S.1 -> G : RR --> RR )
229 ffn 
 |-  ( G : RR --> RR -> G Fn RR )
230 185 228 229 3syl 
 |-  ( ( ph /\ n e. NN ) -> G Fn RR )
231 230 adantr 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( ran F \ { 0 } ) ) -> G Fn RR )
232 fniniseg 
 |-  ( G Fn RR -> ( x e. ( `' G " { k } ) <-> ( x e. RR /\ ( G ` x ) = k ) ) )
233 231 232 syl 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( ran F \ { 0 } ) ) -> ( x e. ( `' G " { k } ) <-> ( x e. RR /\ ( G ` x ) = k ) ) )
234 elin 
 |-  ( x e. ( ( `' F " { k } ) i^i ( A ` n ) ) <-> ( x e. ( `' F " { k } ) /\ x e. ( A ` n ) ) )
235 189 adantr 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( ran F \ { 0 } ) ) -> F Fn RR )
236 fniniseg 
 |-  ( F Fn RR -> ( x e. ( `' F " { k } ) <-> ( x e. RR /\ ( F ` x ) = k ) ) )
237 235 236 syl 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( ran F \ { 0 } ) ) -> ( x e. ( `' F " { k } ) <-> ( x e. RR /\ ( F ` x ) = k ) ) )
238 237 anbi1d 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( ran F \ { 0 } ) ) -> ( ( x e. ( `' F " { k } ) /\ x e. ( A ` n ) ) <-> ( ( x e. RR /\ ( F ` x ) = k ) /\ x e. ( A ` n ) ) ) )
239 234 238 bitrid 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( ran F \ { 0 } ) ) -> ( x e. ( ( `' F " { k } ) i^i ( A ` n ) ) <-> ( ( x e. RR /\ ( F ` x ) = k ) /\ x e. ( A ` n ) ) ) )
240 227 233 239 3bitr4d 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( ran F \ { 0 } ) ) -> ( x e. ( `' G " { k } ) <-> x e. ( ( `' F " { k } ) i^i ( A ` n ) ) ) )
241 240 alrimiv 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( ran F \ { 0 } ) ) -> A. x ( x e. ( `' G " { k } ) <-> x e. ( ( `' F " { k } ) i^i ( A ` n ) ) ) )
242 nfmpt1 
 |-  F/_ x ( x e. RR |-> if ( x e. ( A ` n ) , ( F ` x ) , 0 ) )
243 5 242 nfcxfr 
 |-  F/_ x G
244 243 nfcnv 
 |-  F/_ x `' G
245 nfcv 
 |-  F/_ x { k }
246 244 245 nfima 
 |-  F/_ x ( `' G " { k } )
247 nfcv 
 |-  F/_ x ( ( `' F " { k } ) i^i ( A ` n ) )
248 246 247 cleqf 
 |-  ( ( `' G " { k } ) = ( ( `' F " { k } ) i^i ( A ` n ) ) <-> A. x ( x e. ( `' G " { k } ) <-> x e. ( ( `' F " { k } ) i^i ( A ` n ) ) ) )
249 241 248 sylibr 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( ran F \ { 0 } ) ) -> ( `' G " { k } ) = ( ( `' F " { k } ) i^i ( A ` n ) ) )
250 249 fveq2d 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( ran F \ { 0 } ) ) -> ( vol ` ( `' G " { k } ) ) = ( vol ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) )
251 250 oveq2d 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( ran F \ { 0 } ) ) -> ( k x. ( vol ` ( `' G " { k } ) ) ) = ( k x. ( vol ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) ) )
252 251 sumeq2dv 
 |-  ( ( ph /\ n e. NN ) -> sum_ k e. ( ran F \ { 0 } ) ( k x. ( vol ` ( `' G " { k } ) ) ) = sum_ k e. ( ran F \ { 0 } ) ( k x. ( vol ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) ) )
253 203 252 eqtrd 
 |-  ( ( ph /\ n e. NN ) -> ( S.1 ` G ) = sum_ k e. ( ran F \ { 0 } ) ( k x. ( vol ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) ) )
254 253 mpteq2dva 
 |-  ( ph -> ( n e. NN |-> ( S.1 ` G ) ) = ( n e. NN |-> sum_ k e. ( ran F \ { 0 } ) ( k x. ( vol ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) ) ) )
255 254 fveq1d 
 |-  ( ph -> ( ( n e. NN |-> ( S.1 ` G ) ) ` j ) = ( ( n e. NN |-> sum_ k e. ( ran F \ { 0 } ) ( k x. ( vol ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) ) ) ` j ) )
256 167 sumeq2sdv 
 |-  ( n = j -> sum_ k e. ( ran F \ { 0 } ) ( k x. ( vol ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) ) = sum_ k e. ( ran F \ { 0 } ) ( k x. ( vol ` ( ( `' F " { k } ) i^i ( A ` j ) ) ) ) )
257 eqid 
 |-  ( n e. NN |-> sum_ k e. ( ran F \ { 0 } ) ( k x. ( vol ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) ) ) = ( n e. NN |-> sum_ k e. ( ran F \ { 0 } ) ( k x. ( vol ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) ) )
258 sumex 
 |-  sum_ k e. ( ran F \ { 0 } ) ( k x. ( vol ` ( ( `' F " { k } ) i^i ( A ` j ) ) ) ) e. _V
259 256 257 258 fvmpt 
 |-  ( j e. NN -> ( ( n e. NN |-> sum_ k e. ( ran F \ { 0 } ) ( k x. ( vol ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) ) ) ` j ) = sum_ k e. ( ran F \ { 0 } ) ( k x. ( vol ` ( ( `' F " { k } ) i^i ( A ` j ) ) ) ) )
260 170 sumeq2sdv 
 |-  ( j e. NN -> sum_ k e. ( ran F \ { 0 } ) ( ( n e. NN |-> ( k x. ( vol ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) ) ) ` j ) = sum_ k e. ( ran F \ { 0 } ) ( k x. ( vol ` ( ( `' F " { k } ) i^i ( A ` j ) ) ) ) )
261 259 260 eqtr4d 
 |-  ( j e. NN -> ( ( n e. NN |-> sum_ k e. ( ran F \ { 0 } ) ( k x. ( vol ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) ) ) ` j ) = sum_ k e. ( ran F \ { 0 } ) ( ( n e. NN |-> ( k x. ( vol ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) ) ) ` j ) )
262 255 261 sylan9eq 
 |-  ( ( ph /\ j e. NN ) -> ( ( n e. NN |-> ( S.1 ` G ) ) ` j ) = sum_ k e. ( ran F \ { 0 } ) ( ( n e. NN |-> ( k x. ( vol ` ( ( `' F " { k } ) i^i ( A ` n ) ) ) ) ) ` j ) )
263 6 7 12 174 176 182 262 climfsum 
 |-  ( ph -> ( n e. NN |-> ( S.1 ` G ) ) ~~> sum_ k e. ( ran F \ { 0 } ) ( k x. ( vol ` ( `' F " { k } ) ) ) )
264 itg1val 
 |-  ( F e. dom S.1 -> ( S.1 ` F ) = sum_ k e. ( ran F \ { 0 } ) ( k x. ( vol ` ( `' F " { k } ) ) ) )
265 4 264 syl 
 |-  ( ph -> ( S.1 ` F ) = sum_ k e. ( ran F \ { 0 } ) ( k x. ( vol ` ( `' F " { k } ) ) ) )
266 263 265 breqtrrd 
 |-  ( ph -> ( n e. NN |-> ( S.1 ` G ) ) ~~> ( S.1 ` F ) )