Proof of Theorem issrngd
Step | Hyp | Ref
| Expression |
1 | | eqid 2738 |
. . 3
⊢
(Base‘𝑅) =
(Base‘𝑅) |
2 | | eqid 2738 |
. . 3
⊢
(1r‘𝑅) = (1r‘𝑅) |
3 | | eqid 2738 |
. . . 4
⊢
(oppr‘𝑅) = (oppr‘𝑅) |
4 | 3, 2 | oppr1 19499 |
. . 3
⊢
(1r‘𝑅) =
(1r‘(oppr‘𝑅)) |
5 | | eqid 2738 |
. . 3
⊢
(.r‘𝑅) = (.r‘𝑅) |
6 | | eqid 2738 |
. . 3
⊢
(.r‘(oppr‘𝑅)) =
(.r‘(oppr‘𝑅)) |
7 | | issrngd.r |
. . 3
⊢ (𝜑 → 𝑅 ∈ Ring) |
8 | 3 | opprring 19496 |
. . . 4
⊢ (𝑅 ∈ Ring →
(oppr‘𝑅) ∈ Ring) |
9 | 7, 8 | syl 17 |
. . 3
⊢ (𝜑 →
(oppr‘𝑅) ∈ Ring) |
10 | | id 22 |
. . . . . . . . 9
⊢ (𝑥 = (1r‘𝑅) → 𝑥 = (1r‘𝑅)) |
11 | | fveq2 6668 |
. . . . . . . . . 10
⊢ (𝑥 = (1r‘𝑅) →
((*𝑟‘𝑅)‘𝑥) = ((*𝑟‘𝑅)‘(1r‘𝑅))) |
12 | 11 | fveq2d 6672 |
. . . . . . . . 9
⊢ (𝑥 = (1r‘𝑅) →
((*𝑟‘𝑅)‘((*𝑟‘𝑅)‘𝑥)) = ((*𝑟‘𝑅)‘((*𝑟‘𝑅)‘(1r‘𝑅)))) |
13 | 10, 12 | eqeq12d 2754 |
. . . . . . . 8
⊢ (𝑥 = (1r‘𝑅) → (𝑥 = ((*𝑟‘𝑅)‘((*𝑟‘𝑅)‘𝑥)) ↔ (1r‘𝑅) =
((*𝑟‘𝑅)‘((*𝑟‘𝑅)‘(1r‘𝑅))))) |
14 | | issrngd.id |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐾) → ( ∗ ‘( ∗
‘𝑥)) = 𝑥) |
15 | 14 | ex 416 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑥 ∈ 𝐾 → ( ∗ ‘( ∗
‘𝑥)) = 𝑥)) |
16 | | issrngd.k |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐾 = (Base‘𝑅)) |
17 | 16 | eleq2d 2818 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑥 ∈ 𝐾 ↔ 𝑥 ∈ (Base‘𝑅))) |
18 | | issrngd.c |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ∗ =
(*𝑟‘𝑅)) |
19 | 18 | fveq1d 6670 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ( ∗ ‘𝑥) =
((*𝑟‘𝑅)‘𝑥)) |
20 | 18, 19 | fveq12d 6675 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ( ∗ ‘( ∗
‘𝑥)) =
((*𝑟‘𝑅)‘((*𝑟‘𝑅)‘𝑥))) |
21 | 20 | eqeq1d 2740 |
. . . . . . . . . . . 12
⊢ (𝜑 → (( ∗ ‘( ∗
‘𝑥)) = 𝑥 ↔
((*𝑟‘𝑅)‘((*𝑟‘𝑅)‘𝑥)) = 𝑥)) |
22 | 15, 17, 21 | 3imtr3d 296 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑥 ∈ (Base‘𝑅) → ((*𝑟‘𝑅)‘((*𝑟‘𝑅)‘𝑥)) = 𝑥)) |
23 | 22 | imp 410 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) →
((*𝑟‘𝑅)‘((*𝑟‘𝑅)‘𝑥)) = 𝑥) |
24 | 23 | eqcomd 2744 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → 𝑥 = ((*𝑟‘𝑅)‘((*𝑟‘𝑅)‘𝑥))) |
25 | 24 | ralrimiva 3096 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑥 ∈ (Base‘𝑅)𝑥 = ((*𝑟‘𝑅)‘((*𝑟‘𝑅)‘𝑥))) |
26 | 1, 2 | ringidcl 19433 |
. . . . . . . . 9
⊢ (𝑅 ∈ Ring →
(1r‘𝑅)
∈ (Base‘𝑅)) |
27 | 7, 26 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (1r‘𝑅) ∈ (Base‘𝑅)) |
28 | 13, 25, 27 | rspcdva 3526 |
. . . . . . 7
⊢ (𝜑 → (1r‘𝑅) =
((*𝑟‘𝑅)‘((*𝑟‘𝑅)‘(1r‘𝑅)))) |
29 | 28 | oveq1d 7179 |
. . . . . 6
⊢ (𝜑 →
((1r‘𝑅)(.r‘𝑅)((*𝑟‘𝑅)‘(1r‘𝑅))) =
(((*𝑟‘𝑅)‘((*𝑟‘𝑅)‘(1r‘𝑅)))(.r‘𝑅)((*𝑟‘𝑅)‘(1r‘𝑅)))) |
30 | 11 | eleq1d 2817 |
. . . . . . . 8
⊢ (𝑥 = (1r‘𝑅) →
(((*𝑟‘𝑅)‘𝑥) ∈ (Base‘𝑅) ↔ ((*𝑟‘𝑅)‘(1r‘𝑅)) ∈ (Base‘𝑅))) |
31 | | issrngd.cl |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐾) → ( ∗ ‘𝑥) ∈ 𝐾) |
32 | 31 | ex 416 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ 𝐾 → ( ∗ ‘𝑥) ∈ 𝐾)) |
33 | 19, 16 | eleq12d 2827 |
. . . . . . . . . 10
⊢ (𝜑 → (( ∗ ‘𝑥) ∈ 𝐾 ↔ ((*𝑟‘𝑅)‘𝑥) ∈ (Base‘𝑅))) |
34 | 32, 17, 33 | 3imtr3d 296 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ (Base‘𝑅) → ((*𝑟‘𝑅)‘𝑥) ∈ (Base‘𝑅))) |
35 | 34 | ralrimiv 3095 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑥 ∈ (Base‘𝑅)((*𝑟‘𝑅)‘𝑥) ∈ (Base‘𝑅)) |
36 | 30, 35, 27 | rspcdva 3526 |
. . . . . . 7
⊢ (𝜑 →
((*𝑟‘𝑅)‘(1r‘𝑅)) ∈ (Base‘𝑅)) |
37 | | issrngd.dt |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾) → ( ∗ ‘(𝑥 · 𝑦)) = (( ∗ ‘𝑦) · ( ∗
‘𝑥))) |
38 | 37 | 3expib 1123 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾) → ( ∗ ‘(𝑥 · 𝑦)) = (( ∗ ‘𝑦) · ( ∗
‘𝑥)))) |
39 | 16 | eleq2d 2818 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑦 ∈ 𝐾 ↔ 𝑦 ∈ (Base‘𝑅))) |
40 | 17, 39 | anbi12d 634 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾) ↔ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)))) |
41 | | issrngd.t |
. . . . . . . . . . . 12
⊢ (𝜑 → · =
(.r‘𝑅)) |
42 | 41 | oveqd 7181 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑥 · 𝑦) = (𝑥(.r‘𝑅)𝑦)) |
43 | 18, 42 | fveq12d 6675 |
. . . . . . . . . 10
⊢ (𝜑 → ( ∗ ‘(𝑥 · 𝑦)) = ((*𝑟‘𝑅)‘(𝑥(.r‘𝑅)𝑦))) |
44 | 18 | fveq1d 6670 |
. . . . . . . . . . 11
⊢ (𝜑 → ( ∗ ‘𝑦) =
((*𝑟‘𝑅)‘𝑦)) |
45 | 41, 44, 19 | oveq123d 7185 |
. . . . . . . . . 10
⊢ (𝜑 → (( ∗ ‘𝑦) · ( ∗
‘𝑥)) =
(((*𝑟‘𝑅)‘𝑦)(.r‘𝑅)((*𝑟‘𝑅)‘𝑥))) |
46 | 43, 45 | eqeq12d 2754 |
. . . . . . . . 9
⊢ (𝜑 → (( ∗ ‘(𝑥 · 𝑦)) = (( ∗ ‘𝑦) · ( ∗
‘𝑥)) ↔
((*𝑟‘𝑅)‘(𝑥(.r‘𝑅)𝑦)) = (((*𝑟‘𝑅)‘𝑦)(.r‘𝑅)((*𝑟‘𝑅)‘𝑥)))) |
47 | 38, 40, 46 | 3imtr3d 296 |
. . . . . . . 8
⊢ (𝜑 → ((𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) →
((*𝑟‘𝑅)‘(𝑥(.r‘𝑅)𝑦)) = (((*𝑟‘𝑅)‘𝑦)(.r‘𝑅)((*𝑟‘𝑅)‘𝑥)))) |
48 | 47 | ralrimivv 3102 |
. . . . . . 7
⊢ (𝜑 → ∀𝑥 ∈ (Base‘𝑅)∀𝑦 ∈ (Base‘𝑅)((*𝑟‘𝑅)‘(𝑥(.r‘𝑅)𝑦)) = (((*𝑟‘𝑅)‘𝑦)(.r‘𝑅)((*𝑟‘𝑅)‘𝑥))) |
49 | | fvoveq1 7187 |
. . . . . . . . 9
⊢ (𝑥 = (1r‘𝑅) →
((*𝑟‘𝑅)‘(𝑥(.r‘𝑅)𝑦)) = ((*𝑟‘𝑅)‘((1r‘𝑅)(.r‘𝑅)𝑦))) |
50 | 11 | oveq2d 7180 |
. . . . . . . . 9
⊢ (𝑥 = (1r‘𝑅) →
(((*𝑟‘𝑅)‘𝑦)(.r‘𝑅)((*𝑟‘𝑅)‘𝑥)) = (((*𝑟‘𝑅)‘𝑦)(.r‘𝑅)((*𝑟‘𝑅)‘(1r‘𝑅)))) |
51 | 49, 50 | eqeq12d 2754 |
. . . . . . . 8
⊢ (𝑥 = (1r‘𝑅) →
(((*𝑟‘𝑅)‘(𝑥(.r‘𝑅)𝑦)) = (((*𝑟‘𝑅)‘𝑦)(.r‘𝑅)((*𝑟‘𝑅)‘𝑥)) ↔ ((*𝑟‘𝑅)‘((1r‘𝑅)(.r‘𝑅)𝑦)) = (((*𝑟‘𝑅)‘𝑦)(.r‘𝑅)((*𝑟‘𝑅)‘(1r‘𝑅))))) |
52 | | oveq2 7172 |
. . . . . . . . . 10
⊢ (𝑦 =
((*𝑟‘𝑅)‘(1r‘𝑅)) →
((1r‘𝑅)(.r‘𝑅)𝑦) = ((1r‘𝑅)(.r‘𝑅)((*𝑟‘𝑅)‘(1r‘𝑅)))) |
53 | 52 | fveq2d 6672 |
. . . . . . . . 9
⊢ (𝑦 =
((*𝑟‘𝑅)‘(1r‘𝑅)) →
((*𝑟‘𝑅)‘((1r‘𝑅)(.r‘𝑅)𝑦)) = ((*𝑟‘𝑅)‘((1r‘𝑅)(.r‘𝑅)((*𝑟‘𝑅)‘(1r‘𝑅))))) |
54 | | fveq2 6668 |
. . . . . . . . . 10
⊢ (𝑦 =
((*𝑟‘𝑅)‘(1r‘𝑅)) →
((*𝑟‘𝑅)‘𝑦) = ((*𝑟‘𝑅)‘((*𝑟‘𝑅)‘(1r‘𝑅)))) |
55 | 54 | oveq1d 7179 |
. . . . . . . . 9
⊢ (𝑦 =
((*𝑟‘𝑅)‘(1r‘𝑅)) →
(((*𝑟‘𝑅)‘𝑦)(.r‘𝑅)((*𝑟‘𝑅)‘(1r‘𝑅))) =
(((*𝑟‘𝑅)‘((*𝑟‘𝑅)‘(1r‘𝑅)))(.r‘𝑅)((*𝑟‘𝑅)‘(1r‘𝑅)))) |
56 | 53, 55 | eqeq12d 2754 |
. . . . . . . 8
⊢ (𝑦 =
((*𝑟‘𝑅)‘(1r‘𝑅)) →
(((*𝑟‘𝑅)‘((1r‘𝑅)(.r‘𝑅)𝑦)) = (((*𝑟‘𝑅)‘𝑦)(.r‘𝑅)((*𝑟‘𝑅)‘(1r‘𝑅))) ↔
((*𝑟‘𝑅)‘((1r‘𝑅)(.r‘𝑅)((*𝑟‘𝑅)‘(1r‘𝑅)))) =
(((*𝑟‘𝑅)‘((*𝑟‘𝑅)‘(1r‘𝑅)))(.r‘𝑅)((*𝑟‘𝑅)‘(1r‘𝑅))))) |
57 | 51, 56 | rspc2va 3535 |
. . . . . . 7
⊢
((((1r‘𝑅) ∈ (Base‘𝑅) ∧ ((*𝑟‘𝑅)‘(1r‘𝑅)) ∈ (Base‘𝑅)) ∧ ∀𝑥 ∈ (Base‘𝑅)∀𝑦 ∈ (Base‘𝑅)((*𝑟‘𝑅)‘(𝑥(.r‘𝑅)𝑦)) = (((*𝑟‘𝑅)‘𝑦)(.r‘𝑅)((*𝑟‘𝑅)‘𝑥))) →
((*𝑟‘𝑅)‘((1r‘𝑅)(.r‘𝑅)((*𝑟‘𝑅)‘(1r‘𝑅)))) =
(((*𝑟‘𝑅)‘((*𝑟‘𝑅)‘(1r‘𝑅)))(.r‘𝑅)((*𝑟‘𝑅)‘(1r‘𝑅)))) |
58 | 27, 36, 48, 57 | syl21anc 837 |
. . . . . 6
⊢ (𝜑 →
((*𝑟‘𝑅)‘((1r‘𝑅)(.r‘𝑅)((*𝑟‘𝑅)‘(1r‘𝑅)))) =
(((*𝑟‘𝑅)‘((*𝑟‘𝑅)‘(1r‘𝑅)))(.r‘𝑅)((*𝑟‘𝑅)‘(1r‘𝑅)))) |
59 | 29, 58 | eqtr4d 2776 |
. . . . 5
⊢ (𝜑 →
((1r‘𝑅)(.r‘𝑅)((*𝑟‘𝑅)‘(1r‘𝑅))) =
((*𝑟‘𝑅)‘((1r‘𝑅)(.r‘𝑅)((*𝑟‘𝑅)‘(1r‘𝑅))))) |
60 | 1, 5, 2 | ringlidm 19436 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧
((*𝑟‘𝑅)‘(1r‘𝑅)) ∈ (Base‘𝑅)) →
((1r‘𝑅)(.r‘𝑅)((*𝑟‘𝑅)‘(1r‘𝑅))) =
((*𝑟‘𝑅)‘(1r‘𝑅))) |
61 | 7, 36, 60 | syl2anc 587 |
. . . . 5
⊢ (𝜑 →
((1r‘𝑅)(.r‘𝑅)((*𝑟‘𝑅)‘(1r‘𝑅))) =
((*𝑟‘𝑅)‘(1r‘𝑅))) |
62 | 61 | fveq2d 6672 |
. . . . 5
⊢ (𝜑 →
((*𝑟‘𝑅)‘((1r‘𝑅)(.r‘𝑅)((*𝑟‘𝑅)‘(1r‘𝑅)))) =
((*𝑟‘𝑅)‘((*𝑟‘𝑅)‘(1r‘𝑅)))) |
63 | 59, 61, 62 | 3eqtr3d 2781 |
. . . 4
⊢ (𝜑 →
((*𝑟‘𝑅)‘(1r‘𝑅)) =
((*𝑟‘𝑅)‘((*𝑟‘𝑅)‘(1r‘𝑅)))) |
64 | | eqid 2738 |
. . . . . 6
⊢
(*𝑟‘𝑅) = (*𝑟‘𝑅) |
65 | | eqid 2738 |
. . . . . 6
⊢
(*rf‘𝑅) = (*rf‘𝑅) |
66 | 1, 64, 65 | stafval 19731 |
. . . . 5
⊢
((1r‘𝑅) ∈ (Base‘𝑅) → ((*rf‘𝑅)‘(1r‘𝑅)) =
((*𝑟‘𝑅)‘(1r‘𝑅))) |
67 | 27, 66 | syl 17 |
. . . 4
⊢ (𝜑 →
((*rf‘𝑅)‘(1r‘𝑅)) =
((*𝑟‘𝑅)‘(1r‘𝑅))) |
68 | 63, 67, 28 | 3eqtr4d 2783 |
. . 3
⊢ (𝜑 →
((*rf‘𝑅)‘(1r‘𝑅)) = (1r‘𝑅)) |
69 | 47 | imp 410 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅))) →
((*𝑟‘𝑅)‘(𝑥(.r‘𝑅)𝑦)) = (((*𝑟‘𝑅)‘𝑦)(.r‘𝑅)((*𝑟‘𝑅)‘𝑥))) |
70 | 1, 5, 3, 6 | opprmul 19491 |
. . . . 5
⊢
(((*𝑟‘𝑅)‘𝑥)(.r‘(oppr‘𝑅))((*𝑟‘𝑅)‘𝑦)) = (((*𝑟‘𝑅)‘𝑦)(.r‘𝑅)((*𝑟‘𝑅)‘𝑥)) |
71 | 69, 70 | eqtr4di 2791 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅))) →
((*𝑟‘𝑅)‘(𝑥(.r‘𝑅)𝑦)) = (((*𝑟‘𝑅)‘𝑥)(.r‘(oppr‘𝑅))((*𝑟‘𝑅)‘𝑦))) |
72 | 1, 5 | ringcl 19426 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) → (𝑥(.r‘𝑅)𝑦) ∈ (Base‘𝑅)) |
73 | 72 | 3expb 1121 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅))) → (𝑥(.r‘𝑅)𝑦) ∈ (Base‘𝑅)) |
74 | 7, 73 | sylan 583 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅))) → (𝑥(.r‘𝑅)𝑦) ∈ (Base‘𝑅)) |
75 | 1, 64, 65 | stafval 19731 |
. . . . 5
⊢ ((𝑥(.r‘𝑅)𝑦) ∈ (Base‘𝑅) → ((*rf‘𝑅)‘(𝑥(.r‘𝑅)𝑦)) = ((*𝑟‘𝑅)‘(𝑥(.r‘𝑅)𝑦))) |
76 | 74, 75 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅))) →
((*rf‘𝑅)‘(𝑥(.r‘𝑅)𝑦)) = ((*𝑟‘𝑅)‘(𝑥(.r‘𝑅)𝑦))) |
77 | 1, 64, 65 | stafval 19731 |
. . . . . 6
⊢ (𝑥 ∈ (Base‘𝑅) →
((*rf‘𝑅)‘𝑥) = ((*𝑟‘𝑅)‘𝑥)) |
78 | 1, 64, 65 | stafval 19731 |
. . . . . 6
⊢ (𝑦 ∈ (Base‘𝑅) →
((*rf‘𝑅)‘𝑦) = ((*𝑟‘𝑅)‘𝑦)) |
79 | 77, 78 | oveqan12d 7183 |
. . . . 5
⊢ ((𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) →
(((*rf‘𝑅)‘𝑥)(.r‘(oppr‘𝑅))((*rf‘𝑅)‘𝑦)) = (((*𝑟‘𝑅)‘𝑥)(.r‘(oppr‘𝑅))((*𝑟‘𝑅)‘𝑦))) |
80 | 79 | adantl 485 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅))) →
(((*rf‘𝑅)‘𝑥)(.r‘(oppr‘𝑅))((*rf‘𝑅)‘𝑦)) = (((*𝑟‘𝑅)‘𝑥)(.r‘(oppr‘𝑅))((*𝑟‘𝑅)‘𝑦))) |
81 | 71, 76, 80 | 3eqtr4d 2783 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅))) →
((*rf‘𝑅)‘(𝑥(.r‘𝑅)𝑦)) = (((*rf‘𝑅)‘𝑥)(.r‘(oppr‘𝑅))((*rf‘𝑅)‘𝑦))) |
82 | 3, 1 | opprbas 19494 |
. . 3
⊢
(Base‘𝑅) =
(Base‘(oppr‘𝑅)) |
83 | | eqid 2738 |
. . 3
⊢
(+g‘𝑅) = (+g‘𝑅) |
84 | 3, 83 | oppradd 19495 |
. . 3
⊢
(+g‘𝑅) =
(+g‘(oppr‘𝑅)) |
85 | 34 | imp 410 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) →
((*𝑟‘𝑅)‘𝑥) ∈ (Base‘𝑅)) |
86 | 1, 64, 65 | staffval 19730 |
. . . 4
⊢
(*rf‘𝑅) = (𝑥 ∈ (Base‘𝑅) ↦
((*𝑟‘𝑅)‘𝑥)) |
87 | 85, 86 | fmptd 6882 |
. . 3
⊢ (𝜑 →
(*rf‘𝑅):(Base‘𝑅)⟶(Base‘𝑅)) |
88 | | issrngd.dp |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾) → ( ∗ ‘(𝑥 + 𝑦)) = (( ∗ ‘𝑥) + ( ∗ ‘𝑦))) |
89 | 88 | 3expib 1123 |
. . . . . 6
⊢ (𝜑 → ((𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾) → ( ∗ ‘(𝑥 + 𝑦)) = (( ∗ ‘𝑥) + ( ∗ ‘𝑦)))) |
90 | | issrngd.p |
. . . . . . . . 9
⊢ (𝜑 → + =
(+g‘𝑅)) |
91 | 90 | oveqd 7181 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 + 𝑦) = (𝑥(+g‘𝑅)𝑦)) |
92 | 18, 91 | fveq12d 6675 |
. . . . . . 7
⊢ (𝜑 → ( ∗ ‘(𝑥 + 𝑦)) = ((*𝑟‘𝑅)‘(𝑥(+g‘𝑅)𝑦))) |
93 | 90, 19, 44 | oveq123d 7185 |
. . . . . . 7
⊢ (𝜑 → (( ∗ ‘𝑥) + ( ∗ ‘𝑦)) =
(((*𝑟‘𝑅)‘𝑥)(+g‘𝑅)((*𝑟‘𝑅)‘𝑦))) |
94 | 92, 93 | eqeq12d 2754 |
. . . . . 6
⊢ (𝜑 → (( ∗ ‘(𝑥 + 𝑦)) = (( ∗ ‘𝑥) + ( ∗ ‘𝑦)) ↔
((*𝑟‘𝑅)‘(𝑥(+g‘𝑅)𝑦)) = (((*𝑟‘𝑅)‘𝑥)(+g‘𝑅)((*𝑟‘𝑅)‘𝑦)))) |
95 | 89, 40, 94 | 3imtr3d 296 |
. . . . 5
⊢ (𝜑 → ((𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) →
((*𝑟‘𝑅)‘(𝑥(+g‘𝑅)𝑦)) = (((*𝑟‘𝑅)‘𝑥)(+g‘𝑅)((*𝑟‘𝑅)‘𝑦)))) |
96 | 95 | imp 410 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅))) →
((*𝑟‘𝑅)‘(𝑥(+g‘𝑅)𝑦)) = (((*𝑟‘𝑅)‘𝑥)(+g‘𝑅)((*𝑟‘𝑅)‘𝑦))) |
97 | 1, 83 | ringacl 19443 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) → (𝑥(+g‘𝑅)𝑦) ∈ (Base‘𝑅)) |
98 | 97 | 3expb 1121 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅))) → (𝑥(+g‘𝑅)𝑦) ∈ (Base‘𝑅)) |
99 | 7, 98 | sylan 583 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅))) → (𝑥(+g‘𝑅)𝑦) ∈ (Base‘𝑅)) |
100 | 1, 64, 65 | stafval 19731 |
. . . . 5
⊢ ((𝑥(+g‘𝑅)𝑦) ∈ (Base‘𝑅) → ((*rf‘𝑅)‘(𝑥(+g‘𝑅)𝑦)) = ((*𝑟‘𝑅)‘(𝑥(+g‘𝑅)𝑦))) |
101 | 99, 100 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅))) →
((*rf‘𝑅)‘(𝑥(+g‘𝑅)𝑦)) = ((*𝑟‘𝑅)‘(𝑥(+g‘𝑅)𝑦))) |
102 | 77, 78 | oveqan12d 7183 |
. . . . 5
⊢ ((𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) →
(((*rf‘𝑅)‘𝑥)(+g‘𝑅)((*rf‘𝑅)‘𝑦)) = (((*𝑟‘𝑅)‘𝑥)(+g‘𝑅)((*𝑟‘𝑅)‘𝑦))) |
103 | 102 | adantl 485 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅))) →
(((*rf‘𝑅)‘𝑥)(+g‘𝑅)((*rf‘𝑅)‘𝑦)) = (((*𝑟‘𝑅)‘𝑥)(+g‘𝑅)((*𝑟‘𝑅)‘𝑦))) |
104 | 96, 101, 103 | 3eqtr4d 2783 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅))) →
((*rf‘𝑅)‘(𝑥(+g‘𝑅)𝑦)) = (((*rf‘𝑅)‘𝑥)(+g‘𝑅)((*rf‘𝑅)‘𝑦))) |
105 | 1, 2, 4, 5, 6, 7, 9, 68, 81, 82, 83, 84, 87, 104 | isrhmd 19596 |
. 2
⊢ (𝜑 →
(*rf‘𝑅) ∈ (𝑅 RingHom (oppr‘𝑅))) |
106 | 1, 64, 65 | staffval 19730 |
. . 3
⊢
(*rf‘𝑅) = (𝑦 ∈ (Base‘𝑅) ↦
((*𝑟‘𝑅)‘𝑦)) |
107 | 106 | fmpt 6878 |
. . . . . . 7
⊢
(∀𝑦 ∈
(Base‘𝑅)((*𝑟‘𝑅)‘𝑦) ∈ (Base‘𝑅) ↔ (*rf‘𝑅):(Base‘𝑅)⟶(Base‘𝑅)) |
108 | 87, 107 | sylibr 237 |
. . . . . 6
⊢ (𝜑 → ∀𝑦 ∈ (Base‘𝑅)((*𝑟‘𝑅)‘𝑦) ∈ (Base‘𝑅)) |
109 | 108 | r19.21bi 3120 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝑅)) →
((*𝑟‘𝑅)‘𝑦) ∈ (Base‘𝑅)) |
110 | | id 22 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → 𝑥 = 𝑦) |
111 | | fveq2 6668 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → ((*𝑟‘𝑅)‘𝑥) = ((*𝑟‘𝑅)‘𝑦)) |
112 | 111 | fveq2d 6672 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → ((*𝑟‘𝑅)‘((*𝑟‘𝑅)‘𝑥)) = ((*𝑟‘𝑅)‘((*𝑟‘𝑅)‘𝑦))) |
113 | 110, 112 | eqeq12d 2754 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (𝑥 = ((*𝑟‘𝑅)‘((*𝑟‘𝑅)‘𝑥)) ↔ 𝑦 = ((*𝑟‘𝑅)‘((*𝑟‘𝑅)‘𝑦)))) |
114 | 113 | rspccva 3523 |
. . . . . . . . 9
⊢
((∀𝑥 ∈
(Base‘𝑅)𝑥 =
((*𝑟‘𝑅)‘((*𝑟‘𝑅)‘𝑥)) ∧ 𝑦 ∈ (Base‘𝑅)) → 𝑦 = ((*𝑟‘𝑅)‘((*𝑟‘𝑅)‘𝑦))) |
115 | 25, 114 | sylan 583 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝑅)) → 𝑦 = ((*𝑟‘𝑅)‘((*𝑟‘𝑅)‘𝑦))) |
116 | 115 | adantrl 716 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅))) → 𝑦 = ((*𝑟‘𝑅)‘((*𝑟‘𝑅)‘𝑦))) |
117 | | fveq2 6668 |
. . . . . . . 8
⊢ (𝑥 =
((*𝑟‘𝑅)‘𝑦) → ((*𝑟‘𝑅)‘𝑥) = ((*𝑟‘𝑅)‘((*𝑟‘𝑅)‘𝑦))) |
118 | 117 | eqeq2d 2749 |
. . . . . . 7
⊢ (𝑥 =
((*𝑟‘𝑅)‘𝑦) → (𝑦 = ((*𝑟‘𝑅)‘𝑥) ↔ 𝑦 = ((*𝑟‘𝑅)‘((*𝑟‘𝑅)‘𝑦)))) |
119 | 116, 118 | syl5ibrcom 250 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅))) → (𝑥 = ((*𝑟‘𝑅)‘𝑦) → 𝑦 = ((*𝑟‘𝑅)‘𝑥))) |
120 | 24 | adantrr 717 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅))) → 𝑥 = ((*𝑟‘𝑅)‘((*𝑟‘𝑅)‘𝑥))) |
121 | | fveq2 6668 |
. . . . . . . 8
⊢ (𝑦 =
((*𝑟‘𝑅)‘𝑥) → ((*𝑟‘𝑅)‘𝑦) = ((*𝑟‘𝑅)‘((*𝑟‘𝑅)‘𝑥))) |
122 | 121 | eqeq2d 2749 |
. . . . . . 7
⊢ (𝑦 =
((*𝑟‘𝑅)‘𝑥) → (𝑥 = ((*𝑟‘𝑅)‘𝑦) ↔ 𝑥 = ((*𝑟‘𝑅)‘((*𝑟‘𝑅)‘𝑥)))) |
123 | 120, 122 | syl5ibrcom 250 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅))) → (𝑦 = ((*𝑟‘𝑅)‘𝑥) → 𝑥 = ((*𝑟‘𝑅)‘𝑦))) |
124 | 119, 123 | impbid 215 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅))) → (𝑥 = ((*𝑟‘𝑅)‘𝑦) ↔ 𝑦 = ((*𝑟‘𝑅)‘𝑥))) |
125 | 86, 85, 109, 124 | f1ocnv2d 7408 |
. . . 4
⊢ (𝜑 →
((*rf‘𝑅):(Base‘𝑅)–1-1-onto→(Base‘𝑅) ∧ ◡(*rf‘𝑅) = (𝑦 ∈ (Base‘𝑅) ↦
((*𝑟‘𝑅)‘𝑦)))) |
126 | 125 | simprd 499 |
. . 3
⊢ (𝜑 → ◡(*rf‘𝑅) = (𝑦 ∈ (Base‘𝑅) ↦
((*𝑟‘𝑅)‘𝑦))) |
127 | 106, 126 | eqtr4id 2792 |
. 2
⊢ (𝜑 →
(*rf‘𝑅) = ◡(*rf‘𝑅)) |
128 | 3, 65 | issrng 19733 |
. 2
⊢ (𝑅 ∈ *-Ring ↔
((*rf‘𝑅) ∈ (𝑅 RingHom (oppr‘𝑅)) ∧
(*rf‘𝑅) = ◡(*rf‘𝑅))) |
129 | 105, 127,
128 | sylanbrc 586 |
1
⊢ (𝜑 → 𝑅 ∈ *-Ring) |