Metamath Proof Explorer

Theorem pwsco2rhm

Description: Left composition with a ring homomorphism yields a ring homomorphism of structure powers. (Contributed by Mario Carneiro, 12-Jun-2015)

Ref Expression
Hypotheses pwsco2rhm.y ⊢ 𝑌 = ( 𝑅 ↑s 𝐴 )
pwsco2rhm.z ⊢ 𝑍 = ( 𝑆 ↑s 𝐴 )
pwsco2rhm.b ⊢ 𝐵 = ( Base ‘ 𝑌 )
pwsco2rhm.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
pwsco2rhm.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) )
Assertion pwsco2rhm ( 𝜑 → ( 𝑔 ∈ 𝐵 ↦ ( 𝐹 ∘ 𝑔 ) ) ∈ ( 𝑌 RingHom 𝑍 ) )

Proof

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