Proof of Theorem subrgdv
Step | Hyp | Ref
| Expression |
1 | | subrgdv.1 |
. . . . . 6
⊢ 𝑆 = (𝑅 ↾s 𝐴) |
2 | | eqid 2177 |
. . . . . 6
⊢
(invr‘𝑅) = (invr‘𝑅) |
3 | | subrgdv.3 |
. . . . . 6
⊢ 𝑈 = (Unit‘𝑆) |
4 | | eqid 2177 |
. . . . . 6
⊢
(invr‘𝑆) = (invr‘𝑆) |
5 | 1, 2, 3, 4 | subrginv 13296 |
. . . . 5
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑌 ∈ 𝑈) → ((invr‘𝑅)‘𝑌) = ((invr‘𝑆)‘𝑌)) |
6 | 5 | 3adant2 1016 |
. . . 4
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝑈) → ((invr‘𝑅)‘𝑌) = ((invr‘𝑆)‘𝑌)) |
7 | 6 | oveq2d 5888 |
. . 3
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝑈) → (𝑋(.r‘𝑅)((invr‘𝑅)‘𝑌)) = (𝑋(.r‘𝑅)((invr‘𝑆)‘𝑌))) |
8 | | subrgrcl 13285 |
. . . . . 6
⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝑅 ∈ Ring) |
9 | | eqid 2177 |
. . . . . . 7
⊢
(.r‘𝑅) = (.r‘𝑅) |
10 | 1, 9 | ressmulrg 12595 |
. . . . . 6
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑅 ∈ Ring) →
(.r‘𝑅) =
(.r‘𝑆)) |
11 | 8, 10 | mpdan 421 |
. . . . 5
⊢ (𝐴 ∈ (SubRing‘𝑅) →
(.r‘𝑅) =
(.r‘𝑆)) |
12 | 11 | 3ad2ant1 1018 |
. . . 4
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝑈) → (.r‘𝑅) = (.r‘𝑆)) |
13 | 12 | oveqd 5889 |
. . 3
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝑈) → (𝑋(.r‘𝑅)((invr‘𝑆)‘𝑌)) = (𝑋(.r‘𝑆)((invr‘𝑆)‘𝑌))) |
14 | 7, 13 | eqtrd 2210 |
. 2
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝑈) → (𝑋(.r‘𝑅)((invr‘𝑅)‘𝑌)) = (𝑋(.r‘𝑆)((invr‘𝑆)‘𝑌))) |
15 | | eqidd 2178 |
. . 3
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝑈) → (Base‘𝑅) = (Base‘𝑅)) |
16 | | eqidd 2178 |
. . 3
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝑈) → (.r‘𝑅) = (.r‘𝑅)) |
17 | | eqidd 2178 |
. . 3
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝑈) → (Unit‘𝑅) = (Unit‘𝑅)) |
18 | | eqidd 2178 |
. . 3
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝑈) → (invr‘𝑅) = (invr‘𝑅)) |
19 | | subrgdv.2 |
. . . 4
⊢ / =
(/r‘𝑅) |
20 | 19 | a1i 9 |
. . 3
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝑈) → / =
(/r‘𝑅)) |
21 | 8 | 3ad2ant1 1018 |
. . 3
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝑈) → 𝑅 ∈ Ring) |
22 | | eqid 2177 |
. . . . . 6
⊢
(Base‘𝑅) =
(Base‘𝑅) |
23 | 22 | subrgss 13281 |
. . . . 5
⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐴 ⊆ (Base‘𝑅)) |
24 | 23 | 3ad2ant1 1018 |
. . . 4
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝑈) → 𝐴 ⊆ (Base‘𝑅)) |
25 | | simp2 998 |
. . . 4
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝑈) → 𝑋 ∈ 𝐴) |
26 | 24, 25 | sseldd 3156 |
. . 3
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝑈) → 𝑋 ∈ (Base‘𝑅)) |
27 | | eqid 2177 |
. . . . . 6
⊢
(Unit‘𝑅) =
(Unit‘𝑅) |
28 | 1, 27, 3 | subrguss 13295 |
. . . . 5
⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝑈 ⊆ (Unit‘𝑅)) |
29 | 28 | 3ad2ant1 1018 |
. . . 4
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝑈) → 𝑈 ⊆ (Unit‘𝑅)) |
30 | | simp3 999 |
. . . 4
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝑈) → 𝑌 ∈ 𝑈) |
31 | 29, 30 | sseldd 3156 |
. . 3
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝑈) → 𝑌 ∈ (Unit‘𝑅)) |
32 | 15, 16, 17, 18, 20, 21, 26, 31 | dvrvald 13234 |
. 2
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝑈) → (𝑋 / 𝑌) = (𝑋(.r‘𝑅)((invr‘𝑅)‘𝑌))) |
33 | | eqidd 2178 |
. . 3
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝑈) → (Base‘𝑆) = (Base‘𝑆)) |
34 | | eqidd 2178 |
. . 3
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝑈) → (.r‘𝑆) = (.r‘𝑆)) |
35 | 3 | a1i 9 |
. . 3
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝑈) → 𝑈 = (Unit‘𝑆)) |
36 | | eqidd 2178 |
. . 3
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝑈) → (invr‘𝑆) = (invr‘𝑆)) |
37 | | subrgdv.4 |
. . . 4
⊢ 𝐸 = (/r‘𝑆) |
38 | 37 | a1i 9 |
. . 3
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝑈) → 𝐸 = (/r‘𝑆)) |
39 | 1 | subrgring 13283 |
. . . 4
⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝑆 ∈ Ring) |
40 | 39 | 3ad2ant1 1018 |
. . 3
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝑈) → 𝑆 ∈ Ring) |
41 | 1 | subrgbas 13289 |
. . . . 5
⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐴 = (Base‘𝑆)) |
42 | 41 | 3ad2ant1 1018 |
. . . 4
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝑈) → 𝐴 = (Base‘𝑆)) |
43 | 25, 42 | eleqtrd 2256 |
. . 3
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝑈) → 𝑋 ∈ (Base‘𝑆)) |
44 | 33, 34, 35, 36, 38, 40, 43, 30 | dvrvald 13234 |
. 2
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝑈) → (𝑋𝐸𝑌) = (𝑋(.r‘𝑆)((invr‘𝑆)‘𝑌))) |
45 | 14, 32, 44 | 3eqtr4d 2220 |
1
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝑈) → (𝑋 / 𝑌) = (𝑋𝐸𝑌)) |