Metamath Proof Explorer

Theorem erldi

Description: Main property of 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 )
erldi.1 
|- .0. = ( 0g ` R )
erldi.2 
|- .x. = ( .r ` R )
erldi.3 
|- .- = ( -g ` R )
erldi.4 
|- ( ph -> U .~ V )
Assertion erldi 
|- ( ph -> E. t e. S ( t .x. ( ( ( 1st ` U ) .x. ( 2nd ` V ) ) .- ( ( 1st ` V ) .x. ( 2nd ` U ) ) ) ) = .0. )

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 erldi.1 
 |-  .0. = ( 0g ` R )
5 erldi.2 
 |-  .x. = ( .r ` R )
6 erldi.3 
 |-  .- = ( -g ` R )
7 erldi.4 
 |-  ( ph -> U .~ V )
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 .x. ( ( ( 1st ` a ) .x. ( 2nd ` b ) ) .- ( ( 1st ` b ) .x. ( 2nd ` a ) ) ) ) = .0. ) } = { <. a , b >. | ( ( a e. ( B X. S ) /\ b e. ( B X. S ) ) /\ E. t e. S ( t .x. ( ( ( 1st ` a ) .x. ( 2nd ` b ) ) .- ( ( 1st ` b ) .x. ( 2nd ` a ) ) ) ) = .0. ) }
10 1 4 5 6 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 .x. ( ( ( 1st ` a ) .x. ( 2nd ` b ) ) .- ( ( 1st ` b ) .x. ( 2nd ` a ) ) ) ) = .0. ) } )
11 2 10 eqtrid 
 |-  ( ph -> .~ = { <. a , b >. | ( ( a e. ( B X. S ) /\ b e. ( B X. S ) ) /\ E. t e. S ( t .x. ( ( ( 1st ` a ) .x. ( 2nd ` b ) ) .- ( ( 1st ` b ) .x. ( 2nd ` a ) ) ) ) = .0. ) } )
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 ) .x. ( 2nd ` b ) ) = ( ( 1st ` U ) .x. ( 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 ) .x. ( 2nd ` a ) ) = ( ( 1st ` V ) .x. ( 2nd ` U ) ) )
20 16 19 oveq12d 
 |-  ( ( a = U /\ b = V ) -> ( ( ( 1st ` a ) .x. ( 2nd ` b ) ) .- ( ( 1st ` b ) .x. ( 2nd ` a ) ) ) = ( ( ( 1st ` U ) .x. ( 2nd ` V ) ) .- ( ( 1st ` V ) .x. ( 2nd ` U ) ) ) )
21 20 oveq2d 
 |-  ( ( a = U /\ b = V ) -> ( t .x. ( ( ( 1st ` a ) .x. ( 2nd ` b ) ) .- ( ( 1st ` b ) .x. ( 2nd ` a ) ) ) ) = ( t .x. ( ( ( 1st ` U ) .x. ( 2nd ` V ) ) .- ( ( 1st ` V ) .x. ( 2nd ` U ) ) ) ) )
22 21 eqeq1d 
 |-  ( ( a = U /\ b = V ) -> ( ( t .x. ( ( ( 1st ` a ) .x. ( 2nd ` b ) ) .- ( ( 1st ` b ) .x. ( 2nd ` a ) ) ) ) = .0. <-> ( t .x. ( ( ( 1st ` U ) .x. ( 2nd ` V ) ) .- ( ( 1st ` V ) .x. ( 2nd ` U ) ) ) ) = .0. ) )
23 22 rexbidv 
 |-  ( ( a = U /\ b = V ) -> ( E. t e. S ( t .x. ( ( ( 1st ` a ) .x. ( 2nd ` b ) ) .- ( ( 1st ` b ) .x. ( 2nd ` a ) ) ) ) = .0. <-> E. t e. S ( t .x. ( ( ( 1st ` U ) .x. ( 2nd ` V ) ) .- ( ( 1st ` V ) .x. ( 2nd ` U ) ) ) ) = .0. ) )
24 23 adantl 
 |-  ( ( ph /\ ( a = U /\ b = V ) ) -> ( E. t e. S ( t .x. ( ( ( 1st ` a ) .x. ( 2nd ` b ) ) .- ( ( 1st ` b ) .x. ( 2nd ` a ) ) ) ) = .0. <-> E. t e. S ( t .x. ( ( ( 1st ` U ) .x. ( 2nd ` V ) ) .- ( ( 1st ` V ) .x. ( 2nd ` U ) ) ) ) = .0. ) )
25 11 24 brab2d 
 |-  ( ph -> ( U .~ V <-> ( ( U e. ( B X. S ) /\ V e. ( B X. S ) ) /\ E. t e. S ( t .x. ( ( ( 1st ` U ) .x. ( 2nd ` V ) ) .- ( ( 1st ` V ) .x. ( 2nd ` U ) ) ) ) = .0. ) ) )
26 7 25 mpbid 
 |-  ( ph -> ( ( U e. ( B X. S ) /\ V e. ( B X. S ) ) /\ E. t e. S ( t .x. ( ( ( 1st ` U ) .x. ( 2nd ` V ) ) .- ( ( 1st ` V ) .x. ( 2nd ` U ) ) ) ) = .0. ) )
27 26 simprd 
 |-  ( ph -> E. t e. S ( t .x. ( ( ( 1st ` U ) .x. ( 2nd ` V ) ) .- ( ( 1st ` V ) .x. ( 2nd ` U ) ) ) ) = .0. )