Step | Hyp | Ref
| Expression |
1 | | rhmghm 20422 |
. . 3
⊢ (𝐹 ∈ (𝑀 RingHom 𝑁) → 𝐹 ∈ (𝑀 GrpHom 𝑁)) |
2 | | subrngsubg 20488 |
. . 3
⊢ (𝑋 ∈ (SubRng‘𝑀) → 𝑋 ∈ (SubGrp‘𝑀)) |
3 | | ghmima 19190 |
. . 3
⊢ ((𝐹 ∈ (𝑀 GrpHom 𝑁) ∧ 𝑋 ∈ (SubGrp‘𝑀)) → (𝐹 “ 𝑋) ∈ (SubGrp‘𝑁)) |
4 | 1, 2, 3 | syl2an 594 |
. 2
⊢ ((𝐹 ∈ (𝑀 RingHom 𝑁) ∧ 𝑋 ∈ (SubRng‘𝑀)) → (𝐹 “ 𝑋) ∈ (SubGrp‘𝑁)) |
5 | | eqid 2725 |
. . . 4
⊢
(mulGrp‘𝑀) =
(mulGrp‘𝑀) |
6 | | eqid 2725 |
. . . 4
⊢
(mulGrp‘𝑁) =
(mulGrp‘𝑁) |
7 | 5, 6 | rhmmhm 20417 |
. . 3
⊢ (𝐹 ∈ (𝑀 RingHom 𝑁) → 𝐹 ∈ ((mulGrp‘𝑀) MndHom (mulGrp‘𝑁))) |
8 | | simpl 481 |
. . . . 5
⊢ ((𝐹 ∈ ((mulGrp‘𝑀) MndHom (mulGrp‘𝑁)) ∧ 𝑋 ∈ (SubRng‘𝑀)) → 𝐹 ∈ ((mulGrp‘𝑀) MndHom (mulGrp‘𝑁))) |
9 | | eqid 2725 |
. . . . . . . . 9
⊢
(Base‘𝑀) =
(Base‘𝑀) |
10 | 5, 9 | mgpbas 20079 |
. . . . . . . 8
⊢
(Base‘𝑀) =
(Base‘(mulGrp‘𝑀)) |
11 | 10 | eqcomi 2734 |
. . . . . . 7
⊢
(Base‘(mulGrp‘𝑀)) = (Base‘𝑀) |
12 | 11 | subrngss 20484 |
. . . . . 6
⊢ (𝑋 ∈ (SubRng‘𝑀) → 𝑋 ⊆ (Base‘(mulGrp‘𝑀))) |
13 | 12 | adantl 480 |
. . . . 5
⊢ ((𝐹 ∈ ((mulGrp‘𝑀) MndHom (mulGrp‘𝑁)) ∧ 𝑋 ∈ (SubRng‘𝑀)) → 𝑋 ⊆ (Base‘(mulGrp‘𝑀))) |
14 | | eqidd 2726 |
. . . . 5
⊢ ((𝐹 ∈ ((mulGrp‘𝑀) MndHom (mulGrp‘𝑁)) ∧ 𝑋 ∈ (SubRng‘𝑀)) →
(+g‘(mulGrp‘𝑀)) =
(+g‘(mulGrp‘𝑀))) |
15 | | eqidd 2726 |
. . . . 5
⊢ ((𝐹 ∈ ((mulGrp‘𝑀) MndHom (mulGrp‘𝑁)) ∧ 𝑋 ∈ (SubRng‘𝑀)) →
(+g‘(mulGrp‘𝑁)) =
(+g‘(mulGrp‘𝑁))) |
16 | | eqid 2725 |
. . . . . . . . 9
⊢
(.r‘𝑀) = (.r‘𝑀) |
17 | 5, 16 | mgpplusg 20077 |
. . . . . . . 8
⊢
(.r‘𝑀) = (+g‘(mulGrp‘𝑀)) |
18 | 17 | eqcomi 2734 |
. . . . . . 7
⊢
(+g‘(mulGrp‘𝑀)) = (.r‘𝑀) |
19 | 18 | subrngmcl 20493 |
. . . . . 6
⊢ ((𝑋 ∈ (SubRng‘𝑀) ∧ 𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋) → (𝑧(+g‘(mulGrp‘𝑀))𝑥) ∈ 𝑋) |
20 | 19 | 3adant1l 1173 |
. . . . 5
⊢ (((𝐹 ∈ ((mulGrp‘𝑀) MndHom (mulGrp‘𝑁)) ∧ 𝑋 ∈ (SubRng‘𝑀)) ∧ 𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋) → (𝑧(+g‘(mulGrp‘𝑀))𝑥) ∈ 𝑋) |
21 | 8, 13, 14, 15, 20 | mhmimalem 18775 |
. . . 4
⊢ ((𝐹 ∈ ((mulGrp‘𝑀) MndHom (mulGrp‘𝑁)) ∧ 𝑋 ∈ (SubRng‘𝑀)) → ∀𝑥 ∈ (𝐹 “ 𝑋)∀𝑦 ∈ (𝐹 “ 𝑋)(𝑥(+g‘(mulGrp‘𝑁))𝑦) ∈ (𝐹 “ 𝑋)) |
22 | | eqid 2725 |
. . . . . . . . 9
⊢
(.r‘𝑁) = (.r‘𝑁) |
23 | 6, 22 | mgpplusg 20077 |
. . . . . . . 8
⊢
(.r‘𝑁) = (+g‘(mulGrp‘𝑁)) |
24 | 23 | eqcomi 2734 |
. . . . . . 7
⊢
(+g‘(mulGrp‘𝑁)) = (.r‘𝑁) |
25 | 24 | oveqi 7426 |
. . . . . 6
⊢ (𝑥(+g‘(mulGrp‘𝑁))𝑦) = (𝑥(.r‘𝑁)𝑦) |
26 | 25 | eleq1i 2816 |
. . . . 5
⊢ ((𝑥(+g‘(mulGrp‘𝑁))𝑦) ∈ (𝐹 “ 𝑋) ↔ (𝑥(.r‘𝑁)𝑦) ∈ (𝐹 “ 𝑋)) |
27 | 26 | 2ralbii 3118 |
. . . 4
⊢
(∀𝑥 ∈
(𝐹 “ 𝑋)∀𝑦 ∈ (𝐹 “ 𝑋)(𝑥(+g‘(mulGrp‘𝑁))𝑦) ∈ (𝐹 “ 𝑋) ↔ ∀𝑥 ∈ (𝐹 “ 𝑋)∀𝑦 ∈ (𝐹 “ 𝑋)(𝑥(.r‘𝑁)𝑦) ∈ (𝐹 “ 𝑋)) |
28 | 21, 27 | sylib 217 |
. . 3
⊢ ((𝐹 ∈ ((mulGrp‘𝑀) MndHom (mulGrp‘𝑁)) ∧ 𝑋 ∈ (SubRng‘𝑀)) → ∀𝑥 ∈ (𝐹 “ 𝑋)∀𝑦 ∈ (𝐹 “ 𝑋)(𝑥(.r‘𝑁)𝑦) ∈ (𝐹 “ 𝑋)) |
29 | 7, 28 | sylan 578 |
. 2
⊢ ((𝐹 ∈ (𝑀 RingHom 𝑁) ∧ 𝑋 ∈ (SubRng‘𝑀)) → ∀𝑥 ∈ (𝐹 “ 𝑋)∀𝑦 ∈ (𝐹 “ 𝑋)(𝑥(.r‘𝑁)𝑦) ∈ (𝐹 “ 𝑋)) |
30 | | rhmrcl2 20415 |
. . . . 5
⊢ (𝐹 ∈ (𝑀 RingHom 𝑁) → 𝑁 ∈ Ring) |
31 | | ringrng 20220 |
. . . . 5
⊢ (𝑁 ∈ Ring → 𝑁 ∈ Rng) |
32 | 30, 31 | syl 17 |
. . . 4
⊢ (𝐹 ∈ (𝑀 RingHom 𝑁) → 𝑁 ∈ Rng) |
33 | 32 | adantr 479 |
. . 3
⊢ ((𝐹 ∈ (𝑀 RingHom 𝑁) ∧ 𝑋 ∈ (SubRng‘𝑀)) → 𝑁 ∈ Rng) |
34 | | eqid 2725 |
. . . 4
⊢
(Base‘𝑁) =
(Base‘𝑁) |
35 | 34, 22 | issubrng2 20494 |
. . 3
⊢ (𝑁 ∈ Rng → ((𝐹 “ 𝑋) ∈ (SubRng‘𝑁) ↔ ((𝐹 “ 𝑋) ∈ (SubGrp‘𝑁) ∧ ∀𝑥 ∈ (𝐹 “ 𝑋)∀𝑦 ∈ (𝐹 “ 𝑋)(𝑥(.r‘𝑁)𝑦) ∈ (𝐹 “ 𝑋)))) |
36 | 33, 35 | syl 17 |
. 2
⊢ ((𝐹 ∈ (𝑀 RingHom 𝑁) ∧ 𝑋 ∈ (SubRng‘𝑀)) → ((𝐹 “ 𝑋) ∈ (SubRng‘𝑁) ↔ ((𝐹 “ 𝑋) ∈ (SubGrp‘𝑁) ∧ ∀𝑥 ∈ (𝐹 “ 𝑋)∀𝑦 ∈ (𝐹 “ 𝑋)(𝑥(.r‘𝑁)𝑦) ∈ (𝐹 “ 𝑋)))) |
37 | 4, 29, 36 | mpbir2and 711 |
1
⊢ ((𝐹 ∈ (𝑀 RingHom 𝑁) ∧ 𝑋 ∈ (SubRng‘𝑀)) → (𝐹 “ 𝑋) ∈ (SubRng‘𝑁)) |