Step | Hyp | Ref
| Expression |
1 | | eqid 2193 |
. . . . . 6
⊢
(Base‘𝑅) =
(Base‘𝑅) |
2 | 1 | a1i 9 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) → (Base‘𝑅) = (Base‘𝑅)) |
3 | | unitrrg.u |
. . . . . 6
⊢ 𝑈 = (Unit‘𝑅) |
4 | 3 | a1i 9 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) → 𝑈 = (Unit‘𝑅)) |
5 | | ringsrg 13527 |
. . . . . 6
⊢ (𝑅 ∈ Ring → 𝑅 ∈ SRing) |
6 | 5 | adantr 276 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) → 𝑅 ∈ SRing) |
7 | | simpr 110 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) → 𝑥 ∈ 𝑈) |
8 | 2, 4, 6, 7 | unitcld 13588 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) → 𝑥 ∈ (Base‘𝑅)) |
9 | | oveq2 5918 |
. . . . . 6
⊢ ((𝑥(.r‘𝑅)𝑦) = (0g‘𝑅) → (((invr‘𝑅)‘𝑥)(.r‘𝑅)(𝑥(.r‘𝑅)𝑦)) = (((invr‘𝑅)‘𝑥)(.r‘𝑅)(0g‘𝑅))) |
10 | | eqid 2193 |
. . . . . . . . . . 11
⊢
(invr‘𝑅) = (invr‘𝑅) |
11 | | eqid 2193 |
. . . . . . . . . . 11
⊢
(.r‘𝑅) = (.r‘𝑅) |
12 | | eqid 2193 |
. . . . . . . . . . 11
⊢
(1r‘𝑅) = (1r‘𝑅) |
13 | 3, 10, 11, 12 | unitlinv 13606 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) → (((invr‘𝑅)‘𝑥)(.r‘𝑅)𝑥) = (1r‘𝑅)) |
14 | 13 | adantr 276 |
. . . . . . . . 9
⊢ (((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) → (((invr‘𝑅)‘𝑥)(.r‘𝑅)𝑥) = (1r‘𝑅)) |
15 | 14 | oveq1d 5925 |
. . . . . . . 8
⊢ (((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) → ((((invr‘𝑅)‘𝑥)(.r‘𝑅)𝑥)(.r‘𝑅)𝑦) = ((1r‘𝑅)(.r‘𝑅)𝑦)) |
16 | | simpll 527 |
. . . . . . . . 9
⊢ (((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) → 𝑅 ∈ Ring) |
17 | 3, 10, 1 | ringinvcl 13605 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) → ((invr‘𝑅)‘𝑥) ∈ (Base‘𝑅)) |
18 | 17 | adantr 276 |
. . . . . . . . 9
⊢ (((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) → ((invr‘𝑅)‘𝑥) ∈ (Base‘𝑅)) |
19 | 8 | adantr 276 |
. . . . . . . . 9
⊢ (((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) → 𝑥 ∈ (Base‘𝑅)) |
20 | | simpr 110 |
. . . . . . . . 9
⊢ (((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) → 𝑦 ∈ (Base‘𝑅)) |
21 | 1, 11 | ringass 13496 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Ring ∧
(((invr‘𝑅)‘𝑥) ∈ (Base‘𝑅) ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅))) → ((((invr‘𝑅)‘𝑥)(.r‘𝑅)𝑥)(.r‘𝑅)𝑦) = (((invr‘𝑅)‘𝑥)(.r‘𝑅)(𝑥(.r‘𝑅)𝑦))) |
22 | 16, 18, 19, 20, 21 | syl13anc 1251 |
. . . . . . . 8
⊢ (((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) → ((((invr‘𝑅)‘𝑥)(.r‘𝑅)𝑥)(.r‘𝑅)𝑦) = (((invr‘𝑅)‘𝑥)(.r‘𝑅)(𝑥(.r‘𝑅)𝑦))) |
23 | 1, 11, 12 | ringlidm 13503 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Ring ∧ 𝑦 ∈ (Base‘𝑅)) →
((1r‘𝑅)(.r‘𝑅)𝑦) = 𝑦) |
24 | 23 | adantlr 477 |
. . . . . . . 8
⊢ (((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) → ((1r‘𝑅)(.r‘𝑅)𝑦) = 𝑦) |
25 | 15, 22, 24 | 3eqtr3d 2234 |
. . . . . . 7
⊢ (((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) → (((invr‘𝑅)‘𝑥)(.r‘𝑅)(𝑥(.r‘𝑅)𝑦)) = 𝑦) |
26 | | eqid 2193 |
. . . . . . . . 9
⊢
(0g‘𝑅) = (0g‘𝑅) |
27 | 1, 11, 26 | ringrz 13524 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧
((invr‘𝑅)‘𝑥) ∈ (Base‘𝑅)) → (((invr‘𝑅)‘𝑥)(.r‘𝑅)(0g‘𝑅)) = (0g‘𝑅)) |
28 | 16, 18, 27 | syl2anc 411 |
. . . . . . 7
⊢ (((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) → (((invr‘𝑅)‘𝑥)(.r‘𝑅)(0g‘𝑅)) = (0g‘𝑅)) |
29 | 25, 28 | eqeq12d 2208 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) → ((((invr‘𝑅)‘𝑥)(.r‘𝑅)(𝑥(.r‘𝑅)𝑦)) = (((invr‘𝑅)‘𝑥)(.r‘𝑅)(0g‘𝑅)) ↔ 𝑦 = (0g‘𝑅))) |
30 | 9, 29 | imbitrid 154 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) → ((𝑥(.r‘𝑅)𝑦) = (0g‘𝑅) → 𝑦 = (0g‘𝑅))) |
31 | 30 | ralrimiva 2567 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) → ∀𝑦 ∈ (Base‘𝑅)((𝑥(.r‘𝑅)𝑦) = (0g‘𝑅) → 𝑦 = (0g‘𝑅))) |
32 | | unitrrg.e |
. . . . 5
⊢ 𝐸 = (RLReg‘𝑅) |
33 | 32, 1, 11, 26 | isrrg 13743 |
. . . 4
⊢ (𝑥 ∈ 𝐸 ↔ (𝑥 ∈ (Base‘𝑅) ∧ ∀𝑦 ∈ (Base‘𝑅)((𝑥(.r‘𝑅)𝑦) = (0g‘𝑅) → 𝑦 = (0g‘𝑅)))) |
34 | 8, 31, 33 | sylanbrc 417 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) → 𝑥 ∈ 𝐸) |
35 | 34 | ex 115 |
. 2
⊢ (𝑅 ∈ Ring → (𝑥 ∈ 𝑈 → 𝑥 ∈ 𝐸)) |
36 | 35 | ssrdv 3185 |
1
⊢ (𝑅 ∈ Ring → 𝑈 ⊆ 𝐸) |