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 ‘ 𝑅 ) ) |