Step | Hyp | Ref
| Expression |
1 | | pwsco2rhm.f |
. . . . 5
⊢ (𝜑 → 𝐹 ∈ (𝑅 RingHom 𝑆)) |
2 | | rhmrcl1 18719 |
. . . . 5
⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝑅 ∈ Ring) |
3 | 1, 2 | syl 17 |
. . . 4
⊢ (𝜑 → 𝑅 ∈ Ring) |
4 | | pwsco2rhm.a |
. . . 4
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
5 | | pwsco2rhm.y |
. . . . 5
⊢ 𝑌 = (𝑅 ↑s 𝐴) |
6 | 5 | pwsring 18615 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐴 ∈ 𝑉) → 𝑌 ∈ Ring) |
7 | 3, 4, 6 | syl2anc 693 |
. . 3
⊢ (𝜑 → 𝑌 ∈ Ring) |
8 | | rhmrcl2 18720 |
. . . . 5
⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝑆 ∈ Ring) |
9 | 1, 8 | syl 17 |
. . . 4
⊢ (𝜑 → 𝑆 ∈ Ring) |
10 | | pwsco2rhm.z |
. . . . 5
⊢ 𝑍 = (𝑆 ↑s 𝐴) |
11 | 10 | pwsring 18615 |
. . . 4
⊢ ((𝑆 ∈ Ring ∧ 𝐴 ∈ 𝑉) → 𝑍 ∈ Ring) |
12 | 9, 4, 11 | syl2anc 693 |
. . 3
⊢ (𝜑 → 𝑍 ∈ Ring) |
13 | 7, 12 | jca 554 |
. 2
⊢ (𝜑 → (𝑌 ∈ Ring ∧ 𝑍 ∈ Ring)) |
14 | | pwsco2rhm.b |
. . . . 5
⊢ 𝐵 = (Base‘𝑌) |
15 | | rhmghm 18725 |
. . . . . . 7
⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝐹 ∈ (𝑅 GrpHom 𝑆)) |
16 | 1, 15 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐹 ∈ (𝑅 GrpHom 𝑆)) |
17 | | ghmmhm 17670 |
. . . . . 6
⊢ (𝐹 ∈ (𝑅 GrpHom 𝑆) → 𝐹 ∈ (𝑅 MndHom 𝑆)) |
18 | 16, 17 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝐹 ∈ (𝑅 MndHom 𝑆)) |
19 | 5, 10, 14, 4, 18 | pwsco2mhm 17371 |
. . . 4
⊢ (𝜑 → (𝑔 ∈ 𝐵 ↦ (𝐹 ∘ 𝑔)) ∈ (𝑌 MndHom 𝑍)) |
20 | | ringgrp 18552 |
. . . . . 6
⊢ (𝑌 ∈ Ring → 𝑌 ∈ Grp) |
21 | 7, 20 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑌 ∈ Grp) |
22 | | ringgrp 18552 |
. . . . . 6
⊢ (𝑍 ∈ Ring → 𝑍 ∈ Grp) |
23 | 12, 22 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑍 ∈ Grp) |
24 | | ghmmhmb 17671 |
. . . . 5
⊢ ((𝑌 ∈ Grp ∧ 𝑍 ∈ Grp) → (𝑌 GrpHom 𝑍) = (𝑌 MndHom 𝑍)) |
25 | 21, 23, 24 | syl2anc 693 |
. . . 4
⊢ (𝜑 → (𝑌 GrpHom 𝑍) = (𝑌 MndHom 𝑍)) |
26 | 19, 25 | eleqtrrd 2704 |
. . 3
⊢ (𝜑 → (𝑔 ∈ 𝐵 ↦ (𝐹 ∘ 𝑔)) ∈ (𝑌 GrpHom 𝑍)) |
27 | | eqid 2622 |
. . . . 5
⊢
((mulGrp‘𝑅)
↑s 𝐴) = ((mulGrp‘𝑅) ↑s 𝐴) |
28 | | eqid 2622 |
. . . . 5
⊢
((mulGrp‘𝑆)
↑s 𝐴) = ((mulGrp‘𝑆) ↑s 𝐴) |
29 | | eqid 2622 |
. . . . 5
⊢
(Base‘((mulGrp‘𝑅) ↑s 𝐴)) =
(Base‘((mulGrp‘𝑅) ↑s 𝐴)) |
30 | | eqid 2622 |
. . . . . . 7
⊢
(mulGrp‘𝑅) =
(mulGrp‘𝑅) |
31 | | eqid 2622 |
. . . . . . 7
⊢
(mulGrp‘𝑆) =
(mulGrp‘𝑆) |
32 | 30, 31 | rhmmhm 18722 |
. . . . . 6
⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝐹 ∈ ((mulGrp‘𝑅) MndHom (mulGrp‘𝑆))) |
33 | 1, 32 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝐹 ∈ ((mulGrp‘𝑅) MndHom (mulGrp‘𝑆))) |
34 | 27, 28, 29, 4, 33 | pwsco2mhm 17371 |
. . . 4
⊢ (𝜑 → (𝑔 ∈ (Base‘((mulGrp‘𝑅) ↑s
𝐴)) ↦ (𝐹 ∘ 𝑔)) ∈ (((mulGrp‘𝑅) ↑s 𝐴) MndHom ((mulGrp‘𝑆) ↑s
𝐴))) |
35 | | eqid 2622 |
. . . . . . . . 9
⊢
(Base‘𝑅) =
(Base‘𝑅) |
36 | 5, 35 | pwsbas 16147 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ 𝐴 ∈ 𝑉) → ((Base‘𝑅) ↑𝑚 𝐴) = (Base‘𝑌)) |
37 | 3, 4, 36 | syl2anc 693 |
. . . . . . 7
⊢ (𝜑 → ((Base‘𝑅) ↑𝑚
𝐴) = (Base‘𝑌)) |
38 | 37, 14 | syl6eqr 2674 |
. . . . . 6
⊢ (𝜑 → ((Base‘𝑅) ↑𝑚
𝐴) = 𝐵) |
39 | 30 | ringmgp 18553 |
. . . . . . . 8
⊢ (𝑅 ∈ Ring →
(mulGrp‘𝑅) ∈
Mnd) |
40 | 3, 39 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (mulGrp‘𝑅) ∈ Mnd) |
41 | 30, 35 | mgpbas 18495 |
. . . . . . . 8
⊢
(Base‘𝑅) =
(Base‘(mulGrp‘𝑅)) |
42 | 27, 41 | pwsbas 16147 |
. . . . . . 7
⊢
(((mulGrp‘𝑅)
∈ Mnd ∧ 𝐴 ∈
𝑉) →
((Base‘𝑅)
↑𝑚 𝐴) = (Base‘((mulGrp‘𝑅) ↑s
𝐴))) |
43 | 40, 4, 42 | syl2anc 693 |
. . . . . 6
⊢ (𝜑 → ((Base‘𝑅) ↑𝑚
𝐴) =
(Base‘((mulGrp‘𝑅) ↑s 𝐴))) |
44 | 38, 43 | eqtr3d 2658 |
. . . . 5
⊢ (𝜑 → 𝐵 = (Base‘((mulGrp‘𝑅) ↑s
𝐴))) |
45 | 44 | mpteq1d 4738 |
. . . 4
⊢ (𝜑 → (𝑔 ∈ 𝐵 ↦ (𝐹 ∘ 𝑔)) = (𝑔 ∈ (Base‘((mulGrp‘𝑅) ↑s
𝐴)) ↦ (𝐹 ∘ 𝑔))) |
46 | | eqidd 2623 |
. . . . 5
⊢ (𝜑 →
(Base‘(mulGrp‘𝑌)) = (Base‘(mulGrp‘𝑌))) |
47 | | eqidd 2623 |
. . . . 5
⊢ (𝜑 →
(Base‘(mulGrp‘𝑍)) = (Base‘(mulGrp‘𝑍))) |
48 | | eqid 2622 |
. . . . . . . 8
⊢
(mulGrp‘𝑌) =
(mulGrp‘𝑌) |
49 | | eqid 2622 |
. . . . . . . 8
⊢
(Base‘(mulGrp‘𝑌)) = (Base‘(mulGrp‘𝑌)) |
50 | | eqid 2622 |
. . . . . . . 8
⊢
(+g‘(mulGrp‘𝑌)) =
(+g‘(mulGrp‘𝑌)) |
51 | | eqid 2622 |
. . . . . . . 8
⊢
(+g‘((mulGrp‘𝑅) ↑s 𝐴)) =
(+g‘((mulGrp‘𝑅) ↑s 𝐴)) |
52 | 5, 30, 27, 48, 49, 29, 50, 51 | pwsmgp 18618 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝐴 ∈ 𝑉) → ((Base‘(mulGrp‘𝑌)) =
(Base‘((mulGrp‘𝑅) ↑s 𝐴)) ∧
(+g‘(mulGrp‘𝑌)) =
(+g‘((mulGrp‘𝑅) ↑s 𝐴)))) |
53 | 3, 4, 52 | syl2anc 693 |
. . . . . 6
⊢ (𝜑 →
((Base‘(mulGrp‘𝑌)) = (Base‘((mulGrp‘𝑅) ↑s
𝐴)) ∧
(+g‘(mulGrp‘𝑌)) =
(+g‘((mulGrp‘𝑅) ↑s 𝐴)))) |
54 | 53 | simpld 475 |
. . . . 5
⊢ (𝜑 →
(Base‘(mulGrp‘𝑌)) = (Base‘((mulGrp‘𝑅) ↑s
𝐴))) |
55 | | eqid 2622 |
. . . . . . . 8
⊢
(mulGrp‘𝑍) =
(mulGrp‘𝑍) |
56 | | eqid 2622 |
. . . . . . . 8
⊢
(Base‘(mulGrp‘𝑍)) = (Base‘(mulGrp‘𝑍)) |
57 | | eqid 2622 |
. . . . . . . 8
⊢
(Base‘((mulGrp‘𝑆) ↑s 𝐴)) =
(Base‘((mulGrp‘𝑆) ↑s 𝐴)) |
58 | | eqid 2622 |
. . . . . . . 8
⊢
(+g‘(mulGrp‘𝑍)) =
(+g‘(mulGrp‘𝑍)) |
59 | | eqid 2622 |
. . . . . . . 8
⊢
(+g‘((mulGrp‘𝑆) ↑s 𝐴)) =
(+g‘((mulGrp‘𝑆) ↑s 𝐴)) |
60 | 10, 31, 28, 55, 56, 57, 58, 59 | pwsmgp 18618 |
. . . . . . 7
⊢ ((𝑆 ∈ Ring ∧ 𝐴 ∈ 𝑉) → ((Base‘(mulGrp‘𝑍)) =
(Base‘((mulGrp‘𝑆) ↑s 𝐴)) ∧
(+g‘(mulGrp‘𝑍)) =
(+g‘((mulGrp‘𝑆) ↑s 𝐴)))) |
61 | 9, 4, 60 | syl2anc 693 |
. . . . . 6
⊢ (𝜑 →
((Base‘(mulGrp‘𝑍)) = (Base‘((mulGrp‘𝑆) ↑s
𝐴)) ∧
(+g‘(mulGrp‘𝑍)) =
(+g‘((mulGrp‘𝑆) ↑s 𝐴)))) |
62 | 61 | simpld 475 |
. . . . 5
⊢ (𝜑 →
(Base‘(mulGrp‘𝑍)) = (Base‘((mulGrp‘𝑆) ↑s
𝐴))) |
63 | 53 | simprd 479 |
. . . . . 6
⊢ (𝜑 →
(+g‘(mulGrp‘𝑌)) =
(+g‘((mulGrp‘𝑅) ↑s 𝐴))) |
64 | 63 | oveqdr 6674 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(mulGrp‘𝑌)) ∧ 𝑦 ∈ (Base‘(mulGrp‘𝑌)))) → (𝑥(+g‘(mulGrp‘𝑌))𝑦) = (𝑥(+g‘((mulGrp‘𝑅) ↑s
𝐴))𝑦)) |
65 | 61 | simprd 479 |
. . . . . 6
⊢ (𝜑 →
(+g‘(mulGrp‘𝑍)) =
(+g‘((mulGrp‘𝑆) ↑s 𝐴))) |
66 | 65 | oveqdr 6674 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(mulGrp‘𝑍)) ∧ 𝑦 ∈ (Base‘(mulGrp‘𝑍)))) → (𝑥(+g‘(mulGrp‘𝑍))𝑦) = (𝑥(+g‘((mulGrp‘𝑆) ↑s
𝐴))𝑦)) |
67 | 46, 47, 54, 62, 64, 66 | mhmpropd 17341 |
. . . 4
⊢ (𝜑 → ((mulGrp‘𝑌) MndHom (mulGrp‘𝑍)) = (((mulGrp‘𝑅) ↑s
𝐴) MndHom
((mulGrp‘𝑆)
↑s 𝐴))) |
68 | 34, 45, 67 | 3eltr4d 2716 |
. . 3
⊢ (𝜑 → (𝑔 ∈ 𝐵 ↦ (𝐹 ∘ 𝑔)) ∈ ((mulGrp‘𝑌) MndHom (mulGrp‘𝑍))) |
69 | 26, 68 | jca 554 |
. 2
⊢ (𝜑 → ((𝑔 ∈ 𝐵 ↦ (𝐹 ∘ 𝑔)) ∈ (𝑌 GrpHom 𝑍) ∧ (𝑔 ∈ 𝐵 ↦ (𝐹 ∘ 𝑔)) ∈ ((mulGrp‘𝑌) MndHom (mulGrp‘𝑍)))) |
70 | 48, 55 | isrhm 18721 |
. 2
⊢ ((𝑔 ∈ 𝐵 ↦ (𝐹 ∘ 𝑔)) ∈ (𝑌 RingHom 𝑍) ↔ ((𝑌 ∈ Ring ∧ 𝑍 ∈ Ring) ∧ ((𝑔 ∈ 𝐵 ↦ (𝐹 ∘ 𝑔)) ∈ (𝑌 GrpHom 𝑍) ∧ (𝑔 ∈ 𝐵 ↦ (𝐹 ∘ 𝑔)) ∈ ((mulGrp‘𝑌) MndHom (mulGrp‘𝑍))))) |
71 | 13, 69, 70 | sylanbrc 698 |
1
⊢ (𝜑 → (𝑔 ∈ 𝐵 ↦ (𝐹 ∘ 𝑔)) ∈ (𝑌 RingHom 𝑍)) |