Theorem erlbr2d

Description: Deduce the ring localization equivalence relation. Pairs <. E , G >. and <. T x. E , T x. G >. for T e. S are equivalent under the localization relation. (Contributed by Thierry Arnoux, 4-May-2025)

	Ref	Expression
Hypotheses	erlbr2d.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	erlbr2d.q	⊢ ∼ = ( 𝑅 ~RL 𝑆 )
	erlbr2d.r	⊢ ( 𝜑 → 𝑅 ∈ CRing )
	erlbr2d.s	⊢ ( 𝜑 → 𝑆 ∈ ( SubMnd ‘ ( mulGrp ‘ 𝑅 ) ) )
	erlbr2d.m	⊢ · = ( .r ‘ 𝑅 )
	erlbr2d.u	⊢ ( 𝜑 → 𝑈 = ⟨ 𝐸 , 𝐺 ⟩ )
	erlbr2d.v	⊢ ( 𝜑 → 𝑉 = ⟨ 𝐹 , 𝐻 ⟩ )
	erlbr2d.e	⊢ ( 𝜑 → 𝐸 ∈ 𝐵 )
	erlbr2d.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
	erlbr2d.g	⊢ ( 𝜑 → 𝐺 ∈ 𝑆 )
	erlbr2d.h	⊢ ( 𝜑 → 𝐻 ∈ 𝑆 )
	erlbr2d.1	⊢ ( 𝜑 → 𝑇 ∈ 𝑆 )
	erlbr2d.2	⊢ ( 𝜑 → 𝐹 = ( 𝑇 · 𝐸 ) )
	erlbr2d.3	⊢ ( 𝜑 → 𝐻 = ( 𝑇 · 𝐺 ) )
Assertion	erlbr2d	⊢ ( 𝜑 → 𝑈 ∼ 𝑉 )

Proof

Step	Hyp	Ref	Expression
1		erlbr2d.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		erlbr2d.q	⊢ ∼ = ( 𝑅 ~RL 𝑆 )
3		erlbr2d.r	⊢ ( 𝜑 → 𝑅 ∈ CRing )
4		erlbr2d.s	⊢ ( 𝜑 → 𝑆 ∈ ( SubMnd ‘ ( mulGrp ‘ 𝑅 ) ) )
5		erlbr2d.m	⊢ · = ( .r ‘ 𝑅 )
6		erlbr2d.u	⊢ ( 𝜑 → 𝑈 = ⟨ 𝐸 , 𝐺 ⟩ )
7		erlbr2d.v	⊢ ( 𝜑 → 𝑉 = ⟨ 𝐹 , 𝐻 ⟩ )
8		erlbr2d.e	⊢ ( 𝜑 → 𝐸 ∈ 𝐵 )
9		erlbr2d.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
10		erlbr2d.g	⊢ ( 𝜑 → 𝐺 ∈ 𝑆 )
11		erlbr2d.h	⊢ ( 𝜑 → 𝐻 ∈ 𝑆 )
12		erlbr2d.1	⊢ ( 𝜑 → 𝑇 ∈ 𝑆 )
13		erlbr2d.2	⊢ ( 𝜑 → 𝐹 = ( 𝑇 · 𝐸 ) )
14		erlbr2d.3	⊢ ( 𝜑 → 𝐻 = ( 𝑇 · 𝐺 ) )
15		eqid	⊢ ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
16	15 1	mgpbas	⊢ 𝐵 = ( Base ‘ ( mulGrp ‘ 𝑅 ) )
17	16	submss	⊢ ( 𝑆 ∈ ( SubMnd ‘ ( mulGrp ‘ 𝑅 ) ) → 𝑆 ⊆ 𝐵 )
18	4 17	syl	⊢ ( 𝜑 → 𝑆 ⊆ 𝐵 )
19		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
20		eqid	⊢ ( -g ‘ 𝑅 ) = ( -g ‘ 𝑅 )
21		eqid	⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
22	15 21	ringidval	⊢ ( 1r ‘ 𝑅 ) = ( 0g ‘ ( mulGrp ‘ 𝑅 ) )
23	22	subm0cl	⊢ ( 𝑆 ∈ ( SubMnd ‘ ( mulGrp ‘ 𝑅 ) ) → ( 1r ‘ 𝑅 ) ∈ 𝑆 )
24	4 23	syl	⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) ∈ 𝑆 )
25	14	oveq2d	⊢ ( 𝜑 → ( 𝐸 · 𝐻 ) = ( 𝐸 · ( 𝑇 · 𝐺 ) ) )
26	13	oveq1d	⊢ ( 𝜑 → ( 𝐹 · 𝐺 ) = ( ( 𝑇 · 𝐸 ) · 𝐺 ) )
27	25 26	oveq12d	⊢ ( 𝜑 → ( ( 𝐸 · 𝐻 ) ( -g ‘ 𝑅 ) ( 𝐹 · 𝐺 ) ) = ( ( 𝐸 · ( 𝑇 · 𝐺 ) ) ( -g ‘ 𝑅 ) ( ( 𝑇 · 𝐸 ) · 𝐺 ) ) )
28	18 12	sseldd	⊢ ( 𝜑 → 𝑇 ∈ 𝐵 )
29	18 10	sseldd	⊢ ( 𝜑 → 𝐺 ∈ 𝐵 )
30	1 5 3 28 8 29	cringmul32d	⊢ ( 𝜑 → ( ( 𝑇 · 𝐸 ) · 𝐺 ) = ( ( 𝑇 · 𝐺 ) · 𝐸 ) )
31	3	crngringd	⊢ ( 𝜑 → 𝑅 ∈ Ring )
32	1 5 31 28 29	ringcld	⊢ ( 𝜑 → ( 𝑇 · 𝐺 ) ∈ 𝐵 )
33	1 5 3 32 8	crngcomd	⊢ ( 𝜑 → ( ( 𝑇 · 𝐺 ) · 𝐸 ) = ( 𝐸 · ( 𝑇 · 𝐺 ) ) )
34	30 33	eqtrd	⊢ ( 𝜑 → ( ( 𝑇 · 𝐸 ) · 𝐺 ) = ( 𝐸 · ( 𝑇 · 𝐺 ) ) )
35	34	oveq2d	⊢ ( 𝜑 → ( ( 𝐸 · ( 𝑇 · 𝐺 ) ) ( -g ‘ 𝑅 ) ( ( 𝑇 · 𝐸 ) · 𝐺 ) ) = ( ( 𝐸 · ( 𝑇 · 𝐺 ) ) ( -g ‘ 𝑅 ) ( 𝐸 · ( 𝑇 · 𝐺 ) ) ) )
36	3	crnggrpd	⊢ ( 𝜑 → 𝑅 ∈ Grp )
37	1 5 31 8 32	ringcld	⊢ ( 𝜑 → ( 𝐸 · ( 𝑇 · 𝐺 ) ) ∈ 𝐵 )
38	1 19 20	grpsubid	⊢ ( ( 𝑅 ∈ Grp ∧ ( 𝐸 · ( 𝑇 · 𝐺 ) ) ∈ 𝐵 ) → ( ( 𝐸 · ( 𝑇 · 𝐺 ) ) ( -g ‘ 𝑅 ) ( 𝐸 · ( 𝑇 · 𝐺 ) ) ) = ( 0g ‘ 𝑅 ) )
39	36 37 38	syl2anc	⊢ ( 𝜑 → ( ( 𝐸 · ( 𝑇 · 𝐺 ) ) ( -g ‘ 𝑅 ) ( 𝐸 · ( 𝑇 · 𝐺 ) ) ) = ( 0g ‘ 𝑅 ) )
40	27 35 39	3eqtrd	⊢ ( 𝜑 → ( ( 𝐸 · 𝐻 ) ( -g ‘ 𝑅 ) ( 𝐹 · 𝐺 ) ) = ( 0g ‘ 𝑅 ) )
41	40	oveq2d	⊢ ( 𝜑 → ( ( 1r ‘ 𝑅 ) · ( ( 𝐸 · 𝐻 ) ( -g ‘ 𝑅 ) ( 𝐹 · 𝐺 ) ) ) = ( ( 1r ‘ 𝑅 ) · ( 0g ‘ 𝑅 ) ) )
42	18 24	sseldd	⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) ∈ 𝐵 )
43	1 5 19 31 42	ringrzd	⊢ ( 𝜑 → ( ( 1r ‘ 𝑅 ) · ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) )
44	41 43	eqtrd	⊢ ( 𝜑 → ( ( 1r ‘ 𝑅 ) · ( ( 𝐸 · 𝐻 ) ( -g ‘ 𝑅 ) ( 𝐹 · 𝐺 ) ) ) = ( 0g ‘ 𝑅 ) )
45	1 2 18 19 5 20 6 7 8 9 10 11 24 44	erlbrd	⊢ ( 𝜑 → 𝑈 ∼ 𝑉 )