Step | Hyp | Ref
| Expression |
1 | | idsrngd.k |
. . 3
⊢ 𝐵 = (Base‘𝑅) |
2 | 1 | a1i 11 |
. 2
⊢ (𝜑 → 𝐵 = (Base‘𝑅)) |
3 | | eqidd 2740 |
. 2
⊢ (𝜑 → (+g‘𝑅) = (+g‘𝑅)) |
4 | | eqidd 2740 |
. 2
⊢ (𝜑 → (.r‘𝑅) = (.r‘𝑅)) |
5 | | idsrngd.c |
. . 3
⊢ ∗ =
(*𝑟‘𝑅) |
6 | 5 | a1i 11 |
. 2
⊢ (𝜑 → ∗ =
(*𝑟‘𝑅)) |
7 | | idsrngd.r |
. . 3
⊢ (𝜑 → 𝑅 ∈ CRing) |
8 | | crngring 19776 |
. . 3
⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring) |
9 | 7, 8 | syl 17 |
. 2
⊢ (𝜑 → 𝑅 ∈ Ring) |
10 | | idsrngd.i |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ( ∗ ‘𝑥) = 𝑥) |
11 | 10 | ralrimiva 3109 |
. . . . 5
⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ( ∗ ‘𝑥) = 𝑥) |
12 | 11 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → ∀𝑥 ∈ 𝐵 ( ∗ ‘𝑥) = 𝑥) |
13 | | simpr 484 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → 𝑎 ∈ 𝐵) |
14 | | simpr 484 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ 𝑥 = 𝑎) → 𝑥 = 𝑎) |
15 | 14 | fveq2d 6772 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ 𝑥 = 𝑎) → ( ∗ ‘𝑥) = ( ∗ ‘𝑎)) |
16 | 15, 14 | eqeq12d 2755 |
. . . . 5
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ 𝑥 = 𝑎) → (( ∗ ‘𝑥) = 𝑥 ↔ ( ∗ ‘𝑎) = 𝑎)) |
17 | 13, 16 | rspcdv 3551 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → (∀𝑥 ∈ 𝐵 ( ∗ ‘𝑥) = 𝑥 → ( ∗ ‘𝑎) = 𝑎)) |
18 | 12, 17 | mpd 15 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → ( ∗ ‘𝑎) = 𝑎) |
19 | 18, 13 | eqeltrd 2840 |
. 2
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → ( ∗ ‘𝑎) ∈ 𝐵) |
20 | 11 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ∀𝑥 ∈ 𝐵 ( ∗ ‘𝑥) = 𝑥) |
21 | 20 | 3adant2 1129 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) → ∀𝑥 ∈ 𝐵 ( ∗ ‘𝑥) = 𝑥) |
22 | | ringgrp 19769 |
. . . . . . 7
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp) |
23 | 9, 22 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑅 ∈ Grp) |
24 | | eqid 2739 |
. . . . . . 7
⊢
(+g‘𝑅) = (+g‘𝑅) |
25 | 1, 24 | grpcl 18566 |
. . . . . 6
⊢ ((𝑅 ∈ Grp ∧ 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) → (𝑎(+g‘𝑅)𝑏) ∈ 𝐵) |
26 | 23, 25 | syl3an1 1161 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) → (𝑎(+g‘𝑅)𝑏) ∈ 𝐵) |
27 | | simpr 484 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) ∧ 𝑥 = (𝑎(+g‘𝑅)𝑏)) → 𝑥 = (𝑎(+g‘𝑅)𝑏)) |
28 | 27 | fveq2d 6772 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) ∧ 𝑥 = (𝑎(+g‘𝑅)𝑏)) → ( ∗ ‘𝑥) = ( ∗ ‘(𝑎(+g‘𝑅)𝑏))) |
29 | 28, 27 | eqeq12d 2755 |
. . . . 5
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) ∧ 𝑥 = (𝑎(+g‘𝑅)𝑏)) → (( ∗ ‘𝑥) = 𝑥 ↔ ( ∗ ‘(𝑎(+g‘𝑅)𝑏)) = (𝑎(+g‘𝑅)𝑏))) |
30 | 26, 29 | rspcdv 3551 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) → (∀𝑥 ∈ 𝐵 ( ∗ ‘𝑥) = 𝑥 → ( ∗ ‘(𝑎(+g‘𝑅)𝑏)) = (𝑎(+g‘𝑅)𝑏))) |
31 | 21, 30 | mpd 15 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) → ( ∗ ‘(𝑎(+g‘𝑅)𝑏)) = (𝑎(+g‘𝑅)𝑏)) |
32 | 18 | 3adant3 1130 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) → ( ∗ ‘𝑎) = 𝑎) |
33 | | simpr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → 𝑏 ∈ 𝐵) |
34 | | simpr 484 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ 𝑥 = 𝑏) → 𝑥 = 𝑏) |
35 | 34 | fveq2d 6772 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ 𝑥 = 𝑏) → ( ∗ ‘𝑥) = ( ∗ ‘𝑏)) |
36 | 35, 34 | eqeq12d 2755 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ 𝑥 = 𝑏) → (( ∗ ‘𝑥) = 𝑥 ↔ ( ∗ ‘𝑏) = 𝑏)) |
37 | 33, 36 | rspcdv 3551 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (∀𝑥 ∈ 𝐵 ( ∗ ‘𝑥) = 𝑥 → ( ∗ ‘𝑏) = 𝑏)) |
38 | 20, 37 | mpd 15 |
. . . . 5
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ( ∗ ‘𝑏) = 𝑏) |
39 | 38 | 3adant2 1129 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) → ( ∗ ‘𝑏) = 𝑏) |
40 | 32, 39 | oveq12d 7286 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) → (( ∗ ‘𝑎)(+g‘𝑅)( ∗ ‘𝑏)) = (𝑎(+g‘𝑅)𝑏)) |
41 | 31, 40 | eqtr4d 2782 |
. 2
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) → ( ∗ ‘(𝑎(+g‘𝑅)𝑏)) = (( ∗ ‘𝑎)(+g‘𝑅)( ∗ ‘𝑏))) |
42 | | eqid 2739 |
. . . . 5
⊢
(.r‘𝑅) = (.r‘𝑅) |
43 | 1, 42 | crngcom 19782 |
. . . 4
⊢ ((𝑅 ∈ CRing ∧ 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) → (𝑎(.r‘𝑅)𝑏) = (𝑏(.r‘𝑅)𝑎)) |
44 | 7, 43 | syl3an1 1161 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) → (𝑎(.r‘𝑅)𝑏) = (𝑏(.r‘𝑅)𝑎)) |
45 | 1, 42 | ringcl 19781 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) → (𝑎(.r‘𝑅)𝑏) ∈ 𝐵) |
46 | 9, 45 | syl3an1 1161 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) → (𝑎(.r‘𝑅)𝑏) ∈ 𝐵) |
47 | | simpr 484 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) ∧ 𝑥 = (𝑎(.r‘𝑅)𝑏)) → 𝑥 = (𝑎(.r‘𝑅)𝑏)) |
48 | 47 | fveq2d 6772 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) ∧ 𝑥 = (𝑎(.r‘𝑅)𝑏)) → ( ∗ ‘𝑥) = ( ∗ ‘(𝑎(.r‘𝑅)𝑏))) |
49 | 48, 47 | eqeq12d 2755 |
. . . . 5
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) ∧ 𝑥 = (𝑎(.r‘𝑅)𝑏)) → (( ∗ ‘𝑥) = 𝑥 ↔ ( ∗ ‘(𝑎(.r‘𝑅)𝑏)) = (𝑎(.r‘𝑅)𝑏))) |
50 | 46, 49 | rspcdv 3551 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) → (∀𝑥 ∈ 𝐵 ( ∗ ‘𝑥) = 𝑥 → ( ∗ ‘(𝑎(.r‘𝑅)𝑏)) = (𝑎(.r‘𝑅)𝑏))) |
51 | 21, 50 | mpd 15 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) → ( ∗ ‘(𝑎(.r‘𝑅)𝑏)) = (𝑎(.r‘𝑅)𝑏)) |
52 | 39, 32 | oveq12d 7286 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) → (( ∗ ‘𝑏)(.r‘𝑅)( ∗ ‘𝑎)) = (𝑏(.r‘𝑅)𝑎)) |
53 | 44, 51, 52 | 3eqtr4d 2789 |
. 2
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) → ( ∗ ‘(𝑎(.r‘𝑅)𝑏)) = (( ∗ ‘𝑏)(.r‘𝑅)( ∗ ‘𝑎))) |
54 | 18 | fveq2d 6772 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → ( ∗ ‘( ∗
‘𝑎)) = ( ∗
‘𝑎)) |
55 | 54, 18 | eqtrd 2779 |
. 2
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → ( ∗ ‘( ∗
‘𝑎)) = 𝑎) |
56 | 2, 3, 4, 6, 9, 19,
41, 53, 55 | issrngd 20102 |
1
⊢ (𝜑 → 𝑅 ∈ *-Ring) |