Metamath Proof Explorer

Theorem pwsco1rhm

Description: Right composition with a function on the index sets yields a ring homomorphism of structure powers. (Contributed by Mario Carneiro, 12-Jun-2015)

Ref Expression
Hypotheses pwsco1rhm.y ⊢ 𝑌 = ( 𝑅 ↑s 𝐴 )
pwsco1rhm.z ⊢ 𝑍 = ( 𝑅 ↑s 𝐵 )
pwsco1rhm.c ⊢ 𝐶 = ( Base ‘ 𝑍 )
pwsco1rhm.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
pwsco1rhm.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
pwsco1rhm.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
pwsco1rhm.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
Assertion pwsco1rhm ( 𝜑 → ( 𝑔 ∈ 𝐶 ↦ ( 𝑔 ∘ 𝐹 ) ) ∈ ( 𝑍 RingHom 𝑌 ) )

Proof

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