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

Metamath Proof Explorer

Theorem ringurd

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

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

Proof

Step Hyp Ref Expression
1 ringurd.b ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝑅 ) )
2 ringurd.p ⊢ ( 𝜑 → · = ( .r ‘ 𝑅 ) )
3 ringurd.z ⊢ ( 𝜑 → 1 ∈ 𝐵 )
4 ringurd.i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 1 · 𝑥 ) = 𝑥 )
5 ringurd.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 ‘ 𝑅 ) )