rloc1r

Description: The multiplicative identity of a ring localization. (Contributed by Thierry Arnoux, 4-May-2025)

	Ref	Expression
Hypotheses	rloc0g.1	$⊢ \underset{˙}{0} = 0_{R}$
	rloc0g.2	$⊢ \underset{˙}{1} = 1_{R}$
	rloc0g.3	$⊢ L = R RLocal S$
	rloc0g.4	$⊢ \underset{˙}{\sim} = R ~_{RL} S$
	rloc0g.5	$⊢ φ \to R \in CRing$
	rloc0g.6	$⊢ φ \to S \in SubMnd ({mulGrp}_{R})$
	rloc1r.i	$⊢ I = [⟨\underset{˙}{1}, \underset{˙}{1}⟩] \underset{˙}{\sim}$
Assertion	rloc1r	$⊢ φ \to I = 1_{L}$

Proof

Step	Hyp	Ref	Expression
1		rloc0g.1	$⊢ \underset{˙}{0} = 0_{R}$
2		rloc0g.2	$⊢ \underset{˙}{1} = 1_{R}$
3		rloc0g.3	$⊢ L = R RLocal S$
4		rloc0g.4	$⊢ \underset{˙}{\sim} = R ~_{RL} S$
5		rloc0g.5	$⊢ φ \to R \in CRing$
6		rloc0g.6	$⊢ φ \to S \in SubMnd ({mulGrp}_{R})$
7		rloc1r.i	$⊢ I = [⟨\underset{˙}{1}, \underset{˙}{1}⟩] \underset{˙}{\sim}$
8		eqid	$⊢ {Base}_{R} = {Base}_{R}$
9		eqid	$⊢ \cdot_{R} = \cdot_{R}$
10		eqid	$⊢ +_{R} = +_{R}$
11	8 9 10 3 4 5 6	rloccring	$⊢ φ \to L \in CRing$
12	11	crngringd	$⊢ φ \to L \in Ring$
13		eqid	$⊢ {mulGrp}_{R} = {mulGrp}_{R}$
14	13 8	mgpbas	$⊢ {Base}_{R} = {Base}_{{mulGrp}_{R}}$
15	14	submss	$⊢ S \in SubMnd ({mulGrp}_{R}) \to S \subseteq {Base}_{R}$
16	6 15	syl	$⊢ φ \to S \subseteq {Base}_{R}$
17	13 2	ringidval	$⊢ \underset{˙}{1} = 0_{{mulGrp}_{R}}$
18	17	subm0cl	$⊢ S \in SubMnd ({mulGrp}_{R}) \to \underset{˙}{1} \in S$
19	6 18	syl	$⊢ φ \to \underset{˙}{1} \in S$
20	16 19	sseldd	$⊢ φ \to \underset{˙}{1} \in {Base}_{R}$
21	20 19	opelxpd	$⊢ φ \to ⟨\underset{˙}{1}, \underset{˙}{1}⟩ \in ({Base}_{R} \times S)$
22	4	ovexi	$⊢ \underset{˙}{\sim} \in V$
23	22	ecelqsi	$⊢ ⟨\underset{˙}{1}, \underset{˙}{1}⟩ \in ({Base}_{R} \times S) \to [⟨\underset{˙}{1}, \underset{˙}{1}⟩] \underset{˙}{\sim} \in (({Base}_{R} \times S) / \underset{˙}{\sim})$
24	21 23	syl	$⊢ φ \to [⟨\underset{˙}{1}, \underset{˙}{1}⟩] \underset{˙}{\sim} \in (({Base}_{R} \times S) / \underset{˙}{\sim})$
25		eqid	$⊢ -_{R} = -_{R}$
26		eqid	$⊢ {Base}_{R} \times S = {Base}_{R} \times S$
27	8 1 9 25 26 3 4 5 16	rlocbas	$⊢ φ \to ({Base}_{R} \times S) / \underset{˙}{\sim} = {Base}_{L}$
28	24 27	eleqtrd	$⊢ φ \to [⟨\underset{˙}{1}, \underset{˙}{1}⟩] \underset{˙}{\sim} \in {Base}_{L}$
29	5	ad4antr	$⊢ ((((φ \land x \in {Base}_{L}) \land a \in {Base}_{R}) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \to R \in CRing$
30	6	ad4antr	$⊢ ((((φ \land x \in {Base}_{L}) \land a \in {Base}_{R}) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \to S \in SubMnd ({mulGrp}_{R})$
31	20	ad4antr	$⊢ ((((φ \land x \in {Base}_{L}) \land a \in {Base}_{R}) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \to \underset{˙}{1} \in {Base}_{R}$
32		simpllr	$⊢ ((((φ \land x \in {Base}_{L}) \land a \in {Base}_{R}) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \to a \in {Base}_{R}$
33	30 18	syl	$⊢ ((((φ \land x \in {Base}_{L}) \land a \in {Base}_{R}) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \to \underset{˙}{1} \in S$
34		simplr	$⊢ ((((φ \land x \in {Base}_{L}) \land a \in {Base}_{R}) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \to b \in S$
35		eqid	$⊢ \cdot_{L} = \cdot_{L}$
36	8 9 10 3 4 29 30 31 32 33 34 35	rlocmulval	$⊢ ((((φ \land x \in {Base}_{L}) \land a \in {Base}_{R}) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \to [⟨\underset{˙}{1}, \underset{˙}{1}⟩] \underset{˙}{\sim} \cdot_{L} [⟨a, b⟩] \underset{˙}{\sim} = [⟨\underset{˙}{1} \cdot_{R} a, \underset{˙}{1} \cdot_{R} b⟩] \underset{˙}{\sim}$
37	29	crngringd	$⊢ ((((φ \land x \in {Base}_{L}) \land a \in {Base}_{R}) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \to R \in Ring$
38	8 9 2 37 32	ringlidmd	$⊢ ((((φ \land x \in {Base}_{L}) \land a \in {Base}_{R}) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \to \underset{˙}{1} \cdot_{R} a = a$
39	30 15	syl	$⊢ ((((φ \land x \in {Base}_{L}) \land a \in {Base}_{R}) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \to S \subseteq {Base}_{R}$
40	39 34	sseldd	$⊢ ((((φ \land x \in {Base}_{L}) \land a \in {Base}_{R}) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \to b \in {Base}_{R}$
41	8 9 2 37 40	ringlidmd	$⊢ ((((φ \land x \in {Base}_{L}) \land a \in {Base}_{R}) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \to \underset{˙}{1} \cdot_{R} b = b$
42	38 41	opeq12d	$⊢ ((((φ \land x \in {Base}_{L}) \land a \in {Base}_{R}) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \to ⟨\underset{˙}{1} \cdot_{R} a, \underset{˙}{1} \cdot_{R} b⟩ = ⟨a, b⟩$
43	42	eceq1d	$⊢ ((((φ \land x \in {Base}_{L}) \land a \in {Base}_{R}) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \to [⟨\underset{˙}{1} \cdot_{R} a, \underset{˙}{1} \cdot_{R} b⟩] \underset{˙}{\sim} = [⟨a, b⟩] \underset{˙}{\sim}$
44	36 43	eqtrd	$⊢ ((((φ \land x \in {Base}_{L}) \land a \in {Base}_{R}) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \to [⟨\underset{˙}{1}, \underset{˙}{1}⟩] \underset{˙}{\sim} \cdot_{L} [⟨a, b⟩] \underset{˙}{\sim} = [⟨a, b⟩] \underset{˙}{\sim}$
45		simpr	$⊢ ((((φ \land x \in {Base}_{L}) \land a \in {Base}_{R}) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \to x = [⟨a, b⟩] \underset{˙}{\sim}$
46	45	oveq2d	$⊢ ((((φ \land x \in {Base}_{L}) \land a \in {Base}_{R}) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \to [⟨\underset{˙}{1}, \underset{˙}{1}⟩] \underset{˙}{\sim} \cdot_{L} x = [⟨\underset{˙}{1}, \underset{˙}{1}⟩] \underset{˙}{\sim} \cdot_{L} [⟨a, b⟩] \underset{˙}{\sim}$
47	44 46 45	3eqtr4d	$⊢ ((((φ \land x \in {Base}_{L}) \land a \in {Base}_{R}) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \to [⟨\underset{˙}{1}, \underset{˙}{1}⟩] \underset{˙}{\sim} \cdot_{L} x = x$
48	27	eqcomd	$⊢ φ \to {Base}_{L} = ({Base}_{R} \times S) / \underset{˙}{\sim}$
49	48	eleq2d	$⊢ φ \to (x \in {Base}_{L} \leftrightarrow x \in (({Base}_{R} \times S) / \underset{˙}{\sim}))$
50	49	biimpa	$⊢ (φ \land x \in {Base}_{L}) \to x \in (({Base}_{R} \times S) / \underset{˙}{\sim})$
51	50	elrlocbasi	$⊢ (φ \land x \in {Base}_{L}) \to \exists a \in {Base}_{R} \exists b \in S x = [⟨a, b⟩] \underset{˙}{\sim}$
52	47 51	r19.29vva	$⊢ (φ \land x \in {Base}_{L}) \to [⟨\underset{˙}{1}, \underset{˙}{1}⟩] \underset{˙}{\sim} \cdot_{L} x = x$
53	8 9 10 3 4 29 30 32 31 34 33 35	rlocmulval	$⊢ ((((φ \land x \in {Base}_{L}) \land a \in {Base}_{R}) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \to [⟨a, b⟩] \underset{˙}{\sim} \cdot_{L} [⟨\underset{˙}{1}, \underset{˙}{1}⟩] \underset{˙}{\sim} = [⟨a \cdot_{R} \underset{˙}{1}, b \cdot_{R} \underset{˙}{1}⟩] \underset{˙}{\sim}$
54	8 9 2 37 32	ringridmd	$⊢ ((((φ \land x \in {Base}_{L}) \land a \in {Base}_{R}) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \to a \cdot_{R} \underset{˙}{1} = a$
55	8 9 2 37 40	ringridmd	$⊢ ((((φ \land x \in {Base}_{L}) \land a \in {Base}_{R}) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \to b \cdot_{R} \underset{˙}{1} = b$
56	54 55	opeq12d	$⊢ ((((φ \land x \in {Base}_{L}) \land a \in {Base}_{R}) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \to ⟨a \cdot_{R} \underset{˙}{1}, b \cdot_{R} \underset{˙}{1}⟩ = ⟨a, b⟩$
57	56	eceq1d	$⊢ ((((φ \land x \in {Base}_{L}) \land a \in {Base}_{R}) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \to [⟨a \cdot_{R} \underset{˙}{1}, b \cdot_{R} \underset{˙}{1}⟩] \underset{˙}{\sim} = [⟨a, b⟩] \underset{˙}{\sim}$
58	53 57	eqtrd	$⊢ ((((φ \land x \in {Base}_{L}) \land a \in {Base}_{R}) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \to [⟨a, b⟩] \underset{˙}{\sim} \cdot_{L} [⟨\underset{˙}{1}, \underset{˙}{1}⟩] \underset{˙}{\sim} = [⟨a, b⟩] \underset{˙}{\sim}$
59	45	oveq1d	$⊢ ((((φ \land x \in {Base}_{L}) \land a \in {Base}_{R}) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \to x \cdot_{L} [⟨\underset{˙}{1}, \underset{˙}{1}⟩] \underset{˙}{\sim} = [⟨a, b⟩] \underset{˙}{\sim} \cdot_{L} [⟨\underset{˙}{1}, \underset{˙}{1}⟩] \underset{˙}{\sim}$
60	58 59 45	3eqtr4d	$⊢ ((((φ \land x \in {Base}_{L}) \land a \in {Base}_{R}) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \to x \cdot_{L} [⟨\underset{˙}{1}, \underset{˙}{1}⟩] \underset{˙}{\sim} = x$
61	60 51	r19.29vva	$⊢ (φ \land x \in {Base}_{L}) \to x \cdot_{L} [⟨\underset{˙}{1}, \underset{˙}{1}⟩] \underset{˙}{\sim} = x$
62	52 61	jca	$⊢ (φ \land x \in {Base}_{L}) \to ([⟨\underset{˙}{1}, \underset{˙}{1}⟩] \underset{˙}{\sim} \cdot_{L} x = x \land x \cdot_{L} [⟨\underset{˙}{1}, \underset{˙}{1}⟩] \underset{˙}{\sim} = x)$
63	62	ralrimiva	$⊢ φ \to \forall x \in {Base}_{L} ([⟨\underset{˙}{1}, \underset{˙}{1}⟩] \underset{˙}{\sim} \cdot_{L} x = x \land x \cdot_{L} [⟨\underset{˙}{1}, \underset{˙}{1}⟩] \underset{˙}{\sim} = x)$
64		eqid	$⊢ {Base}_{L} = {Base}_{L}$
65		eqid	$⊢ 1_{L} = 1_{L}$
66	64 35 65	isringid	$⊢ L \in Ring \to (([⟨\underset{˙}{1}, \underset{˙}{1}⟩] \underset{˙}{\sim} \in {Base}_{L} \land \forall x \in {Base}_{L} ([⟨\underset{˙}{1}, \underset{˙}{1}⟩] \underset{˙}{\sim} \cdot_{L} x = x \land x \cdot_{L} [⟨\underset{˙}{1}, \underset{˙}{1}⟩] \underset{˙}{\sim} = x)) \leftrightarrow 1_{L} = [⟨\underset{˙}{1}, \underset{˙}{1}⟩] \underset{˙}{\sim})$
67	66	biimpa	$⊢ (L \in Ring \land ([⟨\underset{˙}{1}, \underset{˙}{1}⟩] \underset{˙}{\sim} \in {Base}_{L} \land \forall x \in {Base}_{L} ([⟨\underset{˙}{1}, \underset{˙}{1}⟩] \underset{˙}{\sim} \cdot_{L} x = x \land x \cdot_{L} [⟨\underset{˙}{1}, \underset{˙}{1}⟩] \underset{˙}{\sim} = x))) \to 1_{L} = [⟨\underset{˙}{1}, \underset{˙}{1}⟩] \underset{˙}{\sim}$
68	12 28 63 67	syl12anc	$⊢ φ \to 1_{L} = [⟨\underset{˙}{1}, \underset{˙}{1}⟩] \underset{˙}{\sim}$
69	7 68	eqtr4id	$⊢ φ \to I = 1_{L}$

Metamath Proof Explorer

Theorem rloc1r

Proof