Theorem imasval 15422

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.) (Revised by AV, 6-Oct-2020.)

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 |-> inf ( 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 15418	. . . 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 |-> inf ( 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 |-> inf ( 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 5858	. . . . 5 |- ( Base ` r ) e. _V
5	4	a1i 11	. . . 4 |- ( ( ph /\ ( f = F /\ r = R ) ) -> ( Base ` r ) e. _V )
6		simplrl 775	. . . . . . . . . 10 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> f = F )
7	6	rneqd 5040	. . . . . . . . 9 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ran f = ran F )
8		imasval.f	. . . . . . . . . . 11 |- ( ph -> F : V -onto-> B )
9		forn 5779	. . . . . . . . . . 11 |- ( F : V -onto-> B -> ran F = B )
10	8, 9	syl 17	. . . . . . . . . 10 |- ( ph -> ran F = B )
11	10	ad2antrr 737	. . . . . . . . 9 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ran F = B )
12	7, 11	eqtrd 2486	. . . . . . . 8 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ran f = B )
13	12	opeq2d 4143	. . . . . . 7 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> <. ( Base ` ndx ) , ran f >. = <. ( Base ` ndx ) , B >. )
14		simplrr 776	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> r = R )
15	14	fveq2d 5852	. . . . . . . . . . 11 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( Base ` r ) = ( Base ` R ) )
16		simpr 467	. . . . . . . . . . 11 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> v = ( Base ` r ) )
17		imasval.v	. . . . . . . . . . . 12 |- ( ph -> V = ( Base ` R ) )
18	17	ad2antrr 737	. . . . . . . . . . 11 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> V = ( Base ` R ) )
19	15, 16, 18	3eqtr4d 2496	. . . . . . . . . 10 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> v = V )
20	6	fveq1d 5850	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( f ` p ) = ( F ` p ) )
21	6	fveq1d 5850	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( f ` q ) = ( F ` q ) )
22	20, 21	opeq12d 4144	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> <. ( f ` p ) , ( f ` q ) >. = <. ( F ` p ) , ( F ` q ) >. )
23	14	fveq2d 5852	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( +g ` r ) = ( +g ` R ) )
24		imasval.p	. . . . . . . . . . . . . . . 16 |- .+ = ( +g ` R )
25	23, 24	syl6eqr 2504	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( +g ` r ) = .+ )
26	25	oveqd 6293	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( p ( +g ` r ) q ) = ( p .+ q ) )
27	6, 26	fveq12d 5854	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( f ` ( p ( +g ` r ) q ) ) = ( F ` ( p .+ q ) ) )
28	22, 27	opeq12d 4144	. . . . . . . . . . . 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 3948	. . . . . . . . . . 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 4274	. . . . . . . . . 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 4274	. . . . . . . . 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 737	. . . . . . . . 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 2489	. . . . . . . 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 4143	. . . . . . 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 5852	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( .r ` r ) = ( .r ` R ) )
37		imasval.m	. . . . . . . . . . . . . . . 16 |- .X. = ( .r ` R )
38	36, 37	syl6eqr 2504	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( .r ` r ) = .X. )
39	38	oveqd 6293	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( p ( .r ` r ) q ) = ( p .X. q ) )
40	6, 39	fveq12d 5854	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( f ` ( p ( .r ` r ) q ) ) = ( F ` ( p .X. q ) ) )
41	22, 40	opeq12d 4144	. . . . . . . . . . . 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 3948	. . . . . . . . . . 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 4274	. . . . . . . . . 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 4274	. . . . . . . . 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 737	. . . . . . . . 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 2489	. . . . . . . 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 4143	. . . . . . 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 4035	. . . . . 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 5852	. . . . . . . . 9 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> (Scalar ` r ) = (Scalar ` R ) )
51		imasval.g	. . . . . . . . 9 |- G = (Scalar ` R )
52	50, 51	syl6eqr 2504	. . . . . . . 8 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> (Scalar ` r ) = G )
53	52	opeq2d 4143	. . . . . . 7 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> <. (Scalar ` ndx ) , (Scalar ` r ) >. = <. (Scalar ` ndx ) , G >. )
54	52	fveq2d 5852	. . . . . . . . . . . 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 2504	. . . . . . . . . . 11 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( Base ` (Scalar ` r ) ) = K )
57	21	sneqd 3948	. . . . . . . . . . 11 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> { ( f ` q ) } = { ( F ` q ) } )
58	14	fveq2d 5852	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( .s ` r ) = ( .s ` R ) )
59		imasval.q	. . . . . . . . . . . . . 14 |- .x. = ( .s ` R )
60	58, 59	syl6eqr 2504	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( .s ` r ) = .x. )
61	60	oveqd 6293	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( p ( .s ` r ) q ) = ( p .x. q ) )
62	6, 61	fveq12d 5854	. . . . . . . . . . 11 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( f ` ( p ( .s ` r ) q ) ) = ( F ` ( p .x. q ) ) )
63	56, 57, 62	mpt2eq123dv 6341	. . . . . . . . . 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 4275	. . . . . . . . 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 4273	. . . . . . . . 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 737	. . . . . . . . 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 2496	. . . . . . . 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 4143	. . . . . . 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 5852	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( .i ` r ) = ( .i ` R ) )
71		imasval.i	. . . . . . . . . . . . . . 15 |- ., = ( .i ` R )
72	70, 71	syl6eqr 2504	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( .i ` r ) = ., )
73	72	oveqd 6293	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( p ( .i ` r ) q ) = ( p ., q ) )
74	22, 73	opeq12d 4144	. . . . . . . . . . . 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 3948	. . . . . . . . . . 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 4274	. . . . . . . . . 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 4274	. . . . . . . . 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 737	. . . . . . . . 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 2489	. . . . . . . 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 4143	. . . . . . 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 4035	. . . . . 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 3557	. . . . 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 5852	. . . . . . . . . 10 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( TopOpen ` r ) = ( TopOpen ` R ) )
85		imasval.j	. . . . . . . . . 10 |- J = ( TopOpen ` R )
86	84, 85	syl6eqr 2504	. . . . . . . . 9 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( TopOpen ` r ) = J )
87	86, 6	oveq12d 6294	. . . . . . . 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 737	. . . . . . . 8 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> O = ( J qTop F ) )
90	87, 89	eqtr4d 2489	. . . . . . 7 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( ( TopOpen ` r ) qTop f ) = O )
91	90	opeq2d 4143	. . . . . 6 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> <. (TopSet ` ndx ) , ( ( TopOpen ` r ) qTop f ) >. = <. (TopSet ` ndx ) , O >. )
92	14	fveq2d 5852	. . . . . . . . . . 11 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( le ` r ) = ( le ` R ) )
93		imasval.n	. . . . . . . . . . 11 |- N = ( le ` R )
94	92, 93	syl6eqr 2504	. . . . . . . . . 10 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( le ` r ) = N )
95	6, 94	coeq12d 4977	. . . . . . . . 9 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( f o. ( le ` r ) ) = ( F o. N ) )
96	6	cnveqd 4988	. . . . . . . . 9 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> `' f = `' F )
97	95, 96	coeq12d 4977	. . . . . . . 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 737	. . . . . . . 8 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> .<_ = ( ( F o. N ) o. `' F ) )
100	97, 99	eqtr4d 2489	. . . . . . 7 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( ( f o. ( le ` r ) ) o. `' f ) = .<_ )
101	100	opeq2d 4143	. . . . . 6 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> <. ( le ` ndx ) , ( ( f o. ( le ` r ) ) o. `' f ) >. = <. ( le ` ndx ) , .<_ >. )
102	19	sqxpeqd 4838	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( v X. v ) = ( V X. V ) )
103	102	oveq1d 6291	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( ( v X. v ) ^m ( 1 ... n ) ) = ( ( V X. V ) ^m ( 1 ... n ) ) )
104	6	fveq1d 5850	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( f ` ( 1st ` ( h ` 1 ) ) ) = ( F ` ( 1st ` ( h ` 1 ) ) ) )
105	104	eqeq1d 2454	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( ( f ` ( 1st ` ( h ` 1 ) ) ) = x <-> ( F ` ( 1st ` ( h ` 1 ) ) ) = x ) )
106	6	fveq1d 5850	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( f ` ( 2nd ` ( h ` n ) ) ) = ( F ` ( 2nd ` ( h ` n ) ) ) )
107	106	eqeq1d 2454	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( ( f ` ( 2nd ` ( h ` n ) ) ) = y <-> ( F ` ( 2nd ` ( h ` n ) ) ) = y ) )
108	6	fveq1d 5850	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( f ` ( 2nd ` ( h ` i ) ) ) = ( F ` ( 2nd ` ( h ` i ) ) ) )
109	6	fveq1d 5850	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( f ` ( 1st ` ( h ` ( i + 1 ) ) ) ) = ( F ` ( 1st ` ( h ` ( i + 1 ) ) ) ) )
110	108, 109	eqeq12d 2467	. . . . . . . . . . . . . . . 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 2810	. . . . . . . . . . . . . . 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 1343	. . . . . . . . . . . . . 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 3008	. . . . . . . . . . . . 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 5852	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( dist ` r ) = ( dist ` R ) )
115		imasval.e	. . . . . . . . . . . . . . . 16 |- E = ( dist ` R )
116	114, 115	syl6eqr 2504	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( dist ` r ) = E )
117	116	coeq1d 4974	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( ( dist ` r ) o. g ) = ( E o. g ) )
118	117	oveq2d 6292	. . . . . . . . . . . . 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 4453	. . . . . . . . . . . 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 5040	. . . . . . . . . . 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 4275	. . . . . . . . . 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	infeq1d 7980	. . . . . . . . 9 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> inf ( 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* , < ) = inf ( 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 6341	. . . . . . . 8 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( x e. ran f , y e. ran f |-> inf ( 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 |-> inf ( 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 |-> inf ( 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 737	. . . . . . . 8 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> D = ( x e. B , y e. B |-> inf ( 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 2489	. . . . . . 7 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( x e. ran f , y e. ran f |-> inf ( 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 4143	. . . . . 6 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> <. ( dist ` ndx ) , ( x e. ran f , y e. ran f |-> inf ( 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 4035	. . . . 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 |-> inf ( 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 3557	. . . 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 |-> inf ( 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 3358	. . 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 |-> inf ( 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 5776	. . . . 5 |- ( F : V -onto-> B -> F : V --> B )
132	8, 131	syl 17	. . . 4 |- ( ph -> F : V --> B )
133		fvex 5858	. . . . 5 |- ( Base ` R ) e. _V
134	17, 133	syl6eqel 2538	. . . 4 |- ( ph -> V e. _V )
135		fex 6124	. . . 4 |- ( ( F : V --> B /\ V e. _V ) -> F e. _V )
136	132, 134, 135	syl2anc 671	. . 3 |- ( ph -> F e. _V )
137		imasval.r	. . . 4 |- ( ph -> R e. Z )
138		elex 3022	. . . 4 |- ( R e. Z -> R e. _V )
139	137, 138	syl 17	. . 3 |- ( ph -> R e. _V )
140		tpex 6578	. . . . . 6 |- { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+b >. , <. ( .r ` ndx ) , .xb >. } e. _V
141		tpex 6578	. . . . . 6 |- { <. (Scalar ` ndx ) , G >. , <. ( .s ` ndx ) , .(x) >. , <. ( .i ` ndx ) , I >. } e. _V
142	140, 141	unex 6577	. . . . 5 |- ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+b >. , <. ( .r ` ndx ) , .xb >. } u. { <. (Scalar ` ndx ) , G >. , <. ( .s ` ndx ) , .(x) >. , <. ( .i ` ndx ) , I >. } ) e. _V
143		tpex 6578	. . . . 5 |- { <. (TopSet ` ndx ) , O >. , <. ( le ` ndx ) , .<_ >. , <. ( dist ` ndx ) , D >. } e. _V
144	142, 143	unex 6577	. . . 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 6412	. 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 2486	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 375   /\ w3a 986   = wceq 1448   e. wcel 1891   A.wral 2737   {crab 2741   _Vcvv 3013   [_csb 3331   u. cun 3370   {csn 3936   {ctp 3940   <.cop 3942   U_ciun 4248   |-> cmpt 4433   X. cxp 4810   `'ccnv 4811   ran crn 4813   o. ccom 4816   -->wf 5557   -onto->wfo 5559   ` cfv 5561  (class class class)co 6276   |-> cmpt2 6278   1stc1st 6779   2ndc2nd 6780   ^m cmap 7459  infcinf 7942   1c1 9527   + caddc 9529   RR*cxr 9661   < clt 9662   - cmin 9847   NNcn 10598   ...cfz 11775   ndxcnx 15129   Basecbs 15132   +g cplusg 15201   .rcmulr 15202  Scalarcsca 15204   .scvsca 15205   .icip 15206  TopSetcts 15207   lecple 15208   distcds 15210   TopOpenctopn 15331   gsum_g cgsu 15350   RR*scxrs 15409   qTop cqtop 15412   "_s cimas 15413

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1673  ax-4 1686  ax-5 1762  ax-6 1809  ax-7 1855  ax-8 1893  ax-9 1900  ax-10 1919  ax-11 1924  ax-12 1937  ax-13 2092  ax-ext 2432  ax-rep 4487  ax-sep 4497  ax-nul 4506  ax-pr 4612  ax-un 6571

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 988  df-tru 1451  df-ex 1668  df-nf 1672  df-sb 1802  df-eu 2304  df-mo 2305  df-clab 2439  df-cleq 2445  df-clel 2448  df-nfc 2582  df-ne 2624  df-ral 2742  df-rex 2743  df-reu 2744  df-rab 2746  df-v 3015  df-sbc 3236  df-csb 3332  df-dif 3375  df-un 3377  df-in 3379  df-ss 3386  df-nul 3700  df-if 3850  df-sn 3937  df-pr 3939  df-tp 3941  df-op 3943  df-uni 4169  df-iun 4250  df-br 4375  df-opab 4434  df-mpt 4435  df-id 4727  df-xp 4818  df-rel 4819  df-cnv 4820  df-co 4821  df-dm 4822  df-rn 4823  df-res 4824  df-ima 4825  df-iota 5525  df-fun 5563  df-fn 5564  df-f 5565  df-f1 5566  df-fo 5567  df-f1o 5568  df-fv 5569  df-ov 6279  df-oprab 6280  df-mpt2 6281  df-sup 7943  df-inf 7944  df-imas 15418

This theorem is referenced by:  imasbas  15424  imasds  15425  imasplusg  15429  imasmulr  15430  imassca  15431  imasvsca  15432  imasip  15433  imastset  15434  imasle  15435