Metamath Proof Explorer

Theorem erld2

Description: Main property of the ring localization equivalence relation. (Contributed by Thierry Arnoux, 4-May-2025)

Ref Expression
Hypotheses erld2.b 
|- B = ( Base ` R )
erld2.e 
|- .~ = ( R ~RL S )
erld2.t 
|- .x. = ( .r ` R )
erld2.r 
|- ( ph -> R e. CRing )
erld2.s 
|- ( ph -> S e. ( SubMnd ` ( mulGrp ` R ) ) )
erld2.x 
|- ( ph -> X e. B )
erld2.y 
|- ( ph -> Y e. S )
erld2.z 
|- ( ph -> Z e. B )
erld2.w 
|- ( ph -> W e. S )
erld2.1 
|- ( ph -> [ <. X , Y >. ] .~ = [ <. Z , W >. ] .~ )
Assertion erld2 
|- ( ph -> E. t e. S ( t .x. ( X .x. W ) ) = ( t .x. ( Z .x. Y ) ) )

Proof

Step Hyp Ref Expression
1 erld2.b 
 |-  B = ( Base ` R )
2 erld2.e 
 |-  .~ = ( R ~RL S )
3 erld2.t 
 |-  .x. = ( .r ` R )
4 erld2.r 
 |-  ( ph -> R e. CRing )
5 erld2.s 
 |-  ( ph -> S e. ( SubMnd ` ( mulGrp ` R ) ) )
6 erld2.x 
 |-  ( ph -> X e. B )
7 erld2.y 
 |-  ( ph -> Y e. S )
8 erld2.z 
 |-  ( ph -> Z e. B )
9 erld2.w 
 |-  ( ph -> W e. S )
10 erld2.1 
 |-  ( ph -> [ <. X , Y >. ] .~ = [ <. Z , W >. ] .~ )
11 eqid 
 |-  ( mulGrp ` R ) = ( mulGrp ` R )
12 11 1 mgpbas 
 |-  B = ( Base ` ( mulGrp ` R ) )
13 12 submss 
 |-  ( S e. ( SubMnd ` ( mulGrp ` R ) ) -> S C_ B )
14 5 13 syl 
 |-  ( ph -> S C_ B )
15 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
16 eqid 
 |-  ( -g ` R ) = ( -g ` R )
17 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
18 eqid 
 |-  ( B X. S ) = ( B X. S )
19 1 15 17 3 16 18 2 4 5 erler 
 |-  ( ph -> .~ Er ( B X. S ) )
20 6 7 opelxpd 
 |-  ( ph -> <. X , Y >. e. ( B X. S ) )
21 19 20 erth 
 |-  ( ph -> ( <. X , Y >. .~ <. Z , W >. <-> [ <. X , Y >. ] .~ = [ <. Z , W >. ] .~ ) )
22 10 21 mpbird 
 |-  ( ph -> <. X , Y >. .~ <. Z , W >. )
23 1 2 14 15 3 16 22 erldi 
 |-  ( ph -> E. t e. S ( t .x. ( ( ( 1st ` <. X , Y >. ) .x. ( 2nd ` <. Z , W >. ) ) ( -g ` R ) ( ( 1st ` <. Z , W >. ) .x. ( 2nd ` <. X , Y >. ) ) ) ) = ( 0g ` R ) )
24 4 crngringd 
 |-  ( ph -> R e. Ring )
25 24 ringgrpd 
 |-  ( ph -> R e. Grp )
26 25 ad2antrr 
 |-  ( ( ( ph /\ t e. S ) /\ ( t .x. ( ( ( 1st ` <. X , Y >. ) .x. ( 2nd ` <. Z , W >. ) ) ( -g ` R ) ( ( 1st ` <. Z , W >. ) .x. ( 2nd ` <. X , Y >. ) ) ) ) = ( 0g ` R ) ) -> R e. Grp )
27 24 adantr 
 |-  ( ( ph /\ t e. S ) -> R e. Ring )
28 27 adantr 
 |-  ( ( ( ph /\ t e. S ) /\ ( t .x. ( ( ( 1st ` <. X , Y >. ) .x. ( 2nd ` <. Z , W >. ) ) ( -g ` R ) ( ( 1st ` <. Z , W >. ) .x. ( 2nd ` <. X , Y >. ) ) ) ) = ( 0g ` R ) ) -> R e. Ring )
29 14 sselda 
 |-  ( ( ph /\ t e. S ) -> t e. B )
30 29 adantr 
 |-  ( ( ( ph /\ t e. S ) /\ ( t .x. ( ( ( 1st ` <. X , Y >. ) .x. ( 2nd ` <. Z , W >. ) ) ( -g ` R ) ( ( 1st ` <. Z , W >. ) .x. ( 2nd ` <. X , Y >. ) ) ) ) = ( 0g ` R ) ) -> t e. B )
31 14 9 sseldd 
 |-  ( ph -> W e. B )
32 1 3 24 6 31 ringcld 
 |-  ( ph -> ( X .x. W ) e. B )
33 32 adantr 
 |-  ( ( ph /\ t e. S ) -> ( X .x. W ) e. B )
34 33 adantr 
 |-  ( ( ( ph /\ t e. S ) /\ ( t .x. ( ( ( 1st ` <. X , Y >. ) .x. ( 2nd ` <. Z , W >. ) ) ( -g ` R ) ( ( 1st ` <. Z , W >. ) .x. ( 2nd ` <. X , Y >. ) ) ) ) = ( 0g ` R ) ) -> ( X .x. W ) e. B )
35 1 3 28 30 34 ringcld 
 |-  ( ( ( ph /\ t e. S ) /\ ( t .x. ( ( ( 1st ` <. X , Y >. ) .x. ( 2nd ` <. Z , W >. ) ) ( -g ` R ) ( ( 1st ` <. Z , W >. ) .x. ( 2nd ` <. X , Y >. ) ) ) ) = ( 0g ` R ) ) -> ( t .x. ( X .x. W ) ) e. B )
36 14 7 sseldd 
 |-  ( ph -> Y e. B )
37 1 3 24 8 36 ringcld 
 |-  ( ph -> ( Z .x. Y ) e. B )
38 37 adantr 
 |-  ( ( ph /\ t e. S ) -> ( Z .x. Y ) e. B )
39 38 adantr 
 |-  ( ( ( ph /\ t e. S ) /\ ( t .x. ( ( ( 1st ` <. X , Y >. ) .x. ( 2nd ` <. Z , W >. ) ) ( -g ` R ) ( ( 1st ` <. Z , W >. ) .x. ( 2nd ` <. X , Y >. ) ) ) ) = ( 0g ` R ) ) -> ( Z .x. Y ) e. B )
40 1 3 28 30 39 ringcld 
 |-  ( ( ( ph /\ t e. S ) /\ ( t .x. ( ( ( 1st ` <. X , Y >. ) .x. ( 2nd ` <. Z , W >. ) ) ( -g ` R ) ( ( 1st ` <. Z , W >. ) .x. ( 2nd ` <. X , Y >. ) ) ) ) = ( 0g ` R ) ) -> ( t .x. ( Z .x. Y ) ) e. B )
41 op1stg 
 |-  ( ( X e. B /\ Y e. S ) -> ( 1st ` <. X , Y >. ) = X )
42 6 7 41 syl2anc 
 |-  ( ph -> ( 1st ` <. X , Y >. ) = X )
43 op2ndg 
 |-  ( ( Z e. B /\ W e. S ) -> ( 2nd ` <. Z , W >. ) = W )
44 8 9 43 syl2anc 
 |-  ( ph -> ( 2nd ` <. Z , W >. ) = W )
45 42 44 oveq12d 
 |-  ( ph -> ( ( 1st ` <. X , Y >. ) .x. ( 2nd ` <. Z , W >. ) ) = ( X .x. W ) )
46 op1stg 
 |-  ( ( Z e. B /\ W e. S ) -> ( 1st ` <. Z , W >. ) = Z )
47 8 9 46 syl2anc 
 |-  ( ph -> ( 1st ` <. Z , W >. ) = Z )
48 op2ndg 
 |-  ( ( X e. B /\ Y e. S ) -> ( 2nd ` <. X , Y >. ) = Y )
49 6 7 48 syl2anc 
 |-  ( ph -> ( 2nd ` <. X , Y >. ) = Y )
50 47 49 oveq12d 
 |-  ( ph -> ( ( 1st ` <. Z , W >. ) .x. ( 2nd ` <. X , Y >. ) ) = ( Z .x. Y ) )
51 45 50 oveq12d 
 |-  ( ph -> ( ( ( 1st ` <. X , Y >. ) .x. ( 2nd ` <. Z , W >. ) ) ( -g ` R ) ( ( 1st ` <. Z , W >. ) .x. ( 2nd ` <. X , Y >. ) ) ) = ( ( X .x. W ) ( -g ` R ) ( Z .x. Y ) ) )
52 51 oveq2d 
 |-  ( ph -> ( t .x. ( ( ( 1st ` <. X , Y >. ) .x. ( 2nd ` <. Z , W >. ) ) ( -g ` R ) ( ( 1st ` <. Z , W >. ) .x. ( 2nd ` <. X , Y >. ) ) ) ) = ( t .x. ( ( X .x. W ) ( -g ` R ) ( Z .x. Y ) ) ) )
53 52 adantr 
 |-  ( ( ph /\ t e. S ) -> ( t .x. ( ( ( 1st ` <. X , Y >. ) .x. ( 2nd ` <. Z , W >. ) ) ( -g ` R ) ( ( 1st ` <. Z , W >. ) .x. ( 2nd ` <. X , Y >. ) ) ) ) = ( t .x. ( ( X .x. W ) ( -g ` R ) ( Z .x. Y ) ) ) )
54 1 3 16 27 29 33 38 ringsubdi 
 |-  ( ( ph /\ t e. S ) -> ( t .x. ( ( X .x. W ) ( -g ` R ) ( Z .x. Y ) ) ) = ( ( t .x. ( X .x. W ) ) ( -g ` R ) ( t .x. ( Z .x. Y ) ) ) )
55 53 54 eqtrd 
 |-  ( ( ph /\ t e. S ) -> ( t .x. ( ( ( 1st ` <. X , Y >. ) .x. ( 2nd ` <. Z , W >. ) ) ( -g ` R ) ( ( 1st ` <. Z , W >. ) .x. ( 2nd ` <. X , Y >. ) ) ) ) = ( ( t .x. ( X .x. W ) ) ( -g ` R ) ( t .x. ( Z .x. Y ) ) ) )
56 55 eqeq1d 
 |-  ( ( ph /\ t e. S ) -> ( ( t .x. ( ( ( 1st ` <. X , Y >. ) .x. ( 2nd ` <. Z , W >. ) ) ( -g ` R ) ( ( 1st ` <. Z , W >. ) .x. ( 2nd ` <. X , Y >. ) ) ) ) = ( 0g ` R ) <-> ( ( t .x. ( X .x. W ) ) ( -g ` R ) ( t .x. ( Z .x. Y ) ) ) = ( 0g ` R ) ) )
57 56 biimpa 
 |-  ( ( ( ph /\ t e. S ) /\ ( t .x. ( ( ( 1st ` <. X , Y >. ) .x. ( 2nd ` <. Z , W >. ) ) ( -g ` R ) ( ( 1st ` <. Z , W >. ) .x. ( 2nd ` <. X , Y >. ) ) ) ) = ( 0g ` R ) ) -> ( ( t .x. ( X .x. W ) ) ( -g ` R ) ( t .x. ( Z .x. Y ) ) ) = ( 0g ` R ) )
58 1 15 16 grpsubeq0 
 |-  ( ( R e. Grp /\ ( t .x. ( X .x. W ) ) e. B /\ ( t .x. ( Z .x. Y ) ) e. B ) -> ( ( ( t .x. ( X .x. W ) ) ( -g ` R ) ( t .x. ( Z .x. Y ) ) ) = ( 0g ` R ) <-> ( t .x. ( X .x. W ) ) = ( t .x. ( Z .x. Y ) ) ) )
59 58 biimpa 
 |-  ( ( ( R e. Grp /\ ( t .x. ( X .x. W ) ) e. B /\ ( t .x. ( Z .x. Y ) ) e. B ) /\ ( ( t .x. ( X .x. W ) ) ( -g ` R ) ( t .x. ( Z .x. Y ) ) ) = ( 0g ` R ) ) -> ( t .x. ( X .x. W ) ) = ( t .x. ( Z .x. Y ) ) )
60 26 35 40 57 59 syl31anc 
 |-  ( ( ( ph /\ t e. S ) /\ ( t .x. ( ( ( 1st ` <. X , Y >. ) .x. ( 2nd ` <. Z , W >. ) ) ( -g ` R ) ( ( 1st ` <. Z , W >. ) .x. ( 2nd ` <. X , Y >. ) ) ) ) = ( 0g ` R ) ) -> ( t .x. ( X .x. W ) ) = ( t .x. ( Z .x. Y ) ) )
61 60 ex 
 |-  ( ( ph /\ t e. S ) -> ( ( t .x. ( ( ( 1st ` <. X , Y >. ) .x. ( 2nd ` <. Z , W >. ) ) ( -g ` R ) ( ( 1st ` <. Z , W >. ) .x. ( 2nd ` <. X , Y >. ) ) ) ) = ( 0g ` R ) -> ( t .x. ( X .x. W ) ) = ( t .x. ( Z .x. Y ) ) ) )
62 61 reximdva 
 |-  ( ph -> ( E. t e. S ( t .x. ( ( ( 1st ` <. X , Y >. ) .x. ( 2nd ` <. Z , W >. ) ) ( -g ` R ) ( ( 1st ` <. Z , W >. ) .x. ( 2nd ` <. X , Y >. ) ) ) ) = ( 0g ` R ) -> E. t e. S ( t .x. ( X .x. W ) ) = ( t .x. ( Z .x. Y ) ) ) )
63 23 62 mpd 
 |-  ( ph -> E. t e. S ( t .x. ( X .x. W ) ) = ( t .x. ( Z .x. Y ) ) )