Step | Hyp | Ref
| Expression |
1 | | unitgrp.1 |
. . . 4
⊢ 𝑈 = (Unit‘𝑅) |
2 | 1 | a1i 9 |
. . 3
⊢ (𝑅 ∈ Ring → 𝑈 = (Unit‘𝑅)) |
3 | | unitgrp.2 |
. . . 4
⊢ 𝐺 = ((mulGrp‘𝑅) ↾s 𝑈) |
4 | 3 | a1i 9 |
. . 3
⊢ (𝑅 ∈ Ring → 𝐺 = ((mulGrp‘𝑅) ↾s 𝑈)) |
5 | | ringsrg 13177 |
. . 3
⊢ (𝑅 ∈ Ring → 𝑅 ∈ SRing) |
6 | 2, 4, 5 | unitgrpbasd 13237 |
. 2
⊢ (𝑅 ∈ Ring → 𝑈 = (Base‘𝐺)) |
7 | | eqid 2177 |
. . . 4
⊢
(mulGrp‘𝑅) =
(mulGrp‘𝑅) |
8 | | eqid 2177 |
. . . 4
⊢
(.r‘𝑅) = (.r‘𝑅) |
9 | 7, 8 | mgpplusgg 13087 |
. . 3
⊢ (𝑅 ∈ Ring →
(.r‘𝑅) =
(+g‘(mulGrp‘𝑅))) |
10 | | basfn 12514 |
. . . . 5
⊢ Base Fn
V |
11 | | elex 2748 |
. . . . 5
⊢ (𝑅 ∈ Ring → 𝑅 ∈ V) |
12 | | funfvex 5532 |
. . . . . 6
⊢ ((Fun
Base ∧ 𝑅 ∈ dom
Base) → (Base‘𝑅)
∈ V) |
13 | 12 | funfni 5316 |
. . . . 5
⊢ ((Base Fn
V ∧ 𝑅 ∈ V) →
(Base‘𝑅) ∈
V) |
14 | 10, 11, 13 | sylancr 414 |
. . . 4
⊢ (𝑅 ∈ Ring →
(Base‘𝑅) ∈
V) |
15 | | eqidd 2178 |
. . . . 5
⊢ (𝑅 ∈ Ring →
(Base‘𝑅) =
(Base‘𝑅)) |
16 | 15, 2, 5 | unitssd 13231 |
. . . 4
⊢ (𝑅 ∈ Ring → 𝑈 ⊆ (Base‘𝑅)) |
17 | 14, 16 | ssexd 4143 |
. . 3
⊢ (𝑅 ∈ Ring → 𝑈 ∈ V) |
18 | 7 | mgpex 13088 |
. . 3
⊢ (𝑅 ∈ Ring →
(mulGrp‘𝑅) ∈
V) |
19 | 4, 9, 17, 18 | ressplusgd 12581 |
. 2
⊢ (𝑅 ∈ Ring →
(.r‘𝑅) =
(+g‘𝐺)) |
20 | 1, 8 | unitmulcl 13235 |
. 2
⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈) → (𝑥(.r‘𝑅)𝑦) ∈ 𝑈) |
21 | | eqidd 2178 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈)) → (Base‘𝑅) = (Base‘𝑅)) |
22 | 1 | a1i 9 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈)) → 𝑈 = (Unit‘𝑅)) |
23 | 5 | adantr 276 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈)) → 𝑅 ∈ SRing) |
24 | | simpr1 1003 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈)) → 𝑥 ∈ 𝑈) |
25 | 21, 22, 23, 24 | unitcld 13230 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈)) → 𝑥 ∈ (Base‘𝑅)) |
26 | | simpr2 1004 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈)) → 𝑦 ∈ 𝑈) |
27 | 21, 22, 23, 26 | unitcld 13230 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈)) → 𝑦 ∈ (Base‘𝑅)) |
28 | | simpr3 1005 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈)) → 𝑧 ∈ 𝑈) |
29 | 21, 22, 23, 28 | unitcld 13230 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈)) → 𝑧 ∈ (Base‘𝑅)) |
30 | 25, 27, 29 | 3jca 1177 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈)) → (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅) ∧ 𝑧 ∈ (Base‘𝑅))) |
31 | | eqid 2177 |
. . . 4
⊢
(Base‘𝑅) =
(Base‘𝑅) |
32 | 31, 8 | ringass 13152 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅) ∧ 𝑧 ∈ (Base‘𝑅))) → ((𝑥(.r‘𝑅)𝑦)(.r‘𝑅)𝑧) = (𝑥(.r‘𝑅)(𝑦(.r‘𝑅)𝑧))) |
33 | 30, 32 | syldan 282 |
. 2
⊢ ((𝑅 ∈ Ring ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈)) → ((𝑥(.r‘𝑅)𝑦)(.r‘𝑅)𝑧) = (𝑥(.r‘𝑅)(𝑦(.r‘𝑅)𝑧))) |
34 | | eqid 2177 |
. . 3
⊢
(1r‘𝑅) = (1r‘𝑅) |
35 | 1, 34 | 1unit 13229 |
. 2
⊢ (𝑅 ∈ Ring →
(1r‘𝑅)
∈ 𝑈) |
36 | | eqidd 2178 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) → (Base‘𝑅) = (Base‘𝑅)) |
37 | 1 | a1i 9 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) → 𝑈 = (Unit‘𝑅)) |
38 | 5 | adantr 276 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) → 𝑅 ∈ SRing) |
39 | | simpr 110 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) → 𝑥 ∈ 𝑈) |
40 | 36, 37, 38, 39 | unitcld 13230 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) → 𝑥 ∈ (Base‘𝑅)) |
41 | 31, 8, 34 | ringlidm 13159 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ (Base‘𝑅)) →
((1r‘𝑅)(.r‘𝑅)𝑥) = 𝑥) |
42 | 40, 41 | syldan 282 |
. 2
⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) → ((1r‘𝑅)(.r‘𝑅)𝑥) = 𝑥) |
43 | | eqidd 2178 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) → (1r‘𝑅) = (1r‘𝑅)) |
44 | | eqidd 2178 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) → (∥r‘𝑅) =
(∥r‘𝑅)) |
45 | | eqidd 2178 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) → (oppr‘𝑅) =
(oppr‘𝑅)) |
46 | | eqidd 2178 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) →
(∥r‘(oppr‘𝑅)) =
(∥r‘(oppr‘𝑅))) |
47 | 37, 43, 44, 45, 46, 38 | isunitd 13228 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) → (𝑥 ∈ 𝑈 ↔ (𝑥(∥r‘𝑅)(1r‘𝑅) ∧ 𝑥(∥r‘(oppr‘𝑅))(1r‘𝑅)))) |
48 | 39, 47 | mpbid 147 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) → (𝑥(∥r‘𝑅)(1r‘𝑅) ∧ 𝑥(∥r‘(oppr‘𝑅))(1r‘𝑅))) |
49 | | eqidd 2178 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) → (.r‘𝑅) = (.r‘𝑅)) |
50 | 36, 44, 38, 49, 40 | dvdsr2d 13217 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) → (𝑥(∥r‘𝑅)(1r‘𝑅) ↔ ∃𝑦 ∈ (Base‘𝑅)(𝑦(.r‘𝑅)𝑥) = (1r‘𝑅))) |
51 | | eqid 2177 |
. . . . . . . 8
⊢
(oppr‘𝑅) = (oppr‘𝑅) |
52 | 51, 31 | opprbasg 13200 |
. . . . . . 7
⊢ (𝑅 ∈ Ring →
(Base‘𝑅) =
(Base‘(oppr‘𝑅))) |
53 | 52 | adantr 276 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) → (Base‘𝑅) =
(Base‘(oppr‘𝑅))) |
54 | 51 | opprring 13202 |
. . . . . . . 8
⊢ (𝑅 ∈ Ring →
(oppr‘𝑅) ∈ Ring) |
55 | | ringsrg 13177 |
. . . . . . . 8
⊢
((oppr‘𝑅) ∈ Ring →
(oppr‘𝑅) ∈ SRing) |
56 | 54, 55 | syl 14 |
. . . . . . 7
⊢ (𝑅 ∈ Ring →
(oppr‘𝑅) ∈ SRing) |
57 | 56 | adantr 276 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) → (oppr‘𝑅) ∈ SRing) |
58 | | eqidd 2178 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) →
(.r‘(oppr‘𝑅)) =
(.r‘(oppr‘𝑅))) |
59 | 53, 46, 57, 58, 40 | dvdsr2d 13217 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) → (𝑥(∥r‘(oppr‘𝑅))(1r‘𝑅) ↔ ∃𝑚 ∈ (Base‘𝑅)(𝑚(.r‘(oppr‘𝑅))𝑥) = (1r‘𝑅))) |
60 | 50, 59 | anbi12d 473 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) → ((𝑥(∥r‘𝑅)(1r‘𝑅) ∧ 𝑥(∥r‘(oppr‘𝑅))(1r‘𝑅)) ↔ (∃𝑦 ∈ (Base‘𝑅)(𝑦(.r‘𝑅)𝑥) =
(1r‘𝑅) ∧ ∃𝑚 ∈ (Base‘𝑅)(𝑚(.r‘(oppr‘𝑅))𝑥) = (1r‘𝑅)))) |
61 | | reeanv 2646 |
. . . . 5
⊢
(∃𝑦 ∈
(Base‘𝑅)∃𝑚 ∈ (Base‘𝑅)((𝑦(.r‘𝑅)𝑥) = (1r‘𝑅) ∧ (𝑚(.r‘(oppr‘𝑅))𝑥) = (1r‘𝑅)) ↔ (∃𝑦 ∈ (Base‘𝑅)(𝑦(.r‘𝑅)𝑥)
= (1r‘𝑅) ∧
∃𝑚 ∈ (Base‘𝑅)(𝑚(.r‘(oppr‘𝑅))𝑥) = (1r‘𝑅))) |
62 | | eqidd 2178 |
. . . . . . . . . . . 12
⊢ ((((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑚 ∈ (Base‘𝑅) ∧ ((𝑦(.r‘𝑅)𝑥) = (1r‘𝑅) ∧ (𝑚(.r‘(oppr‘𝑅))𝑥) = (1r‘𝑅)))) → (Base‘𝑅) = (Base‘𝑅)) |
63 | | eqidd 2178 |
. . . . . . . . . . . 12
⊢ ((((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑚 ∈ (Base‘𝑅) ∧ ((𝑦(.r‘𝑅)𝑥) = (1r‘𝑅) ∧ (𝑚(.r‘(oppr‘𝑅))𝑥) = (1r‘𝑅)))) → (∥r‘𝑅) = (∥r‘𝑅)) |
64 | 38 | ad2antrr 488 |
. . . . . . . . . . . 12
⊢ ((((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑚 ∈ (Base‘𝑅) ∧ ((𝑦(.r‘𝑅)𝑥) = (1r‘𝑅) ∧ (𝑚(.r‘(oppr‘𝑅))𝑥) = (1r‘𝑅)))) → 𝑅 ∈ SRing) |
65 | | eqidd 2178 |
. . . . . . . . . . . 12
⊢ ((((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑚 ∈ (Base‘𝑅) ∧ ((𝑦(.r‘𝑅)𝑥) = (1r‘𝑅) ∧ (𝑚(.r‘(oppr‘𝑅))𝑥) = (1r‘𝑅)))) → (.r‘𝑅) = (.r‘𝑅)) |
66 | | simprl 529 |
. . . . . . . . . . . 12
⊢ ((((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑚 ∈ (Base‘𝑅) ∧ ((𝑦(.r‘𝑅)𝑥) = (1r‘𝑅) ∧ (𝑚(.r‘(oppr‘𝑅))𝑥) = (1r‘𝑅)))) → 𝑚 ∈ (Base‘𝑅)) |
67 | 40 | ad2antrr 488 |
. . . . . . . . . . . 12
⊢ ((((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑚 ∈ (Base‘𝑅) ∧ ((𝑦(.r‘𝑅)𝑥) = (1r‘𝑅) ∧ (𝑚(.r‘(oppr‘𝑅))𝑥) = (1r‘𝑅)))) → 𝑥 ∈ (Base‘𝑅)) |
68 | 62, 63, 64, 65, 66, 67 | dvdsrmuld 13218 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑚 ∈ (Base‘𝑅) ∧ ((𝑦(.r‘𝑅)𝑥) = (1r‘𝑅) ∧ (𝑚(.r‘(oppr‘𝑅))𝑥) = (1r‘𝑅)))) → 𝑚(∥r‘𝑅)(𝑥(.r‘𝑅)𝑚)) |
69 | | simplll 533 |
. . . . . . . . . . . . . 14
⊢ ((((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑚 ∈ (Base‘𝑅) ∧ ((𝑦(.r‘𝑅)𝑥) = (1r‘𝑅) ∧ (𝑚(.r‘(oppr‘𝑅))𝑥) = (1r‘𝑅)))) → 𝑅 ∈ Ring) |
70 | | simplr 528 |
. . . . . . . . . . . . . 14
⊢ ((((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑚 ∈ (Base‘𝑅) ∧ ((𝑦(.r‘𝑅)𝑥) = (1r‘𝑅) ∧ (𝑚(.r‘(oppr‘𝑅))𝑥) = (1r‘𝑅)))) → 𝑦 ∈ (Base‘𝑅)) |
71 | 31, 8 | ringass 13152 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ Ring ∧ (𝑦 ∈ (Base‘𝑅) ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑚 ∈ (Base‘𝑅))) → ((𝑦(.r‘𝑅)𝑥)(.r‘𝑅)𝑚) = (𝑦(.r‘𝑅)(𝑥(.r‘𝑅)𝑚))) |
72 | 69, 70, 67, 66, 71 | syl13anc 1240 |
. . . . . . . . . . . . 13
⊢ ((((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑚 ∈ (Base‘𝑅) ∧ ((𝑦(.r‘𝑅)𝑥) = (1r‘𝑅) ∧ (𝑚(.r‘(oppr‘𝑅))𝑥) = (1r‘𝑅)))) → ((𝑦(.r‘𝑅)𝑥)(.r‘𝑅)𝑚)
= (𝑦(.r‘𝑅)(𝑥(.r‘𝑅)𝑚))) |
73 | | simprrl 539 |
. . . . . . . . . . . . . 14
⊢ ((((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑚 ∈ (Base‘𝑅) ∧ ((𝑦(.r‘𝑅)𝑥) = (1r‘𝑅) ∧ (𝑚(.r‘(oppr‘𝑅))𝑥) = (1r‘𝑅)))) → (𝑦(.r‘𝑅)𝑥)
= (1r‘𝑅)) |
74 | 73 | oveq1d 5889 |
. . . . . . . . . . . . 13
⊢ ((((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑚 ∈ (Base‘𝑅) ∧ ((𝑦(.r‘𝑅)𝑥) = (1r‘𝑅) ∧ (𝑚(.r‘(oppr‘𝑅))𝑥) = (1r‘𝑅)))) → ((𝑦(.r‘𝑅)𝑥)(.r‘𝑅)𝑚)
= ((1r‘𝑅)(.r‘𝑅)𝑚)) |
75 | 39 | ad2antrr 488 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑚 ∈ (Base‘𝑅) ∧ ((𝑦(.r‘𝑅)𝑥) = (1r‘𝑅) ∧ (𝑚(.r‘(oppr‘𝑅))𝑥) = (1r‘𝑅)))) → 𝑥 ∈ 𝑈) |
76 | | eqid 2177 |
. . . . . . . . . . . . . . . . 17
⊢
(.r‘(oppr‘𝑅)) =
(.r‘(oppr‘𝑅)) |
77 | 31, 8, 51, 76 | opprmulg 13196 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑅 ∈ Ring ∧ 𝑚 ∈ (Base‘𝑅) ∧ 𝑥 ∈ 𝑈) → (𝑚(.r‘(oppr‘𝑅))𝑥) = (𝑥(.r‘𝑅)𝑚)) |
78 | 69, 66, 75, 77 | syl3anc 1238 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑚 ∈ (Base‘𝑅) ∧ ((𝑦(.r‘𝑅)𝑥) = (1r‘𝑅) ∧ (𝑚(.r‘(oppr‘𝑅))𝑥) = (1r‘𝑅)))) → (𝑚(.r‘(oppr‘𝑅))𝑥) = (𝑥(.r‘𝑅)𝑚)) |
79 | | simprrr 540 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑚 ∈ (Base‘𝑅) ∧ ((𝑦(.r‘𝑅)𝑥) = (1r‘𝑅) ∧ (𝑚(.r‘(oppr‘𝑅))𝑥) = (1r‘𝑅)))) → (𝑚(.r‘(oppr‘𝑅))𝑥) = (1r‘𝑅)) |
80 | 78, 79 | eqtr3d 2212 |
. . . . . . . . . . . . . 14
⊢ ((((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑚 ∈ (Base‘𝑅) ∧ ((𝑦(.r‘𝑅)𝑥) = (1r‘𝑅) ∧ (𝑚(.r‘(oppr‘𝑅))𝑥) = (1r‘𝑅)))) → (𝑥(.r‘𝑅)𝑚)
= (1r‘𝑅)) |
81 | 80 | oveq2d 5890 |
. . . . . . . . . . . . 13
⊢ ((((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑚 ∈ (Base‘𝑅) ∧ ((𝑦(.r‘𝑅)𝑥) = (1r‘𝑅) ∧ (𝑚(.r‘(oppr‘𝑅))𝑥) = (1r‘𝑅)))) → (𝑦(.r‘𝑅)(𝑥(.r‘𝑅)𝑚)) = (𝑦(.r‘𝑅)(1r‘𝑅))) |
82 | 72, 74, 81 | 3eqtr3d 2218 |
. . . . . . . . . . . 12
⊢ ((((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑚 ∈ (Base‘𝑅) ∧ ((𝑦(.r‘𝑅)𝑥) = (1r‘𝑅) ∧ (𝑚(.r‘(oppr‘𝑅))𝑥) = (1r‘𝑅)))) → ((1r‘𝑅)(.r‘𝑅)𝑚)
= (𝑦(.r‘𝑅)(1r‘𝑅))) |
83 | 31, 8, 34 | ringlidm 13159 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ Ring ∧ 𝑚 ∈ (Base‘𝑅)) →
((1r‘𝑅)(.r‘𝑅)𝑚) = 𝑚) |
84 | 69, 66, 83 | syl2anc 411 |
. . . . . . . . . . . 12
⊢ ((((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑚 ∈ (Base‘𝑅) ∧ ((𝑦(.r‘𝑅)𝑥) = (1r‘𝑅) ∧ (𝑚(.r‘(oppr‘𝑅))𝑥) = (1r‘𝑅)))) → ((1r‘𝑅)(.r‘𝑅)𝑚)
= 𝑚) |
85 | 31, 8, 34 | ringridm 13160 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ Ring ∧ 𝑦 ∈ (Base‘𝑅)) → (𝑦(.r‘𝑅)(1r‘𝑅)) = 𝑦) |
86 | 69, 70, 85 | syl2anc 411 |
. . . . . . . . . . . 12
⊢ ((((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑚 ∈ (Base‘𝑅) ∧ ((𝑦(.r‘𝑅)𝑥) = (1r‘𝑅) ∧ (𝑚(.r‘(oppr‘𝑅))𝑥) = (1r‘𝑅)))) → (𝑦(.r‘𝑅)(1r‘𝑅)) = 𝑦) |
87 | 82, 84, 86 | 3eqtr3d 2218 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑚 ∈ (Base‘𝑅) ∧ ((𝑦(.r‘𝑅)𝑥) = (1r‘𝑅) ∧ (𝑚(.r‘(oppr‘𝑅))𝑥) = (1r‘𝑅)))) → 𝑚 = 𝑦) |
88 | 68, 87, 80 | 3brtr3d 4034 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑚 ∈ (Base‘𝑅) ∧ ((𝑦(.r‘𝑅)𝑥) = (1r‘𝑅) ∧ (𝑚(.r‘(oppr‘𝑅))𝑥) = (1r‘𝑅)))) → 𝑦(∥r‘𝑅)(1r‘𝑅)) |
89 | 69, 52 | syl 14 |
. . . . . . . . . . . 12
⊢ ((((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑚 ∈ (Base‘𝑅) ∧ ((𝑦(.r‘𝑅)𝑥) = (1r‘𝑅) ∧ (𝑚(.r‘(oppr‘𝑅))𝑥) = (1r‘𝑅)))) → (Base‘𝑅) = (Base‘(oppr‘𝑅))) |
90 | | eqidd 2178 |
. . . . . . . . . . . 12
⊢ ((((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑚 ∈ (Base‘𝑅) ∧ ((𝑦(.r‘𝑅)𝑥) = (1r‘𝑅) ∧ (𝑚(.r‘(oppr‘𝑅))𝑥) = (1r‘𝑅)))) →
(∥r‘(oppr‘𝑅)) =
(∥r‘(oppr‘𝑅))) |
91 | 69, 56 | syl 14 |
. . . . . . . . . . . 12
⊢ ((((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑚 ∈ (Base‘𝑅) ∧ ((𝑦(.r‘𝑅)𝑥) = (1r‘𝑅) ∧ (𝑚(.r‘(oppr‘𝑅))𝑥) = (1r‘𝑅)))) → (oppr‘𝑅) ∈ SRing) |
92 | | eqidd 2178 |
. . . . . . . . . . . 12
⊢ ((((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑚 ∈ (Base‘𝑅) ∧ ((𝑦(.r‘𝑅)𝑥) = (1r‘𝑅) ∧ (𝑚(.r‘(oppr‘𝑅))𝑥) = (1r‘𝑅)))) →
(.r‘(oppr‘𝑅)) =
(.r‘(oppr‘𝑅))) |
93 | 89, 90, 91, 92, 70, 67 | dvdsrmuld 13218 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑚 ∈ (Base‘𝑅) ∧ ((𝑦(.r‘𝑅)𝑥) = (1r‘𝑅) ∧ (𝑚(.r‘(oppr‘𝑅))𝑥) = (1r‘𝑅)))) → 𝑦(∥r‘(oppr‘𝑅))(𝑥(.r‘(oppr‘𝑅))𝑦)) |
94 | 31, 8, 51, 76 | opprmulg 13196 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ (Base‘𝑅)) → (𝑥(.r‘(oppr‘𝑅))𝑦) = (𝑦(.r‘𝑅)𝑥)) |
95 | 69, 75, 70, 94 | syl3anc 1238 |
. . . . . . . . . . . 12
⊢ ((((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑚 ∈ (Base‘𝑅) ∧ ((𝑦(.r‘𝑅)𝑥) = (1r‘𝑅) ∧ (𝑚(.r‘(oppr‘𝑅))𝑥) = (1r‘𝑅)))) → (𝑥(.r‘(oppr‘𝑅))𝑦) = (𝑦(.r‘𝑅)𝑥)) |
96 | 95, 73 | eqtrd 2210 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑚 ∈ (Base‘𝑅) ∧ ((𝑦(.r‘𝑅)𝑥) = (1r‘𝑅) ∧ (𝑚(.r‘(oppr‘𝑅))𝑥) = (1r‘𝑅)))) → (𝑥(.r‘(oppr‘𝑅))𝑦) = (1r‘𝑅)) |
97 | 93, 96 | breqtrd 4029 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑚 ∈ (Base‘𝑅) ∧ ((𝑦(.r‘𝑅)𝑥) = (1r‘𝑅) ∧ (𝑚(.r‘(oppr‘𝑅))𝑥) = (1r‘𝑅)))) → 𝑦(∥r‘(oppr‘𝑅))(1r‘𝑅)) |
98 | 1 | a1i 9 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑚 ∈ (Base‘𝑅) ∧ ((𝑦(.r‘𝑅)𝑥) = (1r‘𝑅) ∧ (𝑚(.r‘(oppr‘𝑅))𝑥) = (1r‘𝑅)))) → 𝑈 = (Unit‘𝑅)) |
99 | | eqidd 2178 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑚 ∈ (Base‘𝑅) ∧ ((𝑦(.r‘𝑅)𝑥) = (1r‘𝑅) ∧ (𝑚(.r‘(oppr‘𝑅))𝑥) = (1r‘𝑅)))) → (1r‘𝑅) = (1r‘𝑅)) |
100 | | eqidd 2178 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑚 ∈ (Base‘𝑅) ∧ ((𝑦(.r‘𝑅)𝑥) = (1r‘𝑅) ∧ (𝑚(.r‘(oppr‘𝑅))𝑥) = (1r‘𝑅)))) → (oppr‘𝑅) = (oppr‘𝑅)) |
101 | 98, 99, 63, 100, 90, 64 | isunitd 13228 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑚 ∈ (Base‘𝑅) ∧ ((𝑦(.r‘𝑅)𝑥) = (1r‘𝑅) ∧ (𝑚(.r‘(oppr‘𝑅))𝑥) = (1r‘𝑅)))) → (𝑦 ∈ 𝑈 ↔ (𝑦(∥r‘𝑅)(1r‘𝑅) ∧ 𝑦(∥r‘(oppr‘𝑅))(1r‘𝑅)))) |
102 | 88, 97, 101 | mpbir2and 944 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑚 ∈ (Base‘𝑅) ∧ ((𝑦(.r‘𝑅)𝑥) = (1r‘𝑅) ∧ (𝑚(.r‘(oppr‘𝑅))𝑥) = (1r‘𝑅)))) → 𝑦 ∈ 𝑈) |
103 | 102, 73 | jca 306 |
. . . . . . . 8
⊢ ((((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑚 ∈ (Base‘𝑅) ∧ ((𝑦(.r‘𝑅)𝑥) = (1r‘𝑅) ∧ (𝑚(.r‘(oppr‘𝑅))𝑥) = (1r‘𝑅)))) → (𝑦 ∈ 𝑈 ∧ (𝑦(.r‘𝑅)𝑥)
= (1r‘𝑅))) |
104 | 103 | rexlimdvaa 2595 |
. . . . . . 7
⊢ (((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) → (∃𝑚 ∈ (Base‘𝑅)((𝑦(.r‘𝑅)𝑥) = (1r‘𝑅) ∧ (𝑚(.r‘(oppr‘𝑅))𝑥) = (1r‘𝑅)) → (𝑦 ∈ 𝑈 ∧ (𝑦(.r‘𝑅)𝑥)
= (1r‘𝑅)))) |
105 | 104 | expimpd 363 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) → ((𝑦 ∈ (Base‘𝑅) ∧ ∃𝑚 ∈ (Base‘𝑅)((𝑦(.r‘𝑅)𝑥) = (1r‘𝑅) ∧ (𝑚(.r‘(oppr‘𝑅))𝑥) = (1r‘𝑅))) → (𝑦 ∈ 𝑈 ∧ (𝑦(.r‘𝑅)𝑥)
= (1r‘𝑅)))) |
106 | 105 | reximdv2 2576 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) → (∃𝑦 ∈ (Base‘𝑅)∃𝑚 ∈ (Base‘𝑅)((𝑦(.r‘𝑅)𝑥) = (1r‘𝑅) ∧ (𝑚(.r‘(oppr‘𝑅))𝑥) = (1r‘𝑅)) → ∃𝑦 ∈ 𝑈 (𝑦(.r‘𝑅)𝑥)
= (1r‘𝑅))) |
107 | 61, 106 | biimtrrid 153 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) → ((∃𝑦 ∈ (Base‘𝑅)(𝑦(.r‘𝑅)𝑥) = (1r‘𝑅) ∧ ∃𝑚 ∈ (Base‘𝑅)(𝑚(.r‘(oppr‘𝑅))𝑥) = (1r‘𝑅)) → ∃𝑦 ∈ 𝑈 (𝑦(.r‘𝑅)𝑥)
= (1r‘𝑅))) |
108 | 60, 107 | sylbid 150 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) → ((𝑥(∥r‘𝑅)(1r‘𝑅) ∧ 𝑥(∥r‘(oppr‘𝑅))(1r‘𝑅)) → ∃𝑦 ∈ 𝑈
(𝑦(.r‘𝑅)𝑥) =
(1r‘𝑅))) |
109 | 48, 108 | mpd 13 |
. 2
⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) → ∃𝑦 ∈ 𝑈 (𝑦(.r‘𝑅)𝑥) = (1r‘𝑅)) |
110 | 6, 19, 20, 33, 35, 42, 109 | isgrpde 12852 |
1
⊢ (𝑅 ∈ Ring → 𝐺 ∈ Grp) |