Step | Hyp | Ref
| Expression |
1 | | pwsco2rhm.f |
. . . . 5
⊢ (𝜑 → 𝐹 ∈ (𝑅 RingHom 𝑆)) |
2 | | rhmrcl1 18542 |
. . . . 5
⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝑅 ∈ Ring) |
3 | 1, 2 | syl 17 |
. . . 4
⊢ (𝜑 → 𝑅 ∈ Ring) |
4 | | pwsco2rhm.a |
. . . 4
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
5 | | pwsco2rhm.y |
. . . . 5
⊢ 𝑌 = (𝑅 ↑s 𝐴) |
6 | 5 | pwsring 18438 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐴 ∈ 𝑉) → 𝑌 ∈ Ring) |
7 | 3, 4, 6 | syl2anc 691 |
. . 3
⊢ (𝜑 → 𝑌 ∈ Ring) |
8 | | rhmrcl2 18543 |
. . . . 5
⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝑆 ∈ Ring) |
9 | 1, 8 | syl 17 |
. . . 4
⊢ (𝜑 → 𝑆 ∈ Ring) |
10 | | pwsco2rhm.z |
. . . . 5
⊢ 𝑍 = (𝑆 ↑s 𝐴) |
11 | 10 | pwsring 18438 |
. . . 4
⊢ ((𝑆 ∈ Ring ∧ 𝐴 ∈ 𝑉) → 𝑍 ∈ Ring) |
12 | 9, 4, 11 | syl2anc 691 |
. . 3
⊢ (𝜑 → 𝑍 ∈ Ring) |
13 | 7, 12 | jca 553 |
. 2
⊢ (𝜑 → (𝑌 ∈ Ring ∧ 𝑍 ∈ Ring)) |
14 | | pwsco2rhm.b |
. . . . 5
⊢ 𝐵 = (Base‘𝑌) |
15 | | rhmghm 18548 |
. . . . . . 7
⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝐹 ∈ (𝑅 GrpHom 𝑆)) |
16 | 1, 15 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐹 ∈ (𝑅 GrpHom 𝑆)) |
17 | | ghmmhm 17493 |
. . . . . 6
⊢ (𝐹 ∈ (𝑅 GrpHom 𝑆) → 𝐹 ∈ (𝑅 MndHom 𝑆)) |
18 | 16, 17 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝐹 ∈ (𝑅 MndHom 𝑆)) |
19 | 5, 10, 14, 4, 18 | pwsco2mhm 17194 |
. . . 4
⊢ (𝜑 → (𝑔 ∈ 𝐵 ↦ (𝐹 ∘ 𝑔)) ∈ (𝑌 MndHom 𝑍)) |
20 | | ringgrp 18375 |
. . . . . 6
⊢ (𝑌 ∈ Ring → 𝑌 ∈ Grp) |
21 | 7, 20 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑌 ∈ Grp) |
22 | | ringgrp 18375 |
. . . . . 6
⊢ (𝑍 ∈ Ring → 𝑍 ∈ Grp) |
23 | 12, 22 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑍 ∈ Grp) |
24 | | ghmmhmb 17494 |
. . . . 5
⊢ ((𝑌 ∈ Grp ∧ 𝑍 ∈ Grp) → (𝑌 GrpHom 𝑍) = (𝑌 MndHom 𝑍)) |
25 | 21, 23, 24 | syl2anc 691 |
. . . 4
⊢ (𝜑 → (𝑌 GrpHom 𝑍) = (𝑌 MndHom 𝑍)) |
26 | 19, 25 | eleqtrrd 2691 |
. . 3
⊢ (𝜑 → (𝑔 ∈ 𝐵 ↦ (𝐹 ∘ 𝑔)) ∈ (𝑌 GrpHom 𝑍)) |
27 | | eqid 2610 |
. . . . 5
⊢
((mulGrp‘𝑅)
↑s 𝐴) = ((mulGrp‘𝑅) ↑s 𝐴) |
28 | | eqid 2610 |
. . . . 5
⊢
((mulGrp‘𝑆)
↑s 𝐴) = ((mulGrp‘𝑆) ↑s 𝐴) |
29 | | eqid 2610 |
. . . . 5
⊢
(Base‘((mulGrp‘𝑅) ↑s 𝐴)) =
(Base‘((mulGrp‘𝑅) ↑s 𝐴)) |
30 | | eqid 2610 |
. . . . . . 7
⊢
(mulGrp‘𝑅) =
(mulGrp‘𝑅) |
31 | | eqid 2610 |
. . . . . . 7
⊢
(mulGrp‘𝑆) =
(mulGrp‘𝑆) |
32 | 30, 31 | rhmmhm 18545 |
. . . . . 6
⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝐹 ∈ ((mulGrp‘𝑅) MndHom (mulGrp‘𝑆))) |
33 | 1, 32 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝐹 ∈ ((mulGrp‘𝑅) MndHom (mulGrp‘𝑆))) |
34 | 27, 28, 29, 4, 33 | pwsco2mhm 17194 |
. . . 4
⊢ (𝜑 → (𝑔 ∈ (Base‘((mulGrp‘𝑅) ↑s
𝐴)) ↦ (𝐹 ∘ 𝑔)) ∈ (((mulGrp‘𝑅) ↑s 𝐴) MndHom ((mulGrp‘𝑆) ↑s
𝐴))) |
35 | | eqid 2610 |
. . . . . . . . 9
⊢
(Base‘𝑅) =
(Base‘𝑅) |
36 | 5, 35 | pwsbas 15970 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ 𝐴 ∈ 𝑉) → ((Base‘𝑅) ↑𝑚 𝐴) = (Base‘𝑌)) |
37 | 3, 4, 36 | syl2anc 691 |
. . . . . . 7
⊢ (𝜑 → ((Base‘𝑅) ↑𝑚
𝐴) = (Base‘𝑌)) |
38 | 37, 14 | syl6eqr 2662 |
. . . . . 6
⊢ (𝜑 → ((Base‘𝑅) ↑𝑚
𝐴) = 𝐵) |
39 | 30 | ringmgp 18376 |
. . . . . . . 8
⊢ (𝑅 ∈ Ring →
(mulGrp‘𝑅) ∈
Mnd) |
40 | 3, 39 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (mulGrp‘𝑅) ∈ Mnd) |
41 | 30, 35 | mgpbas 18318 |
. . . . . . . 8
⊢
(Base‘𝑅) =
(Base‘(mulGrp‘𝑅)) |
42 | 27, 41 | pwsbas 15970 |
. . . . . . 7
⊢
(((mulGrp‘𝑅)
∈ Mnd ∧ 𝐴 ∈
𝑉) →
((Base‘𝑅)
↑𝑚 𝐴) = (Base‘((mulGrp‘𝑅) ↑s
𝐴))) |
43 | 40, 4, 42 | syl2anc 691 |
. . . . . 6
⊢ (𝜑 → ((Base‘𝑅) ↑𝑚
𝐴) =
(Base‘((mulGrp‘𝑅) ↑s 𝐴))) |
44 | 38, 43 | eqtr3d 2646 |
. . . . 5
⊢ (𝜑 → 𝐵 = (Base‘((mulGrp‘𝑅) ↑s
𝐴))) |
45 | 44 | mpteq1d 4666 |
. . . 4
⊢ (𝜑 → (𝑔 ∈ 𝐵 ↦ (𝐹 ∘ 𝑔)) = (𝑔 ∈ (Base‘((mulGrp‘𝑅) ↑s
𝐴)) ↦ (𝐹 ∘ 𝑔))) |
46 | | eqidd 2611 |
. . . . 5
⊢ (𝜑 →
(Base‘(mulGrp‘𝑌)) = (Base‘(mulGrp‘𝑌))) |
47 | | eqidd 2611 |
. . . . 5
⊢ (𝜑 →
(Base‘(mulGrp‘𝑍)) = (Base‘(mulGrp‘𝑍))) |
48 | | eqid 2610 |
. . . . . . . 8
⊢
(mulGrp‘𝑌) =
(mulGrp‘𝑌) |
49 | | eqid 2610 |
. . . . . . . 8
⊢
(Base‘(mulGrp‘𝑌)) = (Base‘(mulGrp‘𝑌)) |
50 | | eqid 2610 |
. . . . . . . 8
⊢
(+g‘(mulGrp‘𝑌)) =
(+g‘(mulGrp‘𝑌)) |
51 | | eqid 2610 |
. . . . . . . 8
⊢
(+g‘((mulGrp‘𝑅) ↑s 𝐴)) =
(+g‘((mulGrp‘𝑅) ↑s 𝐴)) |
52 | 5, 30, 27, 48, 49, 29, 50, 51 | pwsmgp 18441 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝐴 ∈ 𝑉) → ((Base‘(mulGrp‘𝑌)) =
(Base‘((mulGrp‘𝑅) ↑s 𝐴)) ∧
(+g‘(mulGrp‘𝑌)) =
(+g‘((mulGrp‘𝑅) ↑s 𝐴)))) |
53 | 3, 4, 52 | syl2anc 691 |
. . . . . 6
⊢ (𝜑 →
((Base‘(mulGrp‘𝑌)) = (Base‘((mulGrp‘𝑅) ↑s
𝐴)) ∧
(+g‘(mulGrp‘𝑌)) =
(+g‘((mulGrp‘𝑅) ↑s 𝐴)))) |
54 | 53 | simpld 474 |
. . . . 5
⊢ (𝜑 →
(Base‘(mulGrp‘𝑌)) = (Base‘((mulGrp‘𝑅) ↑s
𝐴))) |
55 | | eqid 2610 |
. . . . . . . 8
⊢
(mulGrp‘𝑍) =
(mulGrp‘𝑍) |
56 | | eqid 2610 |
. . . . . . . 8
⊢
(Base‘(mulGrp‘𝑍)) = (Base‘(mulGrp‘𝑍)) |
57 | | eqid 2610 |
. . . . . . . 8
⊢
(Base‘((mulGrp‘𝑆) ↑s 𝐴)) =
(Base‘((mulGrp‘𝑆) ↑s 𝐴)) |
58 | | eqid 2610 |
. . . . . . . 8
⊢
(+g‘(mulGrp‘𝑍)) =
(+g‘(mulGrp‘𝑍)) |
59 | | eqid 2610 |
. . . . . . . 8
⊢
(+g‘((mulGrp‘𝑆) ↑s 𝐴)) =
(+g‘((mulGrp‘𝑆) ↑s 𝐴)) |
60 | 10, 31, 28, 55, 56, 57, 58, 59 | pwsmgp 18441 |
. . . . . . 7
⊢ ((𝑆 ∈ Ring ∧ 𝐴 ∈ 𝑉) → ((Base‘(mulGrp‘𝑍)) =
(Base‘((mulGrp‘𝑆) ↑s 𝐴)) ∧
(+g‘(mulGrp‘𝑍)) =
(+g‘((mulGrp‘𝑆) ↑s 𝐴)))) |
61 | 9, 4, 60 | syl2anc 691 |
. . . . . 6
⊢ (𝜑 →
((Base‘(mulGrp‘𝑍)) = (Base‘((mulGrp‘𝑆) ↑s
𝐴)) ∧
(+g‘(mulGrp‘𝑍)) =
(+g‘((mulGrp‘𝑆) ↑s 𝐴)))) |
62 | 61 | simpld 474 |
. . . . 5
⊢ (𝜑 →
(Base‘(mulGrp‘𝑍)) = (Base‘((mulGrp‘𝑆) ↑s
𝐴))) |
63 | 53 | simprd 478 |
. . . . . 6
⊢ (𝜑 →
(+g‘(mulGrp‘𝑌)) =
(+g‘((mulGrp‘𝑅) ↑s 𝐴))) |
64 | 63 | oveqdr 6573 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(mulGrp‘𝑌)) ∧ 𝑦 ∈ (Base‘(mulGrp‘𝑌)))) → (𝑥(+g‘(mulGrp‘𝑌))𝑦) = (𝑥(+g‘((mulGrp‘𝑅) ↑s
𝐴))𝑦)) |
65 | 61 | simprd 478 |
. . . . . 6
⊢ (𝜑 →
(+g‘(mulGrp‘𝑍)) =
(+g‘((mulGrp‘𝑆) ↑s 𝐴))) |
66 | 65 | oveqdr 6573 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(mulGrp‘𝑍)) ∧ 𝑦 ∈ (Base‘(mulGrp‘𝑍)))) → (𝑥(+g‘(mulGrp‘𝑍))𝑦) = (𝑥(+g‘((mulGrp‘𝑆) ↑s
𝐴))𝑦)) |
67 | 46, 47, 54, 62, 64, 66 | mhmpropd 17164 |
. . . 4
⊢ (𝜑 → ((mulGrp‘𝑌) MndHom (mulGrp‘𝑍)) = (((mulGrp‘𝑅) ↑s
𝐴) MndHom
((mulGrp‘𝑆)
↑s 𝐴))) |
68 | 34, 45, 67 | 3eltr4d 2703 |
. . 3
⊢ (𝜑 → (𝑔 ∈ 𝐵 ↦ (𝐹 ∘ 𝑔)) ∈ ((mulGrp‘𝑌) MndHom (mulGrp‘𝑍))) |
69 | 26, 68 | jca 553 |
. 2
⊢ (𝜑 → ((𝑔 ∈ 𝐵 ↦ (𝐹 ∘ 𝑔)) ∈ (𝑌 GrpHom 𝑍) ∧ (𝑔 ∈ 𝐵 ↦ (𝐹 ∘ 𝑔)) ∈ ((mulGrp‘𝑌) MndHom (mulGrp‘𝑍)))) |
70 | 48, 55 | isrhm 18544 |
. 2
⊢ ((𝑔 ∈ 𝐵 ↦ (𝐹 ∘ 𝑔)) ∈ (𝑌 RingHom 𝑍) ↔ ((𝑌 ∈ Ring ∧ 𝑍 ∈ Ring) ∧ ((𝑔 ∈ 𝐵 ↦ (𝐹 ∘ 𝑔)) ∈ (𝑌 GrpHom 𝑍) ∧ (𝑔 ∈ 𝐵 ↦ (𝐹 ∘ 𝑔)) ∈ ((mulGrp‘𝑌) MndHom (mulGrp‘𝑍))))) |
71 | 13, 69, 70 | sylanbrc 695 |
1
⊢ (𝜑 → (𝑔 ∈ 𝐵 ↦ (𝐹 ∘ 𝑔)) ∈ (𝑌 RingHom 𝑍)) |