Metamath Proof Explorer

Theorem rlocval

Description: Expand the value of the ring localization operation. (Contributed by Thierry Arnoux, 4-May-2025)

Ref Expression
Hypotheses rlocval.1 
|- B = ( Base ` R )
rlocval.2 
|- .0. = ( 0g ` R )
rlocval.3 
|- .x. = ( .r ` R )
rlocval.4 
|- .- = ( -g ` R )
rlocval.5 
|- .+ = ( +g ` R )
rlocval.6 
|- .<_ = ( le ` R )
rlocval.7 
|- F = ( Scalar ` R )
rlocval.8 
|- K = ( Base ` F )
rlocval.9 
|- C = ( .s ` R )
rlocval.10 
|- W = ( B X. S )
rlocval.11 
|- .~ = ( R ~RL S )
rlocval.12 
|- J = ( TopSet ` R )
rlocval.13 
|- D = ( dist ` R )
rlocval.14 
|- .(+) = ( a e. W , b e. W |-> <. ( ( ( 1st ` a ) .x. ( 2nd ` b ) ) .+ ( ( 1st ` b ) .x. ( 2nd ` a ) ) ) , ( ( 2nd ` a ) .x. ( 2nd ` b ) ) >. )
rlocval.15 
|- .(x) = ( a e. W , b e. W |-> <. ( ( 1st ` a ) .x. ( 1st ` b ) ) , ( ( 2nd ` a ) .x. ( 2nd ` b ) ) >. )
rlocval.16 
|- .X. = ( k e. K , a e. W |-> <. ( k C ( 1st ` a ) ) , ( 2nd ` a ) >. )
rlocval.17 
|- .c_ = { <. a , b >. | ( ( a e. W /\ b e. W ) /\ ( ( 1st ` a ) .x. ( 2nd ` b ) ) .<_ ( ( 1st ` b ) .x. ( 2nd ` a ) ) ) }
rlocval.18 
|- E = ( a e. W , b e. W |-> ( ( ( 1st ` a ) .x. ( 2nd ` b ) ) D ( ( 1st ` b ) .x. ( 2nd ` a ) ) ) )
rlocval.19 
|- ( ph -> R e. V )
rlocval.20 
|- ( ph -> S C_ B )
Assertion rlocval 
|- ( ph -> ( R RLocal S ) = ( ( ( { <. ( Base ` ndx ) , W >. , <. ( +g ` ndx ) , .(+) >. , <. ( .r ` ndx ) , .(x) >. } u. { <. ( Scalar ` ndx ) , F >. , <. ( .s ` ndx ) , .X. >. , <. ( .i ` ndx ) , (/) >. } ) u. { <. ( TopSet ` ndx ) , ( J tX ( J |`t S ) ) >. , <. ( le ` ndx ) , .c_ >. , <. ( dist ` ndx ) , E >. } ) /s .~ ) )

Proof

Step Hyp Ref Expression
1 rlocval.1 
 |-  B = ( Base ` R )
2 rlocval.2 
 |-  .0. = ( 0g ` R )
3 rlocval.3 
 |-  .x. = ( .r ` R )
4 rlocval.4 
 |-  .- = ( -g ` R )
5 rlocval.5 
 |-  .+ = ( +g ` R )
6 rlocval.6 
 |-  .<_ = ( le ` R )
7 rlocval.7 
 |-  F = ( Scalar ` R )
8 rlocval.8 
 |-  K = ( Base ` F )
9 rlocval.9 
 |-  C = ( .s ` R )
10 rlocval.10 
 |-  W = ( B X. S )
11 rlocval.11 
 |-  .~ = ( R ~RL S )
12 rlocval.12 
 |-  J = ( TopSet ` R )
13 rlocval.13 
 |-  D = ( dist ` R )
14 rlocval.14 
 |-  .(+) = ( a e. W , b e. W |-> <. ( ( ( 1st ` a ) .x. ( 2nd ` b ) ) .+ ( ( 1st ` b ) .x. ( 2nd ` a ) ) ) , ( ( 2nd ` a ) .x. ( 2nd ` b ) ) >. )
15 rlocval.15 
 |-  .(x) = ( a e. W , b e. W |-> <. ( ( 1st ` a ) .x. ( 1st ` b ) ) , ( ( 2nd ` a ) .x. ( 2nd ` b ) ) >. )
16 rlocval.16 
 |-  .X. = ( k e. K , a e. W |-> <. ( k C ( 1st ` a ) ) , ( 2nd ` a ) >. )
17 rlocval.17 
 |-  .c_ = { <. a , b >. | ( ( a e. W /\ b e. W ) /\ ( ( 1st ` a ) .x. ( 2nd ` b ) ) .<_ ( ( 1st ` b ) .x. ( 2nd ` a ) ) ) }
18 rlocval.18 
 |-  E = ( a e. W , b e. W |-> ( ( ( 1st ` a ) .x. ( 2nd ` b ) ) D ( ( 1st ` b ) .x. ( 2nd ` a ) ) ) )
19 rlocval.19 
 |-  ( ph -> R e. V )
20 rlocval.20 
 |-  ( ph -> S C_ B )
21 19 elexd 
 |-  ( ph -> R e. _V )
22 1 fvexi 
 |-  B e. _V
23 22 a1i 
 |-  ( ph -> B e. _V )
24 23 20 ssexd 
 |-  ( ph -> S e. _V )
25 ovexd 
 |-  ( ph -> ( ( ( { <. ( Base ` ndx ) , W >. , <. ( +g ` ndx ) , .(+) >. , <. ( .r ` ndx ) , .(x) >. } u. { <. ( Scalar ` ndx ) , F >. , <. ( .s ` ndx ) , .X. >. , <. ( .i ` ndx ) , (/) >. } ) u. { <. ( TopSet ` ndx ) , ( J tX ( J |`t S ) ) >. , <. ( le ` ndx ) , .c_ >. , <. ( dist ` ndx ) , E >. } ) /s .~ ) e. _V )
26 fvexd 
 |-  ( ( r = R /\ s = S ) -> ( .r ` r ) e. _V )
27 fveq2 
 |-  ( r = R -> ( .r ` r ) = ( .r ` R ) )
28 27 adantr 
 |-  ( ( r = R /\ s = S ) -> ( .r ` r ) = ( .r ` R ) )
29 28 3 eqtr4di 
 |-  ( ( r = R /\ s = S ) -> ( .r ` r ) = .x. )
30 fvexd 
 |-  ( ( ( r = R /\ s = S ) /\ x = .x. ) -> ( Base ` r ) e. _V )
31 vex 
 |-  s e. _V
32 31 a1i 
 |-  ( ( ( r = R /\ s = S ) /\ x = .x. ) -> s e. _V )
33 30 32 xpexd 
 |-  ( ( ( r = R /\ s = S ) /\ x = .x. ) -> ( ( Base ` r ) X. s ) e. _V )
34 fveq2 
 |-  ( r = R -> ( Base ` r ) = ( Base ` R ) )
35 34 ad2antrr 
 |-  ( ( ( r = R /\ s = S ) /\ x = .x. ) -> ( Base ` r ) = ( Base ` R ) )
36 35 1 eqtr4di 
 |-  ( ( ( r = R /\ s = S ) /\ x = .x. ) -> ( Base ` r ) = B )
37 simplr 
 |-  ( ( ( r = R /\ s = S ) /\ x = .x. ) -> s = S )
38 36 37 xpeq12d 
 |-  ( ( ( r = R /\ s = S ) /\ x = .x. ) -> ( ( Base ` r ) X. s ) = ( B X. S ) )
39 38 10 eqtr4di 
 |-  ( ( ( r = R /\ s = S ) /\ x = .x. ) -> ( ( Base ` r ) X. s ) = W )
40 simpr 
 |-  ( ( ( ( r = R /\ s = S ) /\ x = .x. ) /\ w = W ) -> w = W )
41 40 opeq2d 
 |-  ( ( ( ( r = R /\ s = S ) /\ x = .x. ) /\ w = W ) -> <. ( Base ` ndx ) , w >. = <. ( Base ` ndx ) , W >. )
42 simplll 
 |-  ( ( ( ( r = R /\ s = S ) /\ x = .x. ) /\ w = W ) -> r = R )
43 42 fveq2d 
 |-  ( ( ( ( r = R /\ s = S ) /\ x = .x. ) /\ w = W ) -> ( +g ` r ) = ( +g ` R ) )
44 43 5 eqtr4di 
 |-  ( ( ( ( r = R /\ s = S ) /\ x = .x. ) /\ w = W ) -> ( +g ` r ) = .+ )
45 simplr 
 |-  ( ( ( ( r = R /\ s = S ) /\ x = .x. ) /\ w = W ) -> x = .x. )
46 45 oveqd 
 |-  ( ( ( ( r = R /\ s = S ) /\ x = .x. ) /\ w = W ) -> ( ( 1st ` a ) x ( 2nd ` b ) ) = ( ( 1st ` a ) .x. ( 2nd ` b ) ) )
47 45 oveqd 
 |-  ( ( ( ( r = R /\ s = S ) /\ x = .x. ) /\ w = W ) -> ( ( 1st ` b ) x ( 2nd ` a ) ) = ( ( 1st ` b ) .x. ( 2nd ` a ) ) )
48 44 46 47 oveq123d 
 |-  ( ( ( ( r = R /\ s = S ) /\ x = .x. ) /\ w = W ) -> ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( +g ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) = ( ( ( 1st ` a ) .x. ( 2nd ` b ) ) .+ ( ( 1st ` b ) .x. ( 2nd ` a ) ) ) )
49 45 oveqd 
 |-  ( ( ( ( r = R /\ s = S ) /\ x = .x. ) /\ w = W ) -> ( ( 2nd ` a ) x ( 2nd ` b ) ) = ( ( 2nd ` a ) .x. ( 2nd ` b ) ) )
50 48 49 opeq12d 
 |-  ( ( ( ( r = R /\ s = S ) /\ x = .x. ) /\ w = W ) -> <. ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( +g ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) , ( ( 2nd ` a ) x ( 2nd ` b ) ) >. = <. ( ( ( 1st ` a ) .x. ( 2nd ` b ) ) .+ ( ( 1st ` b ) .x. ( 2nd ` a ) ) ) , ( ( 2nd ` a ) .x. ( 2nd ` b ) ) >. )
51 40 40 50 mpoeq123dv 
 |-  ( ( ( ( r = R /\ s = S ) /\ x = .x. ) /\ w = W ) -> ( a e. w , b e. w |-> <. ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( +g ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) , ( ( 2nd ` a ) x ( 2nd ` b ) ) >. ) = ( a e. W , b e. W |-> <. ( ( ( 1st ` a ) .x. ( 2nd ` b ) ) .+ ( ( 1st ` b ) .x. ( 2nd ` a ) ) ) , ( ( 2nd ` a ) .x. ( 2nd ` b ) ) >. ) )
52 51 14 eqtr4di 
 |-  ( ( ( ( r = R /\ s = S ) /\ x = .x. ) /\ w = W ) -> ( a e. w , b e. w |-> <. ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( +g ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) , ( ( 2nd ` a ) x ( 2nd ` b ) ) >. ) = .(+) )
53 52 opeq2d 
 |-  ( ( ( ( r = R /\ s = S ) /\ x = .x. ) /\ w = W ) -> <. ( +g ` ndx ) , ( a e. w , b e. w |-> <. ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( +g ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) , ( ( 2nd ` a ) x ( 2nd ` b ) ) >. ) >. = <. ( +g ` ndx ) , .(+) >. )
54 45 oveqd 
 |-  ( ( ( ( r = R /\ s = S ) /\ x = .x. ) /\ w = W ) -> ( ( 1st ` a ) x ( 1st ` b ) ) = ( ( 1st ` a ) .x. ( 1st ` b ) ) )
55 54 49 opeq12d 
 |-  ( ( ( ( r = R /\ s = S ) /\ x = .x. ) /\ w = W ) -> <. ( ( 1st ` a ) x ( 1st ` b ) ) , ( ( 2nd ` a ) x ( 2nd ` b ) ) >. = <. ( ( 1st ` a ) .x. ( 1st ` b ) ) , ( ( 2nd ` a ) .x. ( 2nd ` b ) ) >. )
56 40 40 55 mpoeq123dv 
 |-  ( ( ( ( r = R /\ s = S ) /\ x = .x. ) /\ w = W ) -> ( a e. w , b e. w |-> <. ( ( 1st ` a ) x ( 1st ` b ) ) , ( ( 2nd ` a ) x ( 2nd ` b ) ) >. ) = ( a e. W , b e. W |-> <. ( ( 1st ` a ) .x. ( 1st ` b ) ) , ( ( 2nd ` a ) .x. ( 2nd ` b ) ) >. ) )
57 56 15 eqtr4di 
 |-  ( ( ( ( r = R /\ s = S ) /\ x = .x. ) /\ w = W ) -> ( a e. w , b e. w |-> <. ( ( 1st ` a ) x ( 1st ` b ) ) , ( ( 2nd ` a ) x ( 2nd ` b ) ) >. ) = .(x) )
58 57 opeq2d 
 |-  ( ( ( ( r = R /\ s = S ) /\ x = .x. ) /\ w = W ) -> <. ( .r ` ndx ) , ( a e. w , b e. w |-> <. ( ( 1st ` a ) x ( 1st ` b ) ) , ( ( 2nd ` a ) x ( 2nd ` b ) ) >. ) >. = <. ( .r ` ndx ) , .(x) >. )
59 41 53 58 tpeq123d 
 |-  ( ( ( ( r = R /\ s = S ) /\ x = .x. ) /\ w = W ) -> { <. ( Base ` ndx ) , w >. , <. ( +g ` ndx ) , ( a e. w , b e. w |-> <. ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( +g ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) , ( ( 2nd ` a ) x ( 2nd ` b ) ) >. ) >. , <. ( .r ` ndx ) , ( a e. w , b e. w |-> <. ( ( 1st ` a ) x ( 1st ` b ) ) , ( ( 2nd ` a ) x ( 2nd ` b ) ) >. ) >. } = { <. ( Base ` ndx ) , W >. , <. ( +g ` ndx ) , .(+) >. , <. ( .r ` ndx ) , .(x) >. } )
60 42 fveq2d 
 |-  ( ( ( ( r = R /\ s = S ) /\ x = .x. ) /\ w = W ) -> ( Scalar ` r ) = ( Scalar ` R ) )
61 60 7 eqtr4di 
 |-  ( ( ( ( r = R /\ s = S ) /\ x = .x. ) /\ w = W ) -> ( Scalar ` r ) = F )
62 61 opeq2d 
 |-  ( ( ( ( r = R /\ s = S ) /\ x = .x. ) /\ w = W ) -> <. ( Scalar ` ndx ) , ( Scalar ` r ) >. = <. ( Scalar ` ndx ) , F >. )
63 60 fveq2d 
 |-  ( ( ( ( r = R /\ s = S ) /\ x = .x. ) /\ w = W ) -> ( Base ` ( Scalar ` r ) ) = ( Base ` ( Scalar ` R ) ) )
64 7 fveq2i 
 |-  ( Base ` F ) = ( Base ` ( Scalar ` R ) )
65 8 64 eqtri 
 |-  K = ( Base ` ( Scalar ` R ) )
66 63 65 eqtr4di 
 |-  ( ( ( ( r = R /\ s = S ) /\ x = .x. ) /\ w = W ) -> ( Base ` ( Scalar ` r ) ) = K )
67 42 fveq2d 
 |-  ( ( ( ( r = R /\ s = S ) /\ x = .x. ) /\ w = W ) -> ( .s ` r ) = ( .s ` R ) )
68 67 9 eqtr4di 
 |-  ( ( ( ( r = R /\ s = S ) /\ x = .x. ) /\ w = W ) -> ( .s ` r ) = C )
69 68 oveqd 
 |-  ( ( ( ( r = R /\ s = S ) /\ x = .x. ) /\ w = W ) -> ( k ( .s ` r ) ( 1st ` a ) ) = ( k C ( 1st ` a ) ) )
70 69 opeq1d 
 |-  ( ( ( ( r = R /\ s = S ) /\ x = .x. ) /\ w = W ) -> <. ( k ( .s ` r ) ( 1st ` a ) ) , ( 2nd ` a ) >. = <. ( k C ( 1st ` a ) ) , ( 2nd ` a ) >. )
71 66 40 70 mpoeq123dv 
 |-  ( ( ( ( r = R /\ s = S ) /\ x = .x. ) /\ w = W ) -> ( k e. ( Base ` ( Scalar ` r ) ) , a e. w |-> <. ( k ( .s ` r ) ( 1st ` a ) ) , ( 2nd ` a ) >. ) = ( k e. K , a e. W |-> <. ( k C ( 1st ` a ) ) , ( 2nd ` a ) >. ) )
72 71 16 eqtr4di 
 |-  ( ( ( ( r = R /\ s = S ) /\ x = .x. ) /\ w = W ) -> ( k e. ( Base ` ( Scalar ` r ) ) , a e. w |-> <. ( k ( .s ` r ) ( 1st ` a ) ) , ( 2nd ` a ) >. ) = .X. )
73 72 opeq2d 
 |-  ( ( ( ( r = R /\ s = S ) /\ x = .x. ) /\ w = W ) -> <. ( .s ` ndx ) , ( k e. ( Base ` ( Scalar ` r ) ) , a e. w |-> <. ( k ( .s ` r ) ( 1st ` a ) ) , ( 2nd ` a ) >. ) >. = <. ( .s ` ndx ) , .X. >. )
74 eqidd 
 |-  ( ( ( ( r = R /\ s = S ) /\ x = .x. ) /\ w = W ) -> <. ( .i ` ndx ) , (/) >. = <. ( .i ` ndx ) , (/) >. )
75 62 73 74 tpeq123d 
 |-  ( ( ( ( r = R /\ s = S ) /\ x = .x. ) /\ w = W ) -> { <. ( Scalar ` ndx ) , ( Scalar ` r ) >. , <. ( .s ` ndx ) , ( k e. ( Base ` ( Scalar ` r ) ) , a e. w |-> <. ( k ( .s ` r ) ( 1st ` a ) ) , ( 2nd ` a ) >. ) >. , <. ( .i ` ndx ) , (/) >. } = { <. ( Scalar ` ndx ) , F >. , <. ( .s ` ndx ) , .X. >. , <. ( .i ` ndx ) , (/) >. } )
76 59 75 uneq12d 
 |-  ( ( ( ( r = R /\ s = S ) /\ x = .x. ) /\ w = W ) -> ( { <. ( Base ` ndx ) , w >. , <. ( +g ` ndx ) , ( a e. w , b e. w |-> <. ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( +g ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) , ( ( 2nd ` a ) x ( 2nd ` b ) ) >. ) >. , <. ( .r ` ndx ) , ( a e. w , b e. w |-> <. ( ( 1st ` a ) x ( 1st ` b ) ) , ( ( 2nd ` a ) x ( 2nd ` b ) ) >. ) >. } u. { <. ( Scalar ` ndx ) , ( Scalar ` r ) >. , <. ( .s ` ndx ) , ( k e. ( Base ` ( Scalar ` r ) ) , a e. w |-> <. ( k ( .s ` r ) ( 1st ` a ) ) , ( 2nd ` a ) >. ) >. , <. ( .i ` ndx ) , (/) >. } ) = ( { <. ( Base ` ndx ) , W >. , <. ( +g ` ndx ) , .(+) >. , <. ( .r ` ndx ) , .(x) >. } u. { <. ( Scalar ` ndx ) , F >. , <. ( .s ` ndx ) , .X. >. , <. ( .i ` ndx ) , (/) >. } ) )
77 42 fveq2d 
 |-  ( ( ( ( r = R /\ s = S ) /\ x = .x. ) /\ w = W ) -> ( TopSet ` r ) = ( TopSet ` R ) )
78 77 12 eqtr4di 
 |-  ( ( ( ( r = R /\ s = S ) /\ x = .x. ) /\ w = W ) -> ( TopSet ` r ) = J )
79 37 adantr 
 |-  ( ( ( ( r = R /\ s = S ) /\ x = .x. ) /\ w = W ) -> s = S )
80 78 79 oveq12d 
 |-  ( ( ( ( r = R /\ s = S ) /\ x = .x. ) /\ w = W ) -> ( ( TopSet ` r ) |`t s ) = ( J |`t S ) )
81 78 80 oveq12d 
 |-  ( ( ( ( r = R /\ s = S ) /\ x = .x. ) /\ w = W ) -> ( ( TopSet ` r ) tX ( ( TopSet ` r ) |`t s ) ) = ( J tX ( J |`t S ) ) )
82 81 opeq2d 
 |-  ( ( ( ( r = R /\ s = S ) /\ x = .x. ) /\ w = W ) -> <. ( TopSet ` ndx ) , ( ( TopSet ` r ) tX ( ( TopSet ` r ) |`t s ) ) >. = <. ( TopSet ` ndx ) , ( J tX ( J |`t S ) ) >. )
83 40 eleq2d 
 |-  ( ( ( ( r = R /\ s = S ) /\ x = .x. ) /\ w = W ) -> ( a e. w <-> a e. W ) )
84 40 eleq2d 
 |-  ( ( ( ( r = R /\ s = S ) /\ x = .x. ) /\ w = W ) -> ( b e. w <-> b e. W ) )
85 83 84 anbi12d 
 |-  ( ( ( ( r = R /\ s = S ) /\ x = .x. ) /\ w = W ) -> ( ( a e. w /\ b e. w ) <-> ( a e. W /\ b e. W ) ) )
86 42 fveq2d 
 |-  ( ( ( ( r = R /\ s = S ) /\ x = .x. ) /\ w = W ) -> ( le ` r ) = ( le ` R ) )
87 86 6 eqtr4di 
 |-  ( ( ( ( r = R /\ s = S ) /\ x = .x. ) /\ w = W ) -> ( le ` r ) = .<_ )
88 46 87 47 breq123d 
 |-  ( ( ( ( r = R /\ s = S ) /\ x = .x. ) /\ w = W ) -> ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( le ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) <-> ( ( 1st ` a ) .x. ( 2nd ` b ) ) .<_ ( ( 1st ` b ) .x. ( 2nd ` a ) ) ) )
89 85 88 anbi12d 
 |-  ( ( ( ( r = R /\ s = S ) /\ x = .x. ) /\ w = W ) -> ( ( ( a e. w /\ b e. w ) /\ ( ( 1st ` a ) x ( 2nd ` b ) ) ( le ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) <-> ( ( a e. W /\ b e. W ) /\ ( ( 1st ` a ) .x. ( 2nd ` b ) ) .<_ ( ( 1st ` b ) .x. ( 2nd ` a ) ) ) ) )
90 89 opabbidv 
 |-  ( ( ( ( r = R /\ s = S ) /\ x = .x. ) /\ w = W ) -> { <. a , b >. | ( ( a e. w /\ b e. w ) /\ ( ( 1st ` a ) x ( 2nd ` b ) ) ( le ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) } = { <. a , b >. | ( ( a e. W /\ b e. W ) /\ ( ( 1st ` a ) .x. ( 2nd ` b ) ) .<_ ( ( 1st ` b ) .x. ( 2nd ` a ) ) ) } )
91 90 17 eqtr4di 
 |-  ( ( ( ( r = R /\ s = S ) /\ x = .x. ) /\ w = W ) -> { <. a , b >. | ( ( a e. w /\ b e. w ) /\ ( ( 1st ` a ) x ( 2nd ` b ) ) ( le ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) } = .c_ )
92 91 opeq2d 
 |-  ( ( ( ( r = R /\ s = S ) /\ x = .x. ) /\ w = W ) -> <. ( le ` ndx ) , { <. a , b >. | ( ( a e. w /\ b e. w ) /\ ( ( 1st ` a ) x ( 2nd ` b ) ) ( le ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) } >. = <. ( le ` ndx ) , .c_ >. )
93 42 fveq2d 
 |-  ( ( ( ( r = R /\ s = S ) /\ x = .x. ) /\ w = W ) -> ( dist ` r ) = ( dist ` R ) )
94 93 13 eqtr4di 
 |-  ( ( ( ( r = R /\ s = S ) /\ x = .x. ) /\ w = W ) -> ( dist ` r ) = D )
95 94 46 47 oveq123d 
 |-  ( ( ( ( r = R /\ s = S ) /\ x = .x. ) /\ w = W ) -> ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( dist ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) = ( ( ( 1st ` a ) .x. ( 2nd ` b ) ) D ( ( 1st ` b ) .x. ( 2nd ` a ) ) ) )
96 40 40 95 mpoeq123dv 
 |-  ( ( ( ( r = R /\ s = S ) /\ x = .x. ) /\ w = W ) -> ( a e. w , b e. w |-> ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( dist ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) ) = ( a e. W , b e. W |-> ( ( ( 1st ` a ) .x. ( 2nd ` b ) ) D ( ( 1st ` b ) .x. ( 2nd ` a ) ) ) ) )
97 96 18 eqtr4di 
 |-  ( ( ( ( r = R /\ s = S ) /\ x = .x. ) /\ w = W ) -> ( a e. w , b e. w |-> ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( dist ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) ) = E )
98 97 opeq2d 
 |-  ( ( ( ( r = R /\ s = S ) /\ x = .x. ) /\ w = W ) -> <. ( dist ` ndx ) , ( a e. w , b e. w |-> ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( dist ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) ) >. = <. ( dist ` ndx ) , E >. )
99 82 92 98 tpeq123d 
 |-  ( ( ( ( r = R /\ s = S ) /\ x = .x. ) /\ w = W ) -> { <. ( TopSet ` ndx ) , ( ( TopSet ` r ) tX ( ( TopSet ` r ) |`t s ) ) >. , <. ( le ` ndx ) , { <. a , b >. | ( ( a e. w /\ b e. w ) /\ ( ( 1st ` a ) x ( 2nd ` b ) ) ( le ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) } >. , <. ( dist ` ndx ) , ( a e. w , b e. w |-> ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( dist ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) ) >. } = { <. ( TopSet ` ndx ) , ( J tX ( J |`t S ) ) >. , <. ( le ` ndx ) , .c_ >. , <. ( dist ` ndx ) , E >. } )
100 76 99 uneq12d 
 |-  ( ( ( ( r = R /\ s = S ) /\ x = .x. ) /\ w = W ) -> ( ( { <. ( Base ` ndx ) , w >. , <. ( +g ` ndx ) , ( a e. w , b e. w |-> <. ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( +g ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) , ( ( 2nd ` a ) x ( 2nd ` b ) ) >. ) >. , <. ( .r ` ndx ) , ( a e. w , b e. w |-> <. ( ( 1st ` a ) x ( 1st ` b ) ) , ( ( 2nd ` a ) x ( 2nd ` b ) ) >. ) >. } u. { <. ( Scalar ` ndx ) , ( Scalar ` r ) >. , <. ( .s ` ndx ) , ( k e. ( Base ` ( Scalar ` r ) ) , a e. w |-> <. ( k ( .s ` r ) ( 1st ` a ) ) , ( 2nd ` a ) >. ) >. , <. ( .i ` ndx ) , (/) >. } ) u. { <. ( TopSet ` ndx ) , ( ( TopSet ` r ) tX ( ( TopSet ` r ) |`t s ) ) >. , <. ( le ` ndx ) , { <. a , b >. | ( ( a e. w /\ b e. w ) /\ ( ( 1st ` a ) x ( 2nd ` b ) ) ( le ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) } >. , <. ( dist ` ndx ) , ( a e. w , b e. w |-> ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( dist ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) ) >. } ) = ( ( { <. ( Base ` ndx ) , W >. , <. ( +g ` ndx ) , .(+) >. , <. ( .r ` ndx ) , .(x) >. } u. { <. ( Scalar ` ndx ) , F >. , <. ( .s ` ndx ) , .X. >. , <. ( .i ` ndx ) , (/) >. } ) u. { <. ( TopSet ` ndx ) , ( J tX ( J |`t S ) ) >. , <. ( le ` ndx ) , .c_ >. , <. ( dist ` ndx ) , E >. } ) )
101 42 79 oveq12d 
 |-  ( ( ( ( r = R /\ s = S ) /\ x = .x. ) /\ w = W ) -> ( r ~RL s ) = ( R ~RL S ) )
102 101 11 eqtr4di 
 |-  ( ( ( ( r = R /\ s = S ) /\ x = .x. ) /\ w = W ) -> ( r ~RL s ) = .~ )
103 100 102 oveq12d 
 |-  ( ( ( ( r = R /\ s = S ) /\ x = .x. ) /\ w = W ) -> ( ( ( { <. ( Base ` ndx ) , w >. , <. ( +g ` ndx ) , ( a e. w , b e. w |-> <. ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( +g ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) , ( ( 2nd ` a ) x ( 2nd ` b ) ) >. ) >. , <. ( .r ` ndx ) , ( a e. w , b e. w |-> <. ( ( 1st ` a ) x ( 1st ` b ) ) , ( ( 2nd ` a ) x ( 2nd ` b ) ) >. ) >. } u. { <. ( Scalar ` ndx ) , ( Scalar ` r ) >. , <. ( .s ` ndx ) , ( k e. ( Base ` ( Scalar ` r ) ) , a e. w |-> <. ( k ( .s ` r ) ( 1st ` a ) ) , ( 2nd ` a ) >. ) >. , <. ( .i ` ndx ) , (/) >. } ) u. { <. ( TopSet ` ndx ) , ( ( TopSet ` r ) tX ( ( TopSet ` r ) |`t s ) ) >. , <. ( le ` ndx ) , { <. a , b >. | ( ( a e. w /\ b e. w ) /\ ( ( 1st ` a ) x ( 2nd ` b ) ) ( le ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) } >. , <. ( dist ` ndx ) , ( a e. w , b e. w |-> ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( dist ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) ) >. } ) /s ( r ~RL s ) ) = ( ( ( { <. ( Base ` ndx ) , W >. , <. ( +g ` ndx ) , .(+) >. , <. ( .r ` ndx ) , .(x) >. } u. { <. ( Scalar ` ndx ) , F >. , <. ( .s ` ndx ) , .X. >. , <. ( .i ` ndx ) , (/) >. } ) u. { <. ( TopSet ` ndx ) , ( J tX ( J |`t S ) ) >. , <. ( le ` ndx ) , .c_ >. , <. ( dist ` ndx ) , E >. } ) /s .~ ) )
104 33 39 103 csbied2 
 |-  ( ( ( r = R /\ s = S ) /\ x = .x. ) -> [_ ( ( Base ` r ) X. s ) / w ]_ ( ( ( { <. ( Base ` ndx ) , w >. , <. ( +g ` ndx ) , ( a e. w , b e. w |-> <. ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( +g ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) , ( ( 2nd ` a ) x ( 2nd ` b ) ) >. ) >. , <. ( .r ` ndx ) , ( a e. w , b e. w |-> <. ( ( 1st ` a ) x ( 1st ` b ) ) , ( ( 2nd ` a ) x ( 2nd ` b ) ) >. ) >. } u. { <. ( Scalar ` ndx ) , ( Scalar ` r ) >. , <. ( .s ` ndx ) , ( k e. ( Base ` ( Scalar ` r ) ) , a e. w |-> <. ( k ( .s ` r ) ( 1st ` a ) ) , ( 2nd ` a ) >. ) >. , <. ( .i ` ndx ) , (/) >. } ) u. { <. ( TopSet ` ndx ) , ( ( TopSet ` r ) tX ( ( TopSet ` r ) |`t s ) ) >. , <. ( le ` ndx ) , { <. a , b >. | ( ( a e. w /\ b e. w ) /\ ( ( 1st ` a ) x ( 2nd ` b ) ) ( le ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) } >. , <. ( dist ` ndx ) , ( a e. w , b e. w |-> ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( dist ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) ) >. } ) /s ( r ~RL s ) ) = ( ( ( { <. ( Base ` ndx ) , W >. , <. ( +g ` ndx ) , .(+) >. , <. ( .r ` ndx ) , .(x) >. } u. { <. ( Scalar ` ndx ) , F >. , <. ( .s ` ndx ) , .X. >. , <. ( .i ` ndx ) , (/) >. } ) u. { <. ( TopSet ` ndx ) , ( J tX ( J |`t S ) ) >. , <. ( le ` ndx ) , .c_ >. , <. ( dist ` ndx ) , E >. } ) /s .~ ) )
105 26 29 104 csbied2 
 |-  ( ( r = R /\ s = S ) -> [_ ( .r ` r ) / x ]_ [_ ( ( Base ` r ) X. s ) / w ]_ ( ( ( { <. ( Base ` ndx ) , w >. , <. ( +g ` ndx ) , ( a e. w , b e. w |-> <. ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( +g ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) , ( ( 2nd ` a ) x ( 2nd ` b ) ) >. ) >. , <. ( .r ` ndx ) , ( a e. w , b e. w |-> <. ( ( 1st ` a ) x ( 1st ` b ) ) , ( ( 2nd ` a ) x ( 2nd ` b ) ) >. ) >. } u. { <. ( Scalar ` ndx ) , ( Scalar ` r ) >. , <. ( .s ` ndx ) , ( k e. ( Base ` ( Scalar ` r ) ) , a e. w |-> <. ( k ( .s ` r ) ( 1st ` a ) ) , ( 2nd ` a ) >. ) >. , <. ( .i ` ndx ) , (/) >. } ) u. { <. ( TopSet ` ndx ) , ( ( TopSet ` r ) tX ( ( TopSet ` r ) |`t s ) ) >. , <. ( le ` ndx ) , { <. a , b >. | ( ( a e. w /\ b e. w ) /\ ( ( 1st ` a ) x ( 2nd ` b ) ) ( le ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) } >. , <. ( dist ` ndx ) , ( a e. w , b e. w |-> ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( dist ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) ) >. } ) /s ( r ~RL s ) ) = ( ( ( { <. ( Base ` ndx ) , W >. , <. ( +g ` ndx ) , .(+) >. , <. ( .r ` ndx ) , .(x) >. } u. { <. ( Scalar ` ndx ) , F >. , <. ( .s ` ndx ) , .X. >. , <. ( .i ` ndx ) , (/) >. } ) u. { <. ( TopSet ` ndx ) , ( J tX ( J |`t S ) ) >. , <. ( le ` ndx ) , .c_ >. , <. ( dist ` ndx ) , E >. } ) /s .~ ) )
106 df-rloc 
 |-  RLocal = ( r e. _V , s e. _V |-> [_ ( .r ` r ) / x ]_ [_ ( ( Base ` r ) X. s ) / w ]_ ( ( ( { <. ( Base ` ndx ) , w >. , <. ( +g ` ndx ) , ( a e. w , b e. w |-> <. ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( +g ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) , ( ( 2nd ` a ) x ( 2nd ` b ) ) >. ) >. , <. ( .r ` ndx ) , ( a e. w , b e. w |-> <. ( ( 1st ` a ) x ( 1st ` b ) ) , ( ( 2nd ` a ) x ( 2nd ` b ) ) >. ) >. } u. { <. ( Scalar ` ndx ) , ( Scalar ` r ) >. , <. ( .s ` ndx ) , ( k e. ( Base ` ( Scalar ` r ) ) , a e. w |-> <. ( k ( .s ` r ) ( 1st ` a ) ) , ( 2nd ` a ) >. ) >. , <. ( .i ` ndx ) , (/) >. } ) u. { <. ( TopSet ` ndx ) , ( ( TopSet ` r ) tX ( ( TopSet ` r ) |`t s ) ) >. , <. ( le ` ndx ) , { <. a , b >. | ( ( a e. w /\ b e. w ) /\ ( ( 1st ` a ) x ( 2nd ` b ) ) ( le ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) } >. , <. ( dist ` ndx ) , ( a e. w , b e. w |-> ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( dist ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) ) >. } ) /s ( r ~RL s ) ) )
107 105 106 ovmpoga 
 |-  ( ( R e. _V /\ S e. _V /\ ( ( ( { <. ( Base ` ndx ) , W >. , <. ( +g ` ndx ) , .(+) >. , <. ( .r ` ndx ) , .(x) >. } u. { <. ( Scalar ` ndx ) , F >. , <. ( .s ` ndx ) , .X. >. , <. ( .i ` ndx ) , (/) >. } ) u. { <. ( TopSet ` ndx ) , ( J tX ( J |`t S ) ) >. , <. ( le ` ndx ) , .c_ >. , <. ( dist ` ndx ) , E >. } ) /s .~ ) e. _V ) -> ( R RLocal S ) = ( ( ( { <. ( Base ` ndx ) , W >. , <. ( +g ` ndx ) , .(+) >. , <. ( .r ` ndx ) , .(x) >. } u. { <. ( Scalar ` ndx ) , F >. , <. ( .s ` ndx ) , .X. >. , <. ( .i ` ndx ) , (/) >. } ) u. { <. ( TopSet ` ndx ) , ( J tX ( J |`t S ) ) >. , <. ( le ` ndx ) , .c_ >. , <. ( dist ` ndx ) , E >. } ) /s .~ ) )
108 21 24 25 107 syl3anc 
 |-  ( ph -> ( R RLocal S ) = ( ( ( { <. ( Base ` ndx ) , W >. , <. ( +g ` ndx ) , .(+) >. , <. ( .r ` ndx ) , .(x) >. } u. { <. ( Scalar ` ndx ) , F >. , <. ( .s ` ndx ) , .X. >. , <. ( .i ` ndx ) , (/) >. } ) u. { <. ( TopSet ` ndx ) , ( J tX ( J |`t S ) ) >. , <. ( le ` ndx ) , .c_ >. , <. ( dist ` ndx ) , E >. } ) /s .~ ) )