Proof of Theorem subrginv
Step | Hyp | Ref
| Expression |
1 | | subrgrcl 18608 |
. . . . 5
⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝑅 ∈ Ring) |
2 | 1 | adantr 480 |
. . . 4
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝑈) → 𝑅 ∈ Ring) |
3 | | subrginv.1 |
. . . . . . . 8
⊢ 𝑆 = (𝑅 ↾s 𝐴) |
4 | 3 | subrgbas 18612 |
. . . . . . 7
⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐴 = (Base‘𝑆)) |
5 | | eqid 2610 |
. . . . . . . 8
⊢
(Base‘𝑅) =
(Base‘𝑅) |
6 | 5 | subrgss 18604 |
. . . . . . 7
⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐴 ⊆ (Base‘𝑅)) |
7 | 4, 6 | eqsstr3d 3603 |
. . . . . 6
⊢ (𝐴 ∈ (SubRing‘𝑅) → (Base‘𝑆) ⊆ (Base‘𝑅)) |
8 | 7 | adantr 480 |
. . . . 5
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝑈) → (Base‘𝑆) ⊆ (Base‘𝑅)) |
9 | 3 | subrgring 18606 |
. . . . . 6
⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝑆 ∈ Ring) |
10 | | subrginv.3 |
. . . . . . 7
⊢ 𝑈 = (Unit‘𝑆) |
11 | | subrginv.4 |
. . . . . . 7
⊢ 𝐽 = (invr‘𝑆) |
12 | | eqid 2610 |
. . . . . . 7
⊢
(Base‘𝑆) =
(Base‘𝑆) |
13 | 10, 11, 12 | ringinvcl 18499 |
. . . . . 6
⊢ ((𝑆 ∈ Ring ∧ 𝑋 ∈ 𝑈) → (𝐽‘𝑋) ∈ (Base‘𝑆)) |
14 | 9, 13 | sylan 487 |
. . . . 5
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝑈) → (𝐽‘𝑋) ∈ (Base‘𝑆)) |
15 | 8, 14 | sseldd 3569 |
. . . 4
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝑈) → (𝐽‘𝑋) ∈ (Base‘𝑅)) |
16 | 12, 10 | unitcl 18482 |
. . . . . 6
⊢ (𝑋 ∈ 𝑈 → 𝑋 ∈ (Base‘𝑆)) |
17 | 16 | adantl 481 |
. . . . 5
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝑈) → 𝑋 ∈ (Base‘𝑆)) |
18 | 8, 17 | sseldd 3569 |
. . . 4
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝑈) → 𝑋 ∈ (Base‘𝑅)) |
19 | | eqid 2610 |
. . . . . . 7
⊢
(Unit‘𝑅) =
(Unit‘𝑅) |
20 | 3, 19, 10 | subrguss 18618 |
. . . . . 6
⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝑈 ⊆ (Unit‘𝑅)) |
21 | 20 | sselda 3568 |
. . . . 5
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝑈) → 𝑋 ∈ (Unit‘𝑅)) |
22 | | subrginv.2 |
. . . . . . 7
⊢ 𝐼 = (invr‘𝑅) |
23 | 19, 22, 5 | ringinvcl 18499 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ (Unit‘𝑅)) → (𝐼‘𝑋) ∈ (Base‘𝑅)) |
24 | 1, 23 | sylan 487 |
. . . . 5
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ (Unit‘𝑅)) → (𝐼‘𝑋) ∈ (Base‘𝑅)) |
25 | 21, 24 | syldan 486 |
. . . 4
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝑈) → (𝐼‘𝑋) ∈ (Base‘𝑅)) |
26 | | eqid 2610 |
. . . . 5
⊢
(.r‘𝑅) = (.r‘𝑅) |
27 | 5, 26 | ringass 18387 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ ((𝐽‘𝑋) ∈ (Base‘𝑅) ∧ 𝑋 ∈ (Base‘𝑅) ∧ (𝐼‘𝑋) ∈ (Base‘𝑅))) → (((𝐽‘𝑋)(.r‘𝑅)𝑋)(.r‘𝑅)(𝐼‘𝑋)) = ((𝐽‘𝑋)(.r‘𝑅)(𝑋(.r‘𝑅)(𝐼‘𝑋)))) |
28 | 2, 15, 18, 25, 27 | syl13anc 1320 |
. . 3
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝑈) → (((𝐽‘𝑋)(.r‘𝑅)𝑋)(.r‘𝑅)(𝐼‘𝑋)) = ((𝐽‘𝑋)(.r‘𝑅)(𝑋(.r‘𝑅)(𝐼‘𝑋)))) |
29 | | eqid 2610 |
. . . . . . 7
⊢
(.r‘𝑆) = (.r‘𝑆) |
30 | | eqid 2610 |
. . . . . . 7
⊢
(1r‘𝑆) = (1r‘𝑆) |
31 | 10, 11, 29, 30 | unitlinv 18500 |
. . . . . 6
⊢ ((𝑆 ∈ Ring ∧ 𝑋 ∈ 𝑈) → ((𝐽‘𝑋)(.r‘𝑆)𝑋) = (1r‘𝑆)) |
32 | 9, 31 | sylan 487 |
. . . . 5
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝑈) → ((𝐽‘𝑋)(.r‘𝑆)𝑋) = (1r‘𝑆)) |
33 | 3, 26 | ressmulr 15829 |
. . . . . . 7
⊢ (𝐴 ∈ (SubRing‘𝑅) →
(.r‘𝑅) =
(.r‘𝑆)) |
34 | 33 | adantr 480 |
. . . . . 6
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝑈) → (.r‘𝑅) = (.r‘𝑆)) |
35 | 34 | oveqd 6566 |
. . . . 5
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝑈) → ((𝐽‘𝑋)(.r‘𝑅)𝑋) = ((𝐽‘𝑋)(.r‘𝑆)𝑋)) |
36 | | eqid 2610 |
. . . . . . 7
⊢
(1r‘𝑅) = (1r‘𝑅) |
37 | 3, 36 | subrg1 18613 |
. . . . . 6
⊢ (𝐴 ∈ (SubRing‘𝑅) →
(1r‘𝑅) =
(1r‘𝑆)) |
38 | 37 | adantr 480 |
. . . . 5
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝑈) → (1r‘𝑅) = (1r‘𝑆)) |
39 | 32, 35, 38 | 3eqtr4d 2654 |
. . . 4
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝑈) → ((𝐽‘𝑋)(.r‘𝑅)𝑋) = (1r‘𝑅)) |
40 | 39 | oveq1d 6564 |
. . 3
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝑈) → (((𝐽‘𝑋)(.r‘𝑅)𝑋)(.r‘𝑅)(𝐼‘𝑋)) = ((1r‘𝑅)(.r‘𝑅)(𝐼‘𝑋))) |
41 | 19, 22, 26, 36 | unitrinv 18501 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ (Unit‘𝑅)) → (𝑋(.r‘𝑅)(𝐼‘𝑋)) = (1r‘𝑅)) |
42 | 1, 41 | sylan 487 |
. . . . 5
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ (Unit‘𝑅)) → (𝑋(.r‘𝑅)(𝐼‘𝑋)) = (1r‘𝑅)) |
43 | 21, 42 | syldan 486 |
. . . 4
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝑈) → (𝑋(.r‘𝑅)(𝐼‘𝑋)) = (1r‘𝑅)) |
44 | 43 | oveq2d 6565 |
. . 3
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝑈) → ((𝐽‘𝑋)(.r‘𝑅)(𝑋(.r‘𝑅)(𝐼‘𝑋))) = ((𝐽‘𝑋)(.r‘𝑅)(1r‘𝑅))) |
45 | 28, 40, 44 | 3eqtr3d 2652 |
. 2
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝑈) → ((1r‘𝑅)(.r‘𝑅)(𝐼‘𝑋)) = ((𝐽‘𝑋)(.r‘𝑅)(1r‘𝑅))) |
46 | 5, 26, 36 | ringlidm 18394 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ (𝐼‘𝑋) ∈ (Base‘𝑅)) → ((1r‘𝑅)(.r‘𝑅)(𝐼‘𝑋)) = (𝐼‘𝑋)) |
47 | 2, 25, 46 | syl2anc 691 |
. 2
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝑈) → ((1r‘𝑅)(.r‘𝑅)(𝐼‘𝑋)) = (𝐼‘𝑋)) |
48 | 5, 26, 36 | ringridm 18395 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ (𝐽‘𝑋) ∈ (Base‘𝑅)) → ((𝐽‘𝑋)(.r‘𝑅)(1r‘𝑅)) = (𝐽‘𝑋)) |
49 | 2, 15, 48 | syl2anc 691 |
. 2
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝑈) → ((𝐽‘𝑋)(.r‘𝑅)(1r‘𝑅)) = (𝐽‘𝑋)) |
50 | 45, 47, 49 | 3eqtr3d 2652 |
1
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝑈) → (𝐼‘𝑋) = (𝐽‘𝑋)) |