Theorem rlocinvunit

Description: In the localization of a ring R at S , inverses of elements of S are units. (Contributed by Thierry Arnoux, 6-Jun-2026)

	Ref	Expression
Hypotheses	rlocinvunit.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	rlocinvunit.1	⊢ 1 = ( 1r ‘ 𝑅 )
	rlocinvunit.e	⊢ ∼ = ( 𝑅 ~RL 𝑆 )
	rlocinvunit.l	⊢ 𝐿 = ( 𝑅 RLocal 𝑆 )
	rlocinvunit.w	⊢ 𝑊 = ( Unit ‘ 𝐿 )
	rlocinvunit.r	⊢ ( 𝜑 → 𝑅 ∈ CRing )
	rlocinvunit.s	⊢ ( 𝜑 → 𝑆 ∈ ( SubMnd ‘ ( mulGrp ‘ 𝑅 ) ) )
	rlocinvunit.q	⊢ ( 𝜑 → 𝑄 ∈ 𝑆 )
Assertion	rlocinvunit	⊢ ( 𝜑 → [ ⟨ 1 , 𝑄 ⟩ ] ∼ ∈ 𝑊 )

Proof

Step	Hyp	Ref	Expression
1		rlocinvunit.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		rlocinvunit.1	⊢ 1 = ( 1r ‘ 𝑅 )
3		rlocinvunit.e	⊢ ∼ = ( 𝑅 ~RL 𝑆 )
4		rlocinvunit.l	⊢ 𝐿 = ( 𝑅 RLocal 𝑆 )
5		rlocinvunit.w	⊢ 𝑊 = ( Unit ‘ 𝐿 )
6		rlocinvunit.r	⊢ ( 𝜑 → 𝑅 ∈ CRing )
7		rlocinvunit.s	⊢ ( 𝜑 → 𝑆 ∈ ( SubMnd ‘ ( mulGrp ‘ 𝑅 ) ) )
8		rlocinvunit.q	⊢ ( 𝜑 → 𝑄 ∈ 𝑆 )
9		oveq2	⊢ ( 𝑎 = [ ⟨ 𝑄 , 1 ⟩ ] ∼ → ( [ ⟨ 1 , 𝑄 ⟩ ] ∼ ( .r ‘ 𝐿 ) 𝑎 ) = ( [ ⟨ 1 , 𝑄 ⟩ ] ∼ ( .r ‘ 𝐿 ) [ ⟨ 𝑄 , 1 ⟩ ] ∼ ) )
10	9	eqeq1d	⊢ ( 𝑎 = [ ⟨ 𝑄 , 1 ⟩ ] ∼ → ( ( [ ⟨ 1 , 𝑄 ⟩ ] ∼ ( .r ‘ 𝐿 ) 𝑎 ) = ( 1r ‘ 𝐿 ) ↔ ( [ ⟨ 1 , 𝑄 ⟩ ] ∼ ( .r ‘ 𝐿 ) [ ⟨ 𝑄 , 1 ⟩ ] ∼ ) = ( 1r ‘ 𝐿 ) ) )
11		eqid	⊢ ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
12	11 1	mgpbas	⊢ 𝐵 = ( Base ‘ ( mulGrp ‘ 𝑅 ) )
13	12	submss	⊢ ( 𝑆 ∈ ( SubMnd ‘ ( mulGrp ‘ 𝑅 ) ) → 𝑆 ⊆ 𝐵 )
14	7 13	syl	⊢ ( 𝜑 → 𝑆 ⊆ 𝐵 )
15	14 8	sseldd	⊢ ( 𝜑 → 𝑄 ∈ 𝐵 )
16	11 2	ringidval	⊢ 1 = ( 0g ‘ ( mulGrp ‘ 𝑅 ) )
17	16	subm0cl	⊢ ( 𝑆 ∈ ( SubMnd ‘ ( mulGrp ‘ 𝑅 ) ) → 1 ∈ 𝑆 )
18	7 17	syl	⊢ ( 𝜑 → 1 ∈ 𝑆 )
19	15 18	opelxpd	⊢ ( 𝜑 → ⟨ 𝑄 , 1 ⟩ ∈ ( 𝐵 × 𝑆 ) )
20	3	ovexi	⊢ ∼ ∈ V
21	20	ecelqsi	⊢ ( ⟨ 𝑄 , 1 ⟩ ∈ ( 𝐵 × 𝑆 ) → [ ⟨ 𝑄 , 1 ⟩ ] ∼ ∈ ( ( 𝐵 × 𝑆 ) / ∼ ) )
22	19 21	syl	⊢ ( 𝜑 → [ ⟨ 𝑄 , 1 ⟩ ] ∼ ∈ ( ( 𝐵 × 𝑆 ) / ∼ ) )
23		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
24		eqid	⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
25		eqid	⊢ ( -g ‘ 𝑅 ) = ( -g ‘ 𝑅 )
26		eqid	⊢ ( 𝐵 × 𝑆 ) = ( 𝐵 × 𝑆 )
27	1 23 24 25 26 4 3 6 14	rlocbas	⊢ ( 𝜑 → ( ( 𝐵 × 𝑆 ) / ∼ ) = ( Base ‘ 𝐿 ) )
28	22 27	eleqtrd	⊢ ( 𝜑 → [ ⟨ 𝑄 , 1 ⟩ ] ∼ ∈ ( Base ‘ 𝐿 ) )
29		eqid	⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
30	6	crngringd	⊢ ( 𝜑 → 𝑅 ∈ Ring )
31	1 2 30	ringidcld	⊢ ( 𝜑 → 1 ∈ 𝐵 )
32		eqid	⊢ ( .r ‘ 𝐿 ) = ( .r ‘ 𝐿 )
33	1 24 29 4 3 6 7 31 15 8 18 32	rlocmulval	⊢ ( 𝜑 → ( [ ⟨ 1 , 𝑄 ⟩ ] ∼ ( .r ‘ 𝐿 ) [ ⟨ 𝑄 , 1 ⟩ ] ∼ ) = [ ⟨ ( 1 ( .r ‘ 𝑅 ) 𝑄 ) , ( 𝑄 ( .r ‘ 𝑅 ) 1 ) ⟩ ] ∼ )
34	1 23 2 24 25 26 3 6 7	erler	⊢ ( 𝜑 → ∼ Er ( 𝐵 × 𝑆 ) )
35		eqidd	⊢ ( 𝜑 → ⟨ 1 , 1 ⟩ = ⟨ 1 , 1 ⟩ )
36	1 24 2 30 15	ringlidmd	⊢ ( 𝜑 → ( 1 ( .r ‘ 𝑅 ) 𝑄 ) = 𝑄 )
37	1 24 2 30 15	ringridmd	⊢ ( 𝜑 → ( 𝑄 ( .r ‘ 𝑅 ) 1 ) = 𝑄 )
38	36 37	opeq12d	⊢ ( 𝜑 → ⟨ ( 1 ( .r ‘ 𝑅 ) 𝑄 ) , ( 𝑄 ( .r ‘ 𝑅 ) 1 ) ⟩ = ⟨ 𝑄 , 𝑄 ⟩ )
39	37	eqcomd	⊢ ( 𝜑 → 𝑄 = ( 𝑄 ( .r ‘ 𝑅 ) 1 ) )
40	1 3 6 7 24 35 38 31 15 18 8 8 39 39	erlbr2d	⊢ ( 𝜑 → ⟨ 1 , 1 ⟩ ∼ ⟨ ( 1 ( .r ‘ 𝑅 ) 𝑄 ) , ( 𝑄 ( .r ‘ 𝑅 ) 1 ) ⟩ )
41	34 40	erthi	⊢ ( 𝜑 → [ ⟨ 1 , 1 ⟩ ] ∼ = [ ⟨ ( 1 ( .r ‘ 𝑅 ) 𝑄 ) , ( 𝑄 ( .r ‘ 𝑅 ) 1 ) ⟩ ] ∼ )
42		eqid	⊢ [ ⟨ 1 , 1 ⟩ ] ∼ = [ ⟨ 1 , 1 ⟩ ] ∼
43	23 2 4 3 6 7 42	rloc1r	⊢ ( 𝜑 → [ ⟨ 1 , 1 ⟩ ] ∼ = ( 1r ‘ 𝐿 ) )
44	33 41 43	3eqtr2d	⊢ ( 𝜑 → ( [ ⟨ 1 , 𝑄 ⟩ ] ∼ ( .r ‘ 𝐿 ) [ ⟨ 𝑄 , 1 ⟩ ] ∼ ) = ( 1r ‘ 𝐿 ) )
45	10 28 44	rspcedvdw	⊢ ( 𝜑 → ∃ 𝑎 ∈ ( Base ‘ 𝐿 ) ( [ ⟨ 1 , 𝑄 ⟩ ] ∼ ( .r ‘ 𝐿 ) 𝑎 ) = ( 1r ‘ 𝐿 ) )
46		eqid	⊢ ( Base ‘ 𝐿 ) = ( Base ‘ 𝐿 )
47		eqid	⊢ ( 1r ‘ 𝐿 ) = ( 1r ‘ 𝐿 )
48	31 8	opelxpd	⊢ ( 𝜑 → ⟨ 1 , 𝑄 ⟩ ∈ ( 𝐵 × 𝑆 ) )
49	20	ecelqsi	⊢ ( ⟨ 1 , 𝑄 ⟩ ∈ ( 𝐵 × 𝑆 ) → [ ⟨ 1 , 𝑄 ⟩ ] ∼ ∈ ( ( 𝐵 × 𝑆 ) / ∼ ) )
50	48 49	syl	⊢ ( 𝜑 → [ ⟨ 1 , 𝑄 ⟩ ] ∼ ∈ ( ( 𝐵 × 𝑆 ) / ∼ ) )
51	50 27	eleqtrd	⊢ ( 𝜑 → [ ⟨ 1 , 𝑄 ⟩ ] ∼ ∈ ( Base ‘ 𝐿 ) )
52	1 24 29 4 3 6 7	rloccring	⊢ ( 𝜑 → 𝐿 ∈ CRing )
53	46 5 32 47 51 52	isunitc	⊢ ( 𝜑 → ( [ ⟨ 1 , 𝑄 ⟩ ] ∼ ∈ 𝑊 ↔ ∃ 𝑎 ∈ ( Base ‘ 𝐿 ) ( [ ⟨ 1 , 𝑄 ⟩ ] ∼ ( .r ‘ 𝐿 ) 𝑎 ) = ( 1r ‘ 𝐿 ) ) )
54	45 53	mpbird	⊢ ( 𝜑 → [ ⟨ 1 , 𝑄 ⟩ ] ∼ ∈ 𝑊 )