| Step | Hyp | Ref
| Expression |
| 1 | | simpr 484 |
. . . . . . . 8
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑥 ∈ 𝑉) → 𝑥 ∈ 𝑉) |
| 2 | | subrguss.3 |
. . . . . . . . 9
⊢ 𝑉 = (Unit‘𝑆) |
| 3 | | eqid 2737 |
. . . . . . . . 9
⊢
(1r‘𝑆) = (1r‘𝑆) |
| 4 | | eqid 2737 |
. . . . . . . . 9
⊢
(∥r‘𝑆) = (∥r‘𝑆) |
| 5 | | eqid 2737 |
. . . . . . . . 9
⊢
(oppr‘𝑆) = (oppr‘𝑆) |
| 6 | | eqid 2737 |
. . . . . . . . 9
⊢
(∥r‘(oppr‘𝑆)) =
(∥r‘(oppr‘𝑆)) |
| 7 | 2, 3, 4, 5, 6 | isunit 20373 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝑉 ↔ (𝑥(∥r‘𝑆)(1r‘𝑆) ∧ 𝑥(∥r‘(oppr‘𝑆))(1r‘𝑆))) |
| 8 | 1, 7 | sylib 218 |
. . . . . . 7
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑥 ∈ 𝑉) → (𝑥(∥r‘𝑆)(1r‘𝑆) ∧ 𝑥(∥r‘(oppr‘𝑆))(1r‘𝑆))) |
| 9 | 8 | simpld 494 |
. . . . . 6
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑥 ∈ 𝑉) → 𝑥(∥r‘𝑆)(1r‘𝑆)) |
| 10 | | subrguss.1 |
. . . . . . . 8
⊢ 𝑆 = (𝑅 ↾s 𝐴) |
| 11 | | eqid 2737 |
. . . . . . . 8
⊢
(1r‘𝑅) = (1r‘𝑅) |
| 12 | 10, 11 | subrg1 20582 |
. . . . . . 7
⊢ (𝐴 ∈ (SubRing‘𝑅) →
(1r‘𝑅) =
(1r‘𝑆)) |
| 13 | 12 | adantr 480 |
. . . . . 6
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑥 ∈ 𝑉) → (1r‘𝑅) = (1r‘𝑆)) |
| 14 | 9, 13 | breqtrrd 5171 |
. . . . 5
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑥 ∈ 𝑉) → 𝑥(∥r‘𝑆)(1r‘𝑅)) |
| 15 | | eqid 2737 |
. . . . . . . 8
⊢
(∥r‘𝑅) = (∥r‘𝑅) |
| 16 | 10, 15, 4 | subrgdvds 20586 |
. . . . . . 7
⊢ (𝐴 ∈ (SubRing‘𝑅) →
(∥r‘𝑆) ⊆ (∥r‘𝑅)) |
| 17 | 16 | adantr 480 |
. . . . . 6
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑥 ∈ 𝑉) → (∥r‘𝑆) ⊆
(∥r‘𝑅)) |
| 18 | 17 | ssbrd 5186 |
. . . . 5
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑥 ∈ 𝑉) → (𝑥(∥r‘𝑆)(1r‘𝑅) → 𝑥(∥r‘𝑅)(1r‘𝑅))) |
| 19 | 14, 18 | mpd 15 |
. . . 4
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑥 ∈ 𝑉) → 𝑥(∥r‘𝑅)(1r‘𝑅)) |
| 20 | 10 | subrgbas 20581 |
. . . . . . . . 9
⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐴 = (Base‘𝑆)) |
| 21 | 20 | adantr 480 |
. . . . . . . 8
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑥 ∈ 𝑉) → 𝐴 = (Base‘𝑆)) |
| 22 | | eqid 2737 |
. . . . . . . . . 10
⊢
(Base‘𝑅) =
(Base‘𝑅) |
| 23 | 22 | subrgss 20572 |
. . . . . . . . 9
⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐴 ⊆ (Base‘𝑅)) |
| 24 | 23 | adantr 480 |
. . . . . . . 8
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑥 ∈ 𝑉) → 𝐴 ⊆ (Base‘𝑅)) |
| 25 | 21, 24 | eqsstrrd 4019 |
. . . . . . 7
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑥 ∈ 𝑉) → (Base‘𝑆) ⊆ (Base‘𝑅)) |
| 26 | | eqid 2737 |
. . . . . . . . 9
⊢
(Base‘𝑆) =
(Base‘𝑆) |
| 27 | 26, 2 | unitcl 20375 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝑉 → 𝑥 ∈ (Base‘𝑆)) |
| 28 | 27 | adantl 481 |
. . . . . . 7
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑥 ∈ 𝑉) → 𝑥 ∈ (Base‘𝑆)) |
| 29 | 25, 28 | sseldd 3984 |
. . . . . 6
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑥 ∈ 𝑉) → 𝑥 ∈ (Base‘𝑅)) |
| 30 | 10 | subrgring 20574 |
. . . . . . . 8
⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝑆 ∈ Ring) |
| 31 | | eqid 2737 |
. . . . . . . . 9
⊢
(invr‘𝑆) = (invr‘𝑆) |
| 32 | 2, 31, 26 | ringinvcl 20392 |
. . . . . . . 8
⊢ ((𝑆 ∈ Ring ∧ 𝑥 ∈ 𝑉) → ((invr‘𝑆)‘𝑥) ∈ (Base‘𝑆)) |
| 33 | 30, 32 | sylan 580 |
. . . . . . 7
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑥 ∈ 𝑉) → ((invr‘𝑆)‘𝑥) ∈ (Base‘𝑆)) |
| 34 | 25, 33 | sseldd 3984 |
. . . . . 6
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑥 ∈ 𝑉) → ((invr‘𝑆)‘𝑥) ∈ (Base‘𝑅)) |
| 35 | | eqid 2737 |
. . . . . . . 8
⊢
(oppr‘𝑅) = (oppr‘𝑅) |
| 36 | 35, 22 | opprbas 20341 |
. . . . . . 7
⊢
(Base‘𝑅) =
(Base‘(oppr‘𝑅)) |
| 37 | | eqid 2737 |
. . . . . . 7
⊢
(∥r‘(oppr‘𝑅)) =
(∥r‘(oppr‘𝑅)) |
| 38 | | eqid 2737 |
. . . . . . 7
⊢
(.r‘(oppr‘𝑅)) =
(.r‘(oppr‘𝑅)) |
| 39 | 36, 37, 38 | dvdsrmul 20364 |
. . . . . 6
⊢ ((𝑥 ∈ (Base‘𝑅) ∧
((invr‘𝑆)‘𝑥) ∈ (Base‘𝑅)) → 𝑥(∥r‘(oppr‘𝑅))(((invr‘𝑆)‘𝑥)(.r‘(oppr‘𝑅))𝑥)) |
| 40 | 29, 34, 39 | syl2anc 584 |
. . . . 5
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑥 ∈ 𝑉) → 𝑥(∥r‘(oppr‘𝑅))(((invr‘𝑆)‘𝑥)(.r‘(oppr‘𝑅))𝑥)) |
| 41 | | eqid 2737 |
. . . . . . 7
⊢
(.r‘𝑅) = (.r‘𝑅) |
| 42 | 22, 41, 35, 38 | opprmul 20337 |
. . . . . 6
⊢
(((invr‘𝑆)‘𝑥)(.r‘(oppr‘𝑅))𝑥) = (𝑥(.r‘𝑅)((invr‘𝑆)‘𝑥)) |
| 43 | | eqid 2737 |
. . . . . . . . 9
⊢
(.r‘𝑆) = (.r‘𝑆) |
| 44 | 2, 31, 43, 3 | unitrinv 20394 |
. . . . . . . 8
⊢ ((𝑆 ∈ Ring ∧ 𝑥 ∈ 𝑉) → (𝑥(.r‘𝑆)((invr‘𝑆)‘𝑥)) = (1r‘𝑆)) |
| 45 | 30, 44 | sylan 580 |
. . . . . . 7
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑥 ∈ 𝑉) → (𝑥(.r‘𝑆)((invr‘𝑆)‘𝑥)) = (1r‘𝑆)) |
| 46 | 10, 41 | ressmulr 17351 |
. . . . . . . . 9
⊢ (𝐴 ∈ (SubRing‘𝑅) →
(.r‘𝑅) =
(.r‘𝑆)) |
| 47 | 46 | adantr 480 |
. . . . . . . 8
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑥 ∈ 𝑉) → (.r‘𝑅) = (.r‘𝑆)) |
| 48 | 47 | oveqd 7448 |
. . . . . . 7
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑥 ∈ 𝑉) → (𝑥(.r‘𝑅)((invr‘𝑆)‘𝑥)) = (𝑥(.r‘𝑆)((invr‘𝑆)‘𝑥))) |
| 49 | 45, 48, 13 | 3eqtr4d 2787 |
. . . . . 6
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑥 ∈ 𝑉) → (𝑥(.r‘𝑅)((invr‘𝑆)‘𝑥)) = (1r‘𝑅)) |
| 50 | 42, 49 | eqtrid 2789 |
. . . . 5
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑥 ∈ 𝑉) → (((invr‘𝑆)‘𝑥)(.r‘(oppr‘𝑅))𝑥) = (1r‘𝑅)) |
| 51 | 40, 50 | breqtrd 5169 |
. . . 4
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑥 ∈ 𝑉) → 𝑥(∥r‘(oppr‘𝑅))(1r‘𝑅)) |
| 52 | | subrguss.2 |
. . . . 5
⊢ 𝑈 = (Unit‘𝑅) |
| 53 | 52, 11, 15, 35, 37 | isunit 20373 |
. . . 4
⊢ (𝑥 ∈ 𝑈 ↔ (𝑥(∥r‘𝑅)(1r‘𝑅) ∧ 𝑥(∥r‘(oppr‘𝑅))(1r‘𝑅))) |
| 54 | 19, 51, 53 | sylanbrc 583 |
. . 3
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑥 ∈ 𝑉) → 𝑥 ∈ 𝑈) |
| 55 | 54 | ex 412 |
. 2
⊢ (𝐴 ∈ (SubRing‘𝑅) → (𝑥 ∈ 𝑉 → 𝑥 ∈ 𝑈)) |
| 56 | 55 | ssrdv 3989 |
1
⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝑉 ⊆ 𝑈) |