Metamath Proof Explorer

Theorem erlbrd

Description: Deduce the ring localization equivalence relation. If for some T e. S we have T x. ( E x. H - F x. G ) = 0 , then pairs <. E , G >. and <. F , H >. are equivalent under the localization 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 )
erlbrd.u 
|- ( ph -> U = <. E , G >. )
erlbrd.v 
|- ( ph -> V = <. F , H >. )
erlbrd.e 
|- ( ph -> E e. B )
erlbrd.f 
|- ( ph -> F e. B )
erlbrd.g 
|- ( ph -> G e. S )
erlbrd.h 
|- ( ph -> H e. S )
erlbrd.1 
|- ( ph -> T e. S )
erlbrd.2 
|- ( ph -> ( T .x. ( ( E .x. H ) .- ( F .x. G ) ) ) = .0. )
Assertion erlbrd 
|- ( ph -> U .~ V )

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 erlbrd.u 
 |-  ( ph -> U = <. E , G >. )
8 erlbrd.v 
 |-  ( ph -> V = <. F , H >. )
9 erlbrd.e 
 |-  ( ph -> E e. B )
10 erlbrd.f 
 |-  ( ph -> F e. B )
11 erlbrd.g 
 |-  ( ph -> G e. S )
12 erlbrd.h 
 |-  ( ph -> H e. S )
13 erlbrd.1 
 |-  ( ph -> T e. S )
14 erlbrd.2 
 |-  ( ph -> ( T .x. ( ( E .x. H ) .- ( F .x. G ) ) ) = .0. )
15 9 11 opelxpd 
 |-  ( ph -> <. E , G >. e. ( B X. S ) )
16 7 15 eqeltrd 
 |-  ( ph -> U e. ( B X. S ) )
17 10 12 opelxpd 
 |-  ( ph -> <. F , H >. e. ( B X. S ) )
18 8 17 eqeltrd 
 |-  ( ph -> V e. ( B X. S ) )
19 16 18 jca 
 |-  ( ph -> ( U e. ( B X. S ) /\ V e. ( B X. S ) ) )
20 simpr 
 |-  ( ( ph /\ t = T ) -> t = T )
21 20 oveq1d 
 |-  ( ( ph /\ t = T ) -> ( t .x. ( ( E .x. H ) .- ( F .x. G ) ) ) = ( T .x. ( ( E .x. H ) .- ( F .x. G ) ) ) )
22 21 eqeq1d 
 |-  ( ( ph /\ t = T ) -> ( ( t .x. ( ( E .x. H ) .- ( F .x. G ) ) ) = .0. <-> ( T .x. ( ( E .x. H ) .- ( F .x. G ) ) ) = .0. ) )
23 13 22 14 rspcedvd 
 |-  ( ph -> E. t e. S ( t .x. ( ( E .x. H ) .- ( F .x. G ) ) ) = .0. )
24 19 23 jca 
 |-  ( ph -> ( ( U e. ( B X. S ) /\ V e. ( B X. S ) ) /\ E. t e. S ( t .x. ( ( E .x. H ) .- ( F .x. G ) ) ) = .0. ) )
25 eqid 
 |-  ( B X. S ) = ( B X. S )
26 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. ) }
27 1 4 5 6 25 26 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. ) } )
28 2 27 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. ) } )
29 simprl 
 |-  ( ( ph /\ ( a = U /\ b = V ) ) -> a = U )
30 29 fveq2d 
 |-  ( ( ph /\ ( a = U /\ b = V ) ) -> ( 1st ` a ) = ( 1st ` U ) )
31 7 fveq2d 
 |-  ( ph -> ( 1st ` U ) = ( 1st ` <. E , G >. ) )
32 op1stg 
 |-  ( ( E e. B /\ G e. S ) -> ( 1st ` <. E , G >. ) = E )
33 9 11 32 syl2anc 
 |-  ( ph -> ( 1st ` <. E , G >. ) = E )
34 31 33 eqtrd 
 |-  ( ph -> ( 1st ` U ) = E )
35 34 adantr 
 |-  ( ( ph /\ ( a = U /\ b = V ) ) -> ( 1st ` U ) = E )
36 30 35 eqtrd 
 |-  ( ( ph /\ ( a = U /\ b = V ) ) -> ( 1st ` a ) = E )
37 simprr 
 |-  ( ( ph /\ ( a = U /\ b = V ) ) -> b = V )
38 37 fveq2d 
 |-  ( ( ph /\ ( a = U /\ b = V ) ) -> ( 2nd ` b ) = ( 2nd ` V ) )
39 8 fveq2d 
 |-  ( ph -> ( 2nd ` V ) = ( 2nd ` <. F , H >. ) )
40 op2ndg 
 |-  ( ( F e. B /\ H e. S ) -> ( 2nd ` <. F , H >. ) = H )
41 10 12 40 syl2anc 
 |-  ( ph -> ( 2nd ` <. F , H >. ) = H )
42 39 41 eqtrd 
 |-  ( ph -> ( 2nd ` V ) = H )
43 42 adantr 
 |-  ( ( ph /\ ( a = U /\ b = V ) ) -> ( 2nd ` V ) = H )
44 38 43 eqtrd 
 |-  ( ( ph /\ ( a = U /\ b = V ) ) -> ( 2nd ` b ) = H )
45 36 44 oveq12d 
 |-  ( ( ph /\ ( a = U /\ b = V ) ) -> ( ( 1st ` a ) .x. ( 2nd ` b ) ) = ( E .x. H ) )
46 37 fveq2d 
 |-  ( ( ph /\ ( a = U /\ b = V ) ) -> ( 1st ` b ) = ( 1st ` V ) )
47 8 fveq2d 
 |-  ( ph -> ( 1st ` V ) = ( 1st ` <. F , H >. ) )
48 op1stg 
 |-  ( ( F e. B /\ H e. S ) -> ( 1st ` <. F , H >. ) = F )
49 10 12 48 syl2anc 
 |-  ( ph -> ( 1st ` <. F , H >. ) = F )
50 47 49 eqtrd 
 |-  ( ph -> ( 1st ` V ) = F )
51 50 adantr 
 |-  ( ( ph /\ ( a = U /\ b = V ) ) -> ( 1st ` V ) = F )
52 46 51 eqtrd 
 |-  ( ( ph /\ ( a = U /\ b = V ) ) -> ( 1st ` b ) = F )
53 29 fveq2d 
 |-  ( ( ph /\ ( a = U /\ b = V ) ) -> ( 2nd ` a ) = ( 2nd ` U ) )
54 7 fveq2d 
 |-  ( ph -> ( 2nd ` U ) = ( 2nd ` <. E , G >. ) )
55 op2ndg 
 |-  ( ( E e. B /\ G e. S ) -> ( 2nd ` <. E , G >. ) = G )
56 9 11 55 syl2anc 
 |-  ( ph -> ( 2nd ` <. E , G >. ) = G )
57 54 56 eqtrd 
 |-  ( ph -> ( 2nd ` U ) = G )
58 57 adantr 
 |-  ( ( ph /\ ( a = U /\ b = V ) ) -> ( 2nd ` U ) = G )
59 53 58 eqtrd 
 |-  ( ( ph /\ ( a = U /\ b = V ) ) -> ( 2nd ` a ) = G )
60 52 59 oveq12d 
 |-  ( ( ph /\ ( a = U /\ b = V ) ) -> ( ( 1st ` b ) .x. ( 2nd ` a ) ) = ( F .x. G ) )
61 45 60 oveq12d 
 |-  ( ( ph /\ ( a = U /\ b = V ) ) -> ( ( ( 1st ` a ) .x. ( 2nd ` b ) ) .- ( ( 1st ` b ) .x. ( 2nd ` a ) ) ) = ( ( E .x. H ) .- ( F .x. G ) ) )
62 61 oveq2d 
 |-  ( ( ph /\ ( a = U /\ b = V ) ) -> ( t .x. ( ( ( 1st ` a ) .x. ( 2nd ` b ) ) .- ( ( 1st ` b ) .x. ( 2nd ` a ) ) ) ) = ( t .x. ( ( E .x. H ) .- ( F .x. G ) ) ) )
63 62 eqeq1d 
 |-  ( ( ph /\ ( a = U /\ b = V ) ) -> ( ( t .x. ( ( ( 1st ` a ) .x. ( 2nd ` b ) ) .- ( ( 1st ` b ) .x. ( 2nd ` a ) ) ) ) = .0. <-> ( t .x. ( ( E .x. H ) .- ( F .x. G ) ) ) = .0. ) )
64 63 rexbidv 
 |-  ( ( 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. ( ( E .x. H ) .- ( F .x. G ) ) ) = .0. ) )
65 28 64 brab2d 
 |-  ( ph -> ( U .~ V <-> ( ( U e. ( B X. S ) /\ V e. ( B X. S ) ) /\ E. t e. S ( t .x. ( ( E .x. H ) .- ( F .x. G ) ) ) = .0. ) ) )
66 24 65 mpbird 
 |-  ( ph -> U .~ V )