Proof of Theorem isrhm2d
Step | Hyp | Ref
| Expression |
1 | | isrhmd.r |
. 2
⊢ (𝜑 → 𝑅 ∈ Ring) |
2 | | isrhmd.s |
. 2
⊢ (𝜑 → 𝑆 ∈ Ring) |
3 | | isrhm2d.f |
. . 3
⊢ (𝜑 → 𝐹 ∈ (𝑅 GrpHom 𝑆)) |
4 | | eqid 2193 |
. . . . . 6
⊢
(mulGrp‘𝑅) =
(mulGrp‘𝑅) |
5 | 4 | ringmgp 13498 |
. . . . 5
⊢ (𝑅 ∈ Ring →
(mulGrp‘𝑅) ∈
Mnd) |
6 | 1, 5 | syl 14 |
. . . 4
⊢ (𝜑 → (mulGrp‘𝑅) ∈ Mnd) |
7 | | eqid 2193 |
. . . . . 6
⊢
(mulGrp‘𝑆) =
(mulGrp‘𝑆) |
8 | 7 | ringmgp 13498 |
. . . . 5
⊢ (𝑆 ∈ Ring →
(mulGrp‘𝑆) ∈
Mnd) |
9 | 2, 8 | syl 14 |
. . . 4
⊢ (𝜑 → (mulGrp‘𝑆) ∈ Mnd) |
10 | | isrhmd.b |
. . . . . . . 8
⊢ 𝐵 = (Base‘𝑅) |
11 | | eqid 2193 |
. . . . . . . 8
⊢
(Base‘𝑆) =
(Base‘𝑆) |
12 | 10, 11 | ghmf 13317 |
. . . . . . 7
⊢ (𝐹 ∈ (𝑅 GrpHom 𝑆) → 𝐹:𝐵⟶(Base‘𝑆)) |
13 | 3, 12 | syl 14 |
. . . . . 6
⊢ (𝜑 → 𝐹:𝐵⟶(Base‘𝑆)) |
14 | 4, 10 | mgpbasg 13422 |
. . . . . . . 8
⊢ (𝑅 ∈ Ring → 𝐵 =
(Base‘(mulGrp‘𝑅))) |
15 | 1, 14 | syl 14 |
. . . . . . 7
⊢ (𝜑 → 𝐵 = (Base‘(mulGrp‘𝑅))) |
16 | 7, 11 | mgpbasg 13422 |
. . . . . . . 8
⊢ (𝑆 ∈ Ring →
(Base‘𝑆) =
(Base‘(mulGrp‘𝑆))) |
17 | 2, 16 | syl 14 |
. . . . . . 7
⊢ (𝜑 → (Base‘𝑆) =
(Base‘(mulGrp‘𝑆))) |
18 | 15, 17 | feq23d 5399 |
. . . . . 6
⊢ (𝜑 → (𝐹:𝐵⟶(Base‘𝑆) ↔ 𝐹:(Base‘(mulGrp‘𝑅))⟶(Base‘(mulGrp‘𝑆)))) |
19 | 13, 18 | mpbid 147 |
. . . . 5
⊢ (𝜑 → 𝐹:(Base‘(mulGrp‘𝑅))⟶(Base‘(mulGrp‘𝑆))) |
20 | | isrhmd.ht |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐹‘(𝑥 · 𝑦)) = ((𝐹‘𝑥) × (𝐹‘𝑦))) |
21 | 20 | ralrimivva 2576 |
. . . . . 6
⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝐹‘(𝑥 · 𝑦)) = ((𝐹‘𝑥) × (𝐹‘𝑦))) |
22 | | isrhmd.t |
. . . . . . . . . . . . 13
⊢ · =
(.r‘𝑅) |
23 | 4, 22 | mgpplusgg 13420 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ Ring → · =
(+g‘(mulGrp‘𝑅))) |
24 | 1, 23 | syl 14 |
. . . . . . . . . . 11
⊢ (𝜑 → · =
(+g‘(mulGrp‘𝑅))) |
25 | 24 | oveqd 5935 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 · 𝑦) = (𝑥(+g‘(mulGrp‘𝑅))𝑦)) |
26 | 25 | fveq2d 5558 |
. . . . . . . . 9
⊢ (𝜑 → (𝐹‘(𝑥 · 𝑦)) = (𝐹‘(𝑥(+g‘(mulGrp‘𝑅))𝑦))) |
27 | | isrhmd.u |
. . . . . . . . . . . 12
⊢ × =
(.r‘𝑆) |
28 | 7, 27 | mgpplusgg 13420 |
. . . . . . . . . . 11
⊢ (𝑆 ∈ Ring → × =
(+g‘(mulGrp‘𝑆))) |
29 | 2, 28 | syl 14 |
. . . . . . . . . 10
⊢ (𝜑 → × =
(+g‘(mulGrp‘𝑆))) |
30 | 29 | oveqd 5935 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐹‘𝑥) × (𝐹‘𝑦)) = ((𝐹‘𝑥)(+g‘(mulGrp‘𝑆))(𝐹‘𝑦))) |
31 | 26, 30 | eqeq12d 2208 |
. . . . . . . 8
⊢ (𝜑 → ((𝐹‘(𝑥 · 𝑦)) = ((𝐹‘𝑥) × (𝐹‘𝑦)) ↔ (𝐹‘(𝑥(+g‘(mulGrp‘𝑅))𝑦)) = ((𝐹‘𝑥)(+g‘(mulGrp‘𝑆))(𝐹‘𝑦)))) |
32 | 15, 31 | raleqbidv 2706 |
. . . . . . 7
⊢ (𝜑 → (∀𝑦 ∈ 𝐵 (𝐹‘(𝑥 · 𝑦)) = ((𝐹‘𝑥) × (𝐹‘𝑦)) ↔ ∀𝑦 ∈ (Base‘(mulGrp‘𝑅))(𝐹‘(𝑥(+g‘(mulGrp‘𝑅))𝑦)) = ((𝐹‘𝑥)(+g‘(mulGrp‘𝑆))(𝐹‘𝑦)))) |
33 | 15, 32 | raleqbidv 2706 |
. . . . . 6
⊢ (𝜑 → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝐹‘(𝑥 · 𝑦)) = ((𝐹‘𝑥) × (𝐹‘𝑦)) ↔ ∀𝑥 ∈ (Base‘(mulGrp‘𝑅))∀𝑦 ∈ (Base‘(mulGrp‘𝑅))(𝐹‘(𝑥(+g‘(mulGrp‘𝑅))𝑦)) = ((𝐹‘𝑥)(+g‘(mulGrp‘𝑆))(𝐹‘𝑦)))) |
34 | 21, 33 | mpbid 147 |
. . . . 5
⊢ (𝜑 → ∀𝑥 ∈ (Base‘(mulGrp‘𝑅))∀𝑦 ∈ (Base‘(mulGrp‘𝑅))(𝐹‘(𝑥(+g‘(mulGrp‘𝑅))𝑦)) = ((𝐹‘𝑥)(+g‘(mulGrp‘𝑆))(𝐹‘𝑦))) |
35 | | isrhmd.ho |
. . . . . 6
⊢ (𝜑 → (𝐹‘ 1 ) = 𝑁) |
36 | | isrhmd.o |
. . . . . . . . 9
⊢ 1 =
(1r‘𝑅) |
37 | 4, 36 | ringidvalg 13457 |
. . . . . . . 8
⊢ (𝑅 ∈ Ring → 1 =
(0g‘(mulGrp‘𝑅))) |
38 | 1, 37 | syl 14 |
. . . . . . 7
⊢ (𝜑 → 1 =
(0g‘(mulGrp‘𝑅))) |
39 | 38 | fveq2d 5558 |
. . . . . 6
⊢ (𝜑 → (𝐹‘ 1 ) = (𝐹‘(0g‘(mulGrp‘𝑅)))) |
40 | | isrhmd.n |
. . . . . . . 8
⊢ 𝑁 = (1r‘𝑆) |
41 | 7, 40 | ringidvalg 13457 |
. . . . . . 7
⊢ (𝑆 ∈ Ring → 𝑁 =
(0g‘(mulGrp‘𝑆))) |
42 | 2, 41 | syl 14 |
. . . . . 6
⊢ (𝜑 → 𝑁 = (0g‘(mulGrp‘𝑆))) |
43 | 35, 39, 42 | 3eqtr3d 2234 |
. . . . 5
⊢ (𝜑 → (𝐹‘(0g‘(mulGrp‘𝑅))) =
(0g‘(mulGrp‘𝑆))) |
44 | 19, 34, 43 | 3jca 1179 |
. . . 4
⊢ (𝜑 → (𝐹:(Base‘(mulGrp‘𝑅))⟶(Base‘(mulGrp‘𝑆)) ∧ ∀𝑥 ∈
(Base‘(mulGrp‘𝑅))∀𝑦 ∈ (Base‘(mulGrp‘𝑅))(𝐹‘(𝑥(+g‘(mulGrp‘𝑅))𝑦)) = ((𝐹‘𝑥)(+g‘(mulGrp‘𝑆))(𝐹‘𝑦)) ∧ (𝐹‘(0g‘(mulGrp‘𝑅))) =
(0g‘(mulGrp‘𝑆)))) |
45 | | eqid 2193 |
. . . . 5
⊢
(Base‘(mulGrp‘𝑅)) = (Base‘(mulGrp‘𝑅)) |
46 | | eqid 2193 |
. . . . 5
⊢
(Base‘(mulGrp‘𝑆)) = (Base‘(mulGrp‘𝑆)) |
47 | | eqid 2193 |
. . . . 5
⊢
(+g‘(mulGrp‘𝑅)) =
(+g‘(mulGrp‘𝑅)) |
48 | | eqid 2193 |
. . . . 5
⊢
(+g‘(mulGrp‘𝑆)) =
(+g‘(mulGrp‘𝑆)) |
49 | | eqid 2193 |
. . . . 5
⊢
(0g‘(mulGrp‘𝑅)) =
(0g‘(mulGrp‘𝑅)) |
50 | | eqid 2193 |
. . . . 5
⊢
(0g‘(mulGrp‘𝑆)) =
(0g‘(mulGrp‘𝑆)) |
51 | 45, 46, 47, 48, 49, 50 | ismhm 13033 |
. . . 4
⊢ (𝐹 ∈ ((mulGrp‘𝑅) MndHom (mulGrp‘𝑆)) ↔ (((mulGrp‘𝑅) ∈ Mnd ∧
(mulGrp‘𝑆) ∈
Mnd) ∧ (𝐹:(Base‘(mulGrp‘𝑅))⟶(Base‘(mulGrp‘𝑆)) ∧ ∀𝑥 ∈
(Base‘(mulGrp‘𝑅))∀𝑦 ∈ (Base‘(mulGrp‘𝑅))(𝐹‘(𝑥(+g‘(mulGrp‘𝑅))𝑦)) = ((𝐹‘𝑥)(+g‘(mulGrp‘𝑆))(𝐹‘𝑦)) ∧ (𝐹‘(0g‘(mulGrp‘𝑅))) =
(0g‘(mulGrp‘𝑆))))) |
52 | 6, 9, 44, 51 | syl21anbrc 1184 |
. . 3
⊢ (𝜑 → 𝐹 ∈ ((mulGrp‘𝑅) MndHom (mulGrp‘𝑆))) |
53 | 3, 52 | jca 306 |
. 2
⊢ (𝜑 → (𝐹 ∈ (𝑅 GrpHom 𝑆) ∧ 𝐹 ∈ ((mulGrp‘𝑅) MndHom (mulGrp‘𝑆)))) |
54 | 4, 7 | isrhm 13654 |
. 2
⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) ↔ ((𝑅 ∈ Ring ∧ 𝑆 ∈ Ring) ∧ (𝐹 ∈ (𝑅 GrpHom 𝑆) ∧ 𝐹 ∈ ((mulGrp‘𝑅) MndHom (mulGrp‘𝑆))))) |
55 | 1, 2, 53, 54 | syl21anbrc 1184 |
1
⊢ (𝜑 → 𝐹 ∈ (𝑅 RingHom 𝑆)) |