Metamath Proof Explorer


Theorem rngurd

Description: Deduce the unit of a ring from its properties. (Contributed by Thierry Arnoux, 6-Sep-2016)

Ref Expression
Hypotheses rngurd.b ( 𝜑𝐵 = ( Base ‘ 𝑅 ) )
rngurd.p ( 𝜑· = ( .r𝑅 ) )
rngurd.z ( 𝜑1𝐵 )
rngurd.i ( ( 𝜑𝑥𝐵 ) → ( 1 · 𝑥 ) = 𝑥 )
rngurd.j ( ( 𝜑𝑥𝐵 ) → ( 𝑥 · 1 ) = 𝑥 )
Assertion rngurd ( 𝜑1 = ( 1r𝑅 ) )

Proof

Step Hyp Ref Expression
1 rngurd.b ( 𝜑𝐵 = ( Base ‘ 𝑅 ) )
2 rngurd.p ( 𝜑· = ( .r𝑅 ) )
3 rngurd.z ( 𝜑1𝐵 )
4 rngurd.i ( ( 𝜑𝑥𝐵 ) → ( 1 · 𝑥 ) = 𝑥 )
5 rngurd.j ( ( 𝜑𝑥𝐵 ) → ( 𝑥 · 1 ) = 𝑥 )
6 eqid ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
7 eqid ( .r𝑅 ) = ( .r𝑅 )
8 eqid ( 1r𝑅 ) = ( 1r𝑅 )
9 6 7 8 dfur2 ( 1r𝑅 ) = ( ℩ 𝑒 ( 𝑒 ∈ ( Base ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ( ( 𝑒 ( .r𝑅 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r𝑅 ) 𝑒 ) = 𝑥 ) ) )
10 3 1 eleqtrd ( 𝜑1 ∈ ( Base ‘ 𝑅 ) )
11 4 5 jca ( ( 𝜑𝑥𝐵 ) → ( ( 1 · 𝑥 ) = 𝑥 ∧ ( 𝑥 · 1 ) = 𝑥 ) )
12 11 ralrimiva ( 𝜑 → ∀ 𝑥𝐵 ( ( 1 · 𝑥 ) = 𝑥 ∧ ( 𝑥 · 1 ) = 𝑥 ) )
13 2 adantr ( ( 𝜑𝑥𝐵 ) → · = ( .r𝑅 ) )
14 13 oveqd ( ( 𝜑𝑥𝐵 ) → ( 1 · 𝑥 ) = ( 1 ( .r𝑅 ) 𝑥 ) )
15 14 eqeq1d ( ( 𝜑𝑥𝐵 ) → ( ( 1 · 𝑥 ) = 𝑥 ↔ ( 1 ( .r𝑅 ) 𝑥 ) = 𝑥 ) )
16 13 oveqd ( ( 𝜑𝑥𝐵 ) → ( 𝑥 · 1 ) = ( 𝑥 ( .r𝑅 ) 1 ) )
17 16 eqeq1d ( ( 𝜑𝑥𝐵 ) → ( ( 𝑥 · 1 ) = 𝑥 ↔ ( 𝑥 ( .r𝑅 ) 1 ) = 𝑥 ) )
18 15 17 anbi12d ( ( 𝜑𝑥𝐵 ) → ( ( ( 1 · 𝑥 ) = 𝑥 ∧ ( 𝑥 · 1 ) = 𝑥 ) ↔ ( ( 1 ( .r𝑅 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r𝑅 ) 1 ) = 𝑥 ) ) )
19 1 18 raleqbidva ( 𝜑 → ( ∀ 𝑥𝐵 ( ( 1 · 𝑥 ) = 𝑥 ∧ ( 𝑥 · 1 ) = 𝑥 ) ↔ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ( ( 1 ( .r𝑅 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r𝑅 ) 1 ) = 𝑥 ) ) )
20 12 19 mpbid ( 𝜑 → ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ( ( 1 ( .r𝑅 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r𝑅 ) 1 ) = 𝑥 ) )
21 1 eleq2d ( 𝜑 → ( 𝑒𝐵𝑒 ∈ ( Base ‘ 𝑅 ) ) )
22 13 oveqd ( ( 𝜑𝑥𝐵 ) → ( 𝑒 · 𝑥 ) = ( 𝑒 ( .r𝑅 ) 𝑥 ) )
23 22 eqeq1d ( ( 𝜑𝑥𝐵 ) → ( ( 𝑒 · 𝑥 ) = 𝑥 ↔ ( 𝑒 ( .r𝑅 ) 𝑥 ) = 𝑥 ) )
24 13 oveqd ( ( 𝜑𝑥𝐵 ) → ( 𝑥 · 𝑒 ) = ( 𝑥 ( .r𝑅 ) 𝑒 ) )
25 24 eqeq1d ( ( 𝜑𝑥𝐵 ) → ( ( 𝑥 · 𝑒 ) = 𝑥 ↔ ( 𝑥 ( .r𝑅 ) 𝑒 ) = 𝑥 ) )
26 23 25 anbi12d ( ( 𝜑𝑥𝐵 ) → ( ( ( 𝑒 · 𝑥 ) = 𝑥 ∧ ( 𝑥 · 𝑒 ) = 𝑥 ) ↔ ( ( 𝑒 ( .r𝑅 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r𝑅 ) 𝑒 ) = 𝑥 ) ) )
27 1 26 raleqbidva ( 𝜑 → ( ∀ 𝑥𝐵 ( ( 𝑒 · 𝑥 ) = 𝑥 ∧ ( 𝑥 · 𝑒 ) = 𝑥 ) ↔ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ( ( 𝑒 ( .r𝑅 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r𝑅 ) 𝑒 ) = 𝑥 ) ) )
28 21 27 anbi12d ( 𝜑 → ( ( 𝑒𝐵 ∧ ∀ 𝑥𝐵 ( ( 𝑒 · 𝑥 ) = 𝑥 ∧ ( 𝑥 · 𝑒 ) = 𝑥 ) ) ↔ ( 𝑒 ∈ ( Base ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ( ( 𝑒 ( .r𝑅 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r𝑅 ) 𝑒 ) = 𝑥 ) ) ) )
29 4 ralrimiva ( 𝜑 → ∀ 𝑥𝐵 ( 1 · 𝑥 ) = 𝑥 )
30 29 adantr ( ( 𝜑𝑒𝐵 ) → ∀ 𝑥𝐵 ( 1 · 𝑥 ) = 𝑥 )
31 simpr ( ( 𝜑𝑒𝐵 ) → 𝑒𝐵 )
32 simpr ( ( ( 𝜑𝑒𝐵 ) ∧ 𝑥 = 𝑒 ) → 𝑥 = 𝑒 )
33 32 oveq2d ( ( ( 𝜑𝑒𝐵 ) ∧ 𝑥 = 𝑒 ) → ( 1 · 𝑥 ) = ( 1 · 𝑒 ) )
34 33 32 eqeq12d ( ( ( 𝜑𝑒𝐵 ) ∧ 𝑥 = 𝑒 ) → ( ( 1 · 𝑥 ) = 𝑥 ↔ ( 1 · 𝑒 ) = 𝑒 ) )
35 31 34 rspcdv ( ( 𝜑𝑒𝐵 ) → ( ∀ 𝑥𝐵 ( 1 · 𝑥 ) = 𝑥 → ( 1 · 𝑒 ) = 𝑒 ) )
36 30 35 mpd ( ( 𝜑𝑒𝐵 ) → ( 1 · 𝑒 ) = 𝑒 )
37 36 adantrr ( ( 𝜑 ∧ ( 𝑒𝐵 ∧ ∀ 𝑥𝐵 ( ( 𝑒 · 𝑥 ) = 𝑥 ∧ ( 𝑥 · 𝑒 ) = 𝑥 ) ) ) → ( 1 · 𝑒 ) = 𝑒 )
38 3 adantr ( ( 𝜑 ∧ ( 𝑒𝐵 ∧ ∀ 𝑥𝐵 ( ( 𝑒 · 𝑥 ) = 𝑥 ∧ ( 𝑥 · 𝑒 ) = 𝑥 ) ) ) → 1𝐵 )
39 simprr ( ( 𝜑 ∧ ( 𝑒𝐵 ∧ ∀ 𝑥𝐵 ( ( 𝑒 · 𝑥 ) = 𝑥 ∧ ( 𝑥 · 𝑒 ) = 𝑥 ) ) ) → ∀ 𝑥𝐵 ( ( 𝑒 · 𝑥 ) = 𝑥 ∧ ( 𝑥 · 𝑒 ) = 𝑥 ) )
40 oveq2 ( 𝑥 = 1 → ( 𝑒 · 𝑥 ) = ( 𝑒 · 1 ) )
41 id ( 𝑥 = 1𝑥 = 1 )
42 40 41 eqeq12d ( 𝑥 = 1 → ( ( 𝑒 · 𝑥 ) = 𝑥 ↔ ( 𝑒 · 1 ) = 1 ) )
43 oveq1 ( 𝑥 = 1 → ( 𝑥 · 𝑒 ) = ( 1 · 𝑒 ) )
44 43 41 eqeq12d ( 𝑥 = 1 → ( ( 𝑥 · 𝑒 ) = 𝑥 ↔ ( 1 · 𝑒 ) = 1 ) )
45 42 44 anbi12d ( 𝑥 = 1 → ( ( ( 𝑒 · 𝑥 ) = 𝑥 ∧ ( 𝑥 · 𝑒 ) = 𝑥 ) ↔ ( ( 𝑒 · 1 ) = 1 ∧ ( 1 · 𝑒 ) = 1 ) ) )
46 45 rspcva ( ( 1𝐵 ∧ ∀ 𝑥𝐵 ( ( 𝑒 · 𝑥 ) = 𝑥 ∧ ( 𝑥 · 𝑒 ) = 𝑥 ) ) → ( ( 𝑒 · 1 ) = 1 ∧ ( 1 · 𝑒 ) = 1 ) )
47 46 simprd ( ( 1𝐵 ∧ ∀ 𝑥𝐵 ( ( 𝑒 · 𝑥 ) = 𝑥 ∧ ( 𝑥 · 𝑒 ) = 𝑥 ) ) → ( 1 · 𝑒 ) = 1 )
48 38 39 47 syl2anc ( ( 𝜑 ∧ ( 𝑒𝐵 ∧ ∀ 𝑥𝐵 ( ( 𝑒 · 𝑥 ) = 𝑥 ∧ ( 𝑥 · 𝑒 ) = 𝑥 ) ) ) → ( 1 · 𝑒 ) = 1 )
49 37 48 eqtr3d ( ( 𝜑 ∧ ( 𝑒𝐵 ∧ ∀ 𝑥𝐵 ( ( 𝑒 · 𝑥 ) = 𝑥 ∧ ( 𝑥 · 𝑒 ) = 𝑥 ) ) ) → 𝑒 = 1 )
50 49 ex ( 𝜑 → ( ( 𝑒𝐵 ∧ ∀ 𝑥𝐵 ( ( 𝑒 · 𝑥 ) = 𝑥 ∧ ( 𝑥 · 𝑒 ) = 𝑥 ) ) → 𝑒 = 1 ) )
51 28 50 sylbird ( 𝜑 → ( ( 𝑒 ∈ ( Base ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ( ( 𝑒 ( .r𝑅 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r𝑅 ) 𝑒 ) = 𝑥 ) ) → 𝑒 = 1 ) )
52 51 alrimiv ( 𝜑 → ∀ 𝑒 ( ( 𝑒 ∈ ( Base ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ( ( 𝑒 ( .r𝑅 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r𝑅 ) 𝑒 ) = 𝑥 ) ) → 𝑒 = 1 ) )
53 eleq1 ( 𝑒 = 1 → ( 𝑒 ∈ ( Base ‘ 𝑅 ) ↔ 1 ∈ ( Base ‘ 𝑅 ) ) )
54 oveq1 ( 𝑒 = 1 → ( 𝑒 ( .r𝑅 ) 𝑥 ) = ( 1 ( .r𝑅 ) 𝑥 ) )
55 54 eqeq1d ( 𝑒 = 1 → ( ( 𝑒 ( .r𝑅 ) 𝑥 ) = 𝑥 ↔ ( 1 ( .r𝑅 ) 𝑥 ) = 𝑥 ) )
56 55 ovanraleqv ( 𝑒 = 1 → ( ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ( ( 𝑒 ( .r𝑅 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r𝑅 ) 𝑒 ) = 𝑥 ) ↔ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ( ( 1 ( .r𝑅 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r𝑅 ) 1 ) = 𝑥 ) ) )
57 53 56 anbi12d ( 𝑒 = 1 → ( ( 𝑒 ∈ ( Base ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ( ( 𝑒 ( .r𝑅 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r𝑅 ) 𝑒 ) = 𝑥 ) ) ↔ ( 1 ∈ ( Base ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ( ( 1 ( .r𝑅 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r𝑅 ) 1 ) = 𝑥 ) ) ) )
58 57 eqeu ( ( 1 ∈ ( Base ‘ 𝑅 ) ∧ ( 1 ∈ ( Base ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ( ( 1 ( .r𝑅 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r𝑅 ) 1 ) = 𝑥 ) ) ∧ ∀ 𝑒 ( ( 𝑒 ∈ ( Base ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ( ( 𝑒 ( .r𝑅 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r𝑅 ) 𝑒 ) = 𝑥 ) ) → 𝑒 = 1 ) ) → ∃! 𝑒 ( 𝑒 ∈ ( Base ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ( ( 𝑒 ( .r𝑅 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r𝑅 ) 𝑒 ) = 𝑥 ) ) )
59 10 10 20 52 58 syl121anc ( 𝜑 → ∃! 𝑒 ( 𝑒 ∈ ( Base ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ( ( 𝑒 ( .r𝑅 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r𝑅 ) 𝑒 ) = 𝑥 ) ) )
60 57 iota2 ( ( 1𝐵 ∧ ∃! 𝑒 ( 𝑒 ∈ ( Base ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ( ( 𝑒 ( .r𝑅 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r𝑅 ) 𝑒 ) = 𝑥 ) ) ) → ( ( 1 ∈ ( Base ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ( ( 1 ( .r𝑅 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r𝑅 ) 1 ) = 𝑥 ) ) ↔ ( ℩ 𝑒 ( 𝑒 ∈ ( Base ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ( ( 𝑒 ( .r𝑅 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r𝑅 ) 𝑒 ) = 𝑥 ) ) ) = 1 ) )
61 3 59 60 syl2anc ( 𝜑 → ( ( 1 ∈ ( Base ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ( ( 1 ( .r𝑅 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r𝑅 ) 1 ) = 𝑥 ) ) ↔ ( ℩ 𝑒 ( 𝑒 ∈ ( Base ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ( ( 𝑒 ( .r𝑅 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r𝑅 ) 𝑒 ) = 𝑥 ) ) ) = 1 ) )
62 10 20 61 mpbi2and ( 𝜑 → ( ℩ 𝑒 ( 𝑒 ∈ ( Base ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ( ( 𝑒 ( .r𝑅 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r𝑅 ) 𝑒 ) = 𝑥 ) ) ) = 1 )
63 9 62 eqtr2id ( 𝜑1 = ( 1r𝑅 ) )