Step |
Hyp |
Ref |
Expression |
1 |
|
isdrngd.b |
⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝑅 ) ) |
2 |
|
isdrngd.t |
⊢ ( 𝜑 → · = ( .r ‘ 𝑅 ) ) |
3 |
|
isdrngd.z |
⊢ ( 𝜑 → 0 = ( 0g ‘ 𝑅 ) ) |
4 |
|
isdrngd.u |
⊢ ( 𝜑 → 1 = ( 1r ‘ 𝑅 ) ) |
5 |
|
isdrngd.r |
⊢ ( 𝜑 → 𝑅 ∈ Ring ) |
6 |
|
isdrngd.n |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ) → ( 𝑥 · 𝑦 ) ≠ 0 ) |
7 |
|
isdrngd.o |
⊢ ( 𝜑 → 1 ≠ 0 ) |
8 |
|
isdrngd.i |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ) → 𝐼 ∈ 𝐵 ) |
9 |
|
isdrngd.j |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ) → 𝐼 ≠ 0 ) |
10 |
|
isdrngrd.k |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ) → ( 𝑥 · 𝐼 ) = 1 ) |
11 |
|
eqid |
⊢ ( oppr ‘ 𝑅 ) = ( oppr ‘ 𝑅 ) |
12 |
|
eqid |
⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 ) |
13 |
11 12
|
opprbas |
⊢ ( Base ‘ 𝑅 ) = ( Base ‘ ( oppr ‘ 𝑅 ) ) |
14 |
1 13
|
eqtrdi |
⊢ ( 𝜑 → 𝐵 = ( Base ‘ ( oppr ‘ 𝑅 ) ) ) |
15 |
|
eqidd |
⊢ ( 𝜑 → ( .r ‘ ( oppr ‘ 𝑅 ) ) = ( .r ‘ ( oppr ‘ 𝑅 ) ) ) |
16 |
|
eqid |
⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 ) |
17 |
11 16
|
oppr0 |
⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ ( oppr ‘ 𝑅 ) ) |
18 |
3 17
|
eqtrdi |
⊢ ( 𝜑 → 0 = ( 0g ‘ ( oppr ‘ 𝑅 ) ) ) |
19 |
|
eqid |
⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 ) |
20 |
11 19
|
oppr1 |
⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ ( oppr ‘ 𝑅 ) ) |
21 |
4 20
|
eqtrdi |
⊢ ( 𝜑 → 1 = ( 1r ‘ ( oppr ‘ 𝑅 ) ) ) |
22 |
11
|
opprring |
⊢ ( 𝑅 ∈ Ring → ( oppr ‘ 𝑅 ) ∈ Ring ) |
23 |
5 22
|
syl |
⊢ ( 𝜑 → ( oppr ‘ 𝑅 ) ∈ Ring ) |
24 |
|
eleq1w |
⊢ ( 𝑦 = 𝑥 → ( 𝑦 ∈ 𝐵 ↔ 𝑥 ∈ 𝐵 ) ) |
25 |
|
neeq1 |
⊢ ( 𝑦 = 𝑥 → ( 𝑦 ≠ 0 ↔ 𝑥 ≠ 0 ) ) |
26 |
24 25
|
anbi12d |
⊢ ( 𝑦 = 𝑥 → ( ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ↔ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ) ) |
27 |
26
|
3anbi2d |
⊢ ( 𝑦 = 𝑥 → ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 ) ) ↔ ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 ) ) ) ) |
28 |
|
oveq1 |
⊢ ( 𝑦 = 𝑥 → ( 𝑦 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑧 ) = ( 𝑥 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑧 ) ) |
29 |
28
|
neeq1d |
⊢ ( 𝑦 = 𝑥 → ( ( 𝑦 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑧 ) ≠ 0 ↔ ( 𝑥 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑧 ) ≠ 0 ) ) |
30 |
27 29
|
imbi12d |
⊢ ( 𝑦 = 𝑥 → ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 ) ) → ( 𝑦 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑧 ) ≠ 0 ) ↔ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 ) ) → ( 𝑥 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑧 ) ≠ 0 ) ) ) |
31 |
|
eleq1w |
⊢ ( 𝑥 = 𝑧 → ( 𝑥 ∈ 𝐵 ↔ 𝑧 ∈ 𝐵 ) ) |
32 |
|
neeq1 |
⊢ ( 𝑥 = 𝑧 → ( 𝑥 ≠ 0 ↔ 𝑧 ≠ 0 ) ) |
33 |
31 32
|
anbi12d |
⊢ ( 𝑥 = 𝑧 → ( ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ↔ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 ) ) ) |
34 |
33
|
3anbi3d |
⊢ ( 𝑥 = 𝑧 → ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ) ↔ ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 ) ) ) ) |
35 |
|
oveq2 |
⊢ ( 𝑥 = 𝑧 → ( 𝑦 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑥 ) = ( 𝑦 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑧 ) ) |
36 |
35
|
neeq1d |
⊢ ( 𝑥 = 𝑧 → ( ( 𝑦 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑥 ) ≠ 0 ↔ ( 𝑦 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑧 ) ≠ 0 ) ) |
37 |
34 36
|
imbi12d |
⊢ ( 𝑥 = 𝑧 → ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ) → ( 𝑦 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑥 ) ≠ 0 ) ↔ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 ) ) → ( 𝑦 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑧 ) ≠ 0 ) ) ) |
38 |
2
|
3ad2ant1 |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ) → · = ( .r ‘ 𝑅 ) ) |
39 |
38
|
oveqd |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ) → ( 𝑥 · 𝑦 ) = ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ) |
40 |
|
eqid |
⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 ) |
41 |
|
eqid |
⊢ ( .r ‘ ( oppr ‘ 𝑅 ) ) = ( .r ‘ ( oppr ‘ 𝑅 ) ) |
42 |
12 40 11 41
|
opprmul |
⊢ ( 𝑦 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑥 ) = ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) |
43 |
39 42
|
eqtr4di |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ) → ( 𝑥 · 𝑦 ) = ( 𝑦 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑥 ) ) |
44 |
43 6
|
eqnetrrd |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ) → ( 𝑦 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑥 ) ≠ 0 ) |
45 |
44
|
3com23 |
⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ) → ( 𝑦 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑥 ) ≠ 0 ) |
46 |
37 45
|
chvarvv |
⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 ) ) → ( 𝑦 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑧 ) ≠ 0 ) |
47 |
30 46
|
chvarvv |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 ) ) → ( 𝑥 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑧 ) ≠ 0 ) |
48 |
12 40 11 41
|
opprmul |
⊢ ( 𝐼 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑥 ) = ( 𝑥 ( .r ‘ 𝑅 ) 𝐼 ) |
49 |
2
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ) → · = ( .r ‘ 𝑅 ) ) |
50 |
49
|
oveqd |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ) → ( 𝑥 · 𝐼 ) = ( 𝑥 ( .r ‘ 𝑅 ) 𝐼 ) ) |
51 |
50 10
|
eqtr3d |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝐼 ) = 1 ) |
52 |
48 51
|
eqtrid |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ) → ( 𝐼 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑥 ) = 1 ) |
53 |
14 15 18 21 23 47 7 8 9 52
|
isdrngd |
⊢ ( 𝜑 → ( oppr ‘ 𝑅 ) ∈ DivRing ) |
54 |
11
|
opprdrng |
⊢ ( 𝑅 ∈ DivRing ↔ ( oppr ‘ 𝑅 ) ∈ DivRing ) |
55 |
53 54
|
sylibr |
⊢ ( 𝜑 → 𝑅 ∈ DivRing ) |