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

Metamath Proof Explorer

Theorem rloc1r

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

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

Proof

Step Hyp Ref Expression
1 rloc0g.1 ⊢ 0 = ( 0g ‘ 𝑅 )
2 rloc0g.2 ⊢ 1 = ( 1r ‘ 𝑅 )
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 = ( 0g ‘ ( 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 ⊢ ( 1r ‘ 𝐿 ) = ( 1r ‘ 𝐿 )
66 64 35 65 isringid ⊢ ( 𝐿 ∈ Ring → ( ( [ ⟨ 1 , 1 ⟩ ] ∼ ∈ ( Base ‘ 𝐿 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐿 ) ( ( [ ⟨ 1 , 1 ⟩ ] ∼ ( .r ‘ 𝐿 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r ‘ 𝐿 ) [ ⟨ 1 , 1 ⟩ ] ∼ ) = 𝑥 ) ) ↔ ( 1r ‘ 𝐿 ) = [ ⟨ 1 , 1 ⟩ ] ∼ ) )
67 66 biimpa ⊢ ( ( 𝐿 ∈ Ring ∧ ( [ ⟨ 1 , 1 ⟩ ] ∼ ∈ ( Base ‘ 𝐿 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐿 ) ( ( [ ⟨ 1 , 1 ⟩ ] ∼ ( .r ‘ 𝐿 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r ‘ 𝐿 ) [ ⟨ 1 , 1 ⟩ ] ∼ ) = 𝑥 ) ) ) → ( 1r ‘ 𝐿 ) = [ ⟨ 1 , 1 ⟩ ] ∼ )
68 12 28 63 67 syl12anc ⊢ ( 𝜑 → ( 1r ‘ 𝐿 ) = [ ⟨ 1 , 1 ⟩ ] ∼ )
69 7 68 eqtr4id ⊢ ( 𝜑 → 𝐼 = ( 1r ‘ 𝐿 ) )