Step | Hyp | Ref
| Expression |
1 | | pwsco2rhm.f |
. . . 4
⊢ (𝜑 → 𝐹 ∈ (𝑅 RingHom 𝑆)) |
2 | | rhmrcl1 19961 |
. . . 4
⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝑅 ∈ Ring) |
3 | 1, 2 | syl 17 |
. . 3
⊢ (𝜑 → 𝑅 ∈ Ring) |
4 | | pwsco2rhm.a |
. . 3
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
5 | | pwsco2rhm.y |
. . . 4
⊢ 𝑌 = (𝑅 ↑s 𝐴) |
6 | 5 | pwsring 19852 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝐴 ∈ 𝑉) → 𝑌 ∈ Ring) |
7 | 3, 4, 6 | syl2anc 584 |
. 2
⊢ (𝜑 → 𝑌 ∈ Ring) |
8 | | rhmrcl2 19962 |
. . . 4
⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝑆 ∈ Ring) |
9 | 1, 8 | syl 17 |
. . 3
⊢ (𝜑 → 𝑆 ∈ Ring) |
10 | | pwsco2rhm.z |
. . . 4
⊢ 𝑍 = (𝑆 ↑s 𝐴) |
11 | 10 | pwsring 19852 |
. . 3
⊢ ((𝑆 ∈ Ring ∧ 𝐴 ∈ 𝑉) → 𝑍 ∈ Ring) |
12 | 9, 4, 11 | syl2anc 584 |
. 2
⊢ (𝜑 → 𝑍 ∈ Ring) |
13 | | pwsco2rhm.b |
. . . . 5
⊢ 𝐵 = (Base‘𝑌) |
14 | | rhmghm 19967 |
. . . . . . 7
⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝐹 ∈ (𝑅 GrpHom 𝑆)) |
15 | 1, 14 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐹 ∈ (𝑅 GrpHom 𝑆)) |
16 | | ghmmhm 18842 |
. . . . . 6
⊢ (𝐹 ∈ (𝑅 GrpHom 𝑆) → 𝐹 ∈ (𝑅 MndHom 𝑆)) |
17 | 15, 16 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝐹 ∈ (𝑅 MndHom 𝑆)) |
18 | 5, 10, 13, 4, 17 | pwsco2mhm 18469 |
. . . 4
⊢ (𝜑 → (𝑔 ∈ 𝐵 ↦ (𝐹 ∘ 𝑔)) ∈ (𝑌 MndHom 𝑍)) |
19 | | ringgrp 19786 |
. . . . . 6
⊢ (𝑌 ∈ Ring → 𝑌 ∈ Grp) |
20 | 7, 19 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑌 ∈ Grp) |
21 | | ringgrp 19786 |
. . . . . 6
⊢ (𝑍 ∈ Ring → 𝑍 ∈ Grp) |
22 | 12, 21 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑍 ∈ Grp) |
23 | | ghmmhmb 18843 |
. . . . 5
⊢ ((𝑌 ∈ Grp ∧ 𝑍 ∈ Grp) → (𝑌 GrpHom 𝑍) = (𝑌 MndHom 𝑍)) |
24 | 20, 22, 23 | syl2anc 584 |
. . . 4
⊢ (𝜑 → (𝑌 GrpHom 𝑍) = (𝑌 MndHom 𝑍)) |
25 | 18, 24 | eleqtrrd 2844 |
. . 3
⊢ (𝜑 → (𝑔 ∈ 𝐵 ↦ (𝐹 ∘ 𝑔)) ∈ (𝑌 GrpHom 𝑍)) |
26 | | eqid 2740 |
. . . . 5
⊢
((mulGrp‘𝑅)
↑s 𝐴) = ((mulGrp‘𝑅) ↑s 𝐴) |
27 | | eqid 2740 |
. . . . 5
⊢
((mulGrp‘𝑆)
↑s 𝐴) = ((mulGrp‘𝑆) ↑s 𝐴) |
28 | | eqid 2740 |
. . . . 5
⊢
(Base‘((mulGrp‘𝑅) ↑s 𝐴)) =
(Base‘((mulGrp‘𝑅) ↑s 𝐴)) |
29 | | eqid 2740 |
. . . . . . 7
⊢
(mulGrp‘𝑅) =
(mulGrp‘𝑅) |
30 | | eqid 2740 |
. . . . . . 7
⊢
(mulGrp‘𝑆) =
(mulGrp‘𝑆) |
31 | 29, 30 | rhmmhm 19964 |
. . . . . 6
⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝐹 ∈ ((mulGrp‘𝑅) MndHom (mulGrp‘𝑆))) |
32 | 1, 31 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝐹 ∈ ((mulGrp‘𝑅) MndHom (mulGrp‘𝑆))) |
33 | 26, 27, 28, 4, 32 | pwsco2mhm 18469 |
. . . 4
⊢ (𝜑 → (𝑔 ∈ (Base‘((mulGrp‘𝑅) ↑s
𝐴)) ↦ (𝐹 ∘ 𝑔)) ∈ (((mulGrp‘𝑅) ↑s 𝐴) MndHom ((mulGrp‘𝑆) ↑s
𝐴))) |
34 | | eqid 2740 |
. . . . . . . . 9
⊢
(Base‘𝑅) =
(Base‘𝑅) |
35 | 5, 34 | pwsbas 17196 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ 𝐴 ∈ 𝑉) → ((Base‘𝑅) ↑m 𝐴) = (Base‘𝑌)) |
36 | 3, 4, 35 | syl2anc 584 |
. . . . . . 7
⊢ (𝜑 → ((Base‘𝑅) ↑m 𝐴) = (Base‘𝑌)) |
37 | 36, 13 | eqtr4di 2798 |
. . . . . 6
⊢ (𝜑 → ((Base‘𝑅) ↑m 𝐴) = 𝐵) |
38 | 29 | ringmgp 19787 |
. . . . . . . 8
⊢ (𝑅 ∈ Ring →
(mulGrp‘𝑅) ∈
Mnd) |
39 | 3, 38 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (mulGrp‘𝑅) ∈ Mnd) |
40 | 29, 34 | mgpbas 19724 |
. . . . . . . 8
⊢
(Base‘𝑅) =
(Base‘(mulGrp‘𝑅)) |
41 | 26, 40 | pwsbas 17196 |
. . . . . . 7
⊢
(((mulGrp‘𝑅)
∈ Mnd ∧ 𝐴 ∈
𝑉) →
((Base‘𝑅)
↑m 𝐴) =
(Base‘((mulGrp‘𝑅) ↑s 𝐴))) |
42 | 39, 4, 41 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → ((Base‘𝑅) ↑m 𝐴) =
(Base‘((mulGrp‘𝑅) ↑s 𝐴))) |
43 | 37, 42 | eqtr3d 2782 |
. . . . 5
⊢ (𝜑 → 𝐵 = (Base‘((mulGrp‘𝑅) ↑s
𝐴))) |
44 | 43 | mpteq1d 5174 |
. . . 4
⊢ (𝜑 → (𝑔 ∈ 𝐵 ↦ (𝐹 ∘ 𝑔)) = (𝑔 ∈ (Base‘((mulGrp‘𝑅) ↑s
𝐴)) ↦ (𝐹 ∘ 𝑔))) |
45 | | eqidd 2741 |
. . . . 5
⊢ (𝜑 →
(Base‘(mulGrp‘𝑌)) = (Base‘(mulGrp‘𝑌))) |
46 | | eqidd 2741 |
. . . . 5
⊢ (𝜑 →
(Base‘(mulGrp‘𝑍)) = (Base‘(mulGrp‘𝑍))) |
47 | | eqid 2740 |
. . . . . . . 8
⊢
(mulGrp‘𝑌) =
(mulGrp‘𝑌) |
48 | | eqid 2740 |
. . . . . . . 8
⊢
(Base‘(mulGrp‘𝑌)) = (Base‘(mulGrp‘𝑌)) |
49 | | eqid 2740 |
. . . . . . . 8
⊢
(+g‘(mulGrp‘𝑌)) =
(+g‘(mulGrp‘𝑌)) |
50 | | eqid 2740 |
. . . . . . . 8
⊢
(+g‘((mulGrp‘𝑅) ↑s 𝐴)) =
(+g‘((mulGrp‘𝑅) ↑s 𝐴)) |
51 | 5, 29, 26, 47, 48, 28, 49, 50 | pwsmgp 19855 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝐴 ∈ 𝑉) → ((Base‘(mulGrp‘𝑌)) =
(Base‘((mulGrp‘𝑅) ↑s 𝐴)) ∧
(+g‘(mulGrp‘𝑌)) =
(+g‘((mulGrp‘𝑅) ↑s 𝐴)))) |
52 | 3, 4, 51 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 →
((Base‘(mulGrp‘𝑌)) = (Base‘((mulGrp‘𝑅) ↑s
𝐴)) ∧
(+g‘(mulGrp‘𝑌)) =
(+g‘((mulGrp‘𝑅) ↑s 𝐴)))) |
53 | 52 | simpld 495 |
. . . . 5
⊢ (𝜑 →
(Base‘(mulGrp‘𝑌)) = (Base‘((mulGrp‘𝑅) ↑s
𝐴))) |
54 | | eqid 2740 |
. . . . . . . 8
⊢
(mulGrp‘𝑍) =
(mulGrp‘𝑍) |
55 | | eqid 2740 |
. . . . . . . 8
⊢
(Base‘(mulGrp‘𝑍)) = (Base‘(mulGrp‘𝑍)) |
56 | | eqid 2740 |
. . . . . . . 8
⊢
(Base‘((mulGrp‘𝑆) ↑s 𝐴)) =
(Base‘((mulGrp‘𝑆) ↑s 𝐴)) |
57 | | eqid 2740 |
. . . . . . . 8
⊢
(+g‘(mulGrp‘𝑍)) =
(+g‘(mulGrp‘𝑍)) |
58 | | eqid 2740 |
. . . . . . . 8
⊢
(+g‘((mulGrp‘𝑆) ↑s 𝐴)) =
(+g‘((mulGrp‘𝑆) ↑s 𝐴)) |
59 | 10, 30, 27, 54, 55, 56, 57, 58 | pwsmgp 19855 |
. . . . . . 7
⊢ ((𝑆 ∈ Ring ∧ 𝐴 ∈ 𝑉) → ((Base‘(mulGrp‘𝑍)) =
(Base‘((mulGrp‘𝑆) ↑s 𝐴)) ∧
(+g‘(mulGrp‘𝑍)) =
(+g‘((mulGrp‘𝑆) ↑s 𝐴)))) |
60 | 9, 4, 59 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 →
((Base‘(mulGrp‘𝑍)) = (Base‘((mulGrp‘𝑆) ↑s
𝐴)) ∧
(+g‘(mulGrp‘𝑍)) =
(+g‘((mulGrp‘𝑆) ↑s 𝐴)))) |
61 | 60 | simpld 495 |
. . . . 5
⊢ (𝜑 →
(Base‘(mulGrp‘𝑍)) = (Base‘((mulGrp‘𝑆) ↑s
𝐴))) |
62 | 52 | simprd 496 |
. . . . . 6
⊢ (𝜑 →
(+g‘(mulGrp‘𝑌)) =
(+g‘((mulGrp‘𝑅) ↑s 𝐴))) |
63 | 62 | oveqdr 7299 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(mulGrp‘𝑌)) ∧ 𝑦 ∈ (Base‘(mulGrp‘𝑌)))) → (𝑥(+g‘(mulGrp‘𝑌))𝑦) = (𝑥(+g‘((mulGrp‘𝑅) ↑s
𝐴))𝑦)) |
64 | 60 | simprd 496 |
. . . . . 6
⊢ (𝜑 →
(+g‘(mulGrp‘𝑍)) =
(+g‘((mulGrp‘𝑆) ↑s 𝐴))) |
65 | 64 | oveqdr 7299 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(mulGrp‘𝑍)) ∧ 𝑦 ∈ (Base‘(mulGrp‘𝑍)))) → (𝑥(+g‘(mulGrp‘𝑍))𝑦) = (𝑥(+g‘((mulGrp‘𝑆) ↑s
𝐴))𝑦)) |
66 | 45, 46, 53, 61, 63, 65 | mhmpropd 18434 |
. . . 4
⊢ (𝜑 → ((mulGrp‘𝑌) MndHom (mulGrp‘𝑍)) = (((mulGrp‘𝑅) ↑s
𝐴) MndHom
((mulGrp‘𝑆)
↑s 𝐴))) |
67 | 33, 44, 66 | 3eltr4d 2856 |
. . 3
⊢ (𝜑 → (𝑔 ∈ 𝐵 ↦ (𝐹 ∘ 𝑔)) ∈ ((mulGrp‘𝑌) MndHom (mulGrp‘𝑍))) |
68 | 25, 67 | jca 512 |
. 2
⊢ (𝜑 → ((𝑔 ∈ 𝐵 ↦ (𝐹 ∘ 𝑔)) ∈ (𝑌 GrpHom 𝑍) ∧ (𝑔 ∈ 𝐵 ↦ (𝐹 ∘ 𝑔)) ∈ ((mulGrp‘𝑌) MndHom (mulGrp‘𝑍)))) |
69 | 47, 54 | isrhm 19963 |
. 2
⊢ ((𝑔 ∈ 𝐵 ↦ (𝐹 ∘ 𝑔)) ∈ (𝑌 RingHom 𝑍) ↔ ((𝑌 ∈ Ring ∧ 𝑍 ∈ Ring) ∧ ((𝑔 ∈ 𝐵 ↦ (𝐹 ∘ 𝑔)) ∈ (𝑌 GrpHom 𝑍) ∧ (𝑔 ∈ 𝐵 ↦ (𝐹 ∘ 𝑔)) ∈ ((mulGrp‘𝑌) MndHom (mulGrp‘𝑍))))) |
70 | 7, 12, 68, 69 | syl21anbrc 1343 |
1
⊢ (𝜑 → (𝑔 ∈ 𝐵 ↦ (𝐹 ∘ 𝑔)) ∈ (𝑌 RingHom 𝑍)) |