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	$$⊢B={\mathrm{Base}}_R$$
	rlocinvunit.1	$$⊢\underset{\dot{}}{1}=1_R$$
	rlocinvunit.e	$$⊢\underset{\dot{}}{\sim }=R{~}_{\mathrm{RL}}S$$
	rlocinvunit.l	$$⊢L=R\mathrm{RLocal}S$$
	rlocinvunit.w	$$⊢W=\mathrm{Unit}\left(L\right)$$
	rlocinvunit.r	$$⊢\phi \to R\in \mathrm{CRing}$$
	rlocinvunit.s	$$⊢\phi \to S\in \mathrm{SubMnd}\left({\mathrm{mulGrp}}_R\right)$$
	rlocinvunit.q	$$⊢\phi \to Q\in S$$
Assertion	rlocinvunit	$$⊢\phi \to \left[⟨\underset{\dot{}}{1},Q⟩\right]\underset{\dot{}}{\sim }\in W$$

Proof

Step	Hyp	Ref	Expression
1		rlocinvunit.b	$$⊢B={\mathrm{Base}}_R$$
2		rlocinvunit.1	$$⊢\underset{\dot{}}{1}=1_R$$
3		rlocinvunit.e	$$⊢\underset{\dot{}}{\sim }=R{~}_{\mathrm{RL}}S$$
4		rlocinvunit.l	$$⊢L=R\mathrm{RLocal}S$$
5		rlocinvunit.w	$$⊢W=\mathrm{Unit}\left(L\right)$$
6		rlocinvunit.r	$$⊢\phi \to R\in \mathrm{CRing}$$
7		rlocinvunit.s	$$⊢\phi \to S\in \mathrm{SubMnd}\left({\mathrm{mulGrp}}_R\right)$$
8		rlocinvunit.q	$$⊢\phi \to Q\in S$$
9		oveq2	$$⊢a=\left[⟨Q,\underset{\dot{}}{1}⟩\right]\underset{\dot{}}{\sim }\to \left[⟨\underset{\dot{}}{1},Q⟩\right]\underset{\dot{}}{\sim }{\cdot }_{L}a=\left[⟨\underset{\dot{}}{1},Q⟩\right]\underset{\dot{}}{\sim }{\cdot }_L\left[⟨Q,\underset{\dot{}}{1}⟩\right]\underset{\dot{}}{\sim }$$
10	9	eqeq1d	$$⊢a=\left[⟨Q,\underset{\dot{}}{1}⟩\right]\underset{\dot{}}{\sim }\to \left(\left[⟨\underset{\dot{}}{1},Q⟩\right]\underset{\dot{}}{\sim }{\cdot }_{L}a=1_L\leftrightarrow \left[⟨\underset{\dot{}}{1},Q⟩\right]\underset{\dot{}}{\sim }{\cdot }_L\left[⟨Q,\underset{\dot{}}{1}⟩\right]\underset{\dot{}}{\sim }=1_L\right)$$
11		eqid	$$⊢{\mathrm{mulGrp}}_R={\mathrm{mulGrp}}_R$$
12	11 1	mgpbas	$$⊢B={\mathrm{Base}}_{{\mathrm{mulGrp}}_R}$$
13	12	submss	$$⊢S\in \mathrm{SubMnd}\left({\mathrm{mulGrp}}_R\right)\to S\subseteq B$$
14	7 13	syl	$$⊢\phi \to S\subseteq B$$
15	14 8	sseldd	$$⊢\phi \to Q\in B$$
16	11 2	ringidval	$$⊢\underset{\dot{}}{1}=0_{{\mathrm{mulGrp}}_R}$$
17	16	subm0cl	$$⊢S\in \mathrm{SubMnd}\left({\mathrm{mulGrp}}_R\right)\to \underset{\dot{}}{1}\in S$$
18	7 17	syl	$$⊢\phi \to \underset{\dot{}}{1}\in S$$
19	15 18	opelxpd	$$⊢\phi \to ⟨Q,\underset{\dot{}}{1}⟩\in \left(B\times S\right)$$
20	3	ovexi	$$⊢\underset{\dot{}}{\sim }\in \mathrm{V}$$
21	20	ecelqsi	$$⊢⟨Q,\underset{\dot{}}{1}⟩\in \left(B\times S\right)\to \left[⟨Q,\underset{\dot{}}{1}⟩\right]\underset{\dot{}}{\sim }\in \left(\left(B\times S\right)/\underset{\dot{}}{\sim }\right)$$
22	19 21	syl	$$⊢\phi \to \left[⟨Q,\underset{\dot{}}{1}⟩\right]\underset{\dot{}}{\sim }\in \left(\left(B\times S\right)/\underset{\dot{}}{\sim }\right)$$
23		eqid	$$⊢0_R=0_R$$
24		eqid	$$⊢{\cdot }_R={\cdot }_R$$
25		eqid	$$⊢{-}_R={-}_R$$
26		eqid	$$⊢B\times S=B\times S$$
27	1 23 24 25 26 4 3 6 14	rlocbas	$$⊢\phi \to \left(B\times S\right)/\underset{\dot{}}{\sim }={\mathrm{Base}}_L$$
28	22 27	eleqtrd	$$⊢\phi \to \left[⟨Q,\underset{\dot{}}{1}⟩\right]\underset{\dot{}}{\sim }\in {\mathrm{Base}}_L$$
29		eqid	$$⊢{+}_R={+}_R$$
30	6	crngringd	$$⊢\phi \to R\in \mathrm{Ring}$$
31	1 2 30	ringidcld	$$⊢\phi \to \underset{\dot{}}{1}\in B$$
32		eqid	$$⊢{\cdot }_L={\cdot }_L$$
33	1 24 29 4 3 6 7 31 15 8 18 32	rlocmulval	$$⊢\phi \to \left[⟨\underset{\dot{}}{1},Q⟩\right]\underset{\dot{}}{\sim }{\cdot }_L\left[⟨Q,\underset{\dot{}}{1}⟩\right]\underset{\dot{}}{\sim }=\left[⟨\underset{\dot{}}{1}{\cdot }_{R}Q,Q{\cdot }_R\underset{\dot{}}{1}⟩\right]\underset{\dot{}}{\sim }$$
34	1 23 2 24 25 26 3 6 7	erler	$$⊢\phi \to \underset{\dot{}}{\sim }\mathrm{Er}\left(B\times S\right)$$
35		eqidd	$$⊢\phi \to ⟨\underset{\dot{}}{1},\underset{\dot{}}{1}⟩=⟨\underset{\dot{}}{1},\underset{\dot{}}{1}⟩$$
36	1 24 2 30 15	ringlidmd	$$⊢\phi \to \underset{\dot{}}{1}{\cdot }_{R}Q=Q$$
37	1 24 2 30 15	ringridmd	$$⊢\phi \to Q{\cdot }_R\underset{\dot{}}{1}=Q$$
38	36 37	opeq12d	$$⊢\phi \to ⟨\underset{\dot{}}{1}{\cdot }_{R}Q,Q{\cdot }_R\underset{\dot{}}{1}⟩=⟨Q,Q⟩$$
39	37	eqcomd	$$⊢\phi \to Q=Q{\cdot }_R\underset{\dot{}}{1}$$
40	1 3 6 7 24 35 38 31 15 18 8 8 39 39	erlbr2d	$$⊢\phi \to ⟨\underset{\dot{}}{1},\underset{\dot{}}{1}⟩\underset{\dot{}}{\sim }⟨\underset{\dot{}}{1}{\cdot }_{R}Q,Q{\cdot }_R\underset{\dot{}}{1}⟩$$
41	34 40	erthi	$$⊢\phi \to \left[⟨\underset{\dot{}}{1},\underset{\dot{}}{1}⟩\right]\underset{\dot{}}{\sim }=\left[⟨\underset{\dot{}}{1}{\cdot }_{R}Q,Q{\cdot }_R\underset{\dot{}}{1}⟩\right]\underset{\dot{}}{\sim }$$
42		eqid	$$⊢\left[⟨\underset{\dot{}}{1},\underset{\dot{}}{1}⟩\right]\underset{\dot{}}{\sim }=\left[⟨\underset{\dot{}}{1},\underset{\dot{}}{1}⟩\right]\underset{\dot{}}{\sim }$$
43	23 2 4 3 6 7 42	rloc1r	$$⊢\phi \to \left[⟨\underset{\dot{}}{1},\underset{\dot{}}{1}⟩\right]\underset{\dot{}}{\sim }=1_L$$
44	33 41 43	3eqtr2d	$$⊢\phi \to \left[⟨\underset{\dot{}}{1},Q⟩\right]\underset{\dot{}}{\sim }{\cdot }_L\left[⟨Q,\underset{\dot{}}{1}⟩\right]\underset{\dot{}}{\sim }=1_L$$
45	10 28 44	rspcedvdw	$$⊢\phi \to \exists a\in {\mathrm{Base}}_L\left[⟨\underset{\dot{}}{1},Q⟩\right]\underset{\dot{}}{\sim }{\cdot }_{L}a=1_L$$
46		eqid	$$⊢{\mathrm{Base}}_L={\mathrm{Base}}_L$$
47		eqid	$$⊢1_L=1_L$$
48	31 8	opelxpd	$$⊢\phi \to ⟨\underset{\dot{}}{1},Q⟩\in \left(B\times S\right)$$
49	20	ecelqsi	$$⊢⟨\underset{\dot{}}{1},Q⟩\in \left(B\times S\right)\to \left[⟨\underset{\dot{}}{1},Q⟩\right]\underset{\dot{}}{\sim }\in \left(\left(B\times S\right)/\underset{\dot{}}{\sim }\right)$$
50	48 49	syl	$$⊢\phi \to \left[⟨\underset{\dot{}}{1},Q⟩\right]\underset{\dot{}}{\sim }\in \left(\left(B\times S\right)/\underset{\dot{}}{\sim }\right)$$
51	50 27	eleqtrd	$$⊢\phi \to \left[⟨\underset{\dot{}}{1},Q⟩\right]\underset{\dot{}}{\sim }\in {\mathrm{Base}}_L$$
52	1 24 29 4 3 6 7	rloccring	$$⊢\phi \to L\in \mathrm{CRing}$$
53	46 5 32 47 51 52	isunitc	$$⊢\phi \to \left(\left[⟨\underset{\dot{}}{1},Q⟩\right]\underset{\dot{}}{\sim }\in W\leftrightarrow \exists a\in {\mathrm{Base}}_L\left[⟨\underset{\dot{}}{1},Q⟩\right]\underset{\dot{}}{\sim }{\cdot }_{L}a=1_L\right)$$
54	45 53	mpbird	$$⊢\phi \to \left[⟨\underset{\dot{}}{1},Q⟩\right]\underset{\dot{}}{\sim }\in W$$