Metamath Proof Explorer

Theorem fracerl

Description: Rewrite the ring localization equivalence relation in the case of a field of fractions. (Contributed by Thierry Arnoux, 5-May-2025)

Ref Expression
Hypotheses fracerl.1 
|- B = ( Base ` R )
fracerl.2 
|- .x. = ( .r ` R )
fracerl.3 
|- .~ = ( R ~RL ( RLReg ` R ) )
fracerl.4 
|- ( ph -> R e. CRing )
fracerl.5 
|- ( ph -> E e. B )
fracerl.6 
|- ( ph -> G e. B )
fracerl.7 
|- ( ph -> F e. ( RLReg ` R ) )
fracerl.8 
|- ( ph -> H e. ( RLReg ` R ) )
Assertion fracerl 
|- ( ph -> ( <. E , F >. .~ <. G , H >. <-> ( E .x. H ) = ( G .x. F ) ) )

Proof

Step Hyp Ref Expression
1 fracerl.1 
 |-  B = ( Base ` R )
2 fracerl.2 
 |-  .x. = ( .r ` R )
3 fracerl.3 
 |-  .~ = ( R ~RL ( RLReg ` R ) )
4 fracerl.4 
 |-  ( ph -> R e. CRing )
5 fracerl.5 
 |-  ( ph -> E e. B )
6 fracerl.6 
 |-  ( ph -> G e. B )
7 fracerl.7 
 |-  ( ph -> F e. ( RLReg ` R ) )
8 fracerl.8 
 |-  ( ph -> H e. ( RLReg ` R ) )
9 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
10 eqid 
 |-  ( -g ` R ) = ( -g ` R )
11 eqid 
 |-  ( B X. ( RLReg ` R ) ) = ( B X. ( RLReg ` R ) )
12 eqid 
 |-  { <. a , b >. | ( ( a e. ( B X. ( RLReg ` R ) ) /\ b e. ( B X. ( RLReg ` R ) ) ) /\ E. t e. ( RLReg ` R ) ( t .x. ( ( ( 1st ` a ) .x. ( 2nd ` b ) ) ( -g ` R ) ( ( 1st ` b ) .x. ( 2nd ` a ) ) ) ) = ( 0g ` R ) ) } = { <. a , b >. | ( ( a e. ( B X. ( RLReg ` R ) ) /\ b e. ( B X. ( RLReg ` R ) ) ) /\ E. t e. ( RLReg ` R ) ( t .x. ( ( ( 1st ` a ) .x. ( 2nd ` b ) ) ( -g ` R ) ( ( 1st ` b ) .x. ( 2nd ` a ) ) ) ) = ( 0g ` R ) ) }
13 eqid 
 |-  ( RLReg ` R ) = ( RLReg ` R )
14 13 1 rrgss 
 |-  ( RLReg ` R ) C_ B
15 14 a1i 
 |-  ( ph -> ( RLReg ` R ) C_ B )
16 1 9 2 10 11 12 15 erlval 
 |-  ( ph -> ( R ~RL ( RLReg ` R ) ) = { <. a , b >. | ( ( a e. ( B X. ( RLReg ` R ) ) /\ b e. ( B X. ( RLReg ` R ) ) ) /\ E. t e. ( RLReg ` R ) ( t .x. ( ( ( 1st ` a ) .x. ( 2nd ` b ) ) ( -g ` R ) ( ( 1st ` b ) .x. ( 2nd ` a ) ) ) ) = ( 0g ` R ) ) } )
17 3 16 eqtrid 
 |-  ( ph -> .~ = { <. a , b >. | ( ( a e. ( B X. ( RLReg ` R ) ) /\ b e. ( B X. ( RLReg ` R ) ) ) /\ E. t e. ( RLReg ` R ) ( t .x. ( ( ( 1st ` a ) .x. ( 2nd ` b ) ) ( -g ` R ) ( ( 1st ` b ) .x. ( 2nd ` a ) ) ) ) = ( 0g ` R ) ) } )
18 simprl 
 |-  ( ( ph /\ ( a = <. E , F >. /\ b = <. G , H >. ) ) -> a = <. E , F >. )
19 18 fveq2d 
 |-  ( ( ph /\ ( a = <. E , F >. /\ b = <. G , H >. ) ) -> ( 1st ` a ) = ( 1st ` <. E , F >. ) )
20 7 adantr 
 |-  ( ( ph /\ ( a = <. E , F >. /\ b = <. G , H >. ) ) -> F e. ( RLReg ` R ) )
21 op1stg 
 |-  ( ( E e. B /\ F e. ( RLReg ` R ) ) -> ( 1st ` <. E , F >. ) = E )
22 5 20 21 syl2an2r 
 |-  ( ( ph /\ ( a = <. E , F >. /\ b = <. G , H >. ) ) -> ( 1st ` <. E , F >. ) = E )
23 19 22 eqtrd 
 |-  ( ( ph /\ ( a = <. E , F >. /\ b = <. G , H >. ) ) -> ( 1st ` a ) = E )
24 simprr 
 |-  ( ( ph /\ ( a = <. E , F >. /\ b = <. G , H >. ) ) -> b = <. G , H >. )
25 24 fveq2d 
 |-  ( ( ph /\ ( a = <. E , F >. /\ b = <. G , H >. ) ) -> ( 2nd ` b ) = ( 2nd ` <. G , H >. ) )
26 8 adantr 
 |-  ( ( ph /\ ( a = <. E , F >. /\ b = <. G , H >. ) ) -> H e. ( RLReg ` R ) )
27 op2ndg 
 |-  ( ( G e. B /\ H e. ( RLReg ` R ) ) -> ( 2nd ` <. G , H >. ) = H )
28 6 26 27 syl2an2r 
 |-  ( ( ph /\ ( a = <. E , F >. /\ b = <. G , H >. ) ) -> ( 2nd ` <. G , H >. ) = H )
29 25 28 eqtrd 
 |-  ( ( ph /\ ( a = <. E , F >. /\ b = <. G , H >. ) ) -> ( 2nd ` b ) = H )
30 23 29 oveq12d 
 |-  ( ( ph /\ ( a = <. E , F >. /\ b = <. G , H >. ) ) -> ( ( 1st ` a ) .x. ( 2nd ` b ) ) = ( E .x. H ) )
31 24 fveq2d 
 |-  ( ( ph /\ ( a = <. E , F >. /\ b = <. G , H >. ) ) -> ( 1st ` b ) = ( 1st ` <. G , H >. ) )
32 op1stg 
 |-  ( ( G e. B /\ H e. ( RLReg ` R ) ) -> ( 1st ` <. G , H >. ) = G )
33 6 26 32 syl2an2r 
 |-  ( ( ph /\ ( a = <. E , F >. /\ b = <. G , H >. ) ) -> ( 1st ` <. G , H >. ) = G )
34 31 33 eqtrd 
 |-  ( ( ph /\ ( a = <. E , F >. /\ b = <. G , H >. ) ) -> ( 1st ` b ) = G )
35 18 fveq2d 
 |-  ( ( ph /\ ( a = <. E , F >. /\ b = <. G , H >. ) ) -> ( 2nd ` a ) = ( 2nd ` <. E , F >. ) )
36 op2ndg 
 |-  ( ( E e. B /\ F e. ( RLReg ` R ) ) -> ( 2nd ` <. E , F >. ) = F )
37 5 20 36 syl2an2r 
 |-  ( ( ph /\ ( a = <. E , F >. /\ b = <. G , H >. ) ) -> ( 2nd ` <. E , F >. ) = F )
38 35 37 eqtrd 
 |-  ( ( ph /\ ( a = <. E , F >. /\ b = <. G , H >. ) ) -> ( 2nd ` a ) = F )
39 34 38 oveq12d 
 |-  ( ( ph /\ ( a = <. E , F >. /\ b = <. G , H >. ) ) -> ( ( 1st ` b ) .x. ( 2nd ` a ) ) = ( G .x. F ) )
40 30 39 oveq12d 
 |-  ( ( ph /\ ( a = <. E , F >. /\ b = <. G , H >. ) ) -> ( ( ( 1st ` a ) .x. ( 2nd ` b ) ) ( -g ` R ) ( ( 1st ` b ) .x. ( 2nd ` a ) ) ) = ( ( E .x. H ) ( -g ` R ) ( G .x. F ) ) )
41 40 oveq2d 
 |-  ( ( ph /\ ( a = <. E , F >. /\ b = <. G , H >. ) ) -> ( t .x. ( ( ( 1st ` a ) .x. ( 2nd ` b ) ) ( -g ` R ) ( ( 1st ` b ) .x. ( 2nd ` a ) ) ) ) = ( t .x. ( ( E .x. H ) ( -g ` R ) ( G .x. F ) ) ) )
42 41 eqeq1d 
 |-  ( ( ph /\ ( a = <. E , F >. /\ b = <. G , H >. ) ) -> ( ( t .x. ( ( ( 1st ` a ) .x. ( 2nd ` b ) ) ( -g ` R ) ( ( 1st ` b ) .x. ( 2nd ` a ) ) ) ) = ( 0g ` R ) <-> ( t .x. ( ( E .x. H ) ( -g ` R ) ( G .x. F ) ) ) = ( 0g ` R ) ) )
43 42 rexbidv 
 |-  ( ( ph /\ ( a = <. E , F >. /\ b = <. G , H >. ) ) -> ( E. t e. ( RLReg ` R ) ( t .x. ( ( ( 1st ` a ) .x. ( 2nd ` b ) ) ( -g ` R ) ( ( 1st ` b ) .x. ( 2nd ` a ) ) ) ) = ( 0g ` R ) <-> E. t e. ( RLReg ` R ) ( t .x. ( ( E .x. H ) ( -g ` R ) ( G .x. F ) ) ) = ( 0g ` R ) ) )
44 17 43 brab2d 
 |-  ( ph -> ( <. E , F >. .~ <. G , H >. <-> ( ( <. E , F >. e. ( B X. ( RLReg ` R ) ) /\ <. G , H >. e. ( B X. ( RLReg ` R ) ) ) /\ E. t e. ( RLReg ` R ) ( t .x. ( ( E .x. H ) ( -g ` R ) ( G .x. F ) ) ) = ( 0g ` R ) ) ) )
45 5 7 opelxpd 
 |-  ( ph -> <. E , F >. e. ( B X. ( RLReg ` R ) ) )
46 6 8 opelxpd 
 |-  ( ph -> <. G , H >. e. ( B X. ( RLReg ` R ) ) )
47 45 46 jca 
 |-  ( ph -> ( <. E , F >. e. ( B X. ( RLReg ` R ) ) /\ <. G , H >. e. ( B X. ( RLReg ` R ) ) ) )
48 47 biantrurd 
 |-  ( ph -> ( E. t e. ( RLReg ` R ) ( t .x. ( ( E .x. H ) ( -g ` R ) ( G .x. F ) ) ) = ( 0g ` R ) <-> ( ( <. E , F >. e. ( B X. ( RLReg ` R ) ) /\ <. G , H >. e. ( B X. ( RLReg ` R ) ) ) /\ E. t e. ( RLReg ` R ) ( t .x. ( ( E .x. H ) ( -g ` R ) ( G .x. F ) ) ) = ( 0g ` R ) ) ) )
49 simplr 
 |-  ( ( ( ph /\ t e. ( RLReg ` R ) ) /\ ( t .x. ( ( E .x. H ) ( -g ` R ) ( G .x. F ) ) ) = ( 0g ` R ) ) -> t e. ( RLReg ` R ) )
50 4 crnggrpd 
 |-  ( ph -> R e. Grp )
51 50 ad2antrr 
 |-  ( ( ( ph /\ t e. ( RLReg ` R ) ) /\ ( t .x. ( ( E .x. H ) ( -g ` R ) ( G .x. F ) ) ) = ( 0g ` R ) ) -> R e. Grp )
52 4 crngringd 
 |-  ( ph -> R e. Ring )
53 52 ad2antrr 
 |-  ( ( ( ph /\ t e. ( RLReg ` R ) ) /\ ( t .x. ( ( E .x. H ) ( -g ` R ) ( G .x. F ) ) ) = ( 0g ` R ) ) -> R e. Ring )
54 5 ad2antrr 
 |-  ( ( ( ph /\ t e. ( RLReg ` R ) ) /\ ( t .x. ( ( E .x. H ) ( -g ` R ) ( G .x. F ) ) ) = ( 0g ` R ) ) -> E e. B )
55 14 8 sselid 
 |-  ( ph -> H e. B )
56 55 ad2antrr 
 |-  ( ( ( ph /\ t e. ( RLReg ` R ) ) /\ ( t .x. ( ( E .x. H ) ( -g ` R ) ( G .x. F ) ) ) = ( 0g ` R ) ) -> H e. B )
57 1 2 53 54 56 ringcld 
 |-  ( ( ( ph /\ t e. ( RLReg ` R ) ) /\ ( t .x. ( ( E .x. H ) ( -g ` R ) ( G .x. F ) ) ) = ( 0g ` R ) ) -> ( E .x. H ) e. B )
58 6 ad2antrr 
 |-  ( ( ( ph /\ t e. ( RLReg ` R ) ) /\ ( t .x. ( ( E .x. H ) ( -g ` R ) ( G .x. F ) ) ) = ( 0g ` R ) ) -> G e. B )
59 14 7 sselid 
 |-  ( ph -> F e. B )
60 59 ad2antrr 
 |-  ( ( ( ph /\ t e. ( RLReg ` R ) ) /\ ( t .x. ( ( E .x. H ) ( -g ` R ) ( G .x. F ) ) ) = ( 0g ` R ) ) -> F e. B )
61 1 2 53 58 60 ringcld 
 |-  ( ( ( ph /\ t e. ( RLReg ` R ) ) /\ ( t .x. ( ( E .x. H ) ( -g ` R ) ( G .x. F ) ) ) = ( 0g ` R ) ) -> ( G .x. F ) e. B )
62 1 10 grpsubcl 
 |-  ( ( R e. Grp /\ ( E .x. H ) e. B /\ ( G .x. F ) e. B ) -> ( ( E .x. H ) ( -g ` R ) ( G .x. F ) ) e. B )
63 51 57 61 62 syl3anc 
 |-  ( ( ( ph /\ t e. ( RLReg ` R ) ) /\ ( t .x. ( ( E .x. H ) ( -g ` R ) ( G .x. F ) ) ) = ( 0g ` R ) ) -> ( ( E .x. H ) ( -g ` R ) ( G .x. F ) ) e. B )
64 simpr 
 |-  ( ( ( ph /\ t e. ( RLReg ` R ) ) /\ ( t .x. ( ( E .x. H ) ( -g ` R ) ( G .x. F ) ) ) = ( 0g ` R ) ) -> ( t .x. ( ( E .x. H ) ( -g ` R ) ( G .x. F ) ) ) = ( 0g ` R ) )
65 13 1 2 9 rrgeq0i 
 |-  ( ( t e. ( RLReg ` R ) /\ ( ( E .x. H ) ( -g ` R ) ( G .x. F ) ) e. B ) -> ( ( t .x. ( ( E .x. H ) ( -g ` R ) ( G .x. F ) ) ) = ( 0g ` R ) -> ( ( E .x. H ) ( -g ` R ) ( G .x. F ) ) = ( 0g ` R ) ) )
66 65 imp 
 |-  ( ( ( t e. ( RLReg ` R ) /\ ( ( E .x. H ) ( -g ` R ) ( G .x. F ) ) e. B ) /\ ( t .x. ( ( E .x. H ) ( -g ` R ) ( G .x. F ) ) ) = ( 0g ` R ) ) -> ( ( E .x. H ) ( -g ` R ) ( G .x. F ) ) = ( 0g ` R ) )
67 49 63 64 66 syl21anc 
 |-  ( ( ( ph /\ t e. ( RLReg ` R ) ) /\ ( t .x. ( ( E .x. H ) ( -g ` R ) ( G .x. F ) ) ) = ( 0g ` R ) ) -> ( ( E .x. H ) ( -g ` R ) ( G .x. F ) ) = ( 0g ` R ) )
68 67 r19.29an 
 |-  ( ( ph /\ E. t e. ( RLReg ` R ) ( t .x. ( ( E .x. H ) ( -g ` R ) ( G .x. F ) ) ) = ( 0g ` R ) ) -> ( ( E .x. H ) ( -g ` R ) ( G .x. F ) ) = ( 0g ` R ) )
69 oveq1 
 |-  ( t = ( 1r ` R ) -> ( t .x. ( ( E .x. H ) ( -g ` R ) ( G .x. F ) ) ) = ( ( 1r ` R ) .x. ( ( E .x. H ) ( -g ` R ) ( G .x. F ) ) ) )
70 69 eqeq1d 
 |-  ( t = ( 1r ` R ) -> ( ( t .x. ( ( E .x. H ) ( -g ` R ) ( G .x. F ) ) ) = ( 0g ` R ) <-> ( ( 1r ` R ) .x. ( ( E .x. H ) ( -g ` R ) ( G .x. F ) ) ) = ( 0g ` R ) ) )
71 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
72 71 13 52 1rrg 
 |-  ( ph -> ( 1r ` R ) e. ( RLReg ` R ) )
73 72 adantr 
 |-  ( ( ph /\ ( ( E .x. H ) ( -g ` R ) ( G .x. F ) ) = ( 0g ` R ) ) -> ( 1r ` R ) e. ( RLReg ` R ) )
74 simpr 
 |-  ( ( ph /\ ( ( E .x. H ) ( -g ` R ) ( G .x. F ) ) = ( 0g ` R ) ) -> ( ( E .x. H ) ( -g ` R ) ( G .x. F ) ) = ( 0g ` R ) )
75 74 oveq2d 
 |-  ( ( ph /\ ( ( E .x. H ) ( -g ` R ) ( G .x. F ) ) = ( 0g ` R ) ) -> ( ( 1r ` R ) .x. ( ( E .x. H ) ( -g ` R ) ( G .x. F ) ) ) = ( ( 1r ` R ) .x. ( 0g ` R ) ) )
76 1 71 ringidcl 
 |-  ( R e. Ring -> ( 1r ` R ) e. B )
77 52 76 syl 
 |-  ( ph -> ( 1r ` R ) e. B )
78 1 2 9 52 77 ringrzd 
 |-  ( ph -> ( ( 1r ` R ) .x. ( 0g ` R ) ) = ( 0g ` R ) )
79 78 adantr 
 |-  ( ( ph /\ ( ( E .x. H ) ( -g ` R ) ( G .x. F ) ) = ( 0g ` R ) ) -> ( ( 1r ` R ) .x. ( 0g ` R ) ) = ( 0g ` R ) )
80 75 79 eqtrd 
 |-  ( ( ph /\ ( ( E .x. H ) ( -g ` R ) ( G .x. F ) ) = ( 0g ` R ) ) -> ( ( 1r ` R ) .x. ( ( E .x. H ) ( -g ` R ) ( G .x. F ) ) ) = ( 0g ` R ) )
81 70 73 80 rspcedvdw 
 |-  ( ( ph /\ ( ( E .x. H ) ( -g ` R ) ( G .x. F ) ) = ( 0g ` R ) ) -> E. t e. ( RLReg ` R ) ( t .x. ( ( E .x. H ) ( -g ` R ) ( G .x. F ) ) ) = ( 0g ` R ) )
82 68 81 impbida 
 |-  ( ph -> ( E. t e. ( RLReg ` R ) ( t .x. ( ( E .x. H ) ( -g ` R ) ( G .x. F ) ) ) = ( 0g ` R ) <-> ( ( E .x. H ) ( -g ` R ) ( G .x. F ) ) = ( 0g ` R ) ) )
83 44 48 82 3bitr2d 
 |-  ( ph -> ( <. E , F >. .~ <. G , H >. <-> ( ( E .x. H ) ( -g ` R ) ( G .x. F ) ) = ( 0g ` R ) ) )
84 1 2 52 5 55 ringcld 
 |-  ( ph -> ( E .x. H ) e. B )
85 1 2 52 6 59 ringcld 
 |-  ( ph -> ( G .x. F ) e. B )
86 1 9 10 grpsubeq0 
 |-  ( ( R e. Grp /\ ( E .x. H ) e. B /\ ( G .x. F ) e. B ) -> ( ( ( E .x. H ) ( -g ` R ) ( G .x. F ) ) = ( 0g ` R ) <-> ( E .x. H ) = ( G .x. F ) ) )
87 50 84 85 86 syl3anc 
 |-  ( ph -> ( ( ( E .x. H ) ( -g ` R ) ( G .x. F ) ) = ( 0g ` R ) <-> ( E .x. H ) = ( G .x. F ) ) )
88 83 87 bitrd 
 |-  ( ph -> ( <. E , F >. .~ <. G , H >. <-> ( E .x. H ) = ( G .x. F ) ) )