Proof of Theorem subrginv
Step | Hyp | Ref
| Expression |
1 | | subrgrcl 20027 |
. . . . 5
⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝑅 ∈ Ring) |
2 | 1 | adantr 481 |
. . . 4
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝑈) → 𝑅 ∈ Ring) |
3 | | subrginv.1 |
. . . . . . . 8
⊢ 𝑆 = (𝑅 ↾s 𝐴) |
4 | 3 | subrgbas 20031 |
. . . . . . 7
⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐴 = (Base‘𝑆)) |
5 | | eqid 2740 |
. . . . . . . 8
⊢
(Base‘𝑅) =
(Base‘𝑅) |
6 | 5 | subrgss 20023 |
. . . . . . 7
⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐴 ⊆ (Base‘𝑅)) |
7 | 4, 6 | eqsstrrd 3965 |
. . . . . 6
⊢ (𝐴 ∈ (SubRing‘𝑅) → (Base‘𝑆) ⊆ (Base‘𝑅)) |
8 | 7 | adantr 481 |
. . . . 5
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝑈) → (Base‘𝑆) ⊆ (Base‘𝑅)) |
9 | 3 | subrgring 20025 |
. . . . . 6
⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝑆 ∈ Ring) |
10 | | subrginv.3 |
. . . . . . 7
⊢ 𝑈 = (Unit‘𝑆) |
11 | | subrginv.4 |
. . . . . . 7
⊢ 𝐽 = (invr‘𝑆) |
12 | | eqid 2740 |
. . . . . . 7
⊢
(Base‘𝑆) =
(Base‘𝑆) |
13 | 10, 11, 12 | ringinvcl 19916 |
. . . . . 6
⊢ ((𝑆 ∈ Ring ∧ 𝑋 ∈ 𝑈) → (𝐽‘𝑋) ∈ (Base‘𝑆)) |
14 | 9, 13 | sylan 580 |
. . . . 5
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝑈) → (𝐽‘𝑋) ∈ (Base‘𝑆)) |
15 | 8, 14 | sseldd 3927 |
. . . 4
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝑈) → (𝐽‘𝑋) ∈ (Base‘𝑅)) |
16 | 12, 10 | unitcl 19899 |
. . . . . 6
⊢ (𝑋 ∈ 𝑈 → 𝑋 ∈ (Base‘𝑆)) |
17 | 16 | adantl 482 |
. . . . 5
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝑈) → 𝑋 ∈ (Base‘𝑆)) |
18 | 8, 17 | sseldd 3927 |
. . . 4
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝑈) → 𝑋 ∈ (Base‘𝑅)) |
19 | | eqid 2740 |
. . . . . . 7
⊢
(Unit‘𝑅) =
(Unit‘𝑅) |
20 | 3, 19, 10 | subrguss 20037 |
. . . . . 6
⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝑈 ⊆ (Unit‘𝑅)) |
21 | 20 | sselda 3926 |
. . . . 5
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝑈) → 𝑋 ∈ (Unit‘𝑅)) |
22 | | subrginv.2 |
. . . . . 6
⊢ 𝐼 = (invr‘𝑅) |
23 | 19, 22, 5 | ringinvcl 19916 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ (Unit‘𝑅)) → (𝐼‘𝑋) ∈ (Base‘𝑅)) |
24 | 1, 21, 23 | syl2an2r 682 |
. . . 4
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝑈) → (𝐼‘𝑋) ∈ (Base‘𝑅)) |
25 | | eqid 2740 |
. . . . 5
⊢
(.r‘𝑅) = (.r‘𝑅) |
26 | 5, 25 | ringass 19801 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ ((𝐽‘𝑋) ∈ (Base‘𝑅) ∧ 𝑋 ∈ (Base‘𝑅) ∧ (𝐼‘𝑋) ∈ (Base‘𝑅))) → (((𝐽‘𝑋)(.r‘𝑅)𝑋)(.r‘𝑅)(𝐼‘𝑋)) = ((𝐽‘𝑋)(.r‘𝑅)(𝑋(.r‘𝑅)(𝐼‘𝑋)))) |
27 | 2, 15, 18, 24, 26 | syl13anc 1371 |
. . 3
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝑈) → (((𝐽‘𝑋)(.r‘𝑅)𝑋)(.r‘𝑅)(𝐼‘𝑋)) = ((𝐽‘𝑋)(.r‘𝑅)(𝑋(.r‘𝑅)(𝐼‘𝑋)))) |
28 | | eqid 2740 |
. . . . . . 7
⊢
(.r‘𝑆) = (.r‘𝑆) |
29 | | eqid 2740 |
. . . . . . 7
⊢
(1r‘𝑆) = (1r‘𝑆) |
30 | 10, 11, 28, 29 | unitlinv 19917 |
. . . . . 6
⊢ ((𝑆 ∈ Ring ∧ 𝑋 ∈ 𝑈) → ((𝐽‘𝑋)(.r‘𝑆)𝑋) = (1r‘𝑆)) |
31 | 9, 30 | sylan 580 |
. . . . 5
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝑈) → ((𝐽‘𝑋)(.r‘𝑆)𝑋) = (1r‘𝑆)) |
32 | 3, 25 | ressmulr 17015 |
. . . . . . 7
⊢ (𝐴 ∈ (SubRing‘𝑅) →
(.r‘𝑅) =
(.r‘𝑆)) |
33 | 32 | adantr 481 |
. . . . . 6
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝑈) → (.r‘𝑅) = (.r‘𝑆)) |
34 | 33 | oveqd 7288 |
. . . . 5
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝑈) → ((𝐽‘𝑋)(.r‘𝑅)𝑋) = ((𝐽‘𝑋)(.r‘𝑆)𝑋)) |
35 | | eqid 2740 |
. . . . . . 7
⊢
(1r‘𝑅) = (1r‘𝑅) |
36 | 3, 35 | subrg1 20032 |
. . . . . 6
⊢ (𝐴 ∈ (SubRing‘𝑅) →
(1r‘𝑅) =
(1r‘𝑆)) |
37 | 36 | adantr 481 |
. . . . 5
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝑈) → (1r‘𝑅) = (1r‘𝑆)) |
38 | 31, 34, 37 | 3eqtr4d 2790 |
. . . 4
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝑈) → ((𝐽‘𝑋)(.r‘𝑅)𝑋) = (1r‘𝑅)) |
39 | 38 | oveq1d 7286 |
. . 3
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝑈) → (((𝐽‘𝑋)(.r‘𝑅)𝑋)(.r‘𝑅)(𝐼‘𝑋)) = ((1r‘𝑅)(.r‘𝑅)(𝐼‘𝑋))) |
40 | 19, 22, 25, 35 | unitrinv 19918 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ (Unit‘𝑅)) → (𝑋(.r‘𝑅)(𝐼‘𝑋)) = (1r‘𝑅)) |
41 | 1, 21, 40 | syl2an2r 682 |
. . . 4
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝑈) → (𝑋(.r‘𝑅)(𝐼‘𝑋)) = (1r‘𝑅)) |
42 | 41 | oveq2d 7287 |
. . 3
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝑈) → ((𝐽‘𝑋)(.r‘𝑅)(𝑋(.r‘𝑅)(𝐼‘𝑋))) = ((𝐽‘𝑋)(.r‘𝑅)(1r‘𝑅))) |
43 | 27, 39, 42 | 3eqtr3d 2788 |
. 2
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝑈) → ((1r‘𝑅)(.r‘𝑅)(𝐼‘𝑋)) = ((𝐽‘𝑋)(.r‘𝑅)(1r‘𝑅))) |
44 | 5, 25, 35 | ringlidm 19808 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ (𝐼‘𝑋) ∈ (Base‘𝑅)) → ((1r‘𝑅)(.r‘𝑅)(𝐼‘𝑋)) = (𝐼‘𝑋)) |
45 | 1, 24, 44 | syl2an2r 682 |
. 2
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝑈) → ((1r‘𝑅)(.r‘𝑅)(𝐼‘𝑋)) = (𝐼‘𝑋)) |
46 | 5, 25, 35 | ringridm 19809 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ (𝐽‘𝑋) ∈ (Base‘𝑅)) → ((𝐽‘𝑋)(.r‘𝑅)(1r‘𝑅)) = (𝐽‘𝑋)) |
47 | 1, 15, 46 | syl2an2r 682 |
. 2
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝑈) → ((𝐽‘𝑋)(.r‘𝑅)(1r‘𝑅)) = (𝐽‘𝑋)) |
48 | 43, 45, 47 | 3eqtr3d 2788 |
1
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝑈) → (𝐼‘𝑋) = (𝐽‘𝑋)) |