Proof of Theorem subrginv
| Step | Hyp | Ref
| Expression |
| 1 | | subrgrcl 20576 |
. . . . 5
⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝑅 ∈ Ring) |
| 2 | 1 | adantr 480 |
. . . 4
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝑈) → 𝑅 ∈ Ring) |
| 3 | | subrginv.1 |
. . . . . . . 8
⊢ 𝑆 = (𝑅 ↾s 𝐴) |
| 4 | 3 | subrgbas 20581 |
. . . . . . 7
⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐴 = (Base‘𝑆)) |
| 5 | | eqid 2737 |
. . . . . . . 8
⊢
(Base‘𝑅) =
(Base‘𝑅) |
| 6 | 5 | subrgss 20572 |
. . . . . . 7
⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐴 ⊆ (Base‘𝑅)) |
| 7 | 4, 6 | eqsstrrd 4019 |
. . . . . 6
⊢ (𝐴 ∈ (SubRing‘𝑅) → (Base‘𝑆) ⊆ (Base‘𝑅)) |
| 8 | 7 | adantr 480 |
. . . . 5
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝑈) → (Base‘𝑆) ⊆ (Base‘𝑅)) |
| 9 | 3 | subrgring 20574 |
. . . . . 6
⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝑆 ∈ Ring) |
| 10 | | subrginv.3 |
. . . . . . 7
⊢ 𝑈 = (Unit‘𝑆) |
| 11 | | subrginv.4 |
. . . . . . 7
⊢ 𝐽 = (invr‘𝑆) |
| 12 | | eqid 2737 |
. . . . . . 7
⊢
(Base‘𝑆) =
(Base‘𝑆) |
| 13 | 10, 11, 12 | ringinvcl 20392 |
. . . . . 6
⊢ ((𝑆 ∈ Ring ∧ 𝑋 ∈ 𝑈) → (𝐽‘𝑋) ∈ (Base‘𝑆)) |
| 14 | 9, 13 | sylan 580 |
. . . . 5
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝑈) → (𝐽‘𝑋) ∈ (Base‘𝑆)) |
| 15 | 8, 14 | sseldd 3984 |
. . . 4
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝑈) → (𝐽‘𝑋) ∈ (Base‘𝑅)) |
| 16 | 12, 10 | unitcl 20375 |
. . . . . 6
⊢ (𝑋 ∈ 𝑈 → 𝑋 ∈ (Base‘𝑆)) |
| 17 | 16 | adantl 481 |
. . . . 5
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝑈) → 𝑋 ∈ (Base‘𝑆)) |
| 18 | 8, 17 | sseldd 3984 |
. . . 4
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝑈) → 𝑋 ∈ (Base‘𝑅)) |
| 19 | | eqid 2737 |
. . . . . . 7
⊢
(Unit‘𝑅) =
(Unit‘𝑅) |
| 20 | 3, 19, 10 | subrguss 20587 |
. . . . . 6
⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝑈 ⊆ (Unit‘𝑅)) |
| 21 | 20 | sselda 3983 |
. . . . 5
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝑈) → 𝑋 ∈ (Unit‘𝑅)) |
| 22 | | subrginv.2 |
. . . . . 6
⊢ 𝐼 = (invr‘𝑅) |
| 23 | 19, 22, 5 | ringinvcl 20392 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ (Unit‘𝑅)) → (𝐼‘𝑋) ∈ (Base‘𝑅)) |
| 24 | 1, 21, 23 | syl2an2r 685 |
. . . 4
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝑈) → (𝐼‘𝑋) ∈ (Base‘𝑅)) |
| 25 | | eqid 2737 |
. . . . 5
⊢
(.r‘𝑅) = (.r‘𝑅) |
| 26 | 5, 25 | ringass 20250 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ ((𝐽‘𝑋) ∈ (Base‘𝑅) ∧ 𝑋 ∈ (Base‘𝑅) ∧ (𝐼‘𝑋) ∈ (Base‘𝑅))) → (((𝐽‘𝑋)(.r‘𝑅)𝑋)(.r‘𝑅)(𝐼‘𝑋)) = ((𝐽‘𝑋)(.r‘𝑅)(𝑋(.r‘𝑅)(𝐼‘𝑋)))) |
| 27 | 2, 15, 18, 24, 26 | syl13anc 1374 |
. . 3
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝑈) → (((𝐽‘𝑋)(.r‘𝑅)𝑋)(.r‘𝑅)(𝐼‘𝑋)) = ((𝐽‘𝑋)(.r‘𝑅)(𝑋(.r‘𝑅)(𝐼‘𝑋)))) |
| 28 | | eqid 2737 |
. . . . . . 7
⊢
(.r‘𝑆) = (.r‘𝑆) |
| 29 | | eqid 2737 |
. . . . . . 7
⊢
(1r‘𝑆) = (1r‘𝑆) |
| 30 | 10, 11, 28, 29 | unitlinv 20393 |
. . . . . 6
⊢ ((𝑆 ∈ Ring ∧ 𝑋 ∈ 𝑈) → ((𝐽‘𝑋)(.r‘𝑆)𝑋) = (1r‘𝑆)) |
| 31 | 9, 30 | sylan 580 |
. . . . 5
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝑈) → ((𝐽‘𝑋)(.r‘𝑆)𝑋) = (1r‘𝑆)) |
| 32 | 3, 25 | ressmulr 17351 |
. . . . . . 7
⊢ (𝐴 ∈ (SubRing‘𝑅) →
(.r‘𝑅) =
(.r‘𝑆)) |
| 33 | 32 | adantr 480 |
. . . . . 6
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝑈) → (.r‘𝑅) = (.r‘𝑆)) |
| 34 | 33 | oveqd 7448 |
. . . . 5
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝑈) → ((𝐽‘𝑋)(.r‘𝑅)𝑋) = ((𝐽‘𝑋)(.r‘𝑆)𝑋)) |
| 35 | | eqid 2737 |
. . . . . . 7
⊢
(1r‘𝑅) = (1r‘𝑅) |
| 36 | 3, 35 | subrg1 20582 |
. . . . . 6
⊢ (𝐴 ∈ (SubRing‘𝑅) →
(1r‘𝑅) =
(1r‘𝑆)) |
| 37 | 36 | adantr 480 |
. . . . 5
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝑈) → (1r‘𝑅) = (1r‘𝑆)) |
| 38 | 31, 34, 37 | 3eqtr4d 2787 |
. . . 4
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝑈) → ((𝐽‘𝑋)(.r‘𝑅)𝑋) = (1r‘𝑅)) |
| 39 | 38 | oveq1d 7446 |
. . 3
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝑈) → (((𝐽‘𝑋)(.r‘𝑅)𝑋)(.r‘𝑅)(𝐼‘𝑋)) = ((1r‘𝑅)(.r‘𝑅)(𝐼‘𝑋))) |
| 40 | 19, 22, 25, 35 | unitrinv 20394 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ (Unit‘𝑅)) → (𝑋(.r‘𝑅)(𝐼‘𝑋)) = (1r‘𝑅)) |
| 41 | 1, 21, 40 | syl2an2r 685 |
. . . 4
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝑈) → (𝑋(.r‘𝑅)(𝐼‘𝑋)) = (1r‘𝑅)) |
| 42 | 41 | oveq2d 7447 |
. . 3
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝑈) → ((𝐽‘𝑋)(.r‘𝑅)(𝑋(.r‘𝑅)(𝐼‘𝑋))) = ((𝐽‘𝑋)(.r‘𝑅)(1r‘𝑅))) |
| 43 | 27, 39, 42 | 3eqtr3d 2785 |
. 2
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝑈) → ((1r‘𝑅)(.r‘𝑅)(𝐼‘𝑋)) = ((𝐽‘𝑋)(.r‘𝑅)(1r‘𝑅))) |
| 44 | 5, 25, 35 | ringlidm 20266 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ (𝐼‘𝑋) ∈ (Base‘𝑅)) → ((1r‘𝑅)(.r‘𝑅)(𝐼‘𝑋)) = (𝐼‘𝑋)) |
| 45 | 1, 24, 44 | syl2an2r 685 |
. 2
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝑈) → ((1r‘𝑅)(.r‘𝑅)(𝐼‘𝑋)) = (𝐼‘𝑋)) |
| 46 | 5, 25, 35 | ringridm 20267 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ (𝐽‘𝑋) ∈ (Base‘𝑅)) → ((𝐽‘𝑋)(.r‘𝑅)(1r‘𝑅)) = (𝐽‘𝑋)) |
| 47 | 1, 15, 46 | syl2an2r 685 |
. 2
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝑈) → ((𝐽‘𝑋)(.r‘𝑅)(1r‘𝑅)) = (𝐽‘𝑋)) |
| 48 | 43, 45, 47 | 3eqtr3d 2785 |
1
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝑈) → (𝐼‘𝑋) = (𝐽‘𝑋)) |