Proof of Theorem elrhmunit
Step | Hyp | Ref
| Expression |
1 | | simpl 486 |
. . . 4
⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐴 ∈ (Unit‘𝑅)) → 𝐹 ∈ (𝑅 RingHom 𝑆)) |
2 | | eqid 2738 |
. . . . . 6
⊢
(Base‘𝑅) =
(Base‘𝑅) |
3 | | eqid 2738 |
. . . . . 6
⊢
(Unit‘𝑅) =
(Unit‘𝑅) |
4 | 2, 3 | unitss 19525 |
. . . . 5
⊢
(Unit‘𝑅)
⊆ (Base‘𝑅) |
5 | | simpr 488 |
. . . . 5
⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐴 ∈ (Unit‘𝑅)) → 𝐴 ∈ (Unit‘𝑅)) |
6 | 4, 5 | sseldi 3873 |
. . . 4
⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐴 ∈ (Unit‘𝑅)) → 𝐴 ∈ (Base‘𝑅)) |
7 | | rhmrcl1 19586 |
. . . . 5
⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝑅 ∈ Ring) |
8 | | eqid 2738 |
. . . . . 6
⊢
(1r‘𝑅) = (1r‘𝑅) |
9 | 2, 8 | ringidcl 19433 |
. . . . 5
⊢ (𝑅 ∈ Ring →
(1r‘𝑅)
∈ (Base‘𝑅)) |
10 | 1, 7, 9 | 3syl 18 |
. . . 4
⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐴 ∈ (Unit‘𝑅)) → (1r‘𝑅) ∈ (Base‘𝑅)) |
11 | | eqid 2738 |
. . . . . . 7
⊢
(∥r‘𝑅) = (∥r‘𝑅) |
12 | | eqid 2738 |
. . . . . . 7
⊢
(oppr‘𝑅) = (oppr‘𝑅) |
13 | | eqid 2738 |
. . . . . . 7
⊢
(∥r‘(oppr‘𝑅)) =
(∥r‘(oppr‘𝑅)) |
14 | 3, 8, 11, 12, 13 | isunit 19522 |
. . . . . 6
⊢ (𝐴 ∈ (Unit‘𝑅) ↔ (𝐴(∥r‘𝑅)(1r‘𝑅) ∧ 𝐴(∥r‘(oppr‘𝑅))(1r‘𝑅))) |
15 | 5, 14 | sylib 221 |
. . . . 5
⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐴 ∈ (Unit‘𝑅)) → (𝐴(∥r‘𝑅)(1r‘𝑅) ∧ 𝐴(∥r‘(oppr‘𝑅))(1r‘𝑅))) |
16 | 15 | simpld 498 |
. . . 4
⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐴 ∈ (Unit‘𝑅)) → 𝐴(∥r‘𝑅)(1r‘𝑅)) |
17 | | eqid 2738 |
. . . . 5
⊢
(∥r‘𝑆) = (∥r‘𝑆) |
18 | 2, 11, 17 | rhmdvdsr 31086 |
. . . 4
⊢ (((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐴 ∈ (Base‘𝑅) ∧ (1r‘𝑅) ∈ (Base‘𝑅)) ∧ 𝐴(∥r‘𝑅)(1r‘𝑅)) → (𝐹‘𝐴)(∥r‘𝑆)(𝐹‘(1r‘𝑅))) |
19 | 1, 6, 10, 16, 18 | syl31anc 1374 |
. . 3
⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐴 ∈ (Unit‘𝑅)) → (𝐹‘𝐴)(∥r‘𝑆)(𝐹‘(1r‘𝑅))) |
20 | | eqid 2738 |
. . . . . 6
⊢
(1r‘𝑆) = (1r‘𝑆) |
21 | 8, 20 | rhm1 19597 |
. . . . 5
⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → (𝐹‘(1r‘𝑅)) = (1r‘𝑆)) |
22 | 21 | breq2d 5039 |
. . . 4
⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → ((𝐹‘𝐴)(∥r‘𝑆)(𝐹‘(1r‘𝑅)) ↔ (𝐹‘𝐴)(∥r‘𝑆)(1r‘𝑆))) |
23 | 22 | adantr 484 |
. . 3
⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐴 ∈ (Unit‘𝑅)) → ((𝐹‘𝐴)(∥r‘𝑆)(𝐹‘(1r‘𝑅)) ↔ (𝐹‘𝐴)(∥r‘𝑆)(1r‘𝑆))) |
24 | 19, 23 | mpbid 235 |
. 2
⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐴 ∈ (Unit‘𝑅)) → (𝐹‘𝐴)(∥r‘𝑆)(1r‘𝑆)) |
25 | | rhmopp 31087 |
. . . . 5
⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝐹 ∈ ((oppr‘𝑅) RingHom
(oppr‘𝑆))) |
26 | 25 | adantr 484 |
. . . 4
⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐴 ∈ (Unit‘𝑅)) → 𝐹 ∈ ((oppr‘𝑅) RingHom
(oppr‘𝑆))) |
27 | 15 | simprd 499 |
. . . 4
⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐴 ∈ (Unit‘𝑅)) → 𝐴(∥r‘(oppr‘𝑅))(1r‘𝑅)) |
28 | 12, 2 | opprbas 19494 |
. . . . 5
⊢
(Base‘𝑅) =
(Base‘(oppr‘𝑅)) |
29 | | eqid 2738 |
. . . . 5
⊢
(∥r‘(oppr‘𝑆)) =
(∥r‘(oppr‘𝑆)) |
30 | 28, 13, 29 | rhmdvdsr 31086 |
. . . 4
⊢ (((𝐹 ∈
((oppr‘𝑅) RingHom
(oppr‘𝑆)) ∧ 𝐴 ∈ (Base‘𝑅) ∧ (1r‘𝑅) ∈ (Base‘𝑅)) ∧ 𝐴(∥r‘(oppr‘𝑅))(1r‘𝑅)) → (𝐹‘𝐴)(∥r‘(oppr‘𝑆))(𝐹‘(1r‘𝑅))) |
31 | 26, 6, 10, 27, 30 | syl31anc 1374 |
. . 3
⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐴 ∈ (Unit‘𝑅)) → (𝐹‘𝐴)(∥r‘(oppr‘𝑆))(𝐹‘(1r‘𝑅))) |
32 | 21 | breq2d 5039 |
. . . 4
⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → ((𝐹‘𝐴)(∥r‘(oppr‘𝑆))(𝐹‘(1r‘𝑅)) ↔ (𝐹‘𝐴)(∥r‘(oppr‘𝑆))(1r‘𝑆))) |
33 | 32 | adantr 484 |
. . 3
⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐴 ∈ (Unit‘𝑅)) → ((𝐹‘𝐴)(∥r‘(oppr‘𝑆))(𝐹‘(1r‘𝑅)) ↔ (𝐹‘𝐴)(∥r‘(oppr‘𝑆))(1r‘𝑆))) |
34 | 31, 33 | mpbid 235 |
. 2
⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐴 ∈ (Unit‘𝑅)) → (𝐹‘𝐴)(∥r‘(oppr‘𝑆))(1r‘𝑆)) |
35 | | eqid 2738 |
. . 3
⊢
(Unit‘𝑆) =
(Unit‘𝑆) |
36 | | eqid 2738 |
. . 3
⊢
(oppr‘𝑆) = (oppr‘𝑆) |
37 | 35, 20, 17, 36, 29 | isunit 19522 |
. 2
⊢ ((𝐹‘𝐴) ∈ (Unit‘𝑆) ↔ ((𝐹‘𝐴)(∥r‘𝑆)(1r‘𝑆) ∧ (𝐹‘𝐴)(∥r‘(oppr‘𝑆))(1r‘𝑆))) |
38 | 24, 34, 37 | sylanbrc 586 |
1
⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐴 ∈ (Unit‘𝑅)) → (𝐹‘𝐴) ∈ (Unit‘𝑆)) |