This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem erlbr2d

Description: Deduce the ring localization equivalence relation. Pairs <. E , G >. and <. T x. E , T x. G >. for T e. S are equivalent under the localization relation. (Contributed by Thierry Arnoux, 4-May-2025)

Ref Expression
Hypotheses erlbr2d.b 
|- B = ( Base ` R )
erlbr2d.q 
|- .~ = ( R ~RL S )
erlbr2d.r 
|- ( ph -> R e. CRing )
erlbr2d.s 
|- ( ph -> S e. ( SubMnd ` ( mulGrp ` R ) ) )
erlbr2d.m 
|- .x. = ( .r ` R )
erlbr2d.u 
|- ( ph -> U = <. E , G >. )
erlbr2d.v 
|- ( ph -> V = <. F , H >. )
erlbr2d.e 
|- ( ph -> E e. B )
erlbr2d.f 
|- ( ph -> F e. B )
erlbr2d.g 
|- ( ph -> G e. S )
erlbr2d.h 
|- ( ph -> H e. S )
erlbr2d.1 
|- ( ph -> T e. S )
erlbr2d.2 
|- ( ph -> F = ( T .x. E ) )
erlbr2d.3 
|- ( ph -> H = ( T .x. G ) )
Assertion erlbr2d 
|- ( ph -> U .~ V )

Proof

Step Hyp Ref Expression
1 erlbr2d.b 
 |-  B = ( Base ` R )
2 erlbr2d.q 
 |-  .~ = ( R ~RL S )
3 erlbr2d.r 
 |-  ( ph -> R e. CRing )
4 erlbr2d.s 
 |-  ( ph -> S e. ( SubMnd ` ( mulGrp ` R ) ) )
5 erlbr2d.m 
 |-  .x. = ( .r ` R )
6 erlbr2d.u 
 |-  ( ph -> U = <. E , G >. )
7 erlbr2d.v 
 |-  ( ph -> V = <. F , H >. )
8 erlbr2d.e 
 |-  ( ph -> E e. B )
9 erlbr2d.f 
 |-  ( ph -> F e. B )
10 erlbr2d.g 
 |-  ( ph -> G e. S )
11 erlbr2d.h 
 |-  ( ph -> H e. S )
12 erlbr2d.1 
 |-  ( ph -> T e. S )
13 erlbr2d.2 
 |-  ( ph -> F = ( T .x. E ) )
14 erlbr2d.3 
 |-  ( ph -> H = ( T .x. G ) )
15 eqid 
 |-  ( mulGrp ` R ) = ( mulGrp ` R )
16 15 1 mgpbas 
 |-  B = ( Base ` ( mulGrp ` R ) )
17 16 submss 
 |-  ( S e. ( SubMnd ` ( mulGrp ` R ) ) -> S C_ B )
18 4 17 syl 
 |-  ( ph -> S C_ B )
19 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
20 eqid 
 |-  ( -g ` R ) = ( -g ` R )
21 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
22 15 21 ringidval 
 |-  ( 1r ` R ) = ( 0g ` ( mulGrp ` R ) )
23 22 subm0cl 
 |-  ( S e. ( SubMnd ` ( mulGrp ` R ) ) -> ( 1r ` R ) e. S )
24 4 23 syl 
 |-  ( ph -> ( 1r ` R ) e. S )
25 14 oveq2d 
 |-  ( ph -> ( E .x. H ) = ( E .x. ( T .x. G ) ) )
26 13 oveq1d 
 |-  ( ph -> ( F .x. G ) = ( ( T .x. E ) .x. G ) )
27 25 26 oveq12d 
 |-  ( ph -> ( ( E .x. H ) ( -g ` R ) ( F .x. G ) ) = ( ( E .x. ( T .x. G ) ) ( -g ` R ) ( ( T .x. E ) .x. G ) ) )
28 18 12 sseldd 
 |-  ( ph -> T e. B )
29 18 10 sseldd 
 |-  ( ph -> G e. B )
30 1 5 3 28 8 29 crng32d 
 |-  ( ph -> ( ( T .x. E ) .x. G ) = ( ( T .x. G ) .x. E ) )
31 3 crngringd 
 |-  ( ph -> R e. Ring )
32 1 5 31 28 29 ringcld 
 |-  ( ph -> ( T .x. G ) e. B )
33 1 5 3 32 8 crngcomd 
 |-  ( ph -> ( ( T .x. G ) .x. E ) = ( E .x. ( T .x. G ) ) )
34 30 33 eqtrd 
 |-  ( ph -> ( ( T .x. E ) .x. G ) = ( E .x. ( T .x. G ) ) )
35 34 oveq2d 
 |-  ( ph -> ( ( E .x. ( T .x. G ) ) ( -g ` R ) ( ( T .x. E ) .x. G ) ) = ( ( E .x. ( T .x. G ) ) ( -g ` R ) ( E .x. ( T .x. G ) ) ) )
36 3 crnggrpd 
 |-  ( ph -> R e. Grp )
37 1 5 31 8 32 ringcld 
 |-  ( ph -> ( E .x. ( T .x. G ) ) e. B )
38 1 19 20 grpsubid 
 |-  ( ( R e. Grp /\ ( E .x. ( T .x. G ) ) e. B ) -> ( ( E .x. ( T .x. G ) ) ( -g ` R ) ( E .x. ( T .x. G ) ) ) = ( 0g ` R ) )
39 36 37 38 syl2anc 
 |-  ( ph -> ( ( E .x. ( T .x. G ) ) ( -g ` R ) ( E .x. ( T .x. G ) ) ) = ( 0g ` R ) )
40 27 35 39 3eqtrd 
 |-  ( ph -> ( ( E .x. H ) ( -g ` R ) ( F .x. G ) ) = ( 0g ` R ) )
41 40 oveq2d 
 |-  ( ph -> ( ( 1r ` R ) .x. ( ( E .x. H ) ( -g ` R ) ( F .x. G ) ) ) = ( ( 1r ` R ) .x. ( 0g ` R ) ) )
42 18 24 sseldd 
 |-  ( ph -> ( 1r ` R ) e. B )
43 1 5 19 31 42 ringrzd 
 |-  ( ph -> ( ( 1r ` R ) .x. ( 0g ` R ) ) = ( 0g ` R ) )
44 41 43 eqtrd 
 |-  ( ph -> ( ( 1r ` R ) .x. ( ( E .x. H ) ( -g ` R ) ( F .x. G ) ) ) = ( 0g ` R ) )
45 1 2 18 19 5 20 6 7 8 9 10 11 24 44 erlbrd 
 |-  ( ph -> U .~ V )