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 )

Metamath Proof Explorer

Theorem erlbrd

Proof