Step | Hyp | Ref
| Expression |
1 | | eqid 2759 |
. . . . . 6
⊢
(Base‘𝑅) =
(Base‘𝑅) |
2 | | rhmimaidl.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝑆) |
3 | 1, 2 | rhmf 19534 |
. . . . 5
⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝐹:(Base‘𝑅)⟶𝐵) |
4 | | fimass 6533 |
. . . . 5
⊢ (𝐹:(Base‘𝑅)⟶𝐵 → (𝐹 “ 𝐼) ⊆ 𝐵) |
5 | 3, 4 | syl 17 |
. . . 4
⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → (𝐹 “ 𝐼) ⊆ 𝐵) |
6 | 5 | ad2antrr 726 |
. . 3
⊢ (((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ ran 𝐹 = 𝐵) ∧ 𝐼 ∈ 𝑇) → (𝐹 “ 𝐼) ⊆ 𝐵) |
7 | 3 | ffnd 6492 |
. . . . . 6
⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝐹 Fn (Base‘𝑅)) |
8 | 7 | ad2antrr 726 |
. . . . 5
⊢ (((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ ran 𝐹 = 𝐵) ∧ 𝐼 ∈ 𝑇) → 𝐹 Fn (Base‘𝑅)) |
9 | | rhmrcl1 19527 |
. . . . . . 7
⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝑅 ∈ Ring) |
10 | 9 | ad2antrr 726 |
. . . . . 6
⊢ (((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ ran 𝐹 = 𝐵) ∧ 𝐼 ∈ 𝑇) → 𝑅 ∈ Ring) |
11 | | eqid 2759 |
. . . . . . 7
⊢
(0g‘𝑅) = (0g‘𝑅) |
12 | 1, 11 | ring0cl 19375 |
. . . . . 6
⊢ (𝑅 ∈ Ring →
(0g‘𝑅)
∈ (Base‘𝑅)) |
13 | 10, 12 | syl 17 |
. . . . 5
⊢ (((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ ran 𝐹 = 𝐵) ∧ 𝐼 ∈ 𝑇) → (0g‘𝑅) ∈ (Base‘𝑅)) |
14 | | simpr 489 |
. . . . . 6
⊢ (((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ ran 𝐹 = 𝐵) ∧ 𝐼 ∈ 𝑇) → 𝐼 ∈ 𝑇) |
15 | | rhmimaidl.t |
. . . . . . 7
⊢ 𝑇 = (LIdeal‘𝑅) |
16 | 15, 11 | lidl0cl 20038 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑇) → (0g‘𝑅) ∈ 𝐼) |
17 | 10, 14, 16 | syl2anc 588 |
. . . . 5
⊢ (((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ ran 𝐹 = 𝐵) ∧ 𝐼 ∈ 𝑇) → (0g‘𝑅) ∈ 𝐼) |
18 | 8, 13, 17 | fnfvimad 6981 |
. . . 4
⊢ (((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ ran 𝐹 = 𝐵) ∧ 𝐼 ∈ 𝑇) → (𝐹‘(0g‘𝑅)) ∈ (𝐹 “ 𝐼)) |
19 | 18 | ne0d 4230 |
. . 3
⊢ (((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ ran 𝐹 = 𝐵) ∧ 𝐼 ∈ 𝑇) → (𝐹 “ 𝐼) ≠ ∅) |
20 | | rhmghm 19533 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝐹 ∈ (𝑅 GrpHom 𝑆)) |
21 | 20 | ad4antr 732 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐼 ∈ 𝑇) ∧ 𝑗 ∈ 𝐼) ∧ 𝑖 ∈ 𝐼) ∧ 𝑧 ∈ (Base‘𝑅)) → 𝐹 ∈ (𝑅 GrpHom 𝑆)) |
22 | 9 | ad4antr 732 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐼 ∈ 𝑇) ∧ 𝑗 ∈ 𝐼) ∧ 𝑖 ∈ 𝐼) ∧ 𝑧 ∈ (Base‘𝑅)) → 𝑅 ∈ Ring) |
23 | | simpr 489 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐼 ∈ 𝑇) ∧ 𝑗 ∈ 𝐼) ∧ 𝑖 ∈ 𝐼) ∧ 𝑧 ∈ (Base‘𝑅)) → 𝑧 ∈ (Base‘𝑅)) |
24 | 1, 15 | lidlss 20036 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐼 ∈ 𝑇 → 𝐼 ⊆ (Base‘𝑅)) |
25 | 24 | ad4antlr 733 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐼 ∈ 𝑇) ∧ 𝑗 ∈ 𝐼) ∧ 𝑖 ∈ 𝐼) ∧ 𝑧 ∈ (Base‘𝑅)) → 𝐼 ⊆ (Base‘𝑅)) |
26 | | simplr 769 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐼 ∈ 𝑇) ∧ 𝑗 ∈ 𝐼) ∧ 𝑖 ∈ 𝐼) ∧ 𝑧 ∈ (Base‘𝑅)) → 𝑖 ∈ 𝐼) |
27 | 25, 26 | sseldd 3889 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐼 ∈ 𝑇) ∧ 𝑗 ∈ 𝐼) ∧ 𝑖 ∈ 𝐼) ∧ 𝑧 ∈ (Base‘𝑅)) → 𝑖 ∈ (Base‘𝑅)) |
28 | | eqid 2759 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(.r‘𝑅) = (.r‘𝑅) |
29 | 1, 28 | ringcl 19367 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑅 ∈ Ring ∧ 𝑧 ∈ (Base‘𝑅) ∧ 𝑖 ∈ (Base‘𝑅)) → (𝑧(.r‘𝑅)𝑖) ∈ (Base‘𝑅)) |
30 | 22, 23, 27, 29 | syl3anc 1369 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐼 ∈ 𝑇) ∧ 𝑗 ∈ 𝐼) ∧ 𝑖 ∈ 𝐼) ∧ 𝑧 ∈ (Base‘𝑅)) → (𝑧(.r‘𝑅)𝑖) ∈ (Base‘𝑅)) |
31 | | simpllr 776 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐼 ∈ 𝑇) ∧ 𝑗 ∈ 𝐼) ∧ 𝑖 ∈ 𝐼) ∧ 𝑧 ∈ (Base‘𝑅)) → 𝑗 ∈ 𝐼) |
32 | 25, 31 | sseldd 3889 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐼 ∈ 𝑇) ∧ 𝑗 ∈ 𝐼) ∧ 𝑖 ∈ 𝐼) ∧ 𝑧 ∈ (Base‘𝑅)) → 𝑗 ∈ (Base‘𝑅)) |
33 | | eqid 2759 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(+g‘𝑅) = (+g‘𝑅) |
34 | | eqid 2759 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(+g‘𝑆) = (+g‘𝑆) |
35 | 1, 33, 34 | ghmlin 18415 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐹 ∈ (𝑅 GrpHom 𝑆) ∧ (𝑧(.r‘𝑅)𝑖) ∈ (Base‘𝑅) ∧ 𝑗 ∈ (Base‘𝑅)) → (𝐹‘((𝑧(.r‘𝑅)𝑖)(+g‘𝑅)𝑗)) = ((𝐹‘(𝑧(.r‘𝑅)𝑖))(+g‘𝑆)(𝐹‘𝑗))) |
36 | 21, 30, 32, 35 | syl3anc 1369 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐼 ∈ 𝑇) ∧ 𝑗 ∈ 𝐼) ∧ 𝑖 ∈ 𝐼) ∧ 𝑧 ∈ (Base‘𝑅)) → (𝐹‘((𝑧(.r‘𝑅)𝑖)(+g‘𝑅)𝑗)) = ((𝐹‘(𝑧(.r‘𝑅)𝑖))(+g‘𝑆)(𝐹‘𝑗))) |
37 | | simp-4l 783 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐼 ∈ 𝑇) ∧ 𝑗 ∈ 𝐼) ∧ 𝑖 ∈ 𝐼) ∧ 𝑧 ∈ (Base‘𝑅)) → 𝐹 ∈ (𝑅 RingHom 𝑆)) |
38 | | eqid 2759 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(.r‘𝑆) = (.r‘𝑆) |
39 | 1, 28, 38 | rhmmul 19535 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝑧 ∈ (Base‘𝑅) ∧ 𝑖 ∈ (Base‘𝑅)) → (𝐹‘(𝑧(.r‘𝑅)𝑖)) = ((𝐹‘𝑧)(.r‘𝑆)(𝐹‘𝑖))) |
40 | 37, 23, 27, 39 | syl3anc 1369 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐼 ∈ 𝑇) ∧ 𝑗 ∈ 𝐼) ∧ 𝑖 ∈ 𝐼) ∧ 𝑧 ∈ (Base‘𝑅)) → (𝐹‘(𝑧(.r‘𝑅)𝑖)) = ((𝐹‘𝑧)(.r‘𝑆)(𝐹‘𝑖))) |
41 | 40 | oveq1d 7158 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐼 ∈ 𝑇) ∧ 𝑗 ∈ 𝐼) ∧ 𝑖 ∈ 𝐼) ∧ 𝑧 ∈ (Base‘𝑅)) → ((𝐹‘(𝑧(.r‘𝑅)𝑖))(+g‘𝑆)(𝐹‘𝑗)) = (((𝐹‘𝑧)(.r‘𝑆)(𝐹‘𝑖))(+g‘𝑆)(𝐹‘𝑗))) |
42 | 36, 41 | eqtrd 2794 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐼 ∈ 𝑇) ∧ 𝑗 ∈ 𝐼) ∧ 𝑖 ∈ 𝐼) ∧ 𝑧 ∈ (Base‘𝑅)) → (𝐹‘((𝑧(.r‘𝑅)𝑖)(+g‘𝑅)𝑗)) = (((𝐹‘𝑧)(.r‘𝑆)(𝐹‘𝑖))(+g‘𝑆)(𝐹‘𝑗))) |
43 | 42 | adantl4r 755 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝐹 ∈
(𝑅 RingHom 𝑆) ∧ ran 𝐹 = 𝐵) ∧ 𝐼 ∈ 𝑇) ∧ 𝑗 ∈ 𝐼) ∧ 𝑖 ∈ 𝐼) ∧ 𝑧 ∈ (Base‘𝑅)) → (𝐹‘((𝑧(.r‘𝑅)𝑖)(+g‘𝑅)𝑗)) = (((𝐹‘𝑧)(.r‘𝑆)(𝐹‘𝑖))(+g‘𝑆)(𝐹‘𝑗))) |
44 | 43 | adantl3r 750 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝐹 ∈
(𝑅 RingHom 𝑆) ∧ ran 𝐹 = 𝐵) ∧ 𝐼 ∈ 𝑇) ∧ 𝑥 ∈ 𝐵) ∧ 𝑗 ∈ 𝐼) ∧ 𝑖 ∈ 𝐼) ∧ 𝑧 ∈ (Base‘𝑅)) → (𝐹‘((𝑧(.r‘𝑅)𝑖)(+g‘𝑅)𝑗)) = (((𝐹‘𝑧)(.r‘𝑆)(𝐹‘𝑖))(+g‘𝑆)(𝐹‘𝑗))) |
45 | 44 | adantl3r 750 |
. . . . . . . . . . . . . 14
⊢
((((((((𝐹 ∈
(𝑅 RingHom 𝑆) ∧ ran 𝐹 = 𝐵) ∧ 𝐼 ∈ 𝑇) ∧ 𝑥 ∈ 𝐵) ∧ 𝑎 ∈ (𝐹 “ 𝐼)) ∧ 𝑗 ∈ 𝐼) ∧ 𝑖 ∈ 𝐼) ∧ 𝑧 ∈ (Base‘𝑅)) → (𝐹‘((𝑧(.r‘𝑅)𝑖)(+g‘𝑅)𝑗)) = (((𝐹‘𝑧)(.r‘𝑆)(𝐹‘𝑖))(+g‘𝑆)(𝐹‘𝑗))) |
46 | 45 | adantl3r 750 |
. . . . . . . . . . . . 13
⊢
(((((((((𝐹 ∈
(𝑅 RingHom 𝑆) ∧ ran 𝐹 = 𝐵) ∧ 𝐼 ∈ 𝑇) ∧ 𝑥 ∈ 𝐵) ∧ 𝑎 ∈ (𝐹 “ 𝐼)) ∧ 𝑏 ∈ (𝐹 “ 𝐼)) ∧ 𝑗 ∈ 𝐼) ∧ 𝑖 ∈ 𝐼) ∧ 𝑧 ∈ (Base‘𝑅)) → (𝐹‘((𝑧(.r‘𝑅)𝑖)(+g‘𝑅)𝑗)) = (((𝐹‘𝑧)(.r‘𝑆)(𝐹‘𝑖))(+g‘𝑆)(𝐹‘𝑗))) |
47 | 46 | adantllr 719 |
. . . . . . . . . . . 12
⊢
((((((((((𝐹 ∈
(𝑅 RingHom 𝑆) ∧ ran 𝐹 = 𝐵) ∧ 𝐼 ∈ 𝑇) ∧ 𝑥 ∈ 𝐵) ∧ 𝑎 ∈ (𝐹 “ 𝐼)) ∧ 𝑏 ∈ (𝐹 “ 𝐼)) ∧ 𝑗 ∈ 𝐼) ∧ (𝐹‘𝑗) = 𝑏) ∧ 𝑖 ∈ 𝐼) ∧ 𝑧 ∈ (Base‘𝑅)) → (𝐹‘((𝑧(.r‘𝑅)𝑖)(+g‘𝑅)𝑗)) = (((𝐹‘𝑧)(.r‘𝑆)(𝐹‘𝑖))(+g‘𝑆)(𝐹‘𝑗))) |
48 | 47 | ad4ant13 751 |
. . . . . . . . . . 11
⊢
((((((((((((𝐹 ∈
(𝑅 RingHom 𝑆) ∧ ran 𝐹 = 𝐵) ∧ 𝐼 ∈ 𝑇) ∧ 𝑥 ∈ 𝐵) ∧ 𝑎 ∈ (𝐹 “ 𝐼)) ∧ 𝑏 ∈ (𝐹 “ 𝐼)) ∧ 𝑗 ∈ 𝐼) ∧ (𝐹‘𝑗) = 𝑏) ∧ 𝑖 ∈ 𝐼) ∧ (𝐹‘𝑖) = 𝑎) ∧ 𝑧 ∈ (Base‘𝑅)) ∧ (𝐹‘𝑧) = 𝑥) → (𝐹‘((𝑧(.r‘𝑅)𝑖)(+g‘𝑅)𝑗)) = (((𝐹‘𝑧)(.r‘𝑆)(𝐹‘𝑖))(+g‘𝑆)(𝐹‘𝑗))) |
49 | | simpr 489 |
. . . . . . . . . . . . 13
⊢
((((((((((((𝐹 ∈
(𝑅 RingHom 𝑆) ∧ ran 𝐹 = 𝐵) ∧ 𝐼 ∈ 𝑇) ∧ 𝑥 ∈ 𝐵) ∧ 𝑎 ∈ (𝐹 “ 𝐼)) ∧ 𝑏 ∈ (𝐹 “ 𝐼)) ∧ 𝑗 ∈ 𝐼) ∧ (𝐹‘𝑗) = 𝑏) ∧ 𝑖 ∈ 𝐼) ∧ (𝐹‘𝑖) = 𝑎) ∧ 𝑧 ∈ (Base‘𝑅)) ∧ (𝐹‘𝑧) = 𝑥) → (𝐹‘𝑧) = 𝑥) |
50 | | simpllr 776 |
. . . . . . . . . . . . 13
⊢
((((((((((((𝐹 ∈
(𝑅 RingHom 𝑆) ∧ ran 𝐹 = 𝐵) ∧ 𝐼 ∈ 𝑇) ∧ 𝑥 ∈ 𝐵) ∧ 𝑎 ∈ (𝐹 “ 𝐼)) ∧ 𝑏 ∈ (𝐹 “ 𝐼)) ∧ 𝑗 ∈ 𝐼) ∧ (𝐹‘𝑗) = 𝑏) ∧ 𝑖 ∈ 𝐼) ∧ (𝐹‘𝑖) = 𝑎) ∧ 𝑧 ∈ (Base‘𝑅)) ∧ (𝐹‘𝑧) = 𝑥) → (𝐹‘𝑖) = 𝑎) |
51 | 49, 50 | oveq12d 7161 |
. . . . . . . . . . . 12
⊢
((((((((((((𝐹 ∈
(𝑅 RingHom 𝑆) ∧ ran 𝐹 = 𝐵) ∧ 𝐼 ∈ 𝑇) ∧ 𝑥 ∈ 𝐵) ∧ 𝑎 ∈ (𝐹 “ 𝐼)) ∧ 𝑏 ∈ (𝐹 “ 𝐼)) ∧ 𝑗 ∈ 𝐼) ∧ (𝐹‘𝑗) = 𝑏) ∧ 𝑖 ∈ 𝐼) ∧ (𝐹‘𝑖) = 𝑎) ∧ 𝑧 ∈ (Base‘𝑅)) ∧ (𝐹‘𝑧) = 𝑥) → ((𝐹‘𝑧)(.r‘𝑆)(𝐹‘𝑖)) = (𝑥(.r‘𝑆)𝑎)) |
52 | | simp-5r 786 |
. . . . . . . . . . . 12
⊢
((((((((((((𝐹 ∈
(𝑅 RingHom 𝑆) ∧ ran 𝐹 = 𝐵) ∧ 𝐼 ∈ 𝑇) ∧ 𝑥 ∈ 𝐵) ∧ 𝑎 ∈ (𝐹 “ 𝐼)) ∧ 𝑏 ∈ (𝐹 “ 𝐼)) ∧ 𝑗 ∈ 𝐼) ∧ (𝐹‘𝑗) = 𝑏) ∧ 𝑖 ∈ 𝐼) ∧ (𝐹‘𝑖) = 𝑎) ∧ 𝑧 ∈ (Base‘𝑅)) ∧ (𝐹‘𝑧) = 𝑥) → (𝐹‘𝑗) = 𝑏) |
53 | 51, 52 | oveq12d 7161 |
. . . . . . . . . . 11
⊢
((((((((((((𝐹 ∈
(𝑅 RingHom 𝑆) ∧ ran 𝐹 = 𝐵) ∧ 𝐼 ∈ 𝑇) ∧ 𝑥 ∈ 𝐵) ∧ 𝑎 ∈ (𝐹 “ 𝐼)) ∧ 𝑏 ∈ (𝐹 “ 𝐼)) ∧ 𝑗 ∈ 𝐼) ∧ (𝐹‘𝑗) = 𝑏) ∧ 𝑖 ∈ 𝐼) ∧ (𝐹‘𝑖) = 𝑎) ∧ 𝑧 ∈ (Base‘𝑅)) ∧ (𝐹‘𝑧) = 𝑥) → (((𝐹‘𝑧)(.r‘𝑆)(𝐹‘𝑖))(+g‘𝑆)(𝐹‘𝑗)) = ((𝑥(.r‘𝑆)𝑎)(+g‘𝑆)𝑏)) |
54 | 48, 53 | eqtrd 2794 |
. . . . . . . . . 10
⊢
((((((((((((𝐹 ∈
(𝑅 RingHom 𝑆) ∧ ran 𝐹 = 𝐵) ∧ 𝐼 ∈ 𝑇) ∧ 𝑥 ∈ 𝐵) ∧ 𝑎 ∈ (𝐹 “ 𝐼)) ∧ 𝑏 ∈ (𝐹 “ 𝐼)) ∧ 𝑗 ∈ 𝐼) ∧ (𝐹‘𝑗) = 𝑏) ∧ 𝑖 ∈ 𝐼) ∧ (𝐹‘𝑖) = 𝑎) ∧ 𝑧 ∈ (Base‘𝑅)) ∧ (𝐹‘𝑧) = 𝑥) → (𝐹‘((𝑧(.r‘𝑅)𝑖)(+g‘𝑅)𝑗)) = ((𝑥(.r‘𝑆)𝑎)(+g‘𝑆)𝑏)) |
55 | 8 | ad9antr 742 |
. . . . . . . . . . 11
⊢
((((((((((((𝐹 ∈
(𝑅 RingHom 𝑆) ∧ ran 𝐹 = 𝐵) ∧ 𝐼 ∈ 𝑇) ∧ 𝑥 ∈ 𝐵) ∧ 𝑎 ∈ (𝐹 “ 𝐼)) ∧ 𝑏 ∈ (𝐹 “ 𝐼)) ∧ 𝑗 ∈ 𝐼) ∧ (𝐹‘𝑗) = 𝑏) ∧ 𝑖 ∈ 𝐼) ∧ (𝐹‘𝑖) = 𝑎) ∧ 𝑧 ∈ (Base‘𝑅)) ∧ (𝐹‘𝑧) = 𝑥) → 𝐹 Fn (Base‘𝑅)) |
56 | 14, 24 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ ran 𝐹 = 𝐵) ∧ 𝐼 ∈ 𝑇) → 𝐼 ⊆ (Base‘𝑅)) |
57 | 56 | ad9antr 742 |
. . . . . . . . . . . 12
⊢
((((((((((((𝐹 ∈
(𝑅 RingHom 𝑆) ∧ ran 𝐹 = 𝐵) ∧ 𝐼 ∈ 𝑇) ∧ 𝑥 ∈ 𝐵) ∧ 𝑎 ∈ (𝐹 “ 𝐼)) ∧ 𝑏 ∈ (𝐹 “ 𝐼)) ∧ 𝑗 ∈ 𝐼) ∧ (𝐹‘𝑗) = 𝑏) ∧ 𝑖 ∈ 𝐼) ∧ (𝐹‘𝑖) = 𝑎) ∧ 𝑧 ∈ (Base‘𝑅)) ∧ (𝐹‘𝑧) = 𝑥) → 𝐼 ⊆ (Base‘𝑅)) |
58 | 14 | ad9antr 742 |
. . . . . . . . . . . . 13
⊢
((((((((((((𝐹 ∈
(𝑅 RingHom 𝑆) ∧ ran 𝐹 = 𝐵) ∧ 𝐼 ∈ 𝑇) ∧ 𝑥 ∈ 𝐵) ∧ 𝑎 ∈ (𝐹 “ 𝐼)) ∧ 𝑏 ∈ (𝐹 “ 𝐼)) ∧ 𝑗 ∈ 𝐼) ∧ (𝐹‘𝑗) = 𝑏) ∧ 𝑖 ∈ 𝐼) ∧ (𝐹‘𝑖) = 𝑎) ∧ 𝑧 ∈ (Base‘𝑅)) ∧ (𝐹‘𝑧) = 𝑥) → 𝐼 ∈ 𝑇) |
59 | | simplr 769 |
. . . . . . . . . . . . 13
⊢
((((((((((((𝐹 ∈
(𝑅 RingHom 𝑆) ∧ ran 𝐹 = 𝐵) ∧ 𝐼 ∈ 𝑇) ∧ 𝑥 ∈ 𝐵) ∧ 𝑎 ∈ (𝐹 “ 𝐼)) ∧ 𝑏 ∈ (𝐹 “ 𝐼)) ∧ 𝑗 ∈ 𝐼) ∧ (𝐹‘𝑗) = 𝑏) ∧ 𝑖 ∈ 𝐼) ∧ (𝐹‘𝑖) = 𝑎) ∧ 𝑧 ∈ (Base‘𝑅)) ∧ (𝐹‘𝑧) = 𝑥) → 𝑧 ∈ (Base‘𝑅)) |
60 | | simp-4r 784 |
. . . . . . . . . . . . 13
⊢
((((((((((((𝐹 ∈
(𝑅 RingHom 𝑆) ∧ ran 𝐹 = 𝐵) ∧ 𝐼 ∈ 𝑇) ∧ 𝑥 ∈ 𝐵) ∧ 𝑎 ∈ (𝐹 “ 𝐼)) ∧ 𝑏 ∈ (𝐹 “ 𝐼)) ∧ 𝑗 ∈ 𝐼) ∧ (𝐹‘𝑗) = 𝑏) ∧ 𝑖 ∈ 𝐼) ∧ (𝐹‘𝑖) = 𝑎) ∧ 𝑧 ∈ (Base‘𝑅)) ∧ (𝐹‘𝑧) = 𝑥) → 𝑖 ∈ 𝐼) |
61 | | simp-6r 788 |
. . . . . . . . . . . . 13
⊢
((((((((((((𝐹 ∈
(𝑅 RingHom 𝑆) ∧ ran 𝐹 = 𝐵) ∧ 𝐼 ∈ 𝑇) ∧ 𝑥 ∈ 𝐵) ∧ 𝑎 ∈ (𝐹 “ 𝐼)) ∧ 𝑏 ∈ (𝐹 “ 𝐼)) ∧ 𝑗 ∈ 𝐼) ∧ (𝐹‘𝑗) = 𝑏) ∧ 𝑖 ∈ 𝐼) ∧ (𝐹‘𝑖) = 𝑎) ∧ 𝑧 ∈ (Base‘𝑅)) ∧ (𝐹‘𝑧) = 𝑥) → 𝑗 ∈ 𝐼) |
62 | 15, 1, 33, 28 | islidl 20037 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐼 ∈ 𝑇 ↔ (𝐼 ⊆ (Base‘𝑅) ∧ 𝐼 ≠ ∅ ∧ ∀𝑧 ∈ (Base‘𝑅)∀𝑖 ∈ 𝐼 ∀𝑗 ∈ 𝐼 ((𝑧(.r‘𝑅)𝑖)(+g‘𝑅)𝑗) ∈ 𝐼)) |
63 | 62 | simp3bi 1145 |
. . . . . . . . . . . . . . . 16
⊢ (𝐼 ∈ 𝑇 → ∀𝑧 ∈ (Base‘𝑅)∀𝑖 ∈ 𝐼 ∀𝑗 ∈ 𝐼 ((𝑧(.r‘𝑅)𝑖)(+g‘𝑅)𝑗) ∈ 𝐼) |
64 | 63 | r19.21bi 3135 |
. . . . . . . . . . . . . . 15
⊢ ((𝐼 ∈ 𝑇 ∧ 𝑧 ∈ (Base‘𝑅)) → ∀𝑖 ∈ 𝐼 ∀𝑗 ∈ 𝐼 ((𝑧(.r‘𝑅)𝑖)(+g‘𝑅)𝑗) ∈ 𝐼) |
65 | 64 | r19.21bi 3135 |
. . . . . . . . . . . . . 14
⊢ (((𝐼 ∈ 𝑇 ∧ 𝑧 ∈ (Base‘𝑅)) ∧ 𝑖 ∈ 𝐼) → ∀𝑗 ∈ 𝐼 ((𝑧(.r‘𝑅)𝑖)(+g‘𝑅)𝑗) ∈ 𝐼) |
66 | 65 | r19.21bi 3135 |
. . . . . . . . . . . . 13
⊢ ((((𝐼 ∈ 𝑇 ∧ 𝑧 ∈ (Base‘𝑅)) ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 ∈ 𝐼) → ((𝑧(.r‘𝑅)𝑖)(+g‘𝑅)𝑗) ∈ 𝐼) |
67 | 58, 59, 60, 61, 66 | syl1111anc 839 |
. . . . . . . . . . . 12
⊢
((((((((((((𝐹 ∈
(𝑅 RingHom 𝑆) ∧ ran 𝐹 = 𝐵) ∧ 𝐼 ∈ 𝑇) ∧ 𝑥 ∈ 𝐵) ∧ 𝑎 ∈ (𝐹 “ 𝐼)) ∧ 𝑏 ∈ (𝐹 “ 𝐼)) ∧ 𝑗 ∈ 𝐼) ∧ (𝐹‘𝑗) = 𝑏) ∧ 𝑖 ∈ 𝐼) ∧ (𝐹‘𝑖) = 𝑎) ∧ 𝑧 ∈ (Base‘𝑅)) ∧ (𝐹‘𝑧) = 𝑥) → ((𝑧(.r‘𝑅)𝑖)(+g‘𝑅)𝑗) ∈ 𝐼) |
68 | 57, 67 | sseldd 3889 |
. . . . . . . . . . 11
⊢
((((((((((((𝐹 ∈
(𝑅 RingHom 𝑆) ∧ ran 𝐹 = 𝐵) ∧ 𝐼 ∈ 𝑇) ∧ 𝑥 ∈ 𝐵) ∧ 𝑎 ∈ (𝐹 “ 𝐼)) ∧ 𝑏 ∈ (𝐹 “ 𝐼)) ∧ 𝑗 ∈ 𝐼) ∧ (𝐹‘𝑗) = 𝑏) ∧ 𝑖 ∈ 𝐼) ∧ (𝐹‘𝑖) = 𝑎) ∧ 𝑧 ∈ (Base‘𝑅)) ∧ (𝐹‘𝑧) = 𝑥) → ((𝑧(.r‘𝑅)𝑖)(+g‘𝑅)𝑗) ∈ (Base‘𝑅)) |
69 | 55, 68, 67 | fnfvimad 6981 |
. . . . . . . . . 10
⊢
((((((((((((𝐹 ∈
(𝑅 RingHom 𝑆) ∧ ran 𝐹 = 𝐵) ∧ 𝐼 ∈ 𝑇) ∧ 𝑥 ∈ 𝐵) ∧ 𝑎 ∈ (𝐹 “ 𝐼)) ∧ 𝑏 ∈ (𝐹 “ 𝐼)) ∧ 𝑗 ∈ 𝐼) ∧ (𝐹‘𝑗) = 𝑏) ∧ 𝑖 ∈ 𝐼) ∧ (𝐹‘𝑖) = 𝑎) ∧ 𝑧 ∈ (Base‘𝑅)) ∧ (𝐹‘𝑧) = 𝑥) → (𝐹‘((𝑧(.r‘𝑅)𝑖)(+g‘𝑅)𝑗)) ∈ (𝐹 “ 𝐼)) |
70 | 54, 69 | eqeltrrd 2852 |
. . . . . . . . 9
⊢
((((((((((((𝐹 ∈
(𝑅 RingHom 𝑆) ∧ ran 𝐹 = 𝐵) ∧ 𝐼 ∈ 𝑇) ∧ 𝑥 ∈ 𝐵) ∧ 𝑎 ∈ (𝐹 “ 𝐼)) ∧ 𝑏 ∈ (𝐹 “ 𝐼)) ∧ 𝑗 ∈ 𝐼) ∧ (𝐹‘𝑗) = 𝑏) ∧ 𝑖 ∈ 𝐼) ∧ (𝐹‘𝑖) = 𝑎) ∧ 𝑧 ∈ (Base‘𝑅)) ∧ (𝐹‘𝑧) = 𝑥) → ((𝑥(.r‘𝑆)𝑎)(+g‘𝑆)𝑏) ∈ (𝐹 “ 𝐼)) |
71 | 3 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ (((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ ran 𝐹 = 𝐵) ∧ 𝐼 ∈ 𝑇) → 𝐹:(Base‘𝑅)⟶𝐵) |
72 | 71 | ffund 6495 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ ran 𝐹 = 𝐵) ∧ 𝐼 ∈ 𝑇) → Fun 𝐹) |
73 | 72 | ad7antr 738 |
. . . . . . . . . 10
⊢
((((((((((𝐹 ∈
(𝑅 RingHom 𝑆) ∧ ran 𝐹 = 𝐵) ∧ 𝐼 ∈ 𝑇) ∧ 𝑥 ∈ 𝐵) ∧ 𝑎 ∈ (𝐹 “ 𝐼)) ∧ 𝑏 ∈ (𝐹 “ 𝐼)) ∧ 𝑗 ∈ 𝐼) ∧ (𝐹‘𝑗) = 𝑏) ∧ 𝑖 ∈ 𝐼) ∧ (𝐹‘𝑖) = 𝑎) → Fun 𝐹) |
74 | | imadmrn 5904 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹 “ dom 𝐹) = ran 𝐹 |
75 | 3 | fdmd 6501 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → dom 𝐹 = (Base‘𝑅)) |
76 | 75 | imaeq2d 5894 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → (𝐹 “ dom 𝐹) = (𝐹 “ (Base‘𝑅))) |
77 | 74, 76 | syl5reqr 2809 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → (𝐹 “ (Base‘𝑅)) = ran 𝐹) |
78 | 77 | eqeq1d 2761 |
. . . . . . . . . . . . . . 15
⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → ((𝐹 “ (Base‘𝑅)) = 𝐵 ↔ ran 𝐹 = 𝐵)) |
79 | 78 | biimpar 482 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ ran 𝐹 = 𝐵) → (𝐹 “ (Base‘𝑅)) = 𝐵) |
80 | 79 | eleq2d 2836 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ ran 𝐹 = 𝐵) → (𝑥 ∈ (𝐹 “ (Base‘𝑅)) ↔ 𝑥 ∈ 𝐵)) |
81 | 80 | biimpar 482 |
. . . . . . . . . . . 12
⊢ (((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ ran 𝐹 = 𝐵) ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ (𝐹 “ (Base‘𝑅))) |
82 | 81 | adantlr 715 |
. . . . . . . . . . 11
⊢ ((((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ ran 𝐹 = 𝐵) ∧ 𝐼 ∈ 𝑇) ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ (𝐹 “ (Base‘𝑅))) |
83 | 82 | ad6antr 736 |
. . . . . . . . . 10
⊢
((((((((((𝐹 ∈
(𝑅 RingHom 𝑆) ∧ ran 𝐹 = 𝐵) ∧ 𝐼 ∈ 𝑇) ∧ 𝑥 ∈ 𝐵) ∧ 𝑎 ∈ (𝐹 “ 𝐼)) ∧ 𝑏 ∈ (𝐹 “ 𝐼)) ∧ 𝑗 ∈ 𝐼) ∧ (𝐹‘𝑗) = 𝑏) ∧ 𝑖 ∈ 𝐼) ∧ (𝐹‘𝑖) = 𝑎) → 𝑥 ∈ (𝐹 “ (Base‘𝑅))) |
84 | | fvelima 6712 |
. . . . . . . . . 10
⊢ ((Fun
𝐹 ∧ 𝑥 ∈ (𝐹 “ (Base‘𝑅))) → ∃𝑧 ∈ (Base‘𝑅)(𝐹‘𝑧) = 𝑥) |
85 | 73, 83, 84 | syl2anc 588 |
. . . . . . . . 9
⊢
((((((((((𝐹 ∈
(𝑅 RingHom 𝑆) ∧ ran 𝐹 = 𝐵) ∧ 𝐼 ∈ 𝑇) ∧ 𝑥 ∈ 𝐵) ∧ 𝑎 ∈ (𝐹 “ 𝐼)) ∧ 𝑏 ∈ (𝐹 “ 𝐼)) ∧ 𝑗 ∈ 𝐼) ∧ (𝐹‘𝑗) = 𝑏) ∧ 𝑖 ∈ 𝐼) ∧ (𝐹‘𝑖) = 𝑎) → ∃𝑧 ∈ (Base‘𝑅)(𝐹‘𝑧) = 𝑥) |
86 | 70, 85 | r19.29a 3211 |
. . . . . . . 8
⊢
((((((((((𝐹 ∈
(𝑅 RingHom 𝑆) ∧ ran 𝐹 = 𝐵) ∧ 𝐼 ∈ 𝑇) ∧ 𝑥 ∈ 𝐵) ∧ 𝑎 ∈ (𝐹 “ 𝐼)) ∧ 𝑏 ∈ (𝐹 “ 𝐼)) ∧ 𝑗 ∈ 𝐼) ∧ (𝐹‘𝑗) = 𝑏) ∧ 𝑖 ∈ 𝐼) ∧ (𝐹‘𝑖) = 𝑎) → ((𝑥(.r‘𝑆)𝑎)(+g‘𝑆)𝑏) ∈ (𝐹 “ 𝐼)) |
87 | 72 | ad5antr 734 |
. . . . . . . . 9
⊢
((((((((𝐹 ∈
(𝑅 RingHom 𝑆) ∧ ran 𝐹 = 𝐵) ∧ 𝐼 ∈ 𝑇) ∧ 𝑥 ∈ 𝐵) ∧ 𝑎 ∈ (𝐹 “ 𝐼)) ∧ 𝑏 ∈ (𝐹 “ 𝐼)) ∧ 𝑗 ∈ 𝐼) ∧ (𝐹‘𝑗) = 𝑏) → Fun 𝐹) |
88 | | simp-4r 784 |
. . . . . . . . 9
⊢
((((((((𝐹 ∈
(𝑅 RingHom 𝑆) ∧ ran 𝐹 = 𝐵) ∧ 𝐼 ∈ 𝑇) ∧ 𝑥 ∈ 𝐵) ∧ 𝑎 ∈ (𝐹 “ 𝐼)) ∧ 𝑏 ∈ (𝐹 “ 𝐼)) ∧ 𝑗 ∈ 𝐼) ∧ (𝐹‘𝑗) = 𝑏) → 𝑎 ∈ (𝐹 “ 𝐼)) |
89 | | fvelima 6712 |
. . . . . . . . 9
⊢ ((Fun
𝐹 ∧ 𝑎 ∈ (𝐹 “ 𝐼)) → ∃𝑖 ∈ 𝐼 (𝐹‘𝑖) = 𝑎) |
90 | 87, 88, 89 | syl2anc 588 |
. . . . . . . 8
⊢
((((((((𝐹 ∈
(𝑅 RingHom 𝑆) ∧ ran 𝐹 = 𝐵) ∧ 𝐼 ∈ 𝑇) ∧ 𝑥 ∈ 𝐵) ∧ 𝑎 ∈ (𝐹 “ 𝐼)) ∧ 𝑏 ∈ (𝐹 “ 𝐼)) ∧ 𝑗 ∈ 𝐼) ∧ (𝐹‘𝑗) = 𝑏) → ∃𝑖 ∈ 𝐼 (𝐹‘𝑖) = 𝑎) |
91 | 86, 90 | r19.29a 3211 |
. . . . . . 7
⊢
((((((((𝐹 ∈
(𝑅 RingHom 𝑆) ∧ ran 𝐹 = 𝐵) ∧ 𝐼 ∈ 𝑇) ∧ 𝑥 ∈ 𝐵) ∧ 𝑎 ∈ (𝐹 “ 𝐼)) ∧ 𝑏 ∈ (𝐹 “ 𝐼)) ∧ 𝑗 ∈ 𝐼) ∧ (𝐹‘𝑗) = 𝑏) → ((𝑥(.r‘𝑆)𝑎)(+g‘𝑆)𝑏) ∈ (𝐹 “ 𝐼)) |
92 | 72 | ad3antrrr 730 |
. . . . . . . 8
⊢
((((((𝐹 ∈
(𝑅 RingHom 𝑆) ∧ ran 𝐹 = 𝐵) ∧ 𝐼 ∈ 𝑇) ∧ 𝑥 ∈ 𝐵) ∧ 𝑎 ∈ (𝐹 “ 𝐼)) ∧ 𝑏 ∈ (𝐹 “ 𝐼)) → Fun 𝐹) |
93 | | simpr 489 |
. . . . . . . 8
⊢
((((((𝐹 ∈
(𝑅 RingHom 𝑆) ∧ ran 𝐹 = 𝐵) ∧ 𝐼 ∈ 𝑇) ∧ 𝑥 ∈ 𝐵) ∧ 𝑎 ∈ (𝐹 “ 𝐼)) ∧ 𝑏 ∈ (𝐹 “ 𝐼)) → 𝑏 ∈ (𝐹 “ 𝐼)) |
94 | | fvelima 6712 |
. . . . . . . 8
⊢ ((Fun
𝐹 ∧ 𝑏 ∈ (𝐹 “ 𝐼)) → ∃𝑗 ∈ 𝐼 (𝐹‘𝑗) = 𝑏) |
95 | 92, 93, 94 | syl2anc 588 |
. . . . . . 7
⊢
((((((𝐹 ∈
(𝑅 RingHom 𝑆) ∧ ran 𝐹 = 𝐵) ∧ 𝐼 ∈ 𝑇) ∧ 𝑥 ∈ 𝐵) ∧ 𝑎 ∈ (𝐹 “ 𝐼)) ∧ 𝑏 ∈ (𝐹 “ 𝐼)) → ∃𝑗 ∈ 𝐼 (𝐹‘𝑗) = 𝑏) |
96 | 91, 95 | r19.29a 3211 |
. . . . . 6
⊢
((((((𝐹 ∈
(𝑅 RingHom 𝑆) ∧ ran 𝐹 = 𝐵) ∧ 𝐼 ∈ 𝑇) ∧ 𝑥 ∈ 𝐵) ∧ 𝑎 ∈ (𝐹 “ 𝐼)) ∧ 𝑏 ∈ (𝐹 “ 𝐼)) → ((𝑥(.r‘𝑆)𝑎)(+g‘𝑆)𝑏) ∈ (𝐹 “ 𝐼)) |
97 | 96 | anasss 471 |
. . . . 5
⊢
(((((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ ran 𝐹 = 𝐵) ∧ 𝐼 ∈ 𝑇) ∧ 𝑥 ∈ 𝐵) ∧ (𝑎 ∈ (𝐹 “ 𝐼) ∧ 𝑏 ∈ (𝐹 “ 𝐼))) → ((𝑥(.r‘𝑆)𝑎)(+g‘𝑆)𝑏) ∈ (𝐹 “ 𝐼)) |
98 | 97 | ralrimivva 3118 |
. . . 4
⊢ ((((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ ran 𝐹 = 𝐵) ∧ 𝐼 ∈ 𝑇) ∧ 𝑥 ∈ 𝐵) → ∀𝑎 ∈ (𝐹 “ 𝐼)∀𝑏 ∈ (𝐹 “ 𝐼)((𝑥(.r‘𝑆)𝑎)(+g‘𝑆)𝑏) ∈ (𝐹 “ 𝐼)) |
99 | 98 | ralrimiva 3111 |
. . 3
⊢ (((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ ran 𝐹 = 𝐵) ∧ 𝐼 ∈ 𝑇) → ∀𝑥 ∈ 𝐵 ∀𝑎 ∈ (𝐹 “ 𝐼)∀𝑏 ∈ (𝐹 “ 𝐼)((𝑥(.r‘𝑆)𝑎)(+g‘𝑆)𝑏) ∈ (𝐹 “ 𝐼)) |
100 | | rhmimaidl.u |
. . . 4
⊢ 𝑈 = (LIdeal‘𝑆) |
101 | 100, 2, 34, 38 | islidl 20037 |
. . 3
⊢ ((𝐹 “ 𝐼) ∈ 𝑈 ↔ ((𝐹 “ 𝐼) ⊆ 𝐵 ∧ (𝐹 “ 𝐼) ≠ ∅ ∧ ∀𝑥 ∈ 𝐵 ∀𝑎 ∈ (𝐹 “ 𝐼)∀𝑏 ∈ (𝐹 “ 𝐼)((𝑥(.r‘𝑆)𝑎)(+g‘𝑆)𝑏) ∈ (𝐹 “ 𝐼))) |
102 | 6, 19, 99, 101 | syl3anbrc 1341 |
. 2
⊢ (((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ ran 𝐹 = 𝐵) ∧ 𝐼 ∈ 𝑇) → (𝐹 “ 𝐼) ∈ 𝑈) |
103 | 102 | 3impa 1108 |
1
⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ ran 𝐹 = 𝐵 ∧ 𝐼 ∈ 𝑇) → (𝐹 “ 𝐼) ∈ 𝑈) |