This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 crng32d ⊢ ( 𝜑 → ( ( 𝑇 · 𝐸 ) · 𝐺 ) = ( ( 𝑇 · 𝐺 ) · 𝐸 ) )
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 ⊢ ( 𝜑 → 𝑈 ∼ 𝑉 )