Proof of Theorem issrngd
Step | Hyp | Ref
| Expression |
1 | | eqid 2622 |
. . 3
⊢
(Base‘𝑅) =
(Base‘𝑅) |
2 | | eqid 2622 |
. . 3
⊢
(1r‘𝑅) = (1r‘𝑅) |
3 | | eqid 2622 |
. . . 4
⊢
(oppr‘𝑅) = (oppr‘𝑅) |
4 | 3, 2 | oppr1 18634 |
. . 3
⊢
(1r‘𝑅) =
(1r‘(oppr‘𝑅)) |
5 | | eqid 2622 |
. . 3
⊢
(.r‘𝑅) = (.r‘𝑅) |
6 | | eqid 2622 |
. . 3
⊢
(.r‘(oppr‘𝑅)) =
(.r‘(oppr‘𝑅)) |
7 | | issrngd.r |
. . 3
⊢ (𝜑 → 𝑅 ∈ Ring) |
8 | 3 | opprring 18631 |
. . . 4
⊢ (𝑅 ∈ Ring →
(oppr‘𝑅) ∈ Ring) |
9 | 7, 8 | syl 17 |
. . 3
⊢ (𝜑 →
(oppr‘𝑅) ∈ Ring) |
10 | 1, 2 | ringidcl 18568 |
. . . . . . . . 9
⊢ (𝑅 ∈ Ring →
(1r‘𝑅)
∈ (Base‘𝑅)) |
11 | 7, 10 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (1r‘𝑅) ∈ (Base‘𝑅)) |
12 | | issrngd.id |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐾) → ( ∗ ‘( ∗
‘𝑥)) = 𝑥) |
13 | 12 | ex 450 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑥 ∈ 𝐾 → ( ∗ ‘( ∗
‘𝑥)) = 𝑥)) |
14 | | issrngd.k |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐾 = (Base‘𝑅)) |
15 | 14 | eleq2d 2687 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑥 ∈ 𝐾 ↔ 𝑥 ∈ (Base‘𝑅))) |
16 | | issrngd.c |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ∗ =
(*𝑟‘𝑅)) |
17 | 16 | fveq1d 6193 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ( ∗ ‘𝑥) =
((*𝑟‘𝑅)‘𝑥)) |
18 | 16, 17 | fveq12d 6197 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ( ∗ ‘( ∗
‘𝑥)) =
((*𝑟‘𝑅)‘((*𝑟‘𝑅)‘𝑥))) |
19 | 18 | eqeq1d 2624 |
. . . . . . . . . . . 12
⊢ (𝜑 → (( ∗ ‘( ∗
‘𝑥)) = 𝑥 ↔
((*𝑟‘𝑅)‘((*𝑟‘𝑅)‘𝑥)) = 𝑥)) |
20 | 13, 15, 19 | 3imtr3d 282 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑥 ∈ (Base‘𝑅) → ((*𝑟‘𝑅)‘((*𝑟‘𝑅)‘𝑥)) = 𝑥)) |
21 | 20 | imp 445 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) →
((*𝑟‘𝑅)‘((*𝑟‘𝑅)‘𝑥)) = 𝑥) |
22 | 21 | eqcomd 2628 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → 𝑥 = ((*𝑟‘𝑅)‘((*𝑟‘𝑅)‘𝑥))) |
23 | 22 | ralrimiva 2966 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑥 ∈ (Base‘𝑅)𝑥 = ((*𝑟‘𝑅)‘((*𝑟‘𝑅)‘𝑥))) |
24 | | id 22 |
. . . . . . . . . 10
⊢ (𝑥 = (1r‘𝑅) → 𝑥 = (1r‘𝑅)) |
25 | | fveq2 6191 |
. . . . . . . . . . 11
⊢ (𝑥 = (1r‘𝑅) →
((*𝑟‘𝑅)‘𝑥) = ((*𝑟‘𝑅)‘(1r‘𝑅))) |
26 | 25 | fveq2d 6195 |
. . . . . . . . . 10
⊢ (𝑥 = (1r‘𝑅) →
((*𝑟‘𝑅)‘((*𝑟‘𝑅)‘𝑥)) = ((*𝑟‘𝑅)‘((*𝑟‘𝑅)‘(1r‘𝑅)))) |
27 | 24, 26 | eqeq12d 2637 |
. . . . . . . . 9
⊢ (𝑥 = (1r‘𝑅) → (𝑥 = ((*𝑟‘𝑅)‘((*𝑟‘𝑅)‘𝑥)) ↔ (1r‘𝑅) =
((*𝑟‘𝑅)‘((*𝑟‘𝑅)‘(1r‘𝑅))))) |
28 | 27 | rspcv 3305 |
. . . . . . . 8
⊢
((1r‘𝑅) ∈ (Base‘𝑅) → (∀𝑥 ∈ (Base‘𝑅)𝑥 = ((*𝑟‘𝑅)‘((*𝑟‘𝑅)‘𝑥)) → (1r‘𝑅) =
((*𝑟‘𝑅)‘((*𝑟‘𝑅)‘(1r‘𝑅))))) |
29 | 11, 23, 28 | sylc 65 |
. . . . . . 7
⊢ (𝜑 → (1r‘𝑅) =
((*𝑟‘𝑅)‘((*𝑟‘𝑅)‘(1r‘𝑅)))) |
30 | 29 | oveq1d 6665 |
. . . . . 6
⊢ (𝜑 →
((1r‘𝑅)(.r‘𝑅)((*𝑟‘𝑅)‘(1r‘𝑅))) =
(((*𝑟‘𝑅)‘((*𝑟‘𝑅)‘(1r‘𝑅)))(.r‘𝑅)((*𝑟‘𝑅)‘(1r‘𝑅)))) |
31 | | issrngd.cl |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐾) → ( ∗ ‘𝑥) ∈ 𝐾) |
32 | 31 | ex 450 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ 𝐾 → ( ∗ ‘𝑥) ∈ 𝐾)) |
33 | 17, 14 | eleq12d 2695 |
. . . . . . . . . 10
⊢ (𝜑 → (( ∗ ‘𝑥) ∈ 𝐾 ↔ ((*𝑟‘𝑅)‘𝑥) ∈ (Base‘𝑅))) |
34 | 32, 15, 33 | 3imtr3d 282 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ (Base‘𝑅) → ((*𝑟‘𝑅)‘𝑥) ∈ (Base‘𝑅))) |
35 | 34 | ralrimiv 2965 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑥 ∈ (Base‘𝑅)((*𝑟‘𝑅)‘𝑥) ∈ (Base‘𝑅)) |
36 | 25 | eleq1d 2686 |
. . . . . . . . 9
⊢ (𝑥 = (1r‘𝑅) →
(((*𝑟‘𝑅)‘𝑥) ∈ (Base‘𝑅) ↔ ((*𝑟‘𝑅)‘(1r‘𝑅)) ∈ (Base‘𝑅))) |
37 | 36 | rspcv 3305 |
. . . . . . . 8
⊢
((1r‘𝑅) ∈ (Base‘𝑅) → (∀𝑥 ∈ (Base‘𝑅)((*𝑟‘𝑅)‘𝑥) ∈ (Base‘𝑅) → ((*𝑟‘𝑅)‘(1r‘𝑅)) ∈ (Base‘𝑅))) |
38 | 11, 35, 37 | sylc 65 |
. . . . . . 7
⊢ (𝜑 →
((*𝑟‘𝑅)‘(1r‘𝑅)) ∈ (Base‘𝑅)) |
39 | | issrngd.dt |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾) → ( ∗ ‘(𝑥 · 𝑦)) = (( ∗ ‘𝑦) · ( ∗
‘𝑥))) |
40 | 39 | 3expib 1268 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾) → ( ∗ ‘(𝑥 · 𝑦)) = (( ∗ ‘𝑦) · ( ∗
‘𝑥)))) |
41 | 14 | eleq2d 2687 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑦 ∈ 𝐾 ↔ 𝑦 ∈ (Base‘𝑅))) |
42 | 15, 41 | anbi12d 747 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾) ↔ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)))) |
43 | | issrngd.t |
. . . . . . . . . . . 12
⊢ (𝜑 → · =
(.r‘𝑅)) |
44 | 43 | oveqd 6667 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑥 · 𝑦) = (𝑥(.r‘𝑅)𝑦)) |
45 | 16, 44 | fveq12d 6197 |
. . . . . . . . . 10
⊢ (𝜑 → ( ∗ ‘(𝑥 · 𝑦)) = ((*𝑟‘𝑅)‘(𝑥(.r‘𝑅)𝑦))) |
46 | 16 | fveq1d 6193 |
. . . . . . . . . . 11
⊢ (𝜑 → ( ∗ ‘𝑦) =
((*𝑟‘𝑅)‘𝑦)) |
47 | 43, 46, 17 | oveq123d 6671 |
. . . . . . . . . 10
⊢ (𝜑 → (( ∗ ‘𝑦) · ( ∗
‘𝑥)) =
(((*𝑟‘𝑅)‘𝑦)(.r‘𝑅)((*𝑟‘𝑅)‘𝑥))) |
48 | 45, 47 | eqeq12d 2637 |
. . . . . . . . 9
⊢ (𝜑 → (( ∗ ‘(𝑥 · 𝑦)) = (( ∗ ‘𝑦) · ( ∗
‘𝑥)) ↔
((*𝑟‘𝑅)‘(𝑥(.r‘𝑅)𝑦)) = (((*𝑟‘𝑅)‘𝑦)(.r‘𝑅)((*𝑟‘𝑅)‘𝑥)))) |
49 | 40, 42, 48 | 3imtr3d 282 |
. . . . . . . 8
⊢ (𝜑 → ((𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) →
((*𝑟‘𝑅)‘(𝑥(.r‘𝑅)𝑦)) = (((*𝑟‘𝑅)‘𝑦)(.r‘𝑅)((*𝑟‘𝑅)‘𝑥)))) |
50 | 49 | ralrimivv 2970 |
. . . . . . 7
⊢ (𝜑 → ∀𝑥 ∈ (Base‘𝑅)∀𝑦 ∈ (Base‘𝑅)((*𝑟‘𝑅)‘(𝑥(.r‘𝑅)𝑦)) = (((*𝑟‘𝑅)‘𝑦)(.r‘𝑅)((*𝑟‘𝑅)‘𝑥))) |
51 | | oveq1 6657 |
. . . . . . . . . 10
⊢ (𝑥 = (1r‘𝑅) → (𝑥(.r‘𝑅)𝑦) = ((1r‘𝑅)(.r‘𝑅)𝑦)) |
52 | 51 | fveq2d 6195 |
. . . . . . . . 9
⊢ (𝑥 = (1r‘𝑅) →
((*𝑟‘𝑅)‘(𝑥(.r‘𝑅)𝑦)) = ((*𝑟‘𝑅)‘((1r‘𝑅)(.r‘𝑅)𝑦))) |
53 | 25 | oveq2d 6666 |
. . . . . . . . 9
⊢ (𝑥 = (1r‘𝑅) →
(((*𝑟‘𝑅)‘𝑦)(.r‘𝑅)((*𝑟‘𝑅)‘𝑥)) = (((*𝑟‘𝑅)‘𝑦)(.r‘𝑅)((*𝑟‘𝑅)‘(1r‘𝑅)))) |
54 | 52, 53 | eqeq12d 2637 |
. . . . . . . 8
⊢ (𝑥 = (1r‘𝑅) →
(((*𝑟‘𝑅)‘(𝑥(.r‘𝑅)𝑦)) = (((*𝑟‘𝑅)‘𝑦)(.r‘𝑅)((*𝑟‘𝑅)‘𝑥)) ↔ ((*𝑟‘𝑅)‘((1r‘𝑅)(.r‘𝑅)𝑦)) = (((*𝑟‘𝑅)‘𝑦)(.r‘𝑅)((*𝑟‘𝑅)‘(1r‘𝑅))))) |
55 | | oveq2 6658 |
. . . . . . . . . 10
⊢ (𝑦 =
((*𝑟‘𝑅)‘(1r‘𝑅)) →
((1r‘𝑅)(.r‘𝑅)𝑦) = ((1r‘𝑅)(.r‘𝑅)((*𝑟‘𝑅)‘(1r‘𝑅)))) |
56 | 55 | fveq2d 6195 |
. . . . . . . . 9
⊢ (𝑦 =
((*𝑟‘𝑅)‘(1r‘𝑅)) →
((*𝑟‘𝑅)‘((1r‘𝑅)(.r‘𝑅)𝑦)) = ((*𝑟‘𝑅)‘((1r‘𝑅)(.r‘𝑅)((*𝑟‘𝑅)‘(1r‘𝑅))))) |
57 | | fveq2 6191 |
. . . . . . . . . 10
⊢ (𝑦 =
((*𝑟‘𝑅)‘(1r‘𝑅)) →
((*𝑟‘𝑅)‘𝑦) = ((*𝑟‘𝑅)‘((*𝑟‘𝑅)‘(1r‘𝑅)))) |
58 | 57 | oveq1d 6665 |
. . . . . . . . 9
⊢ (𝑦 =
((*𝑟‘𝑅)‘(1r‘𝑅)) →
(((*𝑟‘𝑅)‘𝑦)(.r‘𝑅)((*𝑟‘𝑅)‘(1r‘𝑅))) =
(((*𝑟‘𝑅)‘((*𝑟‘𝑅)‘(1r‘𝑅)))(.r‘𝑅)((*𝑟‘𝑅)‘(1r‘𝑅)))) |
59 | 56, 58 | eqeq12d 2637 |
. . . . . . . 8
⊢ (𝑦 =
((*𝑟‘𝑅)‘(1r‘𝑅)) →
(((*𝑟‘𝑅)‘((1r‘𝑅)(.r‘𝑅)𝑦)) = (((*𝑟‘𝑅)‘𝑦)(.r‘𝑅)((*𝑟‘𝑅)‘(1r‘𝑅))) ↔
((*𝑟‘𝑅)‘((1r‘𝑅)(.r‘𝑅)((*𝑟‘𝑅)‘(1r‘𝑅)))) =
(((*𝑟‘𝑅)‘((*𝑟‘𝑅)‘(1r‘𝑅)))(.r‘𝑅)((*𝑟‘𝑅)‘(1r‘𝑅))))) |
60 | 54, 59 | rspc2va 3323 |
. . . . . . 7
⊢
((((1r‘𝑅) ∈ (Base‘𝑅) ∧ ((*𝑟‘𝑅)‘(1r‘𝑅)) ∈ (Base‘𝑅)) ∧ ∀𝑥 ∈ (Base‘𝑅)∀𝑦 ∈ (Base‘𝑅)((*𝑟‘𝑅)‘(𝑥(.r‘𝑅)𝑦)) = (((*𝑟‘𝑅)‘𝑦)(.r‘𝑅)((*𝑟‘𝑅)‘𝑥))) →
((*𝑟‘𝑅)‘((1r‘𝑅)(.r‘𝑅)((*𝑟‘𝑅)‘(1r‘𝑅)))) =
(((*𝑟‘𝑅)‘((*𝑟‘𝑅)‘(1r‘𝑅)))(.r‘𝑅)((*𝑟‘𝑅)‘(1r‘𝑅)))) |
61 | 11, 38, 50, 60 | syl21anc 1325 |
. . . . . 6
⊢ (𝜑 →
((*𝑟‘𝑅)‘((1r‘𝑅)(.r‘𝑅)((*𝑟‘𝑅)‘(1r‘𝑅)))) =
(((*𝑟‘𝑅)‘((*𝑟‘𝑅)‘(1r‘𝑅)))(.r‘𝑅)((*𝑟‘𝑅)‘(1r‘𝑅)))) |
62 | 30, 61 | eqtr4d 2659 |
. . . . 5
⊢ (𝜑 →
((1r‘𝑅)(.r‘𝑅)((*𝑟‘𝑅)‘(1r‘𝑅))) =
((*𝑟‘𝑅)‘((1r‘𝑅)(.r‘𝑅)((*𝑟‘𝑅)‘(1r‘𝑅))))) |
63 | 1, 5, 2 | ringlidm 18571 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧
((*𝑟‘𝑅)‘(1r‘𝑅)) ∈ (Base‘𝑅)) →
((1r‘𝑅)(.r‘𝑅)((*𝑟‘𝑅)‘(1r‘𝑅))) =
((*𝑟‘𝑅)‘(1r‘𝑅))) |
64 | 7, 38, 63 | syl2anc 693 |
. . . . 5
⊢ (𝜑 →
((1r‘𝑅)(.r‘𝑅)((*𝑟‘𝑅)‘(1r‘𝑅))) =
((*𝑟‘𝑅)‘(1r‘𝑅))) |
65 | 64 | fveq2d 6195 |
. . . . 5
⊢ (𝜑 →
((*𝑟‘𝑅)‘((1r‘𝑅)(.r‘𝑅)((*𝑟‘𝑅)‘(1r‘𝑅)))) =
((*𝑟‘𝑅)‘((*𝑟‘𝑅)‘(1r‘𝑅)))) |
66 | 62, 64, 65 | 3eqtr3d 2664 |
. . . 4
⊢ (𝜑 →
((*𝑟‘𝑅)‘(1r‘𝑅)) =
((*𝑟‘𝑅)‘((*𝑟‘𝑅)‘(1r‘𝑅)))) |
67 | | eqid 2622 |
. . . . . 6
⊢
(*𝑟‘𝑅) = (*𝑟‘𝑅) |
68 | | eqid 2622 |
. . . . . 6
⊢
(*rf‘𝑅) = (*rf‘𝑅) |
69 | 1, 67, 68 | stafval 18848 |
. . . . 5
⊢
((1r‘𝑅) ∈ (Base‘𝑅) → ((*rf‘𝑅)‘(1r‘𝑅)) =
((*𝑟‘𝑅)‘(1r‘𝑅))) |
70 | 11, 69 | syl 17 |
. . . 4
⊢ (𝜑 →
((*rf‘𝑅)‘(1r‘𝑅)) =
((*𝑟‘𝑅)‘(1r‘𝑅))) |
71 | 66, 70, 29 | 3eqtr4d 2666 |
. . 3
⊢ (𝜑 →
((*rf‘𝑅)‘(1r‘𝑅)) = (1r‘𝑅)) |
72 | 49 | imp 445 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅))) →
((*𝑟‘𝑅)‘(𝑥(.r‘𝑅)𝑦)) = (((*𝑟‘𝑅)‘𝑦)(.r‘𝑅)((*𝑟‘𝑅)‘𝑥))) |
73 | 1, 5, 3, 6 | opprmul 18626 |
. . . . 5
⊢
(((*𝑟‘𝑅)‘𝑥)(.r‘(oppr‘𝑅))((*𝑟‘𝑅)‘𝑦)) = (((*𝑟‘𝑅)‘𝑦)(.r‘𝑅)((*𝑟‘𝑅)‘𝑥)) |
74 | 72, 73 | syl6eqr 2674 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅))) →
((*𝑟‘𝑅)‘(𝑥(.r‘𝑅)𝑦)) = (((*𝑟‘𝑅)‘𝑥)(.r‘(oppr‘𝑅))((*𝑟‘𝑅)‘𝑦))) |
75 | 1, 5 | ringcl 18561 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) → (𝑥(.r‘𝑅)𝑦) ∈ (Base‘𝑅)) |
76 | 75 | 3expb 1266 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅))) → (𝑥(.r‘𝑅)𝑦) ∈ (Base‘𝑅)) |
77 | 7, 76 | sylan 488 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅))) → (𝑥(.r‘𝑅)𝑦) ∈ (Base‘𝑅)) |
78 | 1, 67, 68 | stafval 18848 |
. . . . 5
⊢ ((𝑥(.r‘𝑅)𝑦) ∈ (Base‘𝑅) → ((*rf‘𝑅)‘(𝑥(.r‘𝑅)𝑦)) = ((*𝑟‘𝑅)‘(𝑥(.r‘𝑅)𝑦))) |
79 | 77, 78 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅))) →
((*rf‘𝑅)‘(𝑥(.r‘𝑅)𝑦)) = ((*𝑟‘𝑅)‘(𝑥(.r‘𝑅)𝑦))) |
80 | 1, 67, 68 | stafval 18848 |
. . . . . 6
⊢ (𝑥 ∈ (Base‘𝑅) →
((*rf‘𝑅)‘𝑥) = ((*𝑟‘𝑅)‘𝑥)) |
81 | 1, 67, 68 | stafval 18848 |
. . . . . 6
⊢ (𝑦 ∈ (Base‘𝑅) →
((*rf‘𝑅)‘𝑦) = ((*𝑟‘𝑅)‘𝑦)) |
82 | 80, 81 | oveqan12d 6669 |
. . . . 5
⊢ ((𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) →
(((*rf‘𝑅)‘𝑥)(.r‘(oppr‘𝑅))((*rf‘𝑅)‘𝑦)) = (((*𝑟‘𝑅)‘𝑥)(.r‘(oppr‘𝑅))((*𝑟‘𝑅)‘𝑦))) |
83 | 82 | adantl 482 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅))) →
(((*rf‘𝑅)‘𝑥)(.r‘(oppr‘𝑅))((*rf‘𝑅)‘𝑦)) = (((*𝑟‘𝑅)‘𝑥)(.r‘(oppr‘𝑅))((*𝑟‘𝑅)‘𝑦))) |
84 | 74, 79, 83 | 3eqtr4d 2666 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅))) →
((*rf‘𝑅)‘(𝑥(.r‘𝑅)𝑦)) = (((*rf‘𝑅)‘𝑥)(.r‘(oppr‘𝑅))((*rf‘𝑅)‘𝑦))) |
85 | 3, 1 | opprbas 18629 |
. . 3
⊢
(Base‘𝑅) =
(Base‘(oppr‘𝑅)) |
86 | | eqid 2622 |
. . 3
⊢
(+g‘𝑅) = (+g‘𝑅) |
87 | 3, 86 | oppradd 18630 |
. . 3
⊢
(+g‘𝑅) =
(+g‘(oppr‘𝑅)) |
88 | 34 | imp 445 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) →
((*𝑟‘𝑅)‘𝑥) ∈ (Base‘𝑅)) |
89 | 1, 67, 68 | staffval 18847 |
. . . 4
⊢
(*rf‘𝑅) = (𝑥 ∈ (Base‘𝑅) ↦
((*𝑟‘𝑅)‘𝑥)) |
90 | 88, 89 | fmptd 6385 |
. . 3
⊢ (𝜑 →
(*rf‘𝑅):(Base‘𝑅)⟶(Base‘𝑅)) |
91 | | issrngd.dp |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾) → ( ∗ ‘(𝑥 + 𝑦)) = (( ∗ ‘𝑥) + ( ∗ ‘𝑦))) |
92 | 91 | 3expib 1268 |
. . . . . 6
⊢ (𝜑 → ((𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾) → ( ∗ ‘(𝑥 + 𝑦)) = (( ∗ ‘𝑥) + ( ∗ ‘𝑦)))) |
93 | | issrngd.p |
. . . . . . . . 9
⊢ (𝜑 → + =
(+g‘𝑅)) |
94 | 93 | oveqd 6667 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 + 𝑦) = (𝑥(+g‘𝑅)𝑦)) |
95 | 16, 94 | fveq12d 6197 |
. . . . . . 7
⊢ (𝜑 → ( ∗ ‘(𝑥 + 𝑦)) = ((*𝑟‘𝑅)‘(𝑥(+g‘𝑅)𝑦))) |
96 | 93, 17, 46 | oveq123d 6671 |
. . . . . . 7
⊢ (𝜑 → (( ∗ ‘𝑥) + ( ∗ ‘𝑦)) =
(((*𝑟‘𝑅)‘𝑥)(+g‘𝑅)((*𝑟‘𝑅)‘𝑦))) |
97 | 95, 96 | eqeq12d 2637 |
. . . . . 6
⊢ (𝜑 → (( ∗ ‘(𝑥 + 𝑦)) = (( ∗ ‘𝑥) + ( ∗ ‘𝑦)) ↔
((*𝑟‘𝑅)‘(𝑥(+g‘𝑅)𝑦)) = (((*𝑟‘𝑅)‘𝑥)(+g‘𝑅)((*𝑟‘𝑅)‘𝑦)))) |
98 | 92, 42, 97 | 3imtr3d 282 |
. . . . 5
⊢ (𝜑 → ((𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) →
((*𝑟‘𝑅)‘(𝑥(+g‘𝑅)𝑦)) = (((*𝑟‘𝑅)‘𝑥)(+g‘𝑅)((*𝑟‘𝑅)‘𝑦)))) |
99 | 98 | imp 445 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅))) →
((*𝑟‘𝑅)‘(𝑥(+g‘𝑅)𝑦)) = (((*𝑟‘𝑅)‘𝑥)(+g‘𝑅)((*𝑟‘𝑅)‘𝑦))) |
100 | 1, 86 | ringacl 18578 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) → (𝑥(+g‘𝑅)𝑦) ∈ (Base‘𝑅)) |
101 | 100 | 3expb 1266 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅))) → (𝑥(+g‘𝑅)𝑦) ∈ (Base‘𝑅)) |
102 | 7, 101 | sylan 488 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅))) → (𝑥(+g‘𝑅)𝑦) ∈ (Base‘𝑅)) |
103 | 1, 67, 68 | stafval 18848 |
. . . . 5
⊢ ((𝑥(+g‘𝑅)𝑦) ∈ (Base‘𝑅) → ((*rf‘𝑅)‘(𝑥(+g‘𝑅)𝑦)) = ((*𝑟‘𝑅)‘(𝑥(+g‘𝑅)𝑦))) |
104 | 102, 103 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅))) →
((*rf‘𝑅)‘(𝑥(+g‘𝑅)𝑦)) = ((*𝑟‘𝑅)‘(𝑥(+g‘𝑅)𝑦))) |
105 | 80, 81 | oveqan12d 6669 |
. . . . 5
⊢ ((𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) →
(((*rf‘𝑅)‘𝑥)(+g‘𝑅)((*rf‘𝑅)‘𝑦)) = (((*𝑟‘𝑅)‘𝑥)(+g‘𝑅)((*𝑟‘𝑅)‘𝑦))) |
106 | 105 | adantl 482 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅))) →
(((*rf‘𝑅)‘𝑥)(+g‘𝑅)((*rf‘𝑅)‘𝑦)) = (((*𝑟‘𝑅)‘𝑥)(+g‘𝑅)((*𝑟‘𝑅)‘𝑦))) |
107 | 99, 104, 106 | 3eqtr4d 2666 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅))) →
((*rf‘𝑅)‘(𝑥(+g‘𝑅)𝑦)) = (((*rf‘𝑅)‘𝑥)(+g‘𝑅)((*rf‘𝑅)‘𝑦))) |
108 | 1, 2, 4, 5, 6, 7, 9, 71, 84, 85, 86, 87, 90, 107 | isrhmd 18729 |
. 2
⊢ (𝜑 →
(*rf‘𝑅) ∈ (𝑅 RingHom (oppr‘𝑅))) |
109 | 1, 67, 68 | staffval 18847 |
. . . . . . . 8
⊢
(*rf‘𝑅) = (𝑦 ∈ (Base‘𝑅) ↦
((*𝑟‘𝑅)‘𝑦)) |
110 | 109 | fmpt 6381 |
. . . . . . 7
⊢
(∀𝑦 ∈
(Base‘𝑅)((*𝑟‘𝑅)‘𝑦) ∈ (Base‘𝑅) ↔ (*rf‘𝑅):(Base‘𝑅)⟶(Base‘𝑅)) |
111 | 90, 110 | sylibr 224 |
. . . . . 6
⊢ (𝜑 → ∀𝑦 ∈ (Base‘𝑅)((*𝑟‘𝑅)‘𝑦) ∈ (Base‘𝑅)) |
112 | 111 | r19.21bi 2932 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝑅)) →
((*𝑟‘𝑅)‘𝑦) ∈ (Base‘𝑅)) |
113 | | id 22 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → 𝑥 = 𝑦) |
114 | | fveq2 6191 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → ((*𝑟‘𝑅)‘𝑥) = ((*𝑟‘𝑅)‘𝑦)) |
115 | 114 | fveq2d 6195 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → ((*𝑟‘𝑅)‘((*𝑟‘𝑅)‘𝑥)) = ((*𝑟‘𝑅)‘((*𝑟‘𝑅)‘𝑦))) |
116 | 113, 115 | eqeq12d 2637 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (𝑥 = ((*𝑟‘𝑅)‘((*𝑟‘𝑅)‘𝑥)) ↔ 𝑦 = ((*𝑟‘𝑅)‘((*𝑟‘𝑅)‘𝑦)))) |
117 | 116 | rspccva 3308 |
. . . . . . . . 9
⊢
((∀𝑥 ∈
(Base‘𝑅)𝑥 =
((*𝑟‘𝑅)‘((*𝑟‘𝑅)‘𝑥)) ∧ 𝑦 ∈ (Base‘𝑅)) → 𝑦 = ((*𝑟‘𝑅)‘((*𝑟‘𝑅)‘𝑦))) |
118 | 23, 117 | sylan 488 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝑅)) → 𝑦 = ((*𝑟‘𝑅)‘((*𝑟‘𝑅)‘𝑦))) |
119 | 118 | adantrl 752 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅))) → 𝑦 = ((*𝑟‘𝑅)‘((*𝑟‘𝑅)‘𝑦))) |
120 | | fveq2 6191 |
. . . . . . . 8
⊢ (𝑥 =
((*𝑟‘𝑅)‘𝑦) → ((*𝑟‘𝑅)‘𝑥) = ((*𝑟‘𝑅)‘((*𝑟‘𝑅)‘𝑦))) |
121 | 120 | eqeq2d 2632 |
. . . . . . 7
⊢ (𝑥 =
((*𝑟‘𝑅)‘𝑦) → (𝑦 = ((*𝑟‘𝑅)‘𝑥) ↔ 𝑦 = ((*𝑟‘𝑅)‘((*𝑟‘𝑅)‘𝑦)))) |
122 | 119, 121 | syl5ibrcom 237 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅))) → (𝑥 = ((*𝑟‘𝑅)‘𝑦) → 𝑦 = ((*𝑟‘𝑅)‘𝑥))) |
123 | 22 | adantrr 753 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅))) → 𝑥 = ((*𝑟‘𝑅)‘((*𝑟‘𝑅)‘𝑥))) |
124 | | fveq2 6191 |
. . . . . . . 8
⊢ (𝑦 =
((*𝑟‘𝑅)‘𝑥) → ((*𝑟‘𝑅)‘𝑦) = ((*𝑟‘𝑅)‘((*𝑟‘𝑅)‘𝑥))) |
125 | 124 | eqeq2d 2632 |
. . . . . . 7
⊢ (𝑦 =
((*𝑟‘𝑅)‘𝑥) → (𝑥 = ((*𝑟‘𝑅)‘𝑦) ↔ 𝑥 = ((*𝑟‘𝑅)‘((*𝑟‘𝑅)‘𝑥)))) |
126 | 123, 125 | syl5ibrcom 237 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅))) → (𝑦 = ((*𝑟‘𝑅)‘𝑥) → 𝑥 = ((*𝑟‘𝑅)‘𝑦))) |
127 | 122, 126 | impbid 202 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅))) → (𝑥 = ((*𝑟‘𝑅)‘𝑦) ↔ 𝑦 = ((*𝑟‘𝑅)‘𝑥))) |
128 | 89, 88, 112, 127 | f1ocnv2d 6886 |
. . . 4
⊢ (𝜑 →
((*rf‘𝑅):(Base‘𝑅)–1-1-onto→(Base‘𝑅) ∧ ◡(*rf‘𝑅) = (𝑦 ∈ (Base‘𝑅) ↦
((*𝑟‘𝑅)‘𝑦)))) |
129 | 128 | simprd 479 |
. . 3
⊢ (𝜑 → ◡(*rf‘𝑅) = (𝑦 ∈ (Base‘𝑅) ↦
((*𝑟‘𝑅)‘𝑦))) |
130 | 129, 109 | syl6reqr 2675 |
. 2
⊢ (𝜑 →
(*rf‘𝑅) = ◡(*rf‘𝑅)) |
131 | 3, 68 | issrng 18850 |
. 2
⊢ (𝑅 ∈ *-Ring ↔
((*rf‘𝑅) ∈ (𝑅 RingHom (oppr‘𝑅)) ∧
(*rf‘𝑅) = ◡(*rf‘𝑅))) |
132 | 108, 130,
131 | sylanbrc 698 |
1
⊢ (𝜑 → 𝑅 ∈ *-Ring) |