| Step | Hyp | Ref
| Expression |
| 1 | | unitmulcl.1 |
. . . 4
⊢ 𝑈 = (Unit‘𝑅) |
| 2 | | unitgrp.2 |
. . . 4
⊢ 𝐺 = ((mulGrp‘𝑅) ↾s 𝑈) |
| 3 | 1, 2 | unitgrpbas 20382 |
. . 3
⊢ 𝑈 = (Base‘𝐺) |
| 4 | 3 | a1i 11 |
. 2
⊢ (𝑅 ∈ Ring → 𝑈 = (Base‘𝐺)) |
| 5 | 1 | fvexi 6920 |
. . 3
⊢ 𝑈 ∈ V |
| 6 | | eqid 2737 |
. . . . 5
⊢
(mulGrp‘𝑅) =
(mulGrp‘𝑅) |
| 7 | | eqid 2737 |
. . . . 5
⊢
(.r‘𝑅) = (.r‘𝑅) |
| 8 | 6, 7 | mgpplusg 20141 |
. . . 4
⊢
(.r‘𝑅) = (+g‘(mulGrp‘𝑅)) |
| 9 | 2, 8 | ressplusg 17334 |
. . 3
⊢ (𝑈 ∈ V →
(.r‘𝑅) =
(+g‘𝐺)) |
| 10 | 5, 9 | mp1i 13 |
. 2
⊢ (𝑅 ∈ Ring →
(.r‘𝑅) =
(+g‘𝐺)) |
| 11 | 1, 7 | unitmulcl 20380 |
. 2
⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈) → (𝑥(.r‘𝑅)𝑦) ∈ 𝑈) |
| 12 | | eqid 2737 |
. . . . 5
⊢
(Base‘𝑅) =
(Base‘𝑅) |
| 13 | 12, 1 | unitcl 20375 |
. . . 4
⊢ (𝑥 ∈ 𝑈 → 𝑥 ∈ (Base‘𝑅)) |
| 14 | 12, 1 | unitcl 20375 |
. . . 4
⊢ (𝑦 ∈ 𝑈 → 𝑦 ∈ (Base‘𝑅)) |
| 15 | 12, 1 | unitcl 20375 |
. . . 4
⊢ (𝑧 ∈ 𝑈 → 𝑧 ∈ (Base‘𝑅)) |
| 16 | 13, 14, 15 | 3anim123i 1152 |
. . 3
⊢ ((𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈) → (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅) ∧ 𝑧 ∈ (Base‘𝑅))) |
| 17 | 12, 7 | ringass 20250 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅) ∧ 𝑧 ∈ (Base‘𝑅))) → ((𝑥(.r‘𝑅)𝑦)(.r‘𝑅)𝑧) = (𝑥(.r‘𝑅)(𝑦(.r‘𝑅)𝑧))) |
| 18 | 16, 17 | sylan2 593 |
. 2
⊢ ((𝑅 ∈ Ring ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈)) → ((𝑥(.r‘𝑅)𝑦)(.r‘𝑅)𝑧) = (𝑥(.r‘𝑅)(𝑦(.r‘𝑅)𝑧))) |
| 19 | | eqid 2737 |
. . 3
⊢
(1r‘𝑅) = (1r‘𝑅) |
| 20 | 1, 19 | 1unit 20374 |
. 2
⊢ (𝑅 ∈ Ring →
(1r‘𝑅)
∈ 𝑈) |
| 21 | 12, 7, 19 | ringlidm 20266 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ (Base‘𝑅)) →
((1r‘𝑅)(.r‘𝑅)𝑥) = 𝑥) |
| 22 | 13, 21 | sylan2 593 |
. 2
⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) → ((1r‘𝑅)(.r‘𝑅)𝑥) = 𝑥) |
| 23 | | simpr 484 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) → 𝑥 ∈ 𝑈) |
| 24 | | eqid 2737 |
. . . . 5
⊢
(∥r‘𝑅) = (∥r‘𝑅) |
| 25 | | eqid 2737 |
. . . . 5
⊢
(oppr‘𝑅) = (oppr‘𝑅) |
| 26 | | eqid 2737 |
. . . . 5
⊢
(∥r‘(oppr‘𝑅)) =
(∥r‘(oppr‘𝑅)) |
| 27 | 1, 19, 24, 25, 26 | isunit 20373 |
. . . 4
⊢ (𝑥 ∈ 𝑈 ↔ (𝑥(∥r‘𝑅)(1r‘𝑅) ∧ 𝑥(∥r‘(oppr‘𝑅))(1r‘𝑅))) |
| 28 | 23, 27 | sylib 218 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) → (𝑥(∥r‘𝑅)(1r‘𝑅) ∧ 𝑥(∥r‘(oppr‘𝑅))(1r‘𝑅))) |
| 29 | 13 | adantl 481 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) → 𝑥 ∈ (Base‘𝑅)) |
| 30 | 12, 24, 7 | dvdsr2 20363 |
. . . . . 6
⊢ (𝑥 ∈ (Base‘𝑅) → (𝑥(∥r‘𝑅)(1r‘𝑅) ↔ ∃𝑦 ∈ (Base‘𝑅)(𝑦(.r‘𝑅)𝑥) = (1r‘𝑅))) |
| 31 | 29, 30 | syl 17 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) → (𝑥(∥r‘𝑅)(1r‘𝑅) ↔ ∃𝑦 ∈ (Base‘𝑅)(𝑦(.r‘𝑅)𝑥) = (1r‘𝑅))) |
| 32 | 25, 12 | opprbas 20341 |
. . . . . . 7
⊢
(Base‘𝑅) =
(Base‘(oppr‘𝑅)) |
| 33 | | eqid 2737 |
. . . . . . 7
⊢
(.r‘(oppr‘𝑅)) =
(.r‘(oppr‘𝑅)) |
| 34 | 32, 26, 33 | dvdsr2 20363 |
. . . . . 6
⊢ (𝑥 ∈ (Base‘𝑅) → (𝑥(∥r‘(oppr‘𝑅))(1r‘𝑅) ↔ ∃𝑚 ∈ (Base‘𝑅)(𝑚(.r‘(oppr‘𝑅))𝑥) = (1r‘𝑅))) |
| 35 | 29, 34 | syl 17 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) → (𝑥(∥r‘(oppr‘𝑅))(1r‘𝑅) ↔ ∃𝑚 ∈ (Base‘𝑅)(𝑚(.r‘(oppr‘𝑅))𝑥) = (1r‘𝑅))) |
| 36 | 31, 35 | anbi12d 632 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) → ((𝑥(∥r‘𝑅)(1r‘𝑅) ∧ 𝑥(∥r‘(oppr‘𝑅))(1r‘𝑅)) ↔ (∃𝑦 ∈ (Base‘𝑅)(𝑦(.r‘𝑅)𝑥) =
(1r‘𝑅) ∧ ∃𝑚 ∈ (Base‘𝑅)(𝑚(.r‘(oppr‘𝑅))𝑥) = (1r‘𝑅)))) |
| 37 | | reeanv 3229 |
. . . . 5
⊢
(∃𝑦 ∈
(Base‘𝑅)∃𝑚 ∈ (Base‘𝑅)((𝑦(.r‘𝑅)𝑥) = (1r‘𝑅) ∧ (𝑚(.r‘(oppr‘𝑅))𝑥) = (1r‘𝑅)) ↔ (∃𝑦 ∈ (Base‘𝑅)(𝑦(.r‘𝑅)𝑥)
= (1r‘𝑅) ∧
∃𝑚 ∈ (Base‘𝑅)(𝑚(.r‘(oppr‘𝑅))𝑥) = (1r‘𝑅))) |
| 38 | | simprl 771 |
. . . . . . . . . . . 12
⊢ ((((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑚 ∈ (Base‘𝑅) ∧ ((𝑦(.r‘𝑅)𝑥) = (1r‘𝑅) ∧ (𝑚(.r‘(oppr‘𝑅))𝑥) = (1r‘𝑅)))) → 𝑚 ∈ (Base‘𝑅)) |
| 39 | 29 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ ((((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑚 ∈ (Base‘𝑅) ∧ ((𝑦(.r‘𝑅)𝑥) = (1r‘𝑅) ∧ (𝑚(.r‘(oppr‘𝑅))𝑥) = (1r‘𝑅)))) → 𝑥 ∈ (Base‘𝑅)) |
| 40 | 12, 24, 7 | dvdsrmul 20364 |
. . . . . . . . . . . 12
⊢ ((𝑚 ∈ (Base‘𝑅) ∧ 𝑥 ∈ (Base‘𝑅)) → 𝑚(∥r‘𝑅)(𝑥(.r‘𝑅)𝑚)) |
| 41 | 38, 39, 40 | syl2anc 584 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑚 ∈ (Base‘𝑅) ∧ ((𝑦(.r‘𝑅)𝑥) = (1r‘𝑅) ∧ (𝑚(.r‘(oppr‘𝑅))𝑥) = (1r‘𝑅)))) → 𝑚(∥r‘𝑅)(𝑥(.r‘𝑅)𝑚)) |
| 42 | | simplll 775 |
. . . . . . . . . . . . . 14
⊢ ((((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑚 ∈ (Base‘𝑅) ∧ ((𝑦(.r‘𝑅)𝑥) = (1r‘𝑅) ∧ (𝑚(.r‘(oppr‘𝑅))𝑥) = (1r‘𝑅)))) → 𝑅 ∈ Ring) |
| 43 | | simplr 769 |
. . . . . . . . . . . . . 14
⊢ ((((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑚 ∈ (Base‘𝑅) ∧ ((𝑦(.r‘𝑅)𝑥) = (1r‘𝑅) ∧ (𝑚(.r‘(oppr‘𝑅))𝑥) = (1r‘𝑅)))) → 𝑦 ∈ (Base‘𝑅)) |
| 44 | 12, 7 | ringass 20250 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ Ring ∧ (𝑦 ∈ (Base‘𝑅) ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑚 ∈ (Base‘𝑅))) → ((𝑦(.r‘𝑅)𝑥)(.r‘𝑅)𝑚) = (𝑦(.r‘𝑅)(𝑥(.r‘𝑅)𝑚))) |
| 45 | 42, 43, 39, 38, 44 | syl13anc 1374 |
. . . . . . . . . . . . 13
⊢ ((((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑚 ∈ (Base‘𝑅) ∧ ((𝑦(.r‘𝑅)𝑥) = (1r‘𝑅) ∧ (𝑚(.r‘(oppr‘𝑅))𝑥) = (1r‘𝑅)))) → ((𝑦(.r‘𝑅)𝑥)(.r‘𝑅)𝑚)
= (𝑦(.r‘𝑅)(𝑥(.r‘𝑅)𝑚))) |
| 46 | | simprrl 781 |
. . . . . . . . . . . . . 14
⊢ ((((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑚 ∈ (Base‘𝑅) ∧ ((𝑦(.r‘𝑅)𝑥) = (1r‘𝑅) ∧ (𝑚(.r‘(oppr‘𝑅))𝑥) = (1r‘𝑅)))) → (𝑦(.r‘𝑅)𝑥)
= (1r‘𝑅)) |
| 47 | 46 | oveq1d 7446 |
. . . . . . . . . . . . 13
⊢ ((((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑚 ∈ (Base‘𝑅) ∧ ((𝑦(.r‘𝑅)𝑥) = (1r‘𝑅) ∧ (𝑚(.r‘(oppr‘𝑅))𝑥) = (1r‘𝑅)))) → ((𝑦(.r‘𝑅)𝑥)(.r‘𝑅)𝑚)
= ((1r‘𝑅)(.r‘𝑅)𝑚)) |
| 48 | 12, 7, 25, 33 | opprmul 20337 |
. . . . . . . . . . . . . . 15
⊢ (𝑚(.r‘(oppr‘𝑅))𝑥) = (𝑥(.r‘𝑅)𝑚) |
| 49 | | simprrr 782 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑚 ∈ (Base‘𝑅) ∧ ((𝑦(.r‘𝑅)𝑥) = (1r‘𝑅) ∧ (𝑚(.r‘(oppr‘𝑅))𝑥) = (1r‘𝑅)))) → (𝑚(.r‘(oppr‘𝑅))𝑥) = (1r‘𝑅)) |
| 50 | 48, 49 | eqtr3id 2791 |
. . . . . . . . . . . . . 14
⊢ ((((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑚 ∈ (Base‘𝑅) ∧ ((𝑦(.r‘𝑅)𝑥) = (1r‘𝑅) ∧ (𝑚(.r‘(oppr‘𝑅))𝑥) = (1r‘𝑅)))) → (𝑥(.r‘𝑅)𝑚)
= (1r‘𝑅)) |
| 51 | 50 | oveq2d 7447 |
. . . . . . . . . . . . 13
⊢ ((((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑚 ∈ (Base‘𝑅) ∧ ((𝑦(.r‘𝑅)𝑥) = (1r‘𝑅) ∧ (𝑚(.r‘(oppr‘𝑅))𝑥) = (1r‘𝑅)))) → (𝑦(.r‘𝑅)(𝑥(.r‘𝑅)𝑚)) = (𝑦(.r‘𝑅)(1r‘𝑅))) |
| 52 | 45, 47, 51 | 3eqtr3d 2785 |
. . . . . . . . . . . 12
⊢ ((((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑚 ∈ (Base‘𝑅) ∧ ((𝑦(.r‘𝑅)𝑥) = (1r‘𝑅) ∧ (𝑚(.r‘(oppr‘𝑅))𝑥) = (1r‘𝑅)))) → ((1r‘𝑅)(.r‘𝑅)𝑚)
= (𝑦(.r‘𝑅)(1r‘𝑅))) |
| 53 | 12, 7, 19 | ringlidm 20266 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ Ring ∧ 𝑚 ∈ (Base‘𝑅)) →
((1r‘𝑅)(.r‘𝑅)𝑚) = 𝑚) |
| 54 | 42, 38, 53 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ ((((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑚 ∈ (Base‘𝑅) ∧ ((𝑦(.r‘𝑅)𝑥) = (1r‘𝑅) ∧ (𝑚(.r‘(oppr‘𝑅))𝑥) = (1r‘𝑅)))) → ((1r‘𝑅)(.r‘𝑅)𝑚)
= 𝑚) |
| 55 | 12, 7, 19 | ringridm 20267 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ Ring ∧ 𝑦 ∈ (Base‘𝑅)) → (𝑦(.r‘𝑅)(1r‘𝑅)) = 𝑦) |
| 56 | 42, 43, 55 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ ((((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑚 ∈ (Base‘𝑅) ∧ ((𝑦(.r‘𝑅)𝑥) = (1r‘𝑅) ∧ (𝑚(.r‘(oppr‘𝑅))𝑥) = (1r‘𝑅)))) → (𝑦(.r‘𝑅)(1r‘𝑅)) = 𝑦) |
| 57 | 52, 54, 56 | 3eqtr3d 2785 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑚 ∈ (Base‘𝑅) ∧ ((𝑦(.r‘𝑅)𝑥) = (1r‘𝑅) ∧ (𝑚(.r‘(oppr‘𝑅))𝑥) = (1r‘𝑅)))) → 𝑚 = 𝑦) |
| 58 | 41, 57, 50 | 3brtr3d 5174 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑚 ∈ (Base‘𝑅) ∧ ((𝑦(.r‘𝑅)𝑥) = (1r‘𝑅) ∧ (𝑚(.r‘(oppr‘𝑅))𝑥) = (1r‘𝑅)))) → 𝑦(∥r‘𝑅)(1r‘𝑅)) |
| 59 | 32, 26, 33 | dvdsrmul 20364 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ (Base‘𝑅) ∧ 𝑥 ∈ (Base‘𝑅)) → 𝑦(∥r‘(oppr‘𝑅))(𝑥(.r‘(oppr‘𝑅))𝑦)) |
| 60 | 43, 39, 59 | syl2anc 584 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑚 ∈ (Base‘𝑅) ∧ ((𝑦(.r‘𝑅)𝑥) = (1r‘𝑅) ∧ (𝑚(.r‘(oppr‘𝑅))𝑥) = (1r‘𝑅)))) → 𝑦(∥r‘(oppr‘𝑅))(𝑥(.r‘(oppr‘𝑅))𝑦)) |
| 61 | 12, 7, 25, 33 | opprmul 20337 |
. . . . . . . . . . . 12
⊢ (𝑥(.r‘(oppr‘𝑅))𝑦) = (𝑦(.r‘𝑅)𝑥) |
| 62 | 61, 46 | eqtrid 2789 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑚 ∈ (Base‘𝑅) ∧ ((𝑦(.r‘𝑅)𝑥) = (1r‘𝑅) ∧ (𝑚(.r‘(oppr‘𝑅))𝑥) = (1r‘𝑅)))) → (𝑥(.r‘(oppr‘𝑅))𝑦) = (1r‘𝑅)) |
| 63 | 60, 62 | breqtrd 5169 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑚 ∈ (Base‘𝑅) ∧ ((𝑦(.r‘𝑅)𝑥) = (1r‘𝑅) ∧ (𝑚(.r‘(oppr‘𝑅))𝑥) = (1r‘𝑅)))) → 𝑦(∥r‘(oppr‘𝑅))(1r‘𝑅)) |
| 64 | 1, 19, 24, 25, 26 | isunit 20373 |
. . . . . . . . . 10
⊢ (𝑦 ∈ 𝑈 ↔ (𝑦(∥r‘𝑅)(1r‘𝑅) ∧ 𝑦(∥r‘(oppr‘𝑅))(1r‘𝑅))) |
| 65 | 58, 63, 64 | sylanbrc 583 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑚 ∈ (Base‘𝑅) ∧ ((𝑦(.r‘𝑅)𝑥) = (1r‘𝑅) ∧ (𝑚(.r‘(oppr‘𝑅))𝑥) = (1r‘𝑅)))) → 𝑦 ∈ 𝑈) |
| 66 | 65, 46 | jca 511 |
. . . . . . . 8
⊢ ((((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑚 ∈ (Base‘𝑅) ∧ ((𝑦(.r‘𝑅)𝑥) = (1r‘𝑅) ∧ (𝑚(.r‘(oppr‘𝑅))𝑥) = (1r‘𝑅)))) → (𝑦 ∈ 𝑈 ∧ (𝑦(.r‘𝑅)𝑥)
= (1r‘𝑅))) |
| 67 | 66 | rexlimdvaa 3156 |
. . . . . . 7
⊢ (((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) → (∃𝑚 ∈ (Base‘𝑅)((𝑦(.r‘𝑅)𝑥) = (1r‘𝑅) ∧ (𝑚(.r‘(oppr‘𝑅))𝑥) = (1r‘𝑅)) → (𝑦 ∈ 𝑈 ∧ (𝑦(.r‘𝑅)𝑥)
= (1r‘𝑅)))) |
| 68 | 67 | expimpd 453 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) → ((𝑦 ∈ (Base‘𝑅) ∧ ∃𝑚 ∈ (Base‘𝑅)((𝑦(.r‘𝑅)𝑥) = (1r‘𝑅) ∧ (𝑚(.r‘(oppr‘𝑅))𝑥) = (1r‘𝑅))) → (𝑦 ∈ 𝑈 ∧ (𝑦(.r‘𝑅)𝑥)
= (1r‘𝑅)))) |
| 69 | 68 | reximdv2 3164 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) → (∃𝑦 ∈ (Base‘𝑅)∃𝑚 ∈ (Base‘𝑅)((𝑦(.r‘𝑅)𝑥) = (1r‘𝑅) ∧ (𝑚(.r‘(oppr‘𝑅))𝑥) = (1r‘𝑅)) → ∃𝑦 ∈ 𝑈 (𝑦(.r‘𝑅)𝑥)
= (1r‘𝑅))) |
| 70 | 37, 69 | biimtrrid 243 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) → ((∃𝑦 ∈ (Base‘𝑅)(𝑦(.r‘𝑅)𝑥) = (1r‘𝑅) ∧ ∃𝑚 ∈ (Base‘𝑅)(𝑚(.r‘(oppr‘𝑅))𝑥) = (1r‘𝑅)) → ∃𝑦 ∈ 𝑈 (𝑦(.r‘𝑅)𝑥)
= (1r‘𝑅))) |
| 71 | 36, 70 | sylbid 240 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) → ((𝑥(∥r‘𝑅)(1r‘𝑅) ∧ 𝑥(∥r‘(oppr‘𝑅))(1r‘𝑅)) → ∃𝑦 ∈ 𝑈
(𝑦(.r‘𝑅)𝑥) =
(1r‘𝑅))) |
| 72 | 28, 71 | mpd 15 |
. 2
⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) → ∃𝑦 ∈ 𝑈 (𝑦(.r‘𝑅)𝑥) = (1r‘𝑅)) |
| 73 | 4, 10, 11, 18, 20, 22, 72 | isgrpde 18975 |
1
⊢ (𝑅 ∈ Ring → 𝐺 ∈ Grp) |