| Step | Hyp | Ref
| Expression |
| 1 | | eqid 2737 |
. . . . . 6
⊢
(Base‘𝑅) =
(Base‘𝑅) |
| 2 | | rhmimaidl.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝑆) |
| 3 | 1, 2 | rhmf 20485 |
. . . . 5
⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝐹:(Base‘𝑅)⟶𝐵) |
| 4 | | fimass 6756 |
. . . . 5
⊢ (𝐹:(Base‘𝑅)⟶𝐵 → (𝐹 “ 𝐼) ⊆ 𝐵) |
| 5 | 3, 4 | syl 17 |
. . . 4
⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → (𝐹 “ 𝐼) ⊆ 𝐵) |
| 6 | 5 | ad2antrr 726 |
. . 3
⊢ (((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ ran 𝐹 = 𝐵) ∧ 𝐼 ∈ 𝑇) → (𝐹 “ 𝐼) ⊆ 𝐵) |
| 7 | 3 | ffnd 6737 |
. . . . . 6
⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝐹 Fn (Base‘𝑅)) |
| 8 | 7 | ad2antrr 726 |
. . . . 5
⊢ (((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ ran 𝐹 = 𝐵) ∧ 𝐼 ∈ 𝑇) → 𝐹 Fn (Base‘𝑅)) |
| 9 | | rhmrcl1 20476 |
. . . . . . 7
⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝑅 ∈ Ring) |
| 10 | 9 | ad2antrr 726 |
. . . . . 6
⊢ (((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ ran 𝐹 = 𝐵) ∧ 𝐼 ∈ 𝑇) → 𝑅 ∈ Ring) |
| 11 | | eqid 2737 |
. . . . . . 7
⊢
(0g‘𝑅) = (0g‘𝑅) |
| 12 | 1, 11 | ring0cl 20264 |
. . . . . 6
⊢ (𝑅 ∈ Ring →
(0g‘𝑅)
∈ (Base‘𝑅)) |
| 13 | 10, 12 | syl 17 |
. . . . 5
⊢ (((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ ran 𝐹 = 𝐵) ∧ 𝐼 ∈ 𝑇) → (0g‘𝑅) ∈ (Base‘𝑅)) |
| 14 | | simpr 484 |
. . . . . 6
⊢ (((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ ran 𝐹 = 𝐵) ∧ 𝐼 ∈ 𝑇) → 𝐼 ∈ 𝑇) |
| 15 | | rhmimaidl.t |
. . . . . . 7
⊢ 𝑇 = (LIdeal‘𝑅) |
| 16 | 15, 11 | lidl0cl 21230 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑇) → (0g‘𝑅) ∈ 𝐼) |
| 17 | 10, 14, 16 | syl2anc 584 |
. . . . 5
⊢ (((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ ran 𝐹 = 𝐵) ∧ 𝐼 ∈ 𝑇) → (0g‘𝑅) ∈ 𝐼) |
| 18 | 8, 13, 17 | fnfvimad 7254 |
. . . 4
⊢ (((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ ran 𝐹 = 𝐵) ∧ 𝐼 ∈ 𝑇) → (𝐹‘(0g‘𝑅)) ∈ (𝐹 “ 𝐼)) |
| 19 | 18 | ne0d 4342 |
. . 3
⊢ (((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ ran 𝐹 = 𝐵) ∧ 𝐼 ∈ 𝑇) → (𝐹 “ 𝐼) ≠ ∅) |
| 20 | | rhmghm 20484 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝐹 ∈ (𝑅 GrpHom 𝑆)) |
| 21 | 20 | ad4antr 732 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐼 ∈ 𝑇) ∧ 𝑗 ∈ 𝐼) ∧ 𝑖 ∈ 𝐼) ∧ 𝑧 ∈ (Base‘𝑅)) → 𝐹 ∈ (𝑅 GrpHom 𝑆)) |
| 22 | 9 | ad4antr 732 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐼 ∈ 𝑇) ∧ 𝑗 ∈ 𝐼) ∧ 𝑖 ∈ 𝐼) ∧ 𝑧 ∈ (Base‘𝑅)) → 𝑅 ∈ Ring) |
| 23 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐼 ∈ 𝑇) ∧ 𝑗 ∈ 𝐼) ∧ 𝑖 ∈ 𝐼) ∧ 𝑧 ∈ (Base‘𝑅)) → 𝑧 ∈ (Base‘𝑅)) |
| 24 | 1, 15 | lidlss 21222 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐼 ∈ 𝑇 → 𝐼 ⊆ (Base‘𝑅)) |
| 25 | 24 | ad4antlr 733 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐼 ∈ 𝑇) ∧ 𝑗 ∈ 𝐼) ∧ 𝑖 ∈ 𝐼) ∧ 𝑧 ∈ (Base‘𝑅)) → 𝐼 ⊆ (Base‘𝑅)) |
| 26 | | simplr 769 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐼 ∈ 𝑇) ∧ 𝑗 ∈ 𝐼) ∧ 𝑖 ∈ 𝐼) ∧ 𝑧 ∈ (Base‘𝑅)) → 𝑖 ∈ 𝐼) |
| 27 | 25, 26 | sseldd 3984 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐼 ∈ 𝑇) ∧ 𝑗 ∈ 𝐼) ∧ 𝑖 ∈ 𝐼) ∧ 𝑧 ∈ (Base‘𝑅)) → 𝑖 ∈ (Base‘𝑅)) |
| 28 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(.r‘𝑅) = (.r‘𝑅) |
| 29 | 1, 28 | ringcl 20247 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑅 ∈ Ring ∧ 𝑧 ∈ (Base‘𝑅) ∧ 𝑖 ∈ (Base‘𝑅)) → (𝑧(.r‘𝑅)𝑖) ∈ (Base‘𝑅)) |
| 30 | 22, 23, 27, 29 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐼 ∈ 𝑇) ∧ 𝑗 ∈ 𝐼) ∧ 𝑖 ∈ 𝐼) ∧ 𝑧 ∈ (Base‘𝑅)) → (𝑧(.r‘𝑅)𝑖) ∈ (Base‘𝑅)) |
| 31 | | simpllr 776 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐼 ∈ 𝑇) ∧ 𝑗 ∈ 𝐼) ∧ 𝑖 ∈ 𝐼) ∧ 𝑧 ∈ (Base‘𝑅)) → 𝑗 ∈ 𝐼) |
| 32 | 25, 31 | sseldd 3984 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐼 ∈ 𝑇) ∧ 𝑗 ∈ 𝐼) ∧ 𝑖 ∈ 𝐼) ∧ 𝑧 ∈ (Base‘𝑅)) → 𝑗 ∈ (Base‘𝑅)) |
| 33 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(+g‘𝑅) = (+g‘𝑅) |
| 34 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(+g‘𝑆) = (+g‘𝑆) |
| 35 | 1, 33, 34 | ghmlin 19239 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐹 ∈ (𝑅 GrpHom 𝑆) ∧ (𝑧(.r‘𝑅)𝑖) ∈ (Base‘𝑅) ∧ 𝑗 ∈ (Base‘𝑅)) → (𝐹‘((𝑧(.r‘𝑅)𝑖)(+g‘𝑅)𝑗)) = ((𝐹‘(𝑧(.r‘𝑅)𝑖))(+g‘𝑆)(𝐹‘𝑗))) |
| 36 | 21, 30, 32, 35 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐼 ∈ 𝑇) ∧ 𝑗 ∈ 𝐼) ∧ 𝑖 ∈ 𝐼) ∧ 𝑧 ∈ (Base‘𝑅)) → (𝐹‘((𝑧(.r‘𝑅)𝑖)(+g‘𝑅)𝑗)) = ((𝐹‘(𝑧(.r‘𝑅)𝑖))(+g‘𝑆)(𝐹‘𝑗))) |
| 37 | | simp-4l 783 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐼 ∈ 𝑇) ∧ 𝑗 ∈ 𝐼) ∧ 𝑖 ∈ 𝐼) ∧ 𝑧 ∈ (Base‘𝑅)) → 𝐹 ∈ (𝑅 RingHom 𝑆)) |
| 38 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(.r‘𝑆) = (.r‘𝑆) |
| 39 | 1, 28, 38 | rhmmul 20486 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝑧 ∈ (Base‘𝑅) ∧ 𝑖 ∈ (Base‘𝑅)) → (𝐹‘(𝑧(.r‘𝑅)𝑖)) = ((𝐹‘𝑧)(.r‘𝑆)(𝐹‘𝑖))) |
| 40 | 37, 23, 27, 39 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐼 ∈ 𝑇) ∧ 𝑗 ∈ 𝐼) ∧ 𝑖 ∈ 𝐼) ∧ 𝑧 ∈ (Base‘𝑅)) → (𝐹‘(𝑧(.r‘𝑅)𝑖)) = ((𝐹‘𝑧)(.r‘𝑆)(𝐹‘𝑖))) |
| 41 | 40 | oveq1d 7446 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐼 ∈ 𝑇) ∧ 𝑗 ∈ 𝐼) ∧ 𝑖 ∈ 𝐼) ∧ 𝑧 ∈ (Base‘𝑅)) → ((𝐹‘(𝑧(.r‘𝑅)𝑖))(+g‘𝑆)(𝐹‘𝑗)) = (((𝐹‘𝑧)(.r‘𝑆)(𝐹‘𝑖))(+g‘𝑆)(𝐹‘𝑗))) |
| 42 | 36, 41 | eqtrd 2777 |
. . . . . . . . . . . . . . . . 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 484 |
. . . . . . . . . . . . 13
⊢
((((((((((((𝐹 ∈
(𝑅 RingHom 𝑆) ∧ ran 𝐹 = 𝐵) ∧ 𝐼 ∈ 𝑇) ∧ 𝑥 ∈ 𝐵) ∧ 𝑎 ∈ (𝐹 “ 𝐼)) ∧ 𝑏 ∈ (𝐹 “ 𝐼)) ∧ 𝑗 ∈ 𝐼) ∧ (𝐹‘𝑗) = 𝑏) ∧ 𝑖 ∈ 𝐼) ∧ (𝐹‘𝑖) = 𝑎) ∧ 𝑧 ∈ (Base‘𝑅)) ∧ (𝐹‘𝑧) = 𝑥) → (𝐹‘𝑧) = 𝑥) |
| 50 | | simpllr 776 |
. . . . . . . . . . . . 13
⊢
((((((((((((𝐹 ∈
(𝑅 RingHom 𝑆) ∧ ran 𝐹 = 𝐵) ∧ 𝐼 ∈ 𝑇) ∧ 𝑥 ∈ 𝐵) ∧ 𝑎 ∈ (𝐹 “ 𝐼)) ∧ 𝑏 ∈ (𝐹 “ 𝐼)) ∧ 𝑗 ∈ 𝐼) ∧ (𝐹‘𝑗) = 𝑏) ∧ 𝑖 ∈ 𝐼) ∧ (𝐹‘𝑖) = 𝑎) ∧ 𝑧 ∈ (Base‘𝑅)) ∧ (𝐹‘𝑧) = 𝑥) → (𝐹‘𝑖) = 𝑎) |
| 51 | 49, 50 | oveq12d 7449 |
. . . . . . . . . . . 12
⊢
((((((((((((𝐹 ∈
(𝑅 RingHom 𝑆) ∧ ran 𝐹 = 𝐵) ∧ 𝐼 ∈ 𝑇) ∧ 𝑥 ∈ 𝐵) ∧ 𝑎 ∈ (𝐹 “ 𝐼)) ∧ 𝑏 ∈ (𝐹 “ 𝐼)) ∧ 𝑗 ∈ 𝐼) ∧ (𝐹‘𝑗) = 𝑏) ∧ 𝑖 ∈ 𝐼) ∧ (𝐹‘𝑖) = 𝑎) ∧ 𝑧 ∈ (Base‘𝑅)) ∧ (𝐹‘𝑧) = 𝑥) → ((𝐹‘𝑧)(.r‘𝑆)(𝐹‘𝑖)) = (𝑥(.r‘𝑆)𝑎)) |
| 52 | | simp-5r 786 |
. . . . . . . . . . . 12
⊢
((((((((((((𝐹 ∈
(𝑅 RingHom 𝑆) ∧ ran 𝐹 = 𝐵) ∧ 𝐼 ∈ 𝑇) ∧ 𝑥 ∈ 𝐵) ∧ 𝑎 ∈ (𝐹 “ 𝐼)) ∧ 𝑏 ∈ (𝐹 “ 𝐼)) ∧ 𝑗 ∈ 𝐼) ∧ (𝐹‘𝑗) = 𝑏) ∧ 𝑖 ∈ 𝐼) ∧ (𝐹‘𝑖) = 𝑎) ∧ 𝑧 ∈ (Base‘𝑅)) ∧ (𝐹‘𝑧) = 𝑥) → (𝐹‘𝑗) = 𝑏) |
| 53 | 51, 52 | oveq12d 7449 |
. . . . . . . . . . 11
⊢
((((((((((((𝐹 ∈
(𝑅 RingHom 𝑆) ∧ ran 𝐹 = 𝐵) ∧ 𝐼 ∈ 𝑇) ∧ 𝑥 ∈ 𝐵) ∧ 𝑎 ∈ (𝐹 “ 𝐼)) ∧ 𝑏 ∈ (𝐹 “ 𝐼)) ∧ 𝑗 ∈ 𝐼) ∧ (𝐹‘𝑗) = 𝑏) ∧ 𝑖 ∈ 𝐼) ∧ (𝐹‘𝑖) = 𝑎) ∧ 𝑧 ∈ (Base‘𝑅)) ∧ (𝐹‘𝑧) = 𝑥) → (((𝐹‘𝑧)(.r‘𝑆)(𝐹‘𝑖))(+g‘𝑆)(𝐹‘𝑗)) = ((𝑥(.r‘𝑆)𝑎)(+g‘𝑆)𝑏)) |
| 54 | 48, 53 | eqtrd 2777 |
. . . . . . . . . 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 21225 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐼 ∈ 𝑇 ↔ (𝐼 ⊆ (Base‘𝑅) ∧ 𝐼 ≠ ∅ ∧ ∀𝑧 ∈ (Base‘𝑅)∀𝑖 ∈ 𝐼 ∀𝑗 ∈ 𝐼 ((𝑧(.r‘𝑅)𝑖)(+g‘𝑅)𝑗) ∈ 𝐼)) |
| 63 | 62 | simp3bi 1148 |
. . . . . . . . . . . . . . . 16
⊢ (𝐼 ∈ 𝑇 → ∀𝑧 ∈ (Base‘𝑅)∀𝑖 ∈ 𝐼 ∀𝑗 ∈ 𝐼 ((𝑧(.r‘𝑅)𝑖)(+g‘𝑅)𝑗) ∈ 𝐼) |
| 64 | 63 | r19.21bi 3251 |
. . . . . . . . . . . . . . 15
⊢ ((𝐼 ∈ 𝑇 ∧ 𝑧 ∈ (Base‘𝑅)) → ∀𝑖 ∈ 𝐼 ∀𝑗 ∈ 𝐼 ((𝑧(.r‘𝑅)𝑖)(+g‘𝑅)𝑗) ∈ 𝐼) |
| 65 | 64 | r19.21bi 3251 |
. . . . . . . . . . . . . 14
⊢ (((𝐼 ∈ 𝑇 ∧ 𝑧 ∈ (Base‘𝑅)) ∧ 𝑖 ∈ 𝐼) → ∀𝑗 ∈ 𝐼 ((𝑧(.r‘𝑅)𝑖)(+g‘𝑅)𝑗) ∈ 𝐼) |
| 66 | 65 | r19.21bi 3251 |
. . . . . . . . . . . . 13
⊢ ((((𝐼 ∈ 𝑇 ∧ 𝑧 ∈ (Base‘𝑅)) ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 ∈ 𝐼) → ((𝑧(.r‘𝑅)𝑖)(+g‘𝑅)𝑗) ∈ 𝐼) |
| 67 | 58, 59, 60, 61, 66 | syl1111anc 841 |
. . . . . . . . . . . 12
⊢
((((((((((((𝐹 ∈
(𝑅 RingHom 𝑆) ∧ ran 𝐹 = 𝐵) ∧ 𝐼 ∈ 𝑇) ∧ 𝑥 ∈ 𝐵) ∧ 𝑎 ∈ (𝐹 “ 𝐼)) ∧ 𝑏 ∈ (𝐹 “ 𝐼)) ∧ 𝑗 ∈ 𝐼) ∧ (𝐹‘𝑗) = 𝑏) ∧ 𝑖 ∈ 𝐼) ∧ (𝐹‘𝑖) = 𝑎) ∧ 𝑧 ∈ (Base‘𝑅)) ∧ (𝐹‘𝑧) = 𝑥) → ((𝑧(.r‘𝑅)𝑖)(+g‘𝑅)𝑗) ∈ 𝐼) |
| 68 | 57, 67 | sseldd 3984 |
. . . . . . . . . . 11
⊢
((((((((((((𝐹 ∈
(𝑅 RingHom 𝑆) ∧ ran 𝐹 = 𝐵) ∧ 𝐼 ∈ 𝑇) ∧ 𝑥 ∈ 𝐵) ∧ 𝑎 ∈ (𝐹 “ 𝐼)) ∧ 𝑏 ∈ (𝐹 “ 𝐼)) ∧ 𝑗 ∈ 𝐼) ∧ (𝐹‘𝑗) = 𝑏) ∧ 𝑖 ∈ 𝐼) ∧ (𝐹‘𝑖) = 𝑎) ∧ 𝑧 ∈ (Base‘𝑅)) ∧ (𝐹‘𝑧) = 𝑥) → ((𝑧(.r‘𝑅)𝑖)(+g‘𝑅)𝑗) ∈ (Base‘𝑅)) |
| 69 | 55, 68, 67 | fnfvimad 7254 |
. . . . . . . . . 10
⊢
((((((((((((𝐹 ∈
(𝑅 RingHom 𝑆) ∧ ran 𝐹 = 𝐵) ∧ 𝐼 ∈ 𝑇) ∧ 𝑥 ∈ 𝐵) ∧ 𝑎 ∈ (𝐹 “ 𝐼)) ∧ 𝑏 ∈ (𝐹 “ 𝐼)) ∧ 𝑗 ∈ 𝐼) ∧ (𝐹‘𝑗) = 𝑏) ∧ 𝑖 ∈ 𝐼) ∧ (𝐹‘𝑖) = 𝑎) ∧ 𝑧 ∈ (Base‘𝑅)) ∧ (𝐹‘𝑧) = 𝑥) → (𝐹‘((𝑧(.r‘𝑅)𝑖)(+g‘𝑅)𝑗)) ∈ (𝐹 “ 𝐼)) |
| 70 | 54, 69 | eqeltrrd 2842 |
. . . . . . . . 9
⊢
((((((((((((𝐹 ∈
(𝑅 RingHom 𝑆) ∧ ran 𝐹 = 𝐵) ∧ 𝐼 ∈ 𝑇) ∧ 𝑥 ∈ 𝐵) ∧ 𝑎 ∈ (𝐹 “ 𝐼)) ∧ 𝑏 ∈ (𝐹 “ 𝐼)) ∧ 𝑗 ∈ 𝐼) ∧ (𝐹‘𝑗) = 𝑏) ∧ 𝑖 ∈ 𝐼) ∧ (𝐹‘𝑖) = 𝑎) ∧ 𝑧 ∈ (Base‘𝑅)) ∧ (𝐹‘𝑧) = 𝑥) → ((𝑥(.r‘𝑆)𝑎)(+g‘𝑆)𝑏) ∈ (𝐹 “ 𝐼)) |
| 71 | 3 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ (((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ ran 𝐹 = 𝐵) ∧ 𝐼 ∈ 𝑇) → 𝐹:(Base‘𝑅)⟶𝐵) |
| 72 | 71 | ffund 6740 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ ran 𝐹 = 𝐵) ∧ 𝐼 ∈ 𝑇) → Fun 𝐹) |
| 73 | 72 | ad7antr 738 |
. . . . . . . . . 10
⊢
((((((((((𝐹 ∈
(𝑅 RingHom 𝑆) ∧ ran 𝐹 = 𝐵) ∧ 𝐼 ∈ 𝑇) ∧ 𝑥 ∈ 𝐵) ∧ 𝑎 ∈ (𝐹 “ 𝐼)) ∧ 𝑏 ∈ (𝐹 “ 𝐼)) ∧ 𝑗 ∈ 𝐼) ∧ (𝐹‘𝑗) = 𝑏) ∧ 𝑖 ∈ 𝐼) ∧ (𝐹‘𝑖) = 𝑎) → Fun 𝐹) |
| 74 | 3 | fdmd 6746 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → dom 𝐹 = (Base‘𝑅)) |
| 75 | 74 | imaeq2d 6078 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → (𝐹 “ dom 𝐹) = (𝐹 “ (Base‘𝑅))) |
| 76 | | imadmrn 6088 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹 “ dom 𝐹) = ran 𝐹 |
| 77 | 75, 76 | eqtr3di 2792 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → (𝐹 “ (Base‘𝑅)) = ran 𝐹) |
| 78 | 77 | eqeq1d 2739 |
. . . . . . . . . . . . . . 15
⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → ((𝐹 “ (Base‘𝑅)) = 𝐵 ↔ ran 𝐹 = 𝐵)) |
| 79 | 78 | biimpar 477 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ ran 𝐹 = 𝐵) → (𝐹 “ (Base‘𝑅)) = 𝐵) |
| 80 | 79 | eleq2d 2827 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ ran 𝐹 = 𝐵) → (𝑥 ∈ (𝐹 “ (Base‘𝑅)) ↔ 𝑥 ∈ 𝐵)) |
| 81 | 80 | biimpar 477 |
. . . . . . . . . . . 12
⊢ (((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ ran 𝐹 = 𝐵) ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ (𝐹 “ (Base‘𝑅))) |
| 82 | 81 | adantlr 715 |
. . . . . . . . . . 11
⊢ ((((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ ran 𝐹 = 𝐵) ∧ 𝐼 ∈ 𝑇) ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ (𝐹 “ (Base‘𝑅))) |
| 83 | 82 | ad6antr 736 |
. . . . . . . . . 10
⊢
((((((((((𝐹 ∈
(𝑅 RingHom 𝑆) ∧ ran 𝐹 = 𝐵) ∧ 𝐼 ∈ 𝑇) ∧ 𝑥 ∈ 𝐵) ∧ 𝑎 ∈ (𝐹 “ 𝐼)) ∧ 𝑏 ∈ (𝐹 “ 𝐼)) ∧ 𝑗 ∈ 𝐼) ∧ (𝐹‘𝑗) = 𝑏) ∧ 𝑖 ∈ 𝐼) ∧ (𝐹‘𝑖) = 𝑎) → 𝑥 ∈ (𝐹 “ (Base‘𝑅))) |
| 84 | | fvelima 6974 |
. . . . . . . . . 10
⊢ ((Fun
𝐹 ∧ 𝑥 ∈ (𝐹 “ (Base‘𝑅))) → ∃𝑧 ∈ (Base‘𝑅)(𝐹‘𝑧) = 𝑥) |
| 85 | 73, 83, 84 | syl2anc 584 |
. . . . . . . . 9
⊢
((((((((((𝐹 ∈
(𝑅 RingHom 𝑆) ∧ ran 𝐹 = 𝐵) ∧ 𝐼 ∈ 𝑇) ∧ 𝑥 ∈ 𝐵) ∧ 𝑎 ∈ (𝐹 “ 𝐼)) ∧ 𝑏 ∈ (𝐹 “ 𝐼)) ∧ 𝑗 ∈ 𝐼) ∧ (𝐹‘𝑗) = 𝑏) ∧ 𝑖 ∈ 𝐼) ∧ (𝐹‘𝑖) = 𝑎) → ∃𝑧 ∈ (Base‘𝑅)(𝐹‘𝑧) = 𝑥) |
| 86 | 70, 85 | r19.29a 3162 |
. . . . . . . 8
⊢
((((((((((𝐹 ∈
(𝑅 RingHom 𝑆) ∧ ran 𝐹 = 𝐵) ∧ 𝐼 ∈ 𝑇) ∧ 𝑥 ∈ 𝐵) ∧ 𝑎 ∈ (𝐹 “ 𝐼)) ∧ 𝑏 ∈ (𝐹 “ 𝐼)) ∧ 𝑗 ∈ 𝐼) ∧ (𝐹‘𝑗) = 𝑏) ∧ 𝑖 ∈ 𝐼) ∧ (𝐹‘𝑖) = 𝑎) → ((𝑥(.r‘𝑆)𝑎)(+g‘𝑆)𝑏) ∈ (𝐹 “ 𝐼)) |
| 87 | 72 | ad5antr 734 |
. . . . . . . . 9
⊢
((((((((𝐹 ∈
(𝑅 RingHom 𝑆) ∧ ran 𝐹 = 𝐵) ∧ 𝐼 ∈ 𝑇) ∧ 𝑥 ∈ 𝐵) ∧ 𝑎 ∈ (𝐹 “ 𝐼)) ∧ 𝑏 ∈ (𝐹 “ 𝐼)) ∧ 𝑗 ∈ 𝐼) ∧ (𝐹‘𝑗) = 𝑏) → Fun 𝐹) |
| 88 | | simp-4r 784 |
. . . . . . . . 9
⊢
((((((((𝐹 ∈
(𝑅 RingHom 𝑆) ∧ ran 𝐹 = 𝐵) ∧ 𝐼 ∈ 𝑇) ∧ 𝑥 ∈ 𝐵) ∧ 𝑎 ∈ (𝐹 “ 𝐼)) ∧ 𝑏 ∈ (𝐹 “ 𝐼)) ∧ 𝑗 ∈ 𝐼) ∧ (𝐹‘𝑗) = 𝑏) → 𝑎 ∈ (𝐹 “ 𝐼)) |
| 89 | | fvelima 6974 |
. . . . . . . . 9
⊢ ((Fun
𝐹 ∧ 𝑎 ∈ (𝐹 “ 𝐼)) → ∃𝑖 ∈ 𝐼 (𝐹‘𝑖) = 𝑎) |
| 90 | 87, 88, 89 | syl2anc 584 |
. . . . . . . 8
⊢
((((((((𝐹 ∈
(𝑅 RingHom 𝑆) ∧ ran 𝐹 = 𝐵) ∧ 𝐼 ∈ 𝑇) ∧ 𝑥 ∈ 𝐵) ∧ 𝑎 ∈ (𝐹 “ 𝐼)) ∧ 𝑏 ∈ (𝐹 “ 𝐼)) ∧ 𝑗 ∈ 𝐼) ∧ (𝐹‘𝑗) = 𝑏) → ∃𝑖 ∈ 𝐼 (𝐹‘𝑖) = 𝑎) |
| 91 | 86, 90 | r19.29a 3162 |
. . . . . . 7
⊢
((((((((𝐹 ∈
(𝑅 RingHom 𝑆) ∧ ran 𝐹 = 𝐵) ∧ 𝐼 ∈ 𝑇) ∧ 𝑥 ∈ 𝐵) ∧ 𝑎 ∈ (𝐹 “ 𝐼)) ∧ 𝑏 ∈ (𝐹 “ 𝐼)) ∧ 𝑗 ∈ 𝐼) ∧ (𝐹‘𝑗) = 𝑏) → ((𝑥(.r‘𝑆)𝑎)(+g‘𝑆)𝑏) ∈ (𝐹 “ 𝐼)) |
| 92 | 72 | ad3antrrr 730 |
. . . . . . . 8
⊢
((((((𝐹 ∈
(𝑅 RingHom 𝑆) ∧ ran 𝐹 = 𝐵) ∧ 𝐼 ∈ 𝑇) ∧ 𝑥 ∈ 𝐵) ∧ 𝑎 ∈ (𝐹 “ 𝐼)) ∧ 𝑏 ∈ (𝐹 “ 𝐼)) → Fun 𝐹) |
| 93 | | simpr 484 |
. . . . . . . 8
⊢
((((((𝐹 ∈
(𝑅 RingHom 𝑆) ∧ ran 𝐹 = 𝐵) ∧ 𝐼 ∈ 𝑇) ∧ 𝑥 ∈ 𝐵) ∧ 𝑎 ∈ (𝐹 “ 𝐼)) ∧ 𝑏 ∈ (𝐹 “ 𝐼)) → 𝑏 ∈ (𝐹 “ 𝐼)) |
| 94 | | fvelima 6974 |
. . . . . . . 8
⊢ ((Fun
𝐹 ∧ 𝑏 ∈ (𝐹 “ 𝐼)) → ∃𝑗 ∈ 𝐼 (𝐹‘𝑗) = 𝑏) |
| 95 | 92, 93, 94 | syl2anc 584 |
. . . . . . 7
⊢
((((((𝐹 ∈
(𝑅 RingHom 𝑆) ∧ ran 𝐹 = 𝐵) ∧ 𝐼 ∈ 𝑇) ∧ 𝑥 ∈ 𝐵) ∧ 𝑎 ∈ (𝐹 “ 𝐼)) ∧ 𝑏 ∈ (𝐹 “ 𝐼)) → ∃𝑗 ∈ 𝐼 (𝐹‘𝑗) = 𝑏) |
| 96 | 91, 95 | r19.29a 3162 |
. . . . . 6
⊢
((((((𝐹 ∈
(𝑅 RingHom 𝑆) ∧ ran 𝐹 = 𝐵) ∧ 𝐼 ∈ 𝑇) ∧ 𝑥 ∈ 𝐵) ∧ 𝑎 ∈ (𝐹 “ 𝐼)) ∧ 𝑏 ∈ (𝐹 “ 𝐼)) → ((𝑥(.r‘𝑆)𝑎)(+g‘𝑆)𝑏) ∈ (𝐹 “ 𝐼)) |
| 97 | 96 | anasss 466 |
. . . . 5
⊢
(((((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ ran 𝐹 = 𝐵) ∧ 𝐼 ∈ 𝑇) ∧ 𝑥 ∈ 𝐵) ∧ (𝑎 ∈ (𝐹 “ 𝐼) ∧ 𝑏 ∈ (𝐹 “ 𝐼))) → ((𝑥(.r‘𝑆)𝑎)(+g‘𝑆)𝑏) ∈ (𝐹 “ 𝐼)) |
| 98 | 97 | ralrimivva 3202 |
. . . 4
⊢ ((((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ ran 𝐹 = 𝐵) ∧ 𝐼 ∈ 𝑇) ∧ 𝑥 ∈ 𝐵) → ∀𝑎 ∈ (𝐹 “ 𝐼)∀𝑏 ∈ (𝐹 “ 𝐼)((𝑥(.r‘𝑆)𝑎)(+g‘𝑆)𝑏) ∈ (𝐹 “ 𝐼)) |
| 99 | 98 | ralrimiva 3146 |
. . 3
⊢ (((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ ran 𝐹 = 𝐵) ∧ 𝐼 ∈ 𝑇) → ∀𝑥 ∈ 𝐵 ∀𝑎 ∈ (𝐹 “ 𝐼)∀𝑏 ∈ (𝐹 “ 𝐼)((𝑥(.r‘𝑆)𝑎)(+g‘𝑆)𝑏) ∈ (𝐹 “ 𝐼)) |
| 100 | | rhmimaidl.u |
. . . 4
⊢ 𝑈 = (LIdeal‘𝑆) |
| 101 | 100, 2, 34, 38 | islidl 21225 |
. . 3
⊢ ((𝐹 “ 𝐼) ∈ 𝑈 ↔ ((𝐹 “ 𝐼) ⊆ 𝐵 ∧ (𝐹 “ 𝐼) ≠ ∅ ∧ ∀𝑥 ∈ 𝐵 ∀𝑎 ∈ (𝐹 “ 𝐼)∀𝑏 ∈ (𝐹 “ 𝐼)((𝑥(.r‘𝑆)𝑎)(+g‘𝑆)𝑏) ∈ (𝐹 “ 𝐼))) |
| 102 | 6, 19, 99, 101 | syl3anbrc 1344 |
. 2
⊢ (((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ ran 𝐹 = 𝐵) ∧ 𝐼 ∈ 𝑇) → (𝐹 “ 𝐼) ∈ 𝑈) |
| 103 | 102 | 3impa 1110 |
1
⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ ran 𝐹 = 𝐵 ∧ 𝐼 ∈ 𝑇) → (𝐹 “ 𝐼) ∈ 𝑈) |