Metamath Proof Explorer

Theorem erlval

Description: Value of the ring localization equivalence relation. (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 )
erlval.w 
|- W = ( B X. S )
erlval.q 
|- .~ = { <. a , b >. | ( ( a e. W /\ b e. W ) /\ E. t e. S ( t .x. ( ( ( 1st ` a ) .x. ( 2nd ` b ) ) .- ( ( 1st ` b ) .x. ( 2nd ` a ) ) ) ) = .0. ) }
erlval.20 
|- ( ph -> S C_ B )
Assertion erlval 
|- ( ph -> ( R ~RL 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 erlval.w 
 |-  W = ( B X. S )
6 erlval.q 
 |-  .~ = { <. a , b >. | ( ( a e. W /\ b e. W ) /\ E. t e. S ( t .x. ( ( ( 1st ` a ) .x. ( 2nd ` b ) ) .- ( ( 1st ` b ) .x. ( 2nd ` a ) ) ) ) = .0. ) }
7 erlval.20 
 |-  ( ph -> S C_ B )
8 simpr 
 |-  ( ( ph /\ R e. _V ) -> R e. _V )
9 1 fvexi 
 |-  B e. _V
10 9 a1i 
 |-  ( ( ph /\ R e. _V ) -> B e. _V )
11 7 adantr 
 |-  ( ( ph /\ R e. _V ) -> S C_ B )
12 10 11 ssexd 
 |-  ( ( ph /\ R e. _V ) -> S e. _V )
13 10 12 xpexd 
 |-  ( ( ph /\ R e. _V ) -> ( B X. S ) e. _V )
14 5 13 eqeltrid 
 |-  ( ( ph /\ R e. _V ) -> W e. _V )
15 14 14 xpexd 
 |-  ( ( ph /\ R e. _V ) -> ( W X. W ) e. _V )
16 simprll 
 |-  ( ( ph /\ ( ( a e. W /\ b e. W ) /\ E. t e. S ( t .x. ( ( ( 1st ` a ) .x. ( 2nd ` b ) ) .- ( ( 1st ` b ) .x. ( 2nd ` a ) ) ) ) = .0. ) ) -> a e. W )
17 simprlr 
 |-  ( ( ph /\ ( ( a e. W /\ b e. W ) /\ E. t e. S ( t .x. ( ( ( 1st ` a ) .x. ( 2nd ` b ) ) .- ( ( 1st ` b ) .x. ( 2nd ` a ) ) ) ) = .0. ) ) -> b e. W )
18 16 17 opabssxpd 
 |-  ( ph -> { <. a , b >. | ( ( a e. W /\ b e. W ) /\ E. t e. S ( t .x. ( ( ( 1st ` a ) .x. ( 2nd ` b ) ) .- ( ( 1st ` b ) .x. ( 2nd ` a ) ) ) ) = .0. ) } C_ ( W X. W ) )
19 18 adantr 
 |-  ( ( ph /\ R e. _V ) -> { <. a , b >. | ( ( a e. W /\ b e. W ) /\ E. t e. S ( t .x. ( ( ( 1st ` a ) .x. ( 2nd ` b ) ) .- ( ( 1st ` b ) .x. ( 2nd ` a ) ) ) ) = .0. ) } C_ ( W X. W ) )
20 15 19 ssexd 
 |-  ( ( ph /\ R e. _V ) -> { <. a , b >. | ( ( a e. W /\ b e. W ) /\ E. t e. S ( t .x. ( ( ( 1st ` a ) .x. ( 2nd ` b ) ) .- ( ( 1st ` b ) .x. ( 2nd ` a ) ) ) ) = .0. ) } e. _V )
21 6 20 eqeltrid 
 |-  ( ( ph /\ R e. _V ) -> .~ e. _V )
22 fvexd 
 |-  ( ( r = R /\ s = S ) -> ( .r ` r ) e. _V )
23 fveq2 
 |-  ( r = R -> ( .r ` r ) = ( .r ` R ) )
24 23 adantr 
 |-  ( ( r = R /\ s = S ) -> ( .r ` r ) = ( .r ` R ) )
25 24 3 eqtr4di 
 |-  ( ( r = R /\ s = S ) -> ( .r ` r ) = .x. )
26 fvexd 
 |-  ( ( ( r = R /\ s = S ) /\ x = .x. ) -> ( Base ` r ) e. _V )
27 vex 
 |-  s e. _V
28 27 a1i 
 |-  ( ( ( r = R /\ s = S ) /\ x = .x. ) -> s e. _V )
29 26 28 xpexd 
 |-  ( ( ( r = R /\ s = S ) /\ x = .x. ) -> ( ( Base ` r ) X. s ) e. _V )
30 fveq2 
 |-  ( r = R -> ( Base ` r ) = ( Base ` R ) )
31 30 ad2antrr 
 |-  ( ( ( r = R /\ s = S ) /\ x = .x. ) -> ( Base ` r ) = ( Base ` R ) )
32 31 1 eqtr4di 
 |-  ( ( ( r = R /\ s = S ) /\ x = .x. ) -> ( Base ` r ) = B )
33 simplr 
 |-  ( ( ( r = R /\ s = S ) /\ x = .x. ) -> s = S )
34 32 33 xpeq12d 
 |-  ( ( ( r = R /\ s = S ) /\ x = .x. ) -> ( ( Base ` r ) X. s ) = ( B X. S ) )
35 34 5 eqtr4di 
 |-  ( ( ( r = R /\ s = S ) /\ x = .x. ) -> ( ( Base ` r ) X. s ) = W )
36 simpr 
 |-  ( ( ( ( r = R /\ s = S ) /\ x = .x. ) /\ w = W ) -> w = W )
37 36 eleq2d 
 |-  ( ( ( ( r = R /\ s = S ) /\ x = .x. ) /\ w = W ) -> ( a e. w <-> a e. W ) )
38 36 eleq2d 
 |-  ( ( ( ( r = R /\ s = S ) /\ x = .x. ) /\ w = W ) -> ( b e. w <-> b e. W ) )
39 37 38 anbi12d 
 |-  ( ( ( ( r = R /\ s = S ) /\ x = .x. ) /\ w = W ) -> ( ( a e. w /\ b e. w ) <-> ( a e. W /\ b e. W ) ) )
40 33 adantr 
 |-  ( ( ( ( r = R /\ s = S ) /\ x = .x. ) /\ w = W ) -> s = S )
41 simplr 
 |-  ( ( ( ( r = R /\ s = S ) /\ x = .x. ) /\ w = W ) -> x = .x. )
42 eqidd 
 |-  ( ( ( ( r = R /\ s = S ) /\ x = .x. ) /\ w = W ) -> t = t )
43 fveq2 
 |-  ( r = R -> ( -g ` r ) = ( -g ` R ) )
44 43 ad3antrrr 
 |-  ( ( ( ( r = R /\ s = S ) /\ x = .x. ) /\ w = W ) -> ( -g ` r ) = ( -g ` R ) )
45 44 4 eqtr4di 
 |-  ( ( ( ( r = R /\ s = S ) /\ x = .x. ) /\ w = W ) -> ( -g ` r ) = .- )
46 41 oveqd 
 |-  ( ( ( ( r = R /\ s = S ) /\ x = .x. ) /\ w = W ) -> ( ( 1st ` a ) x ( 2nd ` b ) ) = ( ( 1st ` a ) .x. ( 2nd ` b ) ) )
47 41 oveqd 
 |-  ( ( ( ( r = R /\ s = S ) /\ x = .x. ) /\ w = W ) -> ( ( 1st ` b ) x ( 2nd ` a ) ) = ( ( 1st ` b ) .x. ( 2nd ` a ) ) )
48 45 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 41 42 48 oveq123d 
 |-  ( ( ( ( r = R /\ s = S ) /\ x = .x. ) /\ w = W ) -> ( t x ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( -g ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) ) = ( t .x. ( ( ( 1st ` a ) .x. ( 2nd ` b ) ) .- ( ( 1st ` b ) .x. ( 2nd ` a ) ) ) ) )
50 fveq2 
 |-  ( r = R -> ( 0g ` r ) = ( 0g ` R ) )
51 50 ad3antrrr 
 |-  ( ( ( ( r = R /\ s = S ) /\ x = .x. ) /\ w = W ) -> ( 0g ` r ) = ( 0g ` R ) )
52 51 2 eqtr4di 
 |-  ( ( ( ( r = R /\ s = S ) /\ x = .x. ) /\ w = W ) -> ( 0g ` r ) = .0. )
53 49 52 eqeq12d 
 |-  ( ( ( ( r = R /\ s = S ) /\ x = .x. ) /\ w = W ) -> ( ( t x ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( -g ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) ) = ( 0g ` r ) <-> ( t .x. ( ( ( 1st ` a ) .x. ( 2nd ` b ) ) .- ( ( 1st ` b ) .x. ( 2nd ` a ) ) ) ) = .0. ) )
54 40 53 rexeqbidv 
 |-  ( ( ( ( r = R /\ s = S ) /\ x = .x. ) /\ w = W ) -> ( E. t e. s ( t x ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( -g ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) ) = ( 0g ` r ) <-> E. t e. S ( t .x. ( ( ( 1st ` a ) .x. ( 2nd ` b ) ) .- ( ( 1st ` b ) .x. ( 2nd ` a ) ) ) ) = .0. ) )
55 39 54 anbi12d 
 |-  ( ( ( ( r = R /\ s = S ) /\ x = .x. ) /\ w = W ) -> ( ( ( a e. w /\ b e. w ) /\ E. t e. s ( t x ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( -g ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) ) = ( 0g ` r ) ) <-> ( ( a e. W /\ b e. W ) /\ E. t e. S ( t .x. ( ( ( 1st ` a ) .x. ( 2nd ` b ) ) .- ( ( 1st ` b ) .x. ( 2nd ` a ) ) ) ) = .0. ) ) )
56 55 opabbidv 
 |-  ( ( ( ( r = R /\ s = S ) /\ x = .x. ) /\ w = W ) -> { <. a , b >. | ( ( a e. w /\ b e. w ) /\ E. t e. s ( t x ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( -g ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) ) = ( 0g ` r ) ) } = { <. a , b >. | ( ( a e. W /\ b e. W ) /\ E. t e. S ( t .x. ( ( ( 1st ` a ) .x. ( 2nd ` b ) ) .- ( ( 1st ` b ) .x. ( 2nd ` a ) ) ) ) = .0. ) } )
57 56 6 eqtr4di 
 |-  ( ( ( ( r = R /\ s = S ) /\ x = .x. ) /\ w = W ) -> { <. a , b >. | ( ( a e. w /\ b e. w ) /\ E. t e. s ( t x ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( -g ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) ) = ( 0g ` r ) ) } = .~ )
58 29 35 57 csbied2 
 |-  ( ( ( r = R /\ s = S ) /\ x = .x. ) -> [_ ( ( Base ` r ) X. s ) / w ]_ { <. a , b >. | ( ( a e. w /\ b e. w ) /\ E. t e. s ( t x ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( -g ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) ) = ( 0g ` r ) ) } = .~ )
59 22 25 58 csbied2 
 |-  ( ( r = R /\ s = S ) -> [_ ( .r ` r ) / x ]_ [_ ( ( Base ` r ) X. s ) / w ]_ { <. a , b >. | ( ( a e. w /\ b e. w ) /\ E. t e. s ( t x ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( -g ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) ) = ( 0g ` r ) ) } = .~ )
60 df-erl 
 |-  ~RL = ( r e. _V , s e. _V |-> [_ ( .r ` r ) / x ]_ [_ ( ( Base ` r ) X. s ) / w ]_ { <. a , b >. | ( ( a e. w /\ b e. w ) /\ E. t e. s ( t x ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( -g ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) ) = ( 0g ` r ) ) } )
61 59 60 ovmpoga 
 |-  ( ( R e. _V /\ S e. _V /\ .~ e. _V ) -> ( R ~RL S ) = .~ )
62 8 12 21 61 syl3anc 
 |-  ( ( ph /\ R e. _V ) -> ( R ~RL S ) = .~ )
63 60 reldmmpo 
 |-  Rel dom ~RL
64 63 ovprc1 
 |-  ( -. R e. _V -> ( R ~RL S ) = (/) )
65 64 adantl 
 |-  ( ( ph /\ -. R e. _V ) -> ( R ~RL S ) = (/) )
66 6 18 eqsstrid 
 |-  ( ph -> .~ C_ ( W X. W ) )
67 66 adantr 
 |-  ( ( ph /\ -. R e. _V ) -> .~ C_ ( W X. W ) )
68 fvprc 
 |-  ( -. R e. _V -> ( Base ` R ) = (/) )
69 1 68 eqtrid 
 |-  ( -. R e. _V -> B = (/) )
70 69 xpeq1d 
 |-  ( -. R e. _V -> ( B X. S ) = ( (/) X. S ) )
71 0xp 
 |-  ( (/) X. S ) = (/)
72 70 71 eqtrdi 
 |-  ( -. R e. _V -> ( B X. S ) = (/) )
73 5 72 eqtrid 
 |-  ( -. R e. _V -> W = (/) )
74 id 
 |-  ( W = (/) -> W = (/) )
75 74 74 xpeq12d 
 |-  ( W = (/) -> ( W X. W ) = ( (/) X. (/) ) )
76 0xp 
 |-  ( (/) X. (/) ) = (/)
77 75 76 eqtrdi 
 |-  ( W = (/) -> ( W X. W ) = (/) )
78 73 77 syl 
 |-  ( -. R e. _V -> ( W X. W ) = (/) )
79 78 adantl 
 |-  ( ( ph /\ -. R e. _V ) -> ( W X. W ) = (/) )
80 67 79 sseqtrd 
 |-  ( ( ph /\ -. R e. _V ) -> .~ C_ (/) )
81 ss0 
 |-  ( .~ C_ (/) -> .~ = (/) )
82 80 81 syl 
 |-  ( ( ph /\ -. R e. _V ) -> .~ = (/) )
83 65 82 eqtr4d 
 |-  ( ( ph /\ -. R e. _V ) -> ( R ~RL S ) = .~ )
84 62 83 pm2.61dan 
 |-  ( ph -> ( R ~RL S ) = .~ )