Step | Hyp | Ref
| Expression |
1 | | unitmulcl.1 |
. . . 4
⊢ 𝑈 = (Unit‘𝑅) |
2 | | unitgrp.2 |
. . . 4
⊢ 𝐺 = ((mulGrp‘𝑅) ↾s 𝑈) |
3 | 1, 2 | unitgrpbas 18666 |
. . 3
⊢ 𝑈 = (Base‘𝐺) |
4 | 3 | a1i 11 |
. 2
⊢ (𝑅 ∈ Ring → 𝑈 = (Base‘𝐺)) |
5 | | fvex 6201 |
. . . 4
⊢
(Base‘𝐺)
∈ V |
6 | 3, 5 | eqeltri 2697 |
. . 3
⊢ 𝑈 ∈ V |
7 | | eqid 2622 |
. . . . 5
⊢
(mulGrp‘𝑅) =
(mulGrp‘𝑅) |
8 | | eqid 2622 |
. . . . 5
⊢
(.r‘𝑅) = (.r‘𝑅) |
9 | 7, 8 | mgpplusg 18493 |
. . . 4
⊢
(.r‘𝑅) = (+g‘(mulGrp‘𝑅)) |
10 | 2, 9 | ressplusg 15993 |
. . 3
⊢ (𝑈 ∈ V →
(.r‘𝑅) =
(+g‘𝐺)) |
11 | 6, 10 | mp1i 13 |
. 2
⊢ (𝑅 ∈ Ring →
(.r‘𝑅) =
(+g‘𝐺)) |
12 | 1, 8 | unitmulcl 18664 |
. 2
⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈) → (𝑥(.r‘𝑅)𝑦) ∈ 𝑈) |
13 | | eqid 2622 |
. . . . 5
⊢
(Base‘𝑅) =
(Base‘𝑅) |
14 | 13, 1 | unitcl 18659 |
. . . 4
⊢ (𝑥 ∈ 𝑈 → 𝑥 ∈ (Base‘𝑅)) |
15 | 13, 1 | unitcl 18659 |
. . . 4
⊢ (𝑦 ∈ 𝑈 → 𝑦 ∈ (Base‘𝑅)) |
16 | 13, 1 | unitcl 18659 |
. . . 4
⊢ (𝑧 ∈ 𝑈 → 𝑧 ∈ (Base‘𝑅)) |
17 | 14, 15, 16 | 3anim123i 1247 |
. . 3
⊢ ((𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈) → (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅) ∧ 𝑧 ∈ (Base‘𝑅))) |
18 | 13, 8 | ringass 18564 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅) ∧ 𝑧 ∈ (Base‘𝑅))) → ((𝑥(.r‘𝑅)𝑦)(.r‘𝑅)𝑧) = (𝑥(.r‘𝑅)(𝑦(.r‘𝑅)𝑧))) |
19 | 17, 18 | sylan2 491 |
. 2
⊢ ((𝑅 ∈ Ring ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈)) → ((𝑥(.r‘𝑅)𝑦)(.r‘𝑅)𝑧) = (𝑥(.r‘𝑅)(𝑦(.r‘𝑅)𝑧))) |
20 | | eqid 2622 |
. . 3
⊢
(1r‘𝑅) = (1r‘𝑅) |
21 | 1, 20 | 1unit 18658 |
. 2
⊢ (𝑅 ∈ Ring →
(1r‘𝑅)
∈ 𝑈) |
22 | 13, 8, 20 | ringlidm 18571 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ (Base‘𝑅)) →
((1r‘𝑅)(.r‘𝑅)𝑥) = 𝑥) |
23 | 14, 22 | sylan2 491 |
. 2
⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) → ((1r‘𝑅)(.r‘𝑅)𝑥) = 𝑥) |
24 | | simpr 477 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) → 𝑥 ∈ 𝑈) |
25 | | eqid 2622 |
. . . . 5
⊢
(∥r‘𝑅) = (∥r‘𝑅) |
26 | | eqid 2622 |
. . . . 5
⊢
(oppr‘𝑅) = (oppr‘𝑅) |
27 | | eqid 2622 |
. . . . 5
⊢
(∥r‘(oppr‘𝑅)) =
(∥r‘(oppr‘𝑅)) |
28 | 1, 20, 25, 26, 27 | isunit 18657 |
. . . 4
⊢ (𝑥 ∈ 𝑈 ↔ (𝑥(∥r‘𝑅)(1r‘𝑅) ∧ 𝑥(∥r‘(oppr‘𝑅))(1r‘𝑅))) |
29 | 24, 28 | sylib 208 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) → (𝑥(∥r‘𝑅)(1r‘𝑅) ∧ 𝑥(∥r‘(oppr‘𝑅))(1r‘𝑅))) |
30 | 14 | adantl 482 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) → 𝑥 ∈ (Base‘𝑅)) |
31 | 13, 25, 8 | dvdsr2 18647 |
. . . . . 6
⊢ (𝑥 ∈ (Base‘𝑅) → (𝑥(∥r‘𝑅)(1r‘𝑅) ↔ ∃𝑦 ∈ (Base‘𝑅)(𝑦(.r‘𝑅)𝑥) = (1r‘𝑅))) |
32 | 30, 31 | syl 17 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) → (𝑥(∥r‘𝑅)(1r‘𝑅) ↔ ∃𝑦 ∈ (Base‘𝑅)(𝑦(.r‘𝑅)𝑥) = (1r‘𝑅))) |
33 | 26, 13 | opprbas 18629 |
. . . . . . 7
⊢
(Base‘𝑅) =
(Base‘(oppr‘𝑅)) |
34 | | eqid 2622 |
. . . . . . 7
⊢
(.r‘(oppr‘𝑅)) =
(.r‘(oppr‘𝑅)) |
35 | 33, 27, 34 | dvdsr2 18647 |
. . . . . 6
⊢ (𝑥 ∈ (Base‘𝑅) → (𝑥(∥r‘(oppr‘𝑅))(1r‘𝑅) ↔ ∃𝑚 ∈ (Base‘𝑅)(𝑚(.r‘(oppr‘𝑅))𝑥) =
(1r‘𝑅))) |
36 | 30, 35 | syl 17 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) → (𝑥(∥r‘(oppr‘𝑅))(1r‘𝑅) ↔ ∃𝑚 ∈ (Base‘𝑅)(𝑚(.r‘(oppr‘𝑅))𝑥) =
(1r‘𝑅))) |
37 | 32, 36 | anbi12d 747 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) → ((𝑥(∥r‘𝑅)(1r‘𝑅) ∧ 𝑥(∥r‘(oppr‘𝑅))(1r‘𝑅)) ↔ (∃𝑦 ∈ (Base‘𝑅)(𝑦(.r‘𝑅)𝑥) =
(1r‘𝑅) ∧ ∃𝑚 ∈ (Base‘𝑅)(𝑚(.r‘(oppr‘𝑅))𝑥) =
(1r‘𝑅)))) |
38 | | reeanv 3107 |
. . . . 5
⊢
(∃𝑦 ∈
(Base‘𝑅)∃𝑚 ∈ (Base‘𝑅)((𝑦(.r‘𝑅)𝑥) = (1r‘𝑅) ∧ (𝑚(.r‘(oppr‘𝑅))𝑥) = (1r‘𝑅)) ↔ (∃𝑦 ∈ (Base‘𝑅)(𝑦(.r‘𝑅)𝑥)
= (1r‘𝑅) ∧
∃𝑚 ∈ (Base‘𝑅)(𝑚(.r‘(oppr‘𝑅))𝑥) = (1r‘𝑅))) |
39 | | simprl 794 |
. . . . . . . . . . . 12
⊢ ((((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑚 ∈ (Base‘𝑅) ∧ ((𝑦(.r‘𝑅)𝑥) = (1r‘𝑅) ∧ (𝑚(.r‘(oppr‘𝑅))𝑥) = (1r‘𝑅)))) → 𝑚 ∈ (Base‘𝑅)) |
40 | 30 | ad2antrr 762 |
. . . . . . . . . . . 12
⊢ ((((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑚 ∈ (Base‘𝑅) ∧ ((𝑦(.r‘𝑅)𝑥) = (1r‘𝑅) ∧ (𝑚(.r‘(oppr‘𝑅))𝑥) = (1r‘𝑅)))) → 𝑥 ∈ (Base‘𝑅)) |
41 | 13, 25, 8 | dvdsrmul 18648 |
. . . . . . . . . . . 12
⊢ ((𝑚 ∈ (Base‘𝑅) ∧ 𝑥 ∈ (Base‘𝑅)) → 𝑚(∥r‘𝑅)(𝑥(.r‘𝑅)𝑚)) |
42 | 39, 40, 41 | syl2anc 693 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑚 ∈ (Base‘𝑅) ∧ ((𝑦(.r‘𝑅)𝑥) = (1r‘𝑅) ∧ (𝑚(.r‘(oppr‘𝑅))𝑥) = (1r‘𝑅)))) → 𝑚(∥r‘𝑅)(𝑥(.r‘𝑅)𝑚)) |
43 | | simplll 798 |
. . . . . . . . . . . . . 14
⊢ ((((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑚 ∈ (Base‘𝑅) ∧ ((𝑦(.r‘𝑅)𝑥) = (1r‘𝑅) ∧ (𝑚(.r‘(oppr‘𝑅))𝑥) = (1r‘𝑅)))) → 𝑅 ∈ Ring) |
44 | | simplr 792 |
. . . . . . . . . . . . . 14
⊢ ((((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑚 ∈ (Base‘𝑅) ∧ ((𝑦(.r‘𝑅)𝑥) = (1r‘𝑅) ∧ (𝑚(.r‘(oppr‘𝑅))𝑥) = (1r‘𝑅)))) → 𝑦 ∈ (Base‘𝑅)) |
45 | 13, 8 | ringass 18564 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ Ring ∧ (𝑦 ∈ (Base‘𝑅) ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑚 ∈ (Base‘𝑅))) → ((𝑦(.r‘𝑅)𝑥)(.r‘𝑅)𝑚) = (𝑦(.r‘𝑅)(𝑥(.r‘𝑅)𝑚))) |
46 | 43, 44, 40, 39, 45 | syl13anc 1328 |
. . . . . . . . . . . . 13
⊢ ((((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑚 ∈ (Base‘𝑅) ∧ ((𝑦(.r‘𝑅)𝑥) = (1r‘𝑅) ∧ (𝑚(.r‘(oppr‘𝑅))𝑥) = (1r‘𝑅)))) → ((𝑦(.r‘𝑅)𝑥)(.r‘𝑅)𝑚)
= (𝑦(.r‘𝑅)(𝑥(.r‘𝑅)𝑚))) |
47 | | simprrl 804 |
. . . . . . . . . . . . . 14
⊢ ((((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑚 ∈ (Base‘𝑅) ∧ ((𝑦(.r‘𝑅)𝑥) = (1r‘𝑅) ∧ (𝑚(.r‘(oppr‘𝑅))𝑥) = (1r‘𝑅)))) → (𝑦(.r‘𝑅)𝑥)
= (1r‘𝑅)) |
48 | 47 | oveq1d 6665 |
. . . . . . . . . . . . 13
⊢ ((((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑚 ∈ (Base‘𝑅) ∧ ((𝑦(.r‘𝑅)𝑥) = (1r‘𝑅) ∧ (𝑚(.r‘(oppr‘𝑅))𝑥) = (1r‘𝑅)))) → ((𝑦(.r‘𝑅)𝑥)(.r‘𝑅)𝑚)
= ((1r‘𝑅)(.r‘𝑅)𝑚)) |
49 | 13, 8, 26, 34 | opprmul 18626 |
. . . . . . . . . . . . . . 15
⊢ (𝑚(.r‘(oppr‘𝑅))𝑥) = (𝑥(.r‘𝑅)𝑚) |
50 | | simprrr 805 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑚 ∈ (Base‘𝑅) ∧ ((𝑦(.r‘𝑅)𝑥) = (1r‘𝑅) ∧ (𝑚(.r‘(oppr‘𝑅))𝑥) = (1r‘𝑅)))) → (𝑚(.r‘(oppr‘𝑅))𝑥) = (1r‘𝑅)) |
51 | 49, 50 | syl5eqr 2670 |
. . . . . . . . . . . . . 14
⊢ ((((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑚 ∈ (Base‘𝑅) ∧ ((𝑦(.r‘𝑅)𝑥) = (1r‘𝑅) ∧ (𝑚(.r‘(oppr‘𝑅))𝑥) = (1r‘𝑅)))) → (𝑥(.r‘𝑅)𝑚)
= (1r‘𝑅)) |
52 | 51 | oveq2d 6666 |
. . . . . . . . . . . . 13
⊢ ((((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑚 ∈ (Base‘𝑅) ∧ ((𝑦(.r‘𝑅)𝑥) = (1r‘𝑅) ∧ (𝑚(.r‘(oppr‘𝑅))𝑥) = (1r‘𝑅)))) → (𝑦(.r‘𝑅)(𝑥(.r‘𝑅)𝑚)) = (𝑦(.r‘𝑅)(1r‘𝑅))) |
53 | 46, 48, 52 | 3eqtr3d 2664 |
. . . . . . . . . . . 12
⊢ ((((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑚 ∈ (Base‘𝑅) ∧ ((𝑦(.r‘𝑅)𝑥) = (1r‘𝑅) ∧ (𝑚(.r‘(oppr‘𝑅))𝑥) = (1r‘𝑅)))) → ((1r‘𝑅)(.r‘𝑅)𝑚)
= (𝑦(.r‘𝑅)(1r‘𝑅))) |
54 | 13, 8, 20 | ringlidm 18571 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ Ring ∧ 𝑚 ∈ (Base‘𝑅)) →
((1r‘𝑅)(.r‘𝑅)𝑚) = 𝑚) |
55 | 43, 39, 54 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ ((((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑚 ∈ (Base‘𝑅) ∧ ((𝑦(.r‘𝑅)𝑥) = (1r‘𝑅) ∧ (𝑚(.r‘(oppr‘𝑅))𝑥) = (1r‘𝑅)))) → ((1r‘𝑅)(.r‘𝑅)𝑚)
= 𝑚) |
56 | 13, 8, 20 | ringridm 18572 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ Ring ∧ 𝑦 ∈ (Base‘𝑅)) → (𝑦(.r‘𝑅)(1r‘𝑅)) = 𝑦) |
57 | 43, 44, 56 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ ((((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑚 ∈ (Base‘𝑅) ∧ ((𝑦(.r‘𝑅)𝑥) = (1r‘𝑅) ∧ (𝑚(.r‘(oppr‘𝑅))𝑥) = (1r‘𝑅)))) → (𝑦(.r‘𝑅)(1r‘𝑅)) = 𝑦) |
58 | 53, 55, 57 | 3eqtr3d 2664 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑚 ∈ (Base‘𝑅) ∧ ((𝑦(.r‘𝑅)𝑥) = (1r‘𝑅) ∧ (𝑚(.r‘(oppr‘𝑅))𝑥) = (1r‘𝑅)))) → 𝑚 = 𝑦) |
59 | 42, 58, 51 | 3brtr3d 4684 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑚 ∈ (Base‘𝑅) ∧ ((𝑦(.r‘𝑅)𝑥) = (1r‘𝑅) ∧ (𝑚(.r‘(oppr‘𝑅))𝑥) = (1r‘𝑅)))) → 𝑦(∥r‘𝑅)(1r‘𝑅)) |
60 | 33, 27, 34 | dvdsrmul 18648 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ (Base‘𝑅) ∧ 𝑥 ∈ (Base‘𝑅)) → 𝑦(∥r‘(oppr‘𝑅))(𝑥(.r‘(oppr‘𝑅))𝑦)) |
61 | 44, 40, 60 | syl2anc 693 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑚 ∈ (Base‘𝑅) ∧ ((𝑦(.r‘𝑅)𝑥) = (1r‘𝑅) ∧ (𝑚(.r‘(oppr‘𝑅))𝑥) = (1r‘𝑅)))) → 𝑦(∥r‘(oppr‘𝑅))(𝑥(.r‘(oppr‘𝑅))𝑦)) |
62 | 13, 8, 26, 34 | opprmul 18626 |
. . . . . . . . . . . 12
⊢ (𝑥(.r‘(oppr‘𝑅))𝑦) = (𝑦(.r‘𝑅)𝑥) |
63 | 62, 47 | syl5eq 2668 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑚 ∈ (Base‘𝑅) ∧ ((𝑦(.r‘𝑅)𝑥) = (1r‘𝑅) ∧ (𝑚(.r‘(oppr‘𝑅))𝑥) = (1r‘𝑅)))) → (𝑥(.r‘(oppr‘𝑅))𝑦) = (1r‘𝑅)) |
64 | 61, 63 | breqtrd 4679 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑚 ∈ (Base‘𝑅) ∧ ((𝑦(.r‘𝑅)𝑥) = (1r‘𝑅) ∧ (𝑚(.r‘(oppr‘𝑅))𝑥) = (1r‘𝑅)))) → 𝑦(∥r‘(oppr‘𝑅))(1r‘𝑅)) |
65 | 1, 20, 25, 26, 27 | isunit 18657 |
. . . . . . . . . 10
⊢ (𝑦 ∈ 𝑈 ↔ (𝑦(∥r‘𝑅)(1r‘𝑅) ∧ 𝑦(∥r‘(oppr‘𝑅))(1r‘𝑅))) |
66 | 59, 64, 65 | sylanbrc 698 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑚 ∈ (Base‘𝑅) ∧ ((𝑦(.r‘𝑅)𝑥) = (1r‘𝑅) ∧ (𝑚(.r‘(oppr‘𝑅))𝑥) = (1r‘𝑅)))) → 𝑦 ∈ 𝑈) |
67 | 66, 47 | jca 554 |
. . . . . . . 8
⊢ ((((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑚 ∈ (Base‘𝑅) ∧ ((𝑦(.r‘𝑅)𝑥) = (1r‘𝑅) ∧ (𝑚(.r‘(oppr‘𝑅))𝑥) = (1r‘𝑅)))) → (𝑦 ∈ 𝑈 ∧ (𝑦(.r‘𝑅)𝑥)
= (1r‘𝑅))) |
68 | 67 | rexlimdvaa 3032 |
. . . . . . 7
⊢ (((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) → (∃𝑚 ∈ (Base‘𝑅)((𝑦(.r‘𝑅)𝑥) = (1r‘𝑅) ∧ (𝑚(.r‘(oppr‘𝑅))𝑥) = (1r‘𝑅)) → (𝑦 ∈ 𝑈 ∧ (𝑦(.r‘𝑅)𝑥)
= (1r‘𝑅)))) |
69 | 68 | expimpd 629 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) → ((𝑦 ∈ (Base‘𝑅) ∧ ∃𝑚 ∈ (Base‘𝑅)((𝑦(.r‘𝑅)𝑥) = (1r‘𝑅) ∧ (𝑚(.r‘(oppr‘𝑅))𝑥) = (1r‘𝑅))) → (𝑦 ∈ 𝑈 ∧ (𝑦(.r‘𝑅)𝑥)
= (1r‘𝑅)))) |
70 | 69 | reximdv2 3014 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) → (∃𝑦 ∈ (Base‘𝑅)∃𝑚 ∈ (Base‘𝑅)((𝑦(.r‘𝑅)𝑥) = (1r‘𝑅) ∧ (𝑚(.r‘(oppr‘𝑅))𝑥) = (1r‘𝑅)) → ∃𝑦 ∈ 𝑈 (𝑦(.r‘𝑅)𝑥)
= (1r‘𝑅))) |
71 | 38, 70 | syl5bir 233 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) → ((∃𝑦 ∈ (Base‘𝑅)(𝑦(.r‘𝑅)𝑥) = (1r‘𝑅) ∧ ∃𝑚 ∈ (Base‘𝑅)(𝑚(.r‘(oppr‘𝑅))𝑥) = (1r‘𝑅)) → ∃𝑦 ∈ 𝑈 (𝑦(.r‘𝑅)𝑥)
= (1r‘𝑅))) |
72 | 37, 71 | sylbid 230 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) → ((𝑥(∥r‘𝑅)(1r‘𝑅) ∧ 𝑥(∥r‘(oppr‘𝑅))(1r‘𝑅)) → ∃𝑦 ∈ 𝑈 (𝑦(.r‘𝑅)𝑥) =
(1r‘𝑅))) |
73 | 29, 72 | mpd 15 |
. 2
⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) → ∃𝑦 ∈ 𝑈 (𝑦(.r‘𝑅)𝑥) = (1r‘𝑅)) |
74 | 4, 11, 12, 19, 21, 23, 73 | isgrpde 17443 |
1
⊢ (𝑅 ∈ Ring → 𝐺 ∈ Grp) |