Theorem imasval 15125

Description: Value of an image structure. (Contributed by Mario Carneiro, 23-Feb-2015.) (Revised by Mario Carneiro, 11-Jul-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.)

Hypotheses

Ref	Expression
imasval.u	|- ( ph -> U = ( F "s R ) )
imasval.v	|- ( ph -> V = ( Base ` R ) )
imasval.p	|- .+ = ( +g ` R )
imasval.m	|- .X. = ( .r ` R )
imasval.g	|- G = (Scalar ` R )
imasval.k	|- K = ( Base ` G )
imasval.q	|- .x. = ( .s ` R )
imasval.i	|- ., = ( .i ` R )
imasval.j	|- J = ( TopOpen ` R )
imasval.e	|- E = ( dist ` R )
imasval.n	|- N = ( le ` R )
imasval.a	|- ( ph -> .+b = U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .+ q ) ) >. } )
imasval.t	|- ( ph -> .xb = U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .X. q ) ) >. } )
imasval.s	|- ( ph -> .(x) = U_ q e. V ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) )
imasval.w	|- ( ph -> I = U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( p ., q ) >. } )
imasval.o	|- ( ph -> O = ( J qTop F ) )
imasval.d	|- ( ph -> D = ( x e. B , y e. B |-> sup ( U_ n e. NN ran ( g e. { h e. ( ( V X. V ) ^m ( 1 ... n ) ) | ( ( F ` ( 1st ` ( h ` 1 ) ) ) = x /\ ( F ` ( 2nd ` ( h ` n ) ) ) = y /\ A. i e. ( 1 ... ( n - 1 ) ) ( F ` ( 2nd ` ( h ` i ) ) ) = ( F ` ( 1st ` ( h ` ( i + 1 ) ) ) ) ) } |-> ( RR*s gsumg ( E o. g ) ) ) , RR* , `' < ) ) )
imasval.l	|- ( ph -> .<_ = ( ( F o. N ) o. `' F ) )
imasval.f	|- ( ph -> F : V -onto-> B )
imasval.r	|- ( ph -> R e. Z )

Assertion

Ref	Expression
imasval	|- ( ph -> U = ( ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+b >. , <. ( .r ` ndx ) , .xb >. } u. { <. (Scalar ` ndx ) , G >. , <. ( .s ` ndx ) , .(x) >. , <. ( .i ` ndx ) , I >. } ) u. { <. (TopSet ` ndx ) , O >. , <. ( le ` ndx ) , .<_ >. , <. ( dist ` ndx ) , D >. } ) )

Distinct variable groups:   g, h, i, n, p, q, x, y, F   R, g, h, i, n, p, q, x, y   h, V, p, q   ph, g, h, i, n, p, q, x, y

Allowed substitution hints:   B( x, y, g, h, i, n, q, p)   D( x, y, g, h, i, n, q, p)   .+ ( x, y, g, h, i, n, q, p)   .+b ( x, y, g, h, i, n, q, p)   .xb ( x, y, g, h, i, n, q, p)   .x. ( x, y, g, h, i, n, q, p)   .X. ( x, y, g, h, i, n, q, p)   .(x) ( x, y, g, h, i, n, q, p)   U( x, y, g, h, i, n, q, p)   E( x, y, g, h, i, n, q, p)   G( x, y, g, h, i, n, q, p)   ., ( x, y, g, h, i, n, q, p)   I( x, y, g, h, i, n, q, p)   J( x, y, g, h, i, n, q, p)   K( x, y, g, h, i, n, q, p)   .<_ ( x, y, g, h, i, n, q, p)   N( x, y, g, h, i, n, q, p)   O( x, y, g, h, i, n, q, p)   V( x, y, g, i, n)   Z( x, y, g, h, i, n, q, p)

Proof of Theorem imasval

Dummy variables f r v are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		imasval.u	. 2 |- ( ph -> U = ( F "s R ) )
2		df-imas 15122	. . . 4 |- "s = ( f e. _V , r e. _V |-> [_ ( Base ` r ) / v ]_ ( ( { <. ( Base ` ndx ) , ran f >. , <. ( +g ` ndx ) , U_ p e. v U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( +g ` r ) q ) ) >. } >. , <. ( .r ` ndx ) , U_ p e. v U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( .r ` r ) q ) ) >. } >. } u. { <. (Scalar ` ndx ) , (Scalar ` r ) >. , <. ( .s ` ndx ) , U_ q e. v ( p e. ( Base ` (Scalar ` r ) ) , x e. { ( f ` q ) } |-> ( f ` ( p ( .s ` r ) q ) ) ) >. , <. ( .i ` ndx ) , U_ p e. v U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( p ( .i ` r ) q ) >. } >. } ) u. { <. (TopSet ` ndx ) , ( ( TopOpen ` r ) qTop f ) >. , <. ( le ` ndx ) , ( ( f o. ( le ` r ) ) o. `' f ) >. , <. ( dist ` ndx ) , ( x e. ran f , y e. ran f |-> sup ( U_ n e. NN ran ( g e. { h e. ( ( v X. v ) ^m ( 1 ... n ) ) | ( ( f ` ( 1st ` ( h ` 1 ) ) ) = x /\ ( f ` ( 2nd ` ( h ` n ) ) ) = y /\ A. i e. ( 1 ... ( n - 1 ) ) ( f ` ( 2nd ` ( h ` i ) ) ) = ( f ` ( 1st ` ( h ` ( i + 1 ) ) ) ) ) } |-> ( RR*s gsumg ( ( dist ` r ) o. g ) ) ) , RR* , `' < ) ) >. } ) )
3	2	a1i 11	. . 3 |- ( ph -> "s = ( f e. _V , r e. _V |-> [_ ( Base ` r ) / v ]_ ( ( { <. ( Base ` ndx ) , ran f >. , <. ( +g ` ndx ) , U_ p e. v U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( +g ` r ) q ) ) >. } >. , <. ( .r ` ndx ) , U_ p e. v U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( .r ` r ) q ) ) >. } >. } u. { <. (Scalar ` ndx ) , (Scalar ` r ) >. , <. ( .s ` ndx ) , U_ q e. v ( p e. ( Base ` (Scalar ` r ) ) , x e. { ( f ` q ) } |-> ( f ` ( p ( .s ` r ) q ) ) ) >. , <. ( .i ` ndx ) , U_ p e. v U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( p ( .i ` r ) q ) >. } >. } ) u. { <. (TopSet ` ndx ) , ( ( TopOpen ` r ) qTop f ) >. , <. ( le ` ndx ) , ( ( f o. ( le ` r ) ) o. `' f ) >. , <. ( dist ` ndx ) , ( x e. ran f , y e. ran f |-> sup ( U_ n e. NN ran ( g e. { h e. ( ( v X. v ) ^m ( 1 ... n ) ) | ( ( f ` ( 1st ` ( h ` 1 ) ) ) = x /\ ( f ` ( 2nd ` ( h ` n ) ) ) = y /\ A. i e. ( 1 ... ( n - 1 ) ) ( f ` ( 2nd ` ( h ` i ) ) ) = ( f ` ( 1st ` ( h ` ( i + 1 ) ) ) ) ) } |-> ( RR*s gsumg ( ( dist ` r ) o. g ) ) ) , RR* , `' < ) ) >. } ) ) )
4		fvex 5859	. . . . 5 |- ( Base ` r ) e. _V
5	4	a1i 11	. . . 4 |- ( ( ph /\ ( f = F /\ r = R ) ) -> ( Base ` r ) e. _V )
6		simplrl 762	. . . . . . . . . 10 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> f = F )
7	6	rneqd 5051	. . . . . . . . 9 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ran f = ran F )
8		imasval.f	. . . . . . . . . . 11 |- ( ph -> F : V -onto-> B )
9		forn 5781	. . . . . . . . . . 11 |- ( F : V -onto-> B -> ran F = B )
10	8, 9	syl 17	. . . . . . . . . 10 |- ( ph -> ran F = B )
11	10	ad2antrr 724	. . . . . . . . 9 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ran F = B )
12	7, 11	eqtrd 2443	. . . . . . . 8 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ran f = B )
13	12	opeq2d 4166	. . . . . . 7 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> <. ( Base ` ndx ) , ran f >. = <. ( Base ` ndx ) , B >. )
14		simplrr 763	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> r = R )
15	14	fveq2d 5853	. . . . . . . . . . 11 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( Base ` r ) = ( Base ` R ) )
16		simpr 459	. . . . . . . . . . 11 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> v = ( Base ` r ) )
17		imasval.v	. . . . . . . . . . . 12 |- ( ph -> V = ( Base ` R ) )
18	17	ad2antrr 724	. . . . . . . . . . 11 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> V = ( Base ` R ) )
19	15, 16, 18	3eqtr4d 2453	. . . . . . . . . 10 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> v = V )
20	6	fveq1d 5851	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( f ` p ) = ( F ` p ) )
21	6	fveq1d 5851	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( f ` q ) = ( F ` q ) )
22	20, 21	opeq12d 4167	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> <. ( f ` p ) , ( f ` q ) >. = <. ( F ` p ) , ( F ` q ) >. )
23	14	fveq2d 5853	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( +g ` r ) = ( +g ` R ) )
24		imasval.p	. . . . . . . . . . . . . . . 16 |- .+ = ( +g ` R )
25	23, 24	syl6eqr 2461	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( +g ` r ) = .+ )
26	25	oveqd 6295	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( p ( +g ` r ) q ) = ( p .+ q ) )
27	6, 26	fveq12d 5855	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( f ` ( p ( +g ` r ) q ) ) = ( F ` ( p .+ q ) ) )
28	22, 27	opeq12d 4167	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( +g ` r ) q ) ) >. = <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .+ q ) ) >. )
29	28	sneqd 3984	. . . . . . . . . . 11 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( +g ` r ) q ) ) >. } = { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .+ q ) ) >. } )
30	19, 29	iuneq12d 4297	. . . . . . . . . 10 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( +g ` r ) q ) ) >. } = U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .+ q ) ) >. } )
31	19, 30	iuneq12d 4297	. . . . . . . . 9 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> U_ p e. v U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( +g ` r ) q ) ) >. } = U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .+ q ) ) >. } )
32		imasval.a	. . . . . . . . . 10 |- ( ph -> .+b = U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .+ q ) ) >. } )
33	32	ad2antrr 724	. . . . . . . . 9 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> .+b = U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .+ q ) ) >. } )
34	31, 33	eqtr4d 2446	. . . . . . . 8 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> U_ p e. v U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( +g ` r ) q ) ) >. } = .+b )
35	34	opeq2d 4166	. . . . . . 7 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> <. ( +g ` ndx ) , U_ p e. v U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( +g ` r ) q ) ) >. } >. = <. ( +g ` ndx ) , .+b >. )
36	14	fveq2d 5853	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( .r ` r ) = ( .r ` R ) )
37		imasval.m	. . . . . . . . . . . . . . . 16 |- .X. = ( .r ` R )
38	36, 37	syl6eqr 2461	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( .r ` r ) = .X. )
39	38	oveqd 6295	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( p ( .r ` r ) q ) = ( p .X. q ) )
40	6, 39	fveq12d 5855	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( f ` ( p ( .r ` r ) q ) ) = ( F ` ( p .X. q ) ) )
41	22, 40	opeq12d 4167	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( .r ` r ) q ) ) >. = <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .X. q ) ) >. )
42	41	sneqd 3984	. . . . . . . . . . 11 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( .r ` r ) q ) ) >. } = { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .X. q ) ) >. } )
43	19, 42	iuneq12d 4297	. . . . . . . . . 10 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( .r ` r ) q ) ) >. } = U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .X. q ) ) >. } )
44	19, 43	iuneq12d 4297	. . . . . . . . 9 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> U_ p e. v U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( .r ` r ) q ) ) >. } = U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .X. q ) ) >. } )
45		imasval.t	. . . . . . . . . 10 |- ( ph -> .xb = U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .X. q ) ) >. } )
46	45	ad2antrr 724	. . . . . . . . 9 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> .xb = U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .X. q ) ) >. } )
47	44, 46	eqtr4d 2446	. . . . . . . 8 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> U_ p e. v U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( .r ` r ) q ) ) >. } = .xb )
48	47	opeq2d 4166	. . . . . . 7 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> <. ( .r ` ndx ) , U_ p e. v U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( .r ` r ) q ) ) >. } >. = <. ( .r ` ndx ) , .xb >. )
49	13, 35, 48	tpeq123d 4066	. . . . . 6 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> { <. ( Base ` ndx ) , ran f >. , <. ( +g ` ndx ) , U_ p e. v U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( +g ` r ) q ) ) >. } >. , <. ( .r ` ndx ) , U_ p e. v U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( .r ` r ) q ) ) >. } >. } = { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+b >. , <. ( .r ` ndx ) , .xb >. } )
50	14	fveq2d 5853	. . . . . . . . 9 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> (Scalar ` r ) = (Scalar ` R ) )
51		imasval.g	. . . . . . . . 9 |- G = (Scalar ` R )
52	50, 51	syl6eqr 2461	. . . . . . . 8 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> (Scalar ` r ) = G )
53	52	opeq2d 4166	. . . . . . 7 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> <. (Scalar ` ndx ) , (Scalar ` r ) >. = <. (Scalar ` ndx ) , G >. )
54	52	fveq2d 5853	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( Base ` (Scalar ` r ) ) = ( Base ` G ) )
55		imasval.k	. . . . . . . . . . . 12 |- K = ( Base ` G )
56	54, 55	syl6eqr 2461	. . . . . . . . . . 11 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( Base ` (Scalar ` r ) ) = K )
57	21	sneqd 3984	. . . . . . . . . . 11 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> { ( f ` q ) } = { ( F ` q ) } )
58	14	fveq2d 5853	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( .s ` r ) = ( .s ` R ) )
59		imasval.q	. . . . . . . . . . . . . 14 |- .x. = ( .s ` R )
60	58, 59	syl6eqr 2461	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( .s ` r ) = .x. )
61	60	oveqd 6295	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( p ( .s ` r ) q ) = ( p .x. q ) )
62	6, 61	fveq12d 5855	. . . . . . . . . . 11 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( f ` ( p ( .s ` r ) q ) ) = ( F ` ( p .x. q ) ) )
63	56, 57, 62	mpt2eq123dv 6340	. . . . . . . . . 10 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( p e. ( Base ` (Scalar ` r ) ) , x e. { ( f ` q ) } |-> ( f ` ( p ( .s ` r ) q ) ) ) = ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) )
64	63	iuneq2d 4298	. . . . . . . . 9 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> U_ q e. V ( p e. ( Base ` (Scalar ` r ) ) , x e. { ( f ` q ) } |-> ( f ` ( p ( .s ` r ) q ) ) ) = U_ q e. V ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) )
65	19	iuneq1d 4296	. . . . . . . . 9 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> U_ q e. v ( p e. ( Base ` (Scalar ` r ) ) , x e. { ( f ` q ) } |-> ( f ` ( p ( .s ` r ) q ) ) ) = U_ q e. V ( p e. ( Base ` (Scalar ` r ) ) , x e. { ( f ` q ) } |-> ( f ` ( p ( .s ` r ) q ) ) ) )
66		imasval.s	. . . . . . . . . 10 |- ( ph -> .(x) = U_ q e. V ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) )
67	66	ad2antrr 724	. . . . . . . . 9 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> .(x) = U_ q e. V ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) )
68	64, 65, 67	3eqtr4d 2453	. . . . . . . 8 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> U_ q e. v ( p e. ( Base ` (Scalar ` r ) ) , x e. { ( f ` q ) } |-> ( f ` ( p ( .s ` r ) q ) ) ) = .(x) )
69	68	opeq2d 4166	. . . . . . 7 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> <. ( .s ` ndx ) , U_ q e. v ( p e. ( Base ` (Scalar ` r ) ) , x e. { ( f ` q ) } |-> ( f ` ( p ( .s ` r ) q ) ) ) >. = <. ( .s ` ndx ) , .(x) >. )
70	14	fveq2d 5853	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( .i ` r ) = ( .i ` R ) )
71		imasval.i	. . . . . . . . . . . . . . 15 |- ., = ( .i ` R )
72	70, 71	syl6eqr 2461	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( .i ` r ) = ., )
73	72	oveqd 6295	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( p ( .i ` r ) q ) = ( p ., q ) )
74	22, 73	opeq12d 4167	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> <. <. ( f ` p ) , ( f ` q ) >. , ( p ( .i ` r ) q ) >. = <. <. ( F ` p ) , ( F ` q ) >. , ( p ., q ) >. )
75	74	sneqd 3984	. . . . . . . . . . 11 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> { <. <. ( f ` p ) , ( f ` q ) >. , ( p ( .i ` r ) q ) >. } = { <. <. ( F ` p ) , ( F ` q ) >. , ( p ., q ) >. } )
76	19, 75	iuneq12d 4297	. . . . . . . . . 10 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( p ( .i ` r ) q ) >. } = U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( p ., q ) >. } )
77	19, 76	iuneq12d 4297	. . . . . . . . 9 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> U_ p e. v U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( p ( .i ` r ) q ) >. } = U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( p ., q ) >. } )
78		imasval.w	. . . . . . . . . 10 |- ( ph -> I = U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( p ., q ) >. } )
79	78	ad2antrr 724	. . . . . . . . 9 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> I = U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( p ., q ) >. } )
80	77, 79	eqtr4d 2446	. . . . . . . 8 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> U_ p e. v U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( p ( .i ` r ) q ) >. } = I )
81	80	opeq2d 4166	. . . . . . 7 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> <. ( .i ` ndx ) , U_ p e. v U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( p ( .i ` r ) q ) >. } >. = <. ( .i ` ndx ) , I >. )
82	53, 69, 81	tpeq123d 4066	. . . . . 6 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> { <. (Scalar ` ndx ) , (Scalar ` r ) >. , <. ( .s ` ndx ) , U_ q e. v ( p e. ( Base ` (Scalar ` r ) ) , x e. { ( f ` q ) } |-> ( f ` ( p ( .s ` r ) q ) ) ) >. , <. ( .i ` ndx ) , U_ p e. v U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( p ( .i ` r ) q ) >. } >. } = { <. (Scalar ` ndx ) , G >. , <. ( .s ` ndx ) , .(x) >. , <. ( .i ` ndx ) , I >. } )
83	49, 82	uneq12d 3598	. . . . 5 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( { <. ( Base ` ndx ) , ran f >. , <. ( +g ` ndx ) , U_ p e. v U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( +g ` r ) q ) ) >. } >. , <. ( .r ` ndx ) , U_ p e. v U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( .r ` r ) q ) ) >. } >. } u. { <. (Scalar ` ndx ) , (Scalar ` r ) >. , <. ( .s ` ndx ) , U_ q e. v ( p e. ( Base ` (Scalar ` r ) ) , x e. { ( f ` q ) } |-> ( f ` ( p ( .s ` r ) q ) ) ) >. , <. ( .i ` ndx ) , U_ p e. v U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( p ( .i ` r ) q ) >. } >. } ) = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+b >. , <. ( .r ` ndx ) , .xb >. } u. { <. (Scalar ` ndx ) , G >. , <. ( .s ` ndx ) , .(x) >. , <. ( .i ` ndx ) , I >. } ) )
84	14	fveq2d 5853	. . . . . . . . . 10 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( TopOpen ` r ) = ( TopOpen ` R ) )
85		imasval.j	. . . . . . . . . 10 |- J = ( TopOpen ` R )
86	84, 85	syl6eqr 2461	. . . . . . . . 9 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( TopOpen ` r ) = J )
87	86, 6	oveq12d 6296	. . . . . . . 8 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( ( TopOpen ` r ) qTop f ) = ( J qTop F ) )
88		imasval.o	. . . . . . . . 9 |- ( ph -> O = ( J qTop F ) )
89	88	ad2antrr 724	. . . . . . . 8 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> O = ( J qTop F ) )
90	87, 89	eqtr4d 2446	. . . . . . 7 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( ( TopOpen ` r ) qTop f ) = O )
91	90	opeq2d 4166	. . . . . 6 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> <. (TopSet ` ndx ) , ( ( TopOpen ` r ) qTop f ) >. = <. (TopSet ` ndx ) , O >. )
92	14	fveq2d 5853	. . . . . . . . . . 11 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( le ` r ) = ( le ` R ) )
93		imasval.n	. . . . . . . . . . 11 |- N = ( le ` R )
94	92, 93	syl6eqr 2461	. . . . . . . . . 10 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( le ` r ) = N )
95	6, 94	coeq12d 4988	. . . . . . . . 9 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( f o. ( le ` r ) ) = ( F o. N ) )
96	6	cnveqd 4999	. . . . . . . . 9 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> `' f = `' F )
97	95, 96	coeq12d 4988	. . . . . . . 8 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( ( f o. ( le ` r ) ) o. `' f ) = ( ( F o. N ) o. `' F ) )
98		imasval.l	. . . . . . . . 9 |- ( ph -> .<_ = ( ( F o. N ) o. `' F ) )
99	98	ad2antrr 724	. . . . . . . 8 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> .<_ = ( ( F o. N ) o. `' F ) )
100	97, 99	eqtr4d 2446	. . . . . . 7 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( ( f o. ( le ` r ) ) o. `' f ) = .<_ )
101	100	opeq2d 4166	. . . . . 6 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> <. ( le ` ndx ) , ( ( f o. ( le ` r ) ) o. `' f ) >. = <. ( le ` ndx ) , .<_ >. )
102	19	sqxpeqd 4849	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( v X. v ) = ( V X. V ) )
103	102	oveq1d 6293	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( ( v X. v ) ^m ( 1 ... n ) ) = ( ( V X. V ) ^m ( 1 ... n ) ) )
104	6	fveq1d 5851	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( f ` ( 1st ` ( h ` 1 ) ) ) = ( F ` ( 1st ` ( h ` 1 ) ) ) )
105	104	eqeq1d 2404	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( ( f ` ( 1st ` ( h ` 1 ) ) ) = x <-> ( F ` ( 1st ` ( h ` 1 ) ) ) = x ) )
106	6	fveq1d 5851	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( f ` ( 2nd ` ( h ` n ) ) ) = ( F ` ( 2nd ` ( h ` n ) ) ) )
107	106	eqeq1d 2404	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( ( f ` ( 2nd ` ( h ` n ) ) ) = y <-> ( F ` ( 2nd ` ( h ` n ) ) ) = y ) )
108	6	fveq1d 5851	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( f ` ( 2nd ` ( h ` i ) ) ) = ( F ` ( 2nd ` ( h ` i ) ) ) )
109	6	fveq1d 5851	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( f ` ( 1st ` ( h ` ( i + 1 ) ) ) ) = ( F ` ( 1st ` ( h ` ( i + 1 ) ) ) ) )
110	108, 109	eqeq12d 2424	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( ( f ` ( 2nd ` ( h ` i ) ) ) = ( f ` ( 1st ` ( h ` ( i + 1 ) ) ) ) <-> ( F ` ( 2nd ` ( h ` i ) ) ) = ( F ` ( 1st ` ( h ` ( i + 1 ) ) ) ) ) )
111	110	ralbidv 2843	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( A. i e. ( 1 ... ( n - 1 ) ) ( f ` ( 2nd ` ( h ` i ) ) ) = ( f ` ( 1st ` ( h ` ( i + 1 ) ) ) ) <-> A. i e. ( 1 ... ( n - 1 ) ) ( F ` ( 2nd ` ( h ` i ) ) ) = ( F ` ( 1st ` ( h ` ( i + 1 ) ) ) ) ) )
112	105, 107, 111	3anbi123d 1301	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( ( ( f ` ( 1st ` ( h ` 1 ) ) ) = x /\ ( f ` ( 2nd ` ( h ` n ) ) ) = y /\ A. i e. ( 1 ... ( n - 1 ) ) ( f ` ( 2nd ` ( h ` i ) ) ) = ( f ` ( 1st ` ( h ` ( i + 1 ) ) ) ) ) <-> ( ( F ` ( 1st ` ( h ` 1 ) ) ) = x /\ ( F ` ( 2nd ` ( h ` n ) ) ) = y /\ A. i e. ( 1 ... ( n - 1 ) ) ( F ` ( 2nd ` ( h ` i ) ) ) = ( F ` ( 1st ` ( h ` ( i + 1 ) ) ) ) ) ) )
113	103, 112	rabeqbidv 3054	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> { h e. ( ( v X. v ) ^m ( 1 ... n ) ) | ( ( f ` ( 1st ` ( h ` 1 ) ) ) = x /\ ( f ` ( 2nd ` ( h ` n ) ) ) = y /\ A. i e. ( 1 ... ( n - 1 ) ) ( f ` ( 2nd ` ( h ` i ) ) ) = ( f ` ( 1st ` ( h ` ( i + 1 ) ) ) ) ) } = { h e. ( ( V X. V ) ^m ( 1 ... n ) ) | ( ( F ` ( 1st ` ( h ` 1 ) ) ) = x /\ ( F ` ( 2nd ` ( h ` n ) ) ) = y /\ A. i e. ( 1 ... ( n - 1 ) ) ( F ` ( 2nd ` ( h ` i ) ) ) = ( F ` ( 1st ` ( h ` ( i + 1 ) ) ) ) ) } )
114	14	fveq2d 5853	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( dist ` r ) = ( dist ` R ) )
115		imasval.e	. . . . . . . . . . . . . . . 16 |- E = ( dist ` R )
116	114, 115	syl6eqr 2461	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( dist ` r ) = E )
117	116	coeq1d 4985	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( ( dist ` r ) o. g ) = ( E o. g ) )
118	117	oveq2d 6294	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( RR*s gsumg ( ( dist ` r ) o. g ) ) = ( RR*s gsumg ( E o. g ) ) )
119	113, 118	mpteq12dv 4473	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( g e. { h e. ( ( v X. v ) ^m ( 1 ... n ) ) | ( ( f ` ( 1st ` ( h ` 1 ) ) ) = x /\ ( f ` ( 2nd ` ( h ` n ) ) ) = y /\ A. i e. ( 1 ... ( n - 1 ) ) ( f ` ( 2nd ` ( h ` i ) ) ) = ( f ` ( 1st ` ( h ` ( i + 1 ) ) ) ) ) } |-> ( RR*s gsumg ( ( dist ` r ) o. g ) ) ) = ( g e. { h e. ( ( V X. V ) ^m ( 1 ... n ) ) | ( ( F ` ( 1st ` ( h ` 1 ) ) ) = x /\ ( F ` ( 2nd ` ( h ` n ) ) ) = y /\ A. i e. ( 1 ... ( n - 1 ) ) ( F ` ( 2nd ` ( h ` i ) ) ) = ( F ` ( 1st ` ( h ` ( i + 1 ) ) ) ) ) } |-> ( RR*s gsumg ( E o. g ) ) ) )
120	119	rneqd 5051	. . . . . . . . . . 11 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ran ( g e. { h e. ( ( v X. v ) ^m ( 1 ... n ) ) | ( ( f ` ( 1st ` ( h ` 1 ) ) ) = x /\ ( f ` ( 2nd ` ( h ` n ) ) ) = y /\ A. i e. ( 1 ... ( n - 1 ) ) ( f ` ( 2nd ` ( h ` i ) ) ) = ( f ` ( 1st ` ( h ` ( i + 1 ) ) ) ) ) } |-> ( RR*s gsumg ( ( dist ` r ) o. g ) ) ) = ran ( g e. { h e. ( ( V X. V ) ^m ( 1 ... n ) ) | ( ( F ` ( 1st ` ( h ` 1 ) ) ) = x /\ ( F ` ( 2nd ` ( h ` n ) ) ) = y /\ A. i e. ( 1 ... ( n - 1 ) ) ( F ` ( 2nd ` ( h ` i ) ) ) = ( F ` ( 1st ` ( h ` ( i + 1 ) ) ) ) ) } |-> ( RR*s gsumg ( E o. g ) ) ) )
121	120	iuneq2d 4298	. . . . . . . . . 10 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> U_ n e. NN ran ( g e. { h e. ( ( v X. v ) ^m ( 1 ... n ) ) | ( ( f ` ( 1st ` ( h ` 1 ) ) ) = x /\ ( f ` ( 2nd ` ( h ` n ) ) ) = y /\ A. i e. ( 1 ... ( n - 1 ) ) ( f ` ( 2nd ` ( h ` i ) ) ) = ( f ` ( 1st ` ( h ` ( i + 1 ) ) ) ) ) } |-> ( RR*s gsumg ( ( dist ` r ) o. g ) ) ) = U_ n e. NN ran ( g e. { h e. ( ( V X. V ) ^m ( 1 ... n ) ) | ( ( F ` ( 1st ` ( h ` 1 ) ) ) = x /\ ( F ` ( 2nd ` ( h ` n ) ) ) = y /\ A. i e. ( 1 ... ( n - 1 ) ) ( F ` ( 2nd ` ( h ` i ) ) ) = ( F ` ( 1st ` ( h ` ( i + 1 ) ) ) ) ) } |-> ( RR*s gsumg ( E o. g ) ) ) )
122	121	supeq1d 7939	. . . . . . . . 9 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> sup ( U_ n e. NN ran ( g e. { h e. ( ( v X. v ) ^m ( 1 ... n ) ) | ( ( f ` ( 1st ` ( h ` 1 ) ) ) = x /\ ( f ` ( 2nd ` ( h ` n ) ) ) = y /\ A. i e. ( 1 ... ( n - 1 ) ) ( f ` ( 2nd ` ( h ` i ) ) ) = ( f ` ( 1st ` ( h ` ( i + 1 ) ) ) ) ) } |-> ( RR*s gsumg ( ( dist ` r ) o. g ) ) ) , RR* , `' < ) = sup ( U_ n e. NN ran ( g e. { h e. ( ( V X. V ) ^m ( 1 ... n ) ) | ( ( F ` ( 1st ` ( h ` 1 ) ) ) = x /\ ( F ` ( 2nd ` ( h ` n ) ) ) = y /\ A. i e. ( 1 ... ( n - 1 ) ) ( F ` ( 2nd ` ( h ` i ) ) ) = ( F ` ( 1st ` ( h ` ( i + 1 ) ) ) ) ) } |-> ( RR*s gsumg ( E o. g ) ) ) , RR* , `' < ) )
123	12, 12, 122	mpt2eq123dv 6340	. . . . . . . 8 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( x e. ran f , y e. ran f |-> sup ( U_ n e. NN ran ( g e. { h e. ( ( v X. v ) ^m ( 1 ... n ) ) | ( ( f ` ( 1st ` ( h ` 1 ) ) ) = x /\ ( f ` ( 2nd ` ( h ` n ) ) ) = y /\ A. i e. ( 1 ... ( n - 1 ) ) ( f ` ( 2nd ` ( h ` i ) ) ) = ( f ` ( 1st ` ( h ` ( i + 1 ) ) ) ) ) } |-> ( RR*s gsumg ( ( dist ` r ) o. g ) ) ) , RR* , `' < ) ) = ( x e. B , y e. B |-> sup ( U_ n e. NN ran ( g e. { h e. ( ( V X. V ) ^m ( 1 ... n ) ) | ( ( F ` ( 1st ` ( h ` 1 ) ) ) = x /\ ( F ` ( 2nd ` ( h ` n ) ) ) = y /\ A. i e. ( 1 ... ( n - 1 ) ) ( F ` ( 2nd ` ( h ` i ) ) ) = ( F ` ( 1st ` ( h ` ( i + 1 ) ) ) ) ) } |-> ( RR*s gsumg ( E o. g ) ) ) , RR* , `' < ) ) )
124		imasval.d	. . . . . . . . 9 |- ( ph -> D = ( x e. B , y e. B |-> sup ( U_ n e. NN ran ( g e. { h e. ( ( V X. V ) ^m ( 1 ... n ) ) | ( ( F ` ( 1st ` ( h ` 1 ) ) ) = x /\ ( F ` ( 2nd ` ( h ` n ) ) ) = y /\ A. i e. ( 1 ... ( n - 1 ) ) ( F ` ( 2nd ` ( h ` i ) ) ) = ( F ` ( 1st ` ( h ` ( i + 1 ) ) ) ) ) } |-> ( RR*s gsumg ( E o. g ) ) ) , RR* , `' < ) ) )
125	124	ad2antrr 724	. . . . . . . 8 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> D = ( x e. B , y e. B |-> sup ( U_ n e. NN ran ( g e. { h e. ( ( V X. V ) ^m ( 1 ... n ) ) | ( ( F ` ( 1st ` ( h ` 1 ) ) ) = x /\ ( F ` ( 2nd ` ( h ` n ) ) ) = y /\ A. i e. ( 1 ... ( n - 1 ) ) ( F ` ( 2nd ` ( h ` i ) ) ) = ( F ` ( 1st ` ( h ` ( i + 1 ) ) ) ) ) } |-> ( RR*s gsumg ( E o. g ) ) ) , RR* , `' < ) ) )
126	123, 125	eqtr4d 2446	. . . . . . 7 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( x e. ran f , y e. ran f |-> sup ( U_ n e. NN ran ( g e. { h e. ( ( v X. v ) ^m ( 1 ... n ) ) | ( ( f ` ( 1st ` ( h ` 1 ) ) ) = x /\ ( f ` ( 2nd ` ( h ` n ) ) ) = y /\ A. i e. ( 1 ... ( n - 1 ) ) ( f ` ( 2nd ` ( h ` i ) ) ) = ( f ` ( 1st ` ( h ` ( i + 1 ) ) ) ) ) } |-> ( RR*s gsumg ( ( dist ` r ) o. g ) ) ) , RR* , `' < ) ) = D )
127	126	opeq2d 4166	. . . . . 6 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> <. ( dist ` ndx ) , ( x e. ran f , y e. ran f |-> sup ( U_ n e. NN ran ( g e. { h e. ( ( v X. v ) ^m ( 1 ... n ) ) | ( ( f ` ( 1st ` ( h ` 1 ) ) ) = x /\ ( f ` ( 2nd ` ( h ` n ) ) ) = y /\ A. i e. ( 1 ... ( n - 1 ) ) ( f ` ( 2nd ` ( h ` i ) ) ) = ( f ` ( 1st ` ( h ` ( i + 1 ) ) ) ) ) } |-> ( RR*s gsumg ( ( dist ` r ) o. g ) ) ) , RR* , `' < ) ) >. = <. ( dist ` ndx ) , D >. )
128	91, 101, 127	tpeq123d 4066	. . . . 5 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> { <. (TopSet ` ndx ) , ( ( TopOpen ` r ) qTop f ) >. , <. ( le ` ndx ) , ( ( f o. ( le ` r ) ) o. `' f ) >. , <. ( dist ` ndx ) , ( x e. ran f , y e. ran f |-> sup ( U_ n e. NN ran ( g e. { h e. ( ( v X. v ) ^m ( 1 ... n ) ) | ( ( f ` ( 1st ` ( h ` 1 ) ) ) = x /\ ( f ` ( 2nd ` ( h ` n ) ) ) = y /\ A. i e. ( 1 ... ( n - 1 ) ) ( f ` ( 2nd ` ( h ` i ) ) ) = ( f ` ( 1st ` ( h ` ( i + 1 ) ) ) ) ) } |-> ( RR*s gsumg ( ( dist ` r ) o. g ) ) ) , RR* , `' < ) ) >. } = { <. (TopSet ` ndx ) , O >. , <. ( le ` ndx ) , .<_ >. , <. ( dist ` ndx ) , D >. } )
129	83, 128	uneq12d 3598	. . . 4 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( ( { <. ( Base ` ndx ) , ran f >. , <. ( +g ` ndx ) , U_ p e. v U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( +g ` r ) q ) ) >. } >. , <. ( .r ` ndx ) , U_ p e. v U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( .r ` r ) q ) ) >. } >. } u. { <. (Scalar ` ndx ) , (Scalar ` r ) >. , <. ( .s ` ndx ) , U_ q e. v ( p e. ( Base ` (Scalar ` r ) ) , x e. { ( f ` q ) } |-> ( f ` ( p ( .s ` r ) q ) ) ) >. , <. ( .i ` ndx ) , U_ p e. v U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( p ( .i ` r ) q ) >. } >. } ) u. { <. (TopSet ` ndx ) , ( ( TopOpen ` r ) qTop f ) >. , <. ( le ` ndx ) , ( ( f o. ( le ` r ) ) o. `' f ) >. , <. ( dist ` ndx ) , ( x e. ran f , y e. ran f |-> sup ( U_ n e. NN ran ( g e. { h e. ( ( v X. v ) ^m ( 1 ... n ) ) | ( ( f ` ( 1st ` ( h ` 1 ) ) ) = x /\ ( f ` ( 2nd ` ( h ` n ) ) ) = y /\ A. i e. ( 1 ... ( n - 1 ) ) ( f ` ( 2nd ` ( h ` i ) ) ) = ( f ` ( 1st ` ( h ` ( i + 1 ) ) ) ) ) } |-> ( RR*s gsumg ( ( dist ` r ) o. g ) ) ) , RR* , `' < ) ) >. } ) = ( ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+b >. , <. ( .r ` ndx ) , .xb >. } u. { <. (Scalar ` ndx ) , G >. , <. ( .s ` ndx ) , .(x) >. , <. ( .i ` ndx ) , I >. } ) u. { <. (TopSet ` ndx ) , O >. , <. ( le ` ndx ) , .<_ >. , <. ( dist ` ndx ) , D >. } ) )
130	5, 129	csbied 3400	. . 3 |- ( ( ph /\ ( f = F /\ r = R ) ) -> [_ ( Base ` r ) / v ]_ ( ( { <. ( Base ` ndx ) , ran f >. , <. ( +g ` ndx ) , U_ p e. v U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( +g ` r ) q ) ) >. } >. , <. ( .r ` ndx ) , U_ p e. v U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( .r ` r ) q ) ) >. } >. } u. { <. (Scalar ` ndx ) , (Scalar ` r ) >. , <. ( .s ` ndx ) , U_ q e. v ( p e. ( Base ` (Scalar ` r ) ) , x e. { ( f ` q ) } |-> ( f ` ( p ( .s ` r ) q ) ) ) >. , <. ( .i ` ndx ) , U_ p e. v U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( p ( .i ` r ) q ) >. } >. } ) u. { <. (TopSet ` ndx ) , ( ( TopOpen ` r ) qTop f ) >. , <. ( le ` ndx ) , ( ( f o. ( le ` r ) ) o. `' f ) >. , <. ( dist ` ndx ) , ( x e. ran f , y e. ran f |-> sup ( U_ n e. NN ran ( g e. { h e. ( ( v X. v ) ^m ( 1 ... n ) ) | ( ( f ` ( 1st ` ( h ` 1 ) ) ) = x /\ ( f ` ( 2nd ` ( h ` n ) ) ) = y /\ A. i e. ( 1 ... ( n - 1 ) ) ( f ` ( 2nd ` ( h ` i ) ) ) = ( f ` ( 1st ` ( h ` ( i + 1 ) ) ) ) ) } |-> ( RR*s gsumg ( ( dist ` r ) o. g ) ) ) , RR* , `' < ) ) >. } ) = ( ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+b >. , <. ( .r ` ndx ) , .xb >. } u. { <. (Scalar ` ndx ) , G >. , <. ( .s ` ndx ) , .(x) >. , <. ( .i ` ndx ) , I >. } ) u. { <. (TopSet ` ndx ) , O >. , <. ( le ` ndx ) , .<_ >. , <. ( dist ` ndx ) , D >. } ) )
131		fof 5778	. . . . 5 |- ( F : V -onto-> B -> F : V --> B )
132	8, 131	syl 17	. . . 4 |- ( ph -> F : V --> B )
133		fvex 5859	. . . . 5 |- ( Base ` R ) e. _V
134	17, 133	syl6eqel 2498	. . . 4 |- ( ph -> V e. _V )
135		fex 6126	. . . 4 |- ( ( F : V --> B /\ V e. _V ) -> F e. _V )
136	132, 134, 135	syl2anc 659	. . 3 |- ( ph -> F e. _V )
137		imasval.r	. . . 4 |- ( ph -> R e. Z )
138		elex 3068	. . . 4 |- ( R e. Z -> R e. _V )
139	137, 138	syl 17	. . 3 |- ( ph -> R e. _V )
140		tpex 6581	. . . . . 6 |- { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+b >. , <. ( .r ` ndx ) , .xb >. } e. _V
141		tpex 6581	. . . . . 6 |- { <. (Scalar ` ndx ) , G >. , <. ( .s ` ndx ) , .(x) >. , <. ( .i ` ndx ) , I >. } e. _V
142	140, 141	unex 6580	. . . . 5 |- ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+b >. , <. ( .r ` ndx ) , .xb >. } u. { <. (Scalar ` ndx ) , G >. , <. ( .s ` ndx ) , .(x) >. , <. ( .i ` ndx ) , I >. } ) e. _V
143		tpex 6581	. . . . 5 |- { <. (TopSet ` ndx ) , O >. , <. ( le ` ndx ) , .<_ >. , <. ( dist ` ndx ) , D >. } e. _V
144	142, 143	unex 6580	. . . 4 |- ( ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+b >. , <. ( .r ` ndx ) , .xb >. } u. { <. (Scalar ` ndx ) , G >. , <. ( .s ` ndx ) , .(x) >. , <. ( .i ` ndx ) , I >. } ) u. { <. (TopSet ` ndx ) , O >. , <. ( le ` ndx ) , .<_ >. , <. ( dist ` ndx ) , D >. } ) e. _V
145	144	a1i 11	. . 3 |- ( ph -> ( ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+b >. , <. ( .r ` ndx ) , .xb >. } u. { <. (Scalar ` ndx ) , G >. , <. ( .s ` ndx ) , .(x) >. , <. ( .i ` ndx ) , I >. } ) u. { <. (TopSet ` ndx ) , O >. , <. ( le ` ndx ) , .<_ >. , <. ( dist ` ndx ) , D >. } ) e. _V )
146	3, 130, 136, 139, 145	ovmpt2d 6411	. 2 |- ( ph -> ( F "s R ) = ( ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+b >. , <. ( .r ` ndx ) , .xb >. } u. { <. (Scalar ` ndx ) , G >. , <. ( .s ` ndx ) , .(x) >. , <. ( .i ` ndx ) , I >. } ) u. { <. (TopSet ` ndx ) , O >. , <. ( le ` ndx ) , .<_ >. , <. ( dist ` ndx ) , D >. } ) )
147	1, 146	eqtrd 2443	1 |- ( ph -> U = ( ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+b >. , <. ( .r ` ndx ) , .xb >. } u. { <. (Scalar ` ndx ) , G >. , <. ( .s ` ndx ) , .(x) >. , <. ( .i ` ndx ) , I >. } ) u. { <. (TopSet ` ndx ) , O >. , <. ( le ` ndx ) , .<_ >. , <. ( dist ` ndx ) , D >. } ) )

Syntax hints:   -> wi 4   /\ wa 367   /\ w3a 974   = wceq 1405   e. wcel 1842   A.wral 2754   {crab 2758   _Vcvv 3059   [_csb 3373   u. cun 3412   {csn 3972   {ctp 3976   <.cop 3978   U_ciun 4271   |-> cmpt 4453   X. cxp 4821   `'ccnv 4822   ran crn 4824   o. ccom 4827   -->wf 5565   -onto->wfo 5567   ` cfv 5569  (class class class)co 6278   |-> cmpt2 6280   1stc1st 6782   2ndc2nd 6783   ^m cmap 7457   supcsup 7934   1c1 9523   + caddc 9525   RR*cxr 9657   < clt 9658   - cmin 9841   NNcn 10576   ...cfz 11726   ndxcnx 14838   Basecbs 14841   +g cplusg 14909   .rcmulr 14910  Scalarcsca 14912   .scvsca 14913   .icip 14914  TopSetcts 14915   lecple 14916   distcds 14918   TopOpenctopn 15036   gsum_g cgsu 15055   RR*scxrs 15114   qTop cqtop 15117   "_s cimas 15118

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-8 1844  ax-9 1846  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-rep 4507  ax-sep 4517  ax-nul 4525  ax-pr 4630  ax-un 6574

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-eu 2242  df-mo 2243  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ne 2600  df-ral 2759  df-rex 2760  df-reu 2761  df-rab 2763  df-v 3061  df-sbc 3278  df-csb 3374  df-dif 3417  df-un 3419  df-in 3421  df-ss 3428  df-nul 3739  df-if 3886  df-sn 3973  df-pr 3975  df-tp 3977  df-op 3979  df-uni 4192  df-iun 4273  df-br 4396  df-opab 4454  df-mpt 4455  df-id 4738  df-xp 4829  df-rel 4830  df-cnv 4831  df-co 4832  df-dm 4833  df-rn 4834  df-res 4835  df-ima 4836  df-iota 5533  df-fun 5571  df-fn 5572  df-f 5573  df-f1 5574  df-fo 5575  df-f1o 5576  df-fv 5577  df-ov 6281  df-oprab 6282  df-mpt2 6283  df-sup 7935  df-imas 15122

This theorem is referenced by:  imasbas  15126  imasds  15127  imasplusg  15131  imasmulr  15132  imassca  15133  imasvsca  15134  imasip  15135  imastset  15136  imasle  15137