rloc1r

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

	Ref	Expression
Hypotheses	rloc0g.1	⊢ 0 = ( 0_g ‘ 𝑅 )
	rloc0g.2	⊢ 1 = ( 1_r ‘ 𝑅 )
	rloc0g.3	⊢ 𝐿 = ( 𝑅 RLocal 𝑆 )
	rloc0g.4	⊢ ∼ = ( 𝑅 ~_RL 𝑆 )
	rloc0g.5	⊢ ( 𝜑 → 𝑅 ∈ CRing )
	rloc0g.6	⊢ ( 𝜑 → 𝑆 ∈ ( SubMnd ‘ ( mulGrp ‘ 𝑅 ) ) )
	rloc1r.i	⊢ 𝐼 = [ ⟨ 1 , 1 ⟩ ] ∼
Assertion	rloc1r	⊢ ( 𝜑 → 𝐼 = ( 1_r ‘ 𝐿 ) )

Proof

Step	Hyp	Ref	Expression
1		rloc0g.1	⊢ 0 = ( 0_g ‘ 𝑅 )
2		rloc0g.2	⊢ 1 = ( 1_r ‘ 𝑅 )
3		rloc0g.3	⊢ 𝐿 = ( 𝑅 RLocal 𝑆 )
4		rloc0g.4	⊢ ∼ = ( 𝑅 ~_RL 𝑆 )
5		rloc0g.5	⊢ ( 𝜑 → 𝑅 ∈ CRing )
6		rloc0g.6	⊢ ( 𝜑 → 𝑆 ∈ ( SubMnd ‘ ( mulGrp ‘ 𝑅 ) ) )
7		rloc1r.i	⊢ 𝐼 = [ ⟨ 1 , 1 ⟩ ] ∼
8		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
9		eqid	⊢ ( ._r ‘ 𝑅 ) = ( ._r ‘ 𝑅 )
10		eqid	⊢ ( +_g ‘ 𝑅 ) = ( +_g ‘ 𝑅 )
11	8 9 10 3 4 5 6	rloccring	⊢ ( 𝜑 → 𝐿 ∈ CRing )
12	11	crngringd	⊢ ( 𝜑 → 𝐿 ∈ Ring )
13		eqid	⊢ ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
14	13 8	mgpbas	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ ( mulGrp ‘ 𝑅 ) )
15	14	submss	⊢ ( 𝑆 ∈ ( SubMnd ‘ ( mulGrp ‘ 𝑅 ) ) → 𝑆 ⊆ ( Base ‘ 𝑅 ) )
16	6 15	syl	⊢ ( 𝜑 → 𝑆 ⊆ ( Base ‘ 𝑅 ) )
17	13 2	ringidval	⊢ 1 = ( 0_g ‘ ( mulGrp ‘ 𝑅 ) )
18	17	subm0cl	⊢ ( 𝑆 ∈ ( SubMnd ‘ ( mulGrp ‘ 𝑅 ) ) → 1 ∈ 𝑆 )
19	6 18	syl	⊢ ( 𝜑 → 1 ∈ 𝑆 )
20	16 19	sseldd	⊢ ( 𝜑 → 1 ∈ ( Base ‘ 𝑅 ) )
21	20 19	opelxpd	⊢ ( 𝜑 → ⟨ 1 , 1 ⟩ ∈ ( ( Base ‘ 𝑅 ) × 𝑆 ) )
22	4	ovexi	⊢ ∼ ∈ V
23	22	ecelqsi	⊢ ( ⟨ 1 , 1 ⟩ ∈ ( ( Base ‘ 𝑅 ) × 𝑆 ) → [ ⟨ 1 , 1 ⟩ ] ∼ ∈ ( ( ( Base ‘ 𝑅 ) × 𝑆 ) / ∼ ) )
24	21 23	syl	⊢ ( 𝜑 → [ ⟨ 1 , 1 ⟩ ] ∼ ∈ ( ( ( Base ‘ 𝑅 ) × 𝑆 ) / ∼ ) )
25		eqid	⊢ ( -_g ‘ 𝑅 ) = ( -_g ‘ 𝑅 )
26		eqid	⊢ ( ( Base ‘ 𝑅 ) × 𝑆 ) = ( ( Base ‘ 𝑅 ) × 𝑆 )
27	8 1 9 25 26 3 4 5 16	rlocbas	⊢ ( 𝜑 → ( ( ( Base ‘ 𝑅 ) × 𝑆 ) / ∼ ) = ( Base ‘ 𝐿 ) )
28	24 27	eleqtrd	⊢ ( 𝜑 → [ ⟨ 1 , 1 ⟩ ] ∼ ∈ ( Base ‘ 𝐿 ) )
29	5	ad4antr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐿 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ 𝑆 ) ∧ 𝑥 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ∼ ) → 𝑅 ∈ CRing )
30	6	ad4antr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐿 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ 𝑆 ) ∧ 𝑥 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ∼ ) → 𝑆 ∈ ( SubMnd ‘ ( mulGrp ‘ 𝑅 ) ) )
31	20	ad4antr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐿 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ 𝑆 ) ∧ 𝑥 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ∼ ) → 1 ∈ ( Base ‘ 𝑅 ) )
32		simpllr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐿 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ 𝑆 ) ∧ 𝑥 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ∼ ) → 𝑎 ∈ ( Base ‘ 𝑅 ) )
33	30 18	syl	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐿 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ 𝑆 ) ∧ 𝑥 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ∼ ) → 1 ∈ 𝑆 )
34		simplr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐿 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ 𝑆 ) ∧ 𝑥 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ∼ ) → 𝑏 ∈ 𝑆 )
35		eqid	⊢ ( ._r ‘ 𝐿 ) = ( ._r ‘ 𝐿 )
36	8 9 10 3 4 29 30 31 32 33 34 35	rlocmulval	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐿 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ 𝑆 ) ∧ 𝑥 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ∼ ) → ( [ ⟨ 1 , 1 ⟩ ] ∼ ( ._r ‘ 𝐿 ) [ ⟨ 𝑎 , 𝑏 ⟩ ] ∼ ) = [ ⟨ ( 1 ( ._r ‘ 𝑅 ) 𝑎 ) , ( 1 ( ._r ‘ 𝑅 ) 𝑏 ) ⟩ ] ∼ )
37	29	crngringd	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐿 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ 𝑆 ) ∧ 𝑥 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ∼ ) → 𝑅 ∈ Ring )
38	8 9 2 37 32	ringlidmd	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐿 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ 𝑆 ) ∧ 𝑥 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ∼ ) → ( 1 ( ._r ‘ 𝑅 ) 𝑎 ) = 𝑎 )
39	30 15	syl	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐿 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ 𝑆 ) ∧ 𝑥 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ∼ ) → 𝑆 ⊆ ( Base ‘ 𝑅 ) )
40	39 34	sseldd	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐿 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ 𝑆 ) ∧ 𝑥 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ∼ ) → 𝑏 ∈ ( Base ‘ 𝑅 ) )
41	8 9 2 37 40	ringlidmd	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐿 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ 𝑆 ) ∧ 𝑥 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ∼ ) → ( 1 ( ._r ‘ 𝑅 ) 𝑏 ) = 𝑏 )
42	38 41	opeq12d	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐿 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ 𝑆 ) ∧ 𝑥 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ∼ ) → ⟨ ( 1 ( ._r ‘ 𝑅 ) 𝑎 ) , ( 1 ( ._r ‘ 𝑅 ) 𝑏 ) ⟩ = ⟨ 𝑎 , 𝑏 ⟩ )
43	42	eceq1d	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐿 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ 𝑆 ) ∧ 𝑥 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ∼ ) → [ ⟨ ( 1 ( ._r ‘ 𝑅 ) 𝑎 ) , ( 1 ( ._r ‘ 𝑅 ) 𝑏 ) ⟩ ] ∼ = [ ⟨ 𝑎 , 𝑏 ⟩ ] ∼ )
44	36 43	eqtrd	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐿 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ 𝑆 ) ∧ 𝑥 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ∼ ) → ( [ ⟨ 1 , 1 ⟩ ] ∼ ( ._r ‘ 𝐿 ) [ ⟨ 𝑎 , 𝑏 ⟩ ] ∼ ) = [ ⟨ 𝑎 , 𝑏 ⟩ ] ∼ )
45		simpr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐿 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ 𝑆 ) ∧ 𝑥 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ∼ ) → 𝑥 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ∼ )
46	45	oveq2d	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐿 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ 𝑆 ) ∧ 𝑥 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ∼ ) → ( [ ⟨ 1 , 1 ⟩ ] ∼ ( ._r ‘ 𝐿 ) 𝑥 ) = ( [ ⟨ 1 , 1 ⟩ ] ∼ ( ._r ‘ 𝐿 ) [ ⟨ 𝑎 , 𝑏 ⟩ ] ∼ ) )
47	44 46 45	3eqtr4d	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐿 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ 𝑆 ) ∧ 𝑥 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ∼ ) → ( [ ⟨ 1 , 1 ⟩ ] ∼ ( ._r ‘ 𝐿 ) 𝑥 ) = 𝑥 )
48	27	eqcomd	⊢ ( 𝜑 → ( Base ‘ 𝐿 ) = ( ( ( Base ‘ 𝑅 ) × 𝑆 ) / ∼ ) )
49	48	eleq2d	⊢ ( 𝜑 → ( 𝑥 ∈ ( Base ‘ 𝐿 ) ↔ 𝑥 ∈ ( ( ( Base ‘ 𝑅 ) × 𝑆 ) / ∼ ) ) )
50	49	biimpa	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐿 ) ) → 𝑥 ∈ ( ( ( Base ‘ 𝑅 ) × 𝑆 ) / ∼ ) )
51	50	elrlocbasi	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐿 ) ) → ∃ 𝑎 ∈ ( Base ‘ 𝑅 ) ∃ 𝑏 ∈ 𝑆 𝑥 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ∼ )
52	47 51	r19.29vva	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐿 ) ) → ( [ ⟨ 1 , 1 ⟩ ] ∼ ( ._r ‘ 𝐿 ) 𝑥 ) = 𝑥 )
53	8 9 10 3 4 29 30 32 31 34 33 35	rlocmulval	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐿 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ 𝑆 ) ∧ 𝑥 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ∼ ) → ( [ ⟨ 𝑎 , 𝑏 ⟩ ] ∼ ( ._r ‘ 𝐿 ) [ ⟨ 1 , 1 ⟩ ] ∼ ) = [ ⟨ ( 𝑎 ( ._r ‘ 𝑅 ) 1 ) , ( 𝑏 ( ._r ‘ 𝑅 ) 1 ) ⟩ ] ∼ )
54	8 9 2 37 32	ringridmd	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐿 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ 𝑆 ) ∧ 𝑥 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ∼ ) → ( 𝑎 ( ._r ‘ 𝑅 ) 1 ) = 𝑎 )
55	8 9 2 37 40	ringridmd	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐿 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ 𝑆 ) ∧ 𝑥 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ∼ ) → ( 𝑏 ( ._r ‘ 𝑅 ) 1 ) = 𝑏 )
56	54 55	opeq12d	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐿 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ 𝑆 ) ∧ 𝑥 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ∼ ) → ⟨ ( 𝑎 ( ._r ‘ 𝑅 ) 1 ) , ( 𝑏 ( ._r ‘ 𝑅 ) 1 ) ⟩ = ⟨ 𝑎 , 𝑏 ⟩ )
57	56	eceq1d	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐿 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ 𝑆 ) ∧ 𝑥 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ∼ ) → [ ⟨ ( 𝑎 ( ._r ‘ 𝑅 ) 1 ) , ( 𝑏 ( ._r ‘ 𝑅 ) 1 ) ⟩ ] ∼ = [ ⟨ 𝑎 , 𝑏 ⟩ ] ∼ )
58	53 57	eqtrd	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐿 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ 𝑆 ) ∧ 𝑥 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ∼ ) → ( [ ⟨ 𝑎 , 𝑏 ⟩ ] ∼ ( ._r ‘ 𝐿 ) [ ⟨ 1 , 1 ⟩ ] ∼ ) = [ ⟨ 𝑎 , 𝑏 ⟩ ] ∼ )
59	45	oveq1d	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐿 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ 𝑆 ) ∧ 𝑥 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ∼ ) → ( 𝑥 ( ._r ‘ 𝐿 ) [ ⟨ 1 , 1 ⟩ ] ∼ ) = ( [ ⟨ 𝑎 , 𝑏 ⟩ ] ∼ ( ._r ‘ 𝐿 ) [ ⟨ 1 , 1 ⟩ ] ∼ ) )
60	58 59 45	3eqtr4d	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐿 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ 𝑆 ) ∧ 𝑥 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ∼ ) → ( 𝑥 ( ._r ‘ 𝐿 ) [ ⟨ 1 , 1 ⟩ ] ∼ ) = 𝑥 )
61	60 51	r19.29vva	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐿 ) ) → ( 𝑥 ( ._r ‘ 𝐿 ) [ ⟨ 1 , 1 ⟩ ] ∼ ) = 𝑥 )
62	52 61	jca	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐿 ) ) → ( ( [ ⟨ 1 , 1 ⟩ ] ∼ ( ._r ‘ 𝐿 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( ._r ‘ 𝐿 ) [ ⟨ 1 , 1 ⟩ ] ∼ ) = 𝑥 ) )
63	62	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ ( Base ‘ 𝐿 ) ( ( [ ⟨ 1 , 1 ⟩ ] ∼ ( ._r ‘ 𝐿 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( ._r ‘ 𝐿 ) [ ⟨ 1 , 1 ⟩ ] ∼ ) = 𝑥 ) )
64		eqid	⊢ ( Base ‘ 𝐿 ) = ( Base ‘ 𝐿 )
65		eqid	⊢ ( 1_r ‘ 𝐿 ) = ( 1_r ‘ 𝐿 )
66	64 35 65	isringid	⊢ ( 𝐿 ∈ Ring → ( ( [ ⟨ 1 , 1 ⟩ ] ∼ ∈ ( Base ‘ 𝐿 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐿 ) ( ( [ ⟨ 1 , 1 ⟩ ] ∼ ( ._r ‘ 𝐿 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( ._r ‘ 𝐿 ) [ ⟨ 1 , 1 ⟩ ] ∼ ) = 𝑥 ) ) ↔ ( 1_r ‘ 𝐿 ) = [ ⟨ 1 , 1 ⟩ ] ∼ ) )
67	66	biimpa	⊢ ( ( 𝐿 ∈ Ring ∧ ( [ ⟨ 1 , 1 ⟩ ] ∼ ∈ ( Base ‘ 𝐿 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐿 ) ( ( [ ⟨ 1 , 1 ⟩ ] ∼ ( ._r ‘ 𝐿 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( ._r ‘ 𝐿 ) [ ⟨ 1 , 1 ⟩ ] ∼ ) = 𝑥 ) ) ) → ( 1_r ‘ 𝐿 ) = [ ⟨ 1 , 1 ⟩ ] ∼ )
68	12 28 63 67	syl12anc	⊢ ( 𝜑 → ( 1_r ‘ 𝐿 ) = [ ⟨ 1 , 1 ⟩ ] ∼ )
69	7 68	eqtr4id	⊢ ( 𝜑 → 𝐼 = ( 1_r ‘ 𝐿 ) )

Metamath Proof Explorer

Theorem rloc1r

Proof