Metamath Proof Explorer

Theorem erlcl1

Description: Closure for the ring localization equivalence relation. (Contributed by Thierry Arnoux, 4-May-2025)

Ref Expression
Hypotheses erlcl1.b 
|- B = ( Base ` R )
erlcl1.e 
|- .~ = ( R ~RL S )
erlcl1.s 
|- ( ph -> S C_ B )
erlcl1.1 
|- ( ph -> U .~ V )
Assertion erlcl1 
|- ( ph -> U e. ( B X. S ) )

Proof

Step Hyp Ref Expression
1 erlcl1.b 
 |-  B = ( Base ` R )
2 erlcl1.e 
 |-  .~ = ( R ~RL S )
3 erlcl1.s 
 |-  ( ph -> S C_ B )
4 erlcl1.1 
 |-  ( ph -> U .~ V )
5 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
6 eqid 
 |-  ( .r ` R ) = ( .r ` R )
7 eqid 
 |-  ( -g ` R ) = ( -g ` R )
8 eqid 
 |-  ( B X. S ) = ( B X. S )
9 eqid 
 |-  { <. a , b >. | ( ( a e. ( B X. S ) /\ b e. ( B X. S ) ) /\ E. t e. S ( t ( .r ` R ) ( ( ( 1st ` a ) ( .r ` R ) ( 2nd ` b ) ) ( -g ` R ) ( ( 1st ` b ) ( .r ` R ) ( 2nd ` a ) ) ) ) = ( 0g ` R ) ) } = { <. a , b >. | ( ( a e. ( B X. S ) /\ b e. ( B X. S ) ) /\ E. t e. S ( t ( .r ` R ) ( ( ( 1st ` a ) ( .r ` R ) ( 2nd ` b ) ) ( -g ` R ) ( ( 1st ` b ) ( .r ` R ) ( 2nd ` a ) ) ) ) = ( 0g ` R ) ) }
10 1 5 6 7 8 9 3 erlval 
 |-  ( ph -> ( R ~RL S ) = { <. a , b >. | ( ( a e. ( B X. S ) /\ b e. ( B X. S ) ) /\ E. t e. S ( t ( .r ` R ) ( ( ( 1st ` a ) ( .r ` R ) ( 2nd ` b ) ) ( -g ` R ) ( ( 1st ` b ) ( .r ` R ) ( 2nd ` a ) ) ) ) = ( 0g ` R ) ) } )
11 2 10 eqtrid 
 |-  ( ph -> .~ = { <. a , b >. | ( ( a e. ( B X. S ) /\ b e. ( B X. S ) ) /\ E. t e. S ( t ( .r ` R ) ( ( ( 1st ` a ) ( .r ` R ) ( 2nd ` b ) ) ( -g ` R ) ( ( 1st ` b ) ( .r ` R ) ( 2nd ` a ) ) ) ) = ( 0g ` R ) ) } )
12 simpl 
 |-  ( ( a = U /\ b = V ) -> a = U )
13 12 fveq2d 
 |-  ( ( a = U /\ b = V ) -> ( 1st ` a ) = ( 1st ` U ) )
14 simpr 
 |-  ( ( a = U /\ b = V ) -> b = V )
15 14 fveq2d 
 |-  ( ( a = U /\ b = V ) -> ( 2nd ` b ) = ( 2nd ` V ) )
16 13 15 oveq12d 
 |-  ( ( a = U /\ b = V ) -> ( ( 1st ` a ) ( .r ` R ) ( 2nd ` b ) ) = ( ( 1st ` U ) ( .r ` R ) ( 2nd ` V ) ) )
17 14 fveq2d 
 |-  ( ( a = U /\ b = V ) -> ( 1st ` b ) = ( 1st ` V ) )
18 12 fveq2d 
 |-  ( ( a = U /\ b = V ) -> ( 2nd ` a ) = ( 2nd ` U ) )
19 17 18 oveq12d 
 |-  ( ( a = U /\ b = V ) -> ( ( 1st ` b ) ( .r ` R ) ( 2nd ` a ) ) = ( ( 1st ` V ) ( .r ` R ) ( 2nd ` U ) ) )
20 16 19 oveq12d 
 |-  ( ( a = U /\ b = V ) -> ( ( ( 1st ` a ) ( .r ` R ) ( 2nd ` b ) ) ( -g ` R ) ( ( 1st ` b ) ( .r ` R ) ( 2nd ` a ) ) ) = ( ( ( 1st ` U ) ( .r ` R ) ( 2nd ` V ) ) ( -g ` R ) ( ( 1st ` V ) ( .r ` R ) ( 2nd ` U ) ) ) )
21 20 oveq2d 
 |-  ( ( a = U /\ b = V ) -> ( t ( .r ` R ) ( ( ( 1st ` a ) ( .r ` R ) ( 2nd ` b ) ) ( -g ` R ) ( ( 1st ` b ) ( .r ` R ) ( 2nd ` a ) ) ) ) = ( t ( .r ` R ) ( ( ( 1st ` U ) ( .r ` R ) ( 2nd ` V ) ) ( -g ` R ) ( ( 1st ` V ) ( .r ` R ) ( 2nd ` U ) ) ) ) )
22 21 eqeq1d 
 |-  ( ( a = U /\ b = V ) -> ( ( t ( .r ` R ) ( ( ( 1st ` a ) ( .r ` R ) ( 2nd ` b ) ) ( -g ` R ) ( ( 1st ` b ) ( .r ` R ) ( 2nd ` a ) ) ) ) = ( 0g ` R ) <-> ( t ( .r ` R ) ( ( ( 1st ` U ) ( .r ` R ) ( 2nd ` V ) ) ( -g ` R ) ( ( 1st ` V ) ( .r ` R ) ( 2nd ` U ) ) ) ) = ( 0g ` R ) ) )
23 22 rexbidv 
 |-  ( ( a = U /\ b = V ) -> ( E. t e. S ( t ( .r ` R ) ( ( ( 1st ` a ) ( .r ` R ) ( 2nd ` b ) ) ( -g ` R ) ( ( 1st ` b ) ( .r ` R ) ( 2nd ` a ) ) ) ) = ( 0g ` R ) <-> E. t e. S ( t ( .r ` R ) ( ( ( 1st ` U ) ( .r ` R ) ( 2nd ` V ) ) ( -g ` R ) ( ( 1st ` V ) ( .r ` R ) ( 2nd ` U ) ) ) ) = ( 0g ` R ) ) )
24 23 adantl 
 |-  ( ( ph /\ ( a = U /\ b = V ) ) -> ( E. t e. S ( t ( .r ` R ) ( ( ( 1st ` a ) ( .r ` R ) ( 2nd ` b ) ) ( -g ` R ) ( ( 1st ` b ) ( .r ` R ) ( 2nd ` a ) ) ) ) = ( 0g ` R ) <-> E. t e. S ( t ( .r ` R ) ( ( ( 1st ` U ) ( .r ` R ) ( 2nd ` V ) ) ( -g ` R ) ( ( 1st ` V ) ( .r ` R ) ( 2nd ` U ) ) ) ) = ( 0g ` R ) ) )
25 11 24 brab2d 
 |-  ( ph -> ( U .~ V <-> ( ( U e. ( B X. S ) /\ V e. ( B X. S ) ) /\ E. t e. S ( t ( .r ` R ) ( ( ( 1st ` U ) ( .r ` R ) ( 2nd ` V ) ) ( -g ` R ) ( ( 1st ` V ) ( .r ` R ) ( 2nd ` U ) ) ) ) = ( 0g ` R ) ) ) )
26 4 25 mpbid 
 |-  ( ph -> ( ( U e. ( B X. S ) /\ V e. ( B X. S ) ) /\ E. t e. S ( t ( .r ` R ) ( ( ( 1st ` U ) ( .r ` R ) ( 2nd ` V ) ) ( -g ` R ) ( ( 1st ` V ) ( .r ` R ) ( 2nd ` U ) ) ) ) = ( 0g ` R ) ) )
27 26 simplld 
 |-  ( ph -> U e. ( B X. S ) )