erld2

Description: Main property of the ring localization equivalence relation. (Contributed by Thierry Arnoux, 4-May-2025)

	Ref	Expression
Hypotheses	erld2.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	erld2.e	⊢ ∼ = ( 𝑅 ~_RL 𝑆 )
	erld2.t	⊢ · = ( ._r ‘ 𝑅 )
	erld2.r	⊢ ( 𝜑 → 𝑅 ∈ CRing )
	erld2.s	⊢ ( 𝜑 → 𝑆 ∈ ( SubMnd ‘ ( mulGrp ‘ 𝑅 ) ) )
	erld2.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	erld2.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑆 )
	erld2.z	⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
	erld2.w	⊢ ( 𝜑 → 𝑊 ∈ 𝑆 )
	erld2.1	⊢ ( 𝜑 → [ ⟨ 𝑋 , 𝑌 ⟩ ] ∼ = [ ⟨ 𝑍 , 𝑊 ⟩ ] ∼ )
Assertion	erld2	⊢ ( 𝜑 → ∃ 𝑡 ∈ 𝑆 ( 𝑡 · ( 𝑋 · 𝑊 ) ) = ( 𝑡 · ( 𝑍 · 𝑌 ) ) )

Proof

Step	Hyp	Ref	Expression
1		erld2.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		erld2.e	⊢ ∼ = ( 𝑅 ~_RL 𝑆 )
3		erld2.t	⊢ · = ( ._r ‘ 𝑅 )
4		erld2.r	⊢ ( 𝜑 → 𝑅 ∈ CRing )
5		erld2.s	⊢ ( 𝜑 → 𝑆 ∈ ( SubMnd ‘ ( mulGrp ‘ 𝑅 ) ) )
6		erld2.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
7		erld2.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑆 )
8		erld2.z	⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
9		erld2.w	⊢ ( 𝜑 → 𝑊 ∈ 𝑆 )
10		erld2.1	⊢ ( 𝜑 → [ ⟨ 𝑋 , 𝑌 ⟩ ] ∼ = [ ⟨ 𝑍 , 𝑊 ⟩ ] ∼ )
11		eqid	⊢ ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
12	11 1	mgpbas	⊢ 𝐵 = ( Base ‘ ( mulGrp ‘ 𝑅 ) )
13	12	submss	⊢ ( 𝑆 ∈ ( SubMnd ‘ ( mulGrp ‘ 𝑅 ) ) → 𝑆 ⊆ 𝐵 )
14	5 13	syl	⊢ ( 𝜑 → 𝑆 ⊆ 𝐵 )
15		eqid	⊢ ( 0_g ‘ 𝑅 ) = ( 0_g ‘ 𝑅 )
16		eqid	⊢ ( -_g ‘ 𝑅 ) = ( -_g ‘ 𝑅 )
17		eqid	⊢ ( 1_r ‘ 𝑅 ) = ( 1_r ‘ 𝑅 )
18		eqid	⊢ ( 𝐵 × 𝑆 ) = ( 𝐵 × 𝑆 )
19	1 15 17 3 16 18 2 4 5	erler	⊢ ( 𝜑 → ∼ Er ( 𝐵 × 𝑆 ) )
20	6 7	opelxpd	⊢ ( 𝜑 → ⟨ 𝑋 , 𝑌 ⟩ ∈ ( 𝐵 × 𝑆 ) )
21	19 20	erth	⊢ ( 𝜑 → ( ⟨ 𝑋 , 𝑌 ⟩ ∼ ⟨ 𝑍 , 𝑊 ⟩ ↔ [ ⟨ 𝑋 , 𝑌 ⟩ ] ∼ = [ ⟨ 𝑍 , 𝑊 ⟩ ] ∼ ) )
22	10 21	mpbird	⊢ ( 𝜑 → ⟨ 𝑋 , 𝑌 ⟩ ∼ ⟨ 𝑍 , 𝑊 ⟩ )
23	1 2 14 15 3 16 22	erldi	⊢ ( 𝜑 → ∃ 𝑡 ∈ 𝑆 ( 𝑡 · ( ( ( 1^st ‘ ⟨ 𝑋 , 𝑌 ⟩ ) · ( 2^nd ‘ ⟨ 𝑍 , 𝑊 ⟩ ) ) ( -_g ‘ 𝑅 ) ( ( 1^st ‘ ⟨ 𝑍 , 𝑊 ⟩ ) · ( 2^nd ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ) ) ) = ( 0_g ‘ 𝑅 ) )
24	4	crngringd	⊢ ( 𝜑 → 𝑅 ∈ Ring )
25	24	ringgrpd	⊢ ( 𝜑 → 𝑅 ∈ Grp )
26	25	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑆 ) ∧ ( 𝑡 · ( ( ( 1^st ‘ ⟨ 𝑋 , 𝑌 ⟩ ) · ( 2^nd ‘ ⟨ 𝑍 , 𝑊 ⟩ ) ) ( -_g ‘ 𝑅 ) ( ( 1^st ‘ ⟨ 𝑍 , 𝑊 ⟩ ) · ( 2^nd ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ) ) ) = ( 0_g ‘ 𝑅 ) ) → 𝑅 ∈ Grp )
27	24	adantr	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑆 ) → 𝑅 ∈ Ring )
28	27	adantr	⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑆 ) ∧ ( 𝑡 · ( ( ( 1^st ‘ ⟨ 𝑋 , 𝑌 ⟩ ) · ( 2^nd ‘ ⟨ 𝑍 , 𝑊 ⟩ ) ) ( -_g ‘ 𝑅 ) ( ( 1^st ‘ ⟨ 𝑍 , 𝑊 ⟩ ) · ( 2^nd ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ) ) ) = ( 0_g ‘ 𝑅 ) ) → 𝑅 ∈ Ring )
29	14	sselda	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑆 ) → 𝑡 ∈ 𝐵 )
30	29	adantr	⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑆 ) ∧ ( 𝑡 · ( ( ( 1^st ‘ ⟨ 𝑋 , 𝑌 ⟩ ) · ( 2^nd ‘ ⟨ 𝑍 , 𝑊 ⟩ ) ) ( -_g ‘ 𝑅 ) ( ( 1^st ‘ ⟨ 𝑍 , 𝑊 ⟩ ) · ( 2^nd ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ) ) ) = ( 0_g ‘ 𝑅 ) ) → 𝑡 ∈ 𝐵 )
31	14 9	sseldd	⊢ ( 𝜑 → 𝑊 ∈ 𝐵 )
32	1 3 24 6 31	ringcld	⊢ ( 𝜑 → ( 𝑋 · 𝑊 ) ∈ 𝐵 )
33	32	adantr	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑆 ) → ( 𝑋 · 𝑊 ) ∈ 𝐵 )
34	33	adantr	⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑆 ) ∧ ( 𝑡 · ( ( ( 1^st ‘ ⟨ 𝑋 , 𝑌 ⟩ ) · ( 2^nd ‘ ⟨ 𝑍 , 𝑊 ⟩ ) ) ( -_g ‘ 𝑅 ) ( ( 1^st ‘ ⟨ 𝑍 , 𝑊 ⟩ ) · ( 2^nd ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ) ) ) = ( 0_g ‘ 𝑅 ) ) → ( 𝑋 · 𝑊 ) ∈ 𝐵 )
35	1 3 28 30 34	ringcld	⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑆 ) ∧ ( 𝑡 · ( ( ( 1^st ‘ ⟨ 𝑋 , 𝑌 ⟩ ) · ( 2^nd ‘ ⟨ 𝑍 , 𝑊 ⟩ ) ) ( -_g ‘ 𝑅 ) ( ( 1^st ‘ ⟨ 𝑍 , 𝑊 ⟩ ) · ( 2^nd ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ) ) ) = ( 0_g ‘ 𝑅 ) ) → ( 𝑡 · ( 𝑋 · 𝑊 ) ) ∈ 𝐵 )
36	14 7	sseldd	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
37	1 3 24 8 36	ringcld	⊢ ( 𝜑 → ( 𝑍 · 𝑌 ) ∈ 𝐵 )
38	37	adantr	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑆 ) → ( 𝑍 · 𝑌 ) ∈ 𝐵 )
39	38	adantr	⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑆 ) ∧ ( 𝑡 · ( ( ( 1^st ‘ ⟨ 𝑋 , 𝑌 ⟩ ) · ( 2^nd ‘ ⟨ 𝑍 , 𝑊 ⟩ ) ) ( -_g ‘ 𝑅 ) ( ( 1^st ‘ ⟨ 𝑍 , 𝑊 ⟩ ) · ( 2^nd ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ) ) ) = ( 0_g ‘ 𝑅 ) ) → ( 𝑍 · 𝑌 ) ∈ 𝐵 )
40	1 3 28 30 39	ringcld	⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑆 ) ∧ ( 𝑡 · ( ( ( 1^st ‘ ⟨ 𝑋 , 𝑌 ⟩ ) · ( 2^nd ‘ ⟨ 𝑍 , 𝑊 ⟩ ) ) ( -_g ‘ 𝑅 ) ( ( 1^st ‘ ⟨ 𝑍 , 𝑊 ⟩ ) · ( 2^nd ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ) ) ) = ( 0_g ‘ 𝑅 ) ) → ( 𝑡 · ( 𝑍 · 𝑌 ) ) ∈ 𝐵 )
41		op1stg	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑆 ) → ( 1^st ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = 𝑋 )
42	6 7 41	syl2anc	⊢ ( 𝜑 → ( 1^st ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = 𝑋 )
43		op2ndg	⊢ ( ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝑆 ) → ( 2^nd ‘ ⟨ 𝑍 , 𝑊 ⟩ ) = 𝑊 )
44	8 9 43	syl2anc	⊢ ( 𝜑 → ( 2^nd ‘ ⟨ 𝑍 , 𝑊 ⟩ ) = 𝑊 )
45	42 44	oveq12d	⊢ ( 𝜑 → ( ( 1^st ‘ ⟨ 𝑋 , 𝑌 ⟩ ) · ( 2^nd ‘ ⟨ 𝑍 , 𝑊 ⟩ ) ) = ( 𝑋 · 𝑊 ) )
46		op1stg	⊢ ( ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝑆 ) → ( 1^st ‘ ⟨ 𝑍 , 𝑊 ⟩ ) = 𝑍 )
47	8 9 46	syl2anc	⊢ ( 𝜑 → ( 1^st ‘ ⟨ 𝑍 , 𝑊 ⟩ ) = 𝑍 )
48		op2ndg	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑆 ) → ( 2^nd ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = 𝑌 )
49	6 7 48	syl2anc	⊢ ( 𝜑 → ( 2^nd ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = 𝑌 )
50	47 49	oveq12d	⊢ ( 𝜑 → ( ( 1^st ‘ ⟨ 𝑍 , 𝑊 ⟩ ) · ( 2^nd ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ) = ( 𝑍 · 𝑌 ) )
51	45 50	oveq12d	⊢ ( 𝜑 → ( ( ( 1^st ‘ ⟨ 𝑋 , 𝑌 ⟩ ) · ( 2^nd ‘ ⟨ 𝑍 , 𝑊 ⟩ ) ) ( -_g ‘ 𝑅 ) ( ( 1^st ‘ ⟨ 𝑍 , 𝑊 ⟩ ) · ( 2^nd ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ) ) = ( ( 𝑋 · 𝑊 ) ( -_g ‘ 𝑅 ) ( 𝑍 · 𝑌 ) ) )
52	51	oveq2d	⊢ ( 𝜑 → ( 𝑡 · ( ( ( 1^st ‘ ⟨ 𝑋 , 𝑌 ⟩ ) · ( 2^nd ‘ ⟨ 𝑍 , 𝑊 ⟩ ) ) ( -_g ‘ 𝑅 ) ( ( 1^st ‘ ⟨ 𝑍 , 𝑊 ⟩ ) · ( 2^nd ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ) ) ) = ( 𝑡 · ( ( 𝑋 · 𝑊 ) ( -_g ‘ 𝑅 ) ( 𝑍 · 𝑌 ) ) ) )
53	52	adantr	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑆 ) → ( 𝑡 · ( ( ( 1^st ‘ ⟨ 𝑋 , 𝑌 ⟩ ) · ( 2^nd ‘ ⟨ 𝑍 , 𝑊 ⟩ ) ) ( -_g ‘ 𝑅 ) ( ( 1^st ‘ ⟨ 𝑍 , 𝑊 ⟩ ) · ( 2^nd ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ) ) ) = ( 𝑡 · ( ( 𝑋 · 𝑊 ) ( -_g ‘ 𝑅 ) ( 𝑍 · 𝑌 ) ) ) )
54	1 3 16 27 29 33 38	ringsubdi	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑆 ) → ( 𝑡 · ( ( 𝑋 · 𝑊 ) ( -_g ‘ 𝑅 ) ( 𝑍 · 𝑌 ) ) ) = ( ( 𝑡 · ( 𝑋 · 𝑊 ) ) ( -_g ‘ 𝑅 ) ( 𝑡 · ( 𝑍 · 𝑌 ) ) ) )
55	53 54	eqtrd	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑆 ) → ( 𝑡 · ( ( ( 1^st ‘ ⟨ 𝑋 , 𝑌 ⟩ ) · ( 2^nd ‘ ⟨ 𝑍 , 𝑊 ⟩ ) ) ( -_g ‘ 𝑅 ) ( ( 1^st ‘ ⟨ 𝑍 , 𝑊 ⟩ ) · ( 2^nd ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ) ) ) = ( ( 𝑡 · ( 𝑋 · 𝑊 ) ) ( -_g ‘ 𝑅 ) ( 𝑡 · ( 𝑍 · 𝑌 ) ) ) )
56	55	eqeq1d	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑆 ) → ( ( 𝑡 · ( ( ( 1^st ‘ ⟨ 𝑋 , 𝑌 ⟩ ) · ( 2^nd ‘ ⟨ 𝑍 , 𝑊 ⟩ ) ) ( -_g ‘ 𝑅 ) ( ( 1^st ‘ ⟨ 𝑍 , 𝑊 ⟩ ) · ( 2^nd ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ) ) ) = ( 0_g ‘ 𝑅 ) ↔ ( ( 𝑡 · ( 𝑋 · 𝑊 ) ) ( -_g ‘ 𝑅 ) ( 𝑡 · ( 𝑍 · 𝑌 ) ) ) = ( 0_g ‘ 𝑅 ) ) )
57	56	biimpa	⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑆 ) ∧ ( 𝑡 · ( ( ( 1^st ‘ ⟨ 𝑋 , 𝑌 ⟩ ) · ( 2^nd ‘ ⟨ 𝑍 , 𝑊 ⟩ ) ) ( -_g ‘ 𝑅 ) ( ( 1^st ‘ ⟨ 𝑍 , 𝑊 ⟩ ) · ( 2^nd ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ) ) ) = ( 0_g ‘ 𝑅 ) ) → ( ( 𝑡 · ( 𝑋 · 𝑊 ) ) ( -_g ‘ 𝑅 ) ( 𝑡 · ( 𝑍 · 𝑌 ) ) ) = ( 0_g ‘ 𝑅 ) )
58	1 15 16	grpsubeq0	⊢ ( ( 𝑅 ∈ Grp ∧ ( 𝑡 · ( 𝑋 · 𝑊 ) ) ∈ 𝐵 ∧ ( 𝑡 · ( 𝑍 · 𝑌 ) ) ∈ 𝐵 ) → ( ( ( 𝑡 · ( 𝑋 · 𝑊 ) ) ( -_g ‘ 𝑅 ) ( 𝑡 · ( 𝑍 · 𝑌 ) ) ) = ( 0_g ‘ 𝑅 ) ↔ ( 𝑡 · ( 𝑋 · 𝑊 ) ) = ( 𝑡 · ( 𝑍 · 𝑌 ) ) ) )
59	58	biimpa	⊢ ( ( ( 𝑅 ∈ Grp ∧ ( 𝑡 · ( 𝑋 · 𝑊 ) ) ∈ 𝐵 ∧ ( 𝑡 · ( 𝑍 · 𝑌 ) ) ∈ 𝐵 ) ∧ ( ( 𝑡 · ( 𝑋 · 𝑊 ) ) ( -_g ‘ 𝑅 ) ( 𝑡 · ( 𝑍 · 𝑌 ) ) ) = ( 0_g ‘ 𝑅 ) ) → ( 𝑡 · ( 𝑋 · 𝑊 ) ) = ( 𝑡 · ( 𝑍 · 𝑌 ) ) )
60	26 35 40 57 59	syl31anc	⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑆 ) ∧ ( 𝑡 · ( ( ( 1^st ‘ ⟨ 𝑋 , 𝑌 ⟩ ) · ( 2^nd ‘ ⟨ 𝑍 , 𝑊 ⟩ ) ) ( -_g ‘ 𝑅 ) ( ( 1^st ‘ ⟨ 𝑍 , 𝑊 ⟩ ) · ( 2^nd ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ) ) ) = ( 0_g ‘ 𝑅 ) ) → ( 𝑡 · ( 𝑋 · 𝑊 ) ) = ( 𝑡 · ( 𝑍 · 𝑌 ) ) )
61	60	ex	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑆 ) → ( ( 𝑡 · ( ( ( 1^st ‘ ⟨ 𝑋 , 𝑌 ⟩ ) · ( 2^nd ‘ ⟨ 𝑍 , 𝑊 ⟩ ) ) ( -_g ‘ 𝑅 ) ( ( 1^st ‘ ⟨ 𝑍 , 𝑊 ⟩ ) · ( 2^nd ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ) ) ) = ( 0_g ‘ 𝑅 ) → ( 𝑡 · ( 𝑋 · 𝑊 ) ) = ( 𝑡 · ( 𝑍 · 𝑌 ) ) ) )
62	61	reximdva	⊢ ( 𝜑 → ( ∃ 𝑡 ∈ 𝑆 ( 𝑡 · ( ( ( 1^st ‘ ⟨ 𝑋 , 𝑌 ⟩ ) · ( 2^nd ‘ ⟨ 𝑍 , 𝑊 ⟩ ) ) ( -_g ‘ 𝑅 ) ( ( 1^st ‘ ⟨ 𝑍 , 𝑊 ⟩ ) · ( 2^nd ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ) ) ) = ( 0_g ‘ 𝑅 ) → ∃ 𝑡 ∈ 𝑆 ( 𝑡 · ( 𝑋 · 𝑊 ) ) = ( 𝑡 · ( 𝑍 · 𝑌 ) ) ) )
63	23 62	mpd	⊢ ( 𝜑 → ∃ 𝑡 ∈ 𝑆 ( 𝑡 · ( 𝑋 · 𝑊 ) ) = ( 𝑡 · ( 𝑍 · 𝑌 ) ) )

Metamath Proof Explorer

Theorem erld2

Proof