Metamath Proof Explorer

Theorem pwspjmhmmgpd

Description: The projection given by pwspjmhm is also a monoid homomorphism between the respective multiplicative groups. (Contributed by SN, 30-Jul-2024)

Ref Expression
Hypotheses pwspjmhmmgpd.y ⊢ 𝑌 = ( 𝑅 ↑s 𝐼 )
pwspjmhmmgpd.b ⊢ 𝐵 = ( Base ‘ 𝑌 )
pwspjmhmmgpd.m ⊢ 𝑀 = ( mulGrp ‘ 𝑌 )
pwspjmhmmgpd.t ⊢ 𝑇 = ( mulGrp ‘ 𝑅 )
pwspjmhmmgpd.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
pwspjmhmmgpd.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
pwspjmhmmgpd.a ⊢ ( 𝜑 → 𝐴 ∈ 𝐼 )
Assertion pwspjmhmmgpd ( 𝜑 → ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 ‘ 𝐴 ) ) ∈ ( 𝑀 MndHom 𝑇 ) )

Proof

Step Hyp Ref Expression
1 pwspjmhmmgpd.y ⊢ 𝑌 = ( 𝑅 ↑s 𝐼 )
2 pwspjmhmmgpd.b ⊢ 𝐵 = ( Base ‘ 𝑌 )
3 pwspjmhmmgpd.m ⊢ 𝑀 = ( mulGrp ‘ 𝑌 )
4 pwspjmhmmgpd.t ⊢ 𝑇 = ( mulGrp ‘ 𝑅 )
5 pwspjmhmmgpd.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
6 pwspjmhmmgpd.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
7 pwspjmhmmgpd.a ⊢ ( 𝜑 → 𝐴 ∈ 𝐼 )
8 3 2 mgpbas ⊢ 𝐵 = ( Base ‘ 𝑀 )
9 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
10 4 9 mgpbas ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑇 )
11 eqid ⊢ ( .r ‘ 𝑌 ) = ( .r ‘ 𝑌 )
12 3 11 mgpplusg ⊢ ( .r ‘ 𝑌 ) = ( +g ‘ 𝑀 )
13 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
14 4 13 mgpplusg ⊢ ( .r ‘ 𝑅 ) = ( +g ‘ 𝑇 )
15 eqid ⊢ ( 1r ‘ 𝑌 ) = ( 1r ‘ 𝑌 )
16 3 15 ringidval ⊢ ( 1r ‘ 𝑌 ) = ( 0g ‘ 𝑀 )
17 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
18 4 17 ringidval ⊢ ( 1r ‘ 𝑅 ) = ( 0g ‘ 𝑇 )
19 1 pwsring ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) → 𝑌 ∈ Ring )
20 5 6 19 syl2anc ⊢ ( 𝜑 → 𝑌 ∈ Ring )
21 3 ringmgp ⊢ ( 𝑌 ∈ Ring → 𝑀 ∈ Mnd )
22 20 21 syl ⊢ ( 𝜑 → 𝑀 ∈ Mnd )
23 4 ringmgp ⊢ ( 𝑅 ∈ Ring → 𝑇 ∈ Mnd )
24 5 23 syl ⊢ ( 𝜑 → 𝑇 ∈ Mnd )
25 5 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝑅 ∈ Ring )
26 6 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝐼 ∈ 𝑉 )
27 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ 𝐵 )
28 1 9 2 25 26 27 pwselbas ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝑥 : 𝐼 ⟶ ( Base ‘ 𝑅 ) )
29 7 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝐴 ∈ 𝐼 )
30 28 29 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 ‘ 𝐴 ) ∈ ( Base ‘ 𝑅 ) )
31 30 fmpttd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 ‘ 𝐴 ) ) : 𝐵 ⟶ ( Base ‘ 𝑅 ) )
32 5 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → 𝑅 ∈ Ring )
33 6 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → 𝐼 ∈ 𝑉 )
34 simprl ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → 𝑎 ∈ 𝐵 )
35 simprr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → 𝑏 ∈ 𝐵 )
36 1 2 32 33 34 35 13 11 pwsmulrval ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑎 ( .r ‘ 𝑌 ) 𝑏 ) = ( 𝑎 ∘f ( .r ‘ 𝑅 ) 𝑏 ) )
37 36 fveq1d ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( ( 𝑎 ( .r ‘ 𝑌 ) 𝑏 ) ‘ 𝐴 ) = ( ( 𝑎 ∘f ( .r ‘ 𝑅 ) 𝑏 ) ‘ 𝐴 ) )
38 1 9 2 32 33 34 pwselbas ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → 𝑎 : 𝐼 ⟶ ( Base ‘ 𝑅 ) )
39 38 ffnd ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → 𝑎 Fn 𝐼 )
40 1 9 2 32 33 35 pwselbas ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → 𝑏 : 𝐼 ⟶ ( Base ‘ 𝑅 ) )
41 40 ffnd ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → 𝑏 Fn 𝐼 )
42 inidm ⊢ ( 𝐼 ∩ 𝐼 ) = 𝐼
43 eqidd ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) ∧ 𝐴 ∈ 𝐼 ) → ( 𝑎 ‘ 𝐴 ) = ( 𝑎 ‘ 𝐴 ) )
44 eqidd ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) ∧ 𝐴 ∈ 𝐼 ) → ( 𝑏 ‘ 𝐴 ) = ( 𝑏 ‘ 𝐴 ) )
45 39 41 33 33 42 43 44 ofval ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) ∧ 𝐴 ∈ 𝐼 ) → ( ( 𝑎 ∘f ( .r ‘ 𝑅 ) 𝑏 ) ‘ 𝐴 ) = ( ( 𝑎 ‘ 𝐴 ) ( .r ‘ 𝑅 ) ( 𝑏 ‘ 𝐴 ) ) )
46 7 45 mpidan ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( ( 𝑎 ∘f ( .r ‘ 𝑅 ) 𝑏 ) ‘ 𝐴 ) = ( ( 𝑎 ‘ 𝐴 ) ( .r ‘ 𝑅 ) ( 𝑏 ‘ 𝐴 ) ) )
47 37 46 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( ( 𝑎 ( .r ‘ 𝑌 ) 𝑏 ) ‘ 𝐴 ) = ( ( 𝑎 ‘ 𝐴 ) ( .r ‘ 𝑅 ) ( 𝑏 ‘ 𝐴 ) ) )
48 2 11 ringcl ⊢ ( ( 𝑌 ∈ Ring ∧ 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑎 ( .r ‘ 𝑌 ) 𝑏 ) ∈ 𝐵 )
49 20 48 syl3an1 ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑎 ( .r ‘ 𝑌 ) 𝑏 ) ∈ 𝐵 )
50 49 3expb ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑎 ( .r ‘ 𝑌 ) 𝑏 ) ∈ 𝐵 )
51 fveq1 ⊢ ( 𝑥 = ( 𝑎 ( .r ‘ 𝑌 ) 𝑏 ) → ( 𝑥 ‘ 𝐴 ) = ( ( 𝑎 ( .r ‘ 𝑌 ) 𝑏 ) ‘ 𝐴 ) )
52 eqid ⊢ ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 ‘ 𝐴 ) ) = ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 ‘ 𝐴 ) )
53 fvex ⊢ ( ( 𝑎 ( .r ‘ 𝑌 ) 𝑏 ) ‘ 𝐴 ) ∈ V
54 51 52 53 fvmpt ⊢ ( ( 𝑎 ( .r ‘ 𝑌 ) 𝑏 ) ∈ 𝐵 → ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 ‘ 𝐴 ) ) ‘ ( 𝑎 ( .r ‘ 𝑌 ) 𝑏 ) ) = ( ( 𝑎 ( .r ‘ 𝑌 ) 𝑏 ) ‘ 𝐴 ) )
55 50 54 syl ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 ‘ 𝐴 ) ) ‘ ( 𝑎 ( .r ‘ 𝑌 ) 𝑏 ) ) = ( ( 𝑎 ( .r ‘ 𝑌 ) 𝑏 ) ‘ 𝐴 ) )
56 fveq1 ⊢ ( 𝑥 = 𝑎 → ( 𝑥 ‘ 𝐴 ) = ( 𝑎 ‘ 𝐴 ) )
57 fvex ⊢ ( 𝑎 ‘ 𝐴 ) ∈ V
58 56 52 57 fvmpt ⊢ ( 𝑎 ∈ 𝐵 → ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 ‘ 𝐴 ) ) ‘ 𝑎 ) = ( 𝑎 ‘ 𝐴 ) )
59 34 58 syl ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 ‘ 𝐴 ) ) ‘ 𝑎 ) = ( 𝑎 ‘ 𝐴 ) )
60 fveq1 ⊢ ( 𝑥 = 𝑏 → ( 𝑥 ‘ 𝐴 ) = ( 𝑏 ‘ 𝐴 ) )
61 fvex ⊢ ( 𝑏 ‘ 𝐴 ) ∈ V
62 60 52 61 fvmpt ⊢ ( 𝑏 ∈ 𝐵 → ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 ‘ 𝐴 ) ) ‘ 𝑏 ) = ( 𝑏 ‘ 𝐴 ) )
63 35 62 syl ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 ‘ 𝐴 ) ) ‘ 𝑏 ) = ( 𝑏 ‘ 𝐴 ) )
64 59 63 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 ‘ 𝐴 ) ) ‘ 𝑎 ) ( .r ‘ 𝑅 ) ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 ‘ 𝐴 ) ) ‘ 𝑏 ) ) = ( ( 𝑎 ‘ 𝐴 ) ( .r ‘ 𝑅 ) ( 𝑏 ‘ 𝐴 ) ) )
65 47 55 64 3eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 ‘ 𝐴 ) ) ‘ ( 𝑎 ( .r ‘ 𝑌 ) 𝑏 ) ) = ( ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 ‘ 𝐴 ) ) ‘ 𝑎 ) ( .r ‘ 𝑅 ) ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 ‘ 𝐴 ) ) ‘ 𝑏 ) ) )
66 2 15 ringidcl ⊢ ( 𝑌 ∈ Ring → ( 1r ‘ 𝑌 ) ∈ 𝐵 )
67 fveq1 ⊢ ( 𝑥 = ( 1r ‘ 𝑌 ) → ( 𝑥 ‘ 𝐴 ) = ( ( 1r ‘ 𝑌 ) ‘ 𝐴 ) )
68 fvex ⊢ ( ( 1r ‘ 𝑌 ) ‘ 𝐴 ) ∈ V
69 67 52 68 fvmpt ⊢ ( ( 1r ‘ 𝑌 ) ∈ 𝐵 → ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 ‘ 𝐴 ) ) ‘ ( 1r ‘ 𝑌 ) ) = ( ( 1r ‘ 𝑌 ) ‘ 𝐴 ) )
70 20 66 69 3syl ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 ‘ 𝐴 ) ) ‘ ( 1r ‘ 𝑌 ) ) = ( ( 1r ‘ 𝑌 ) ‘ 𝐴 ) )
71 1 17 pws1 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) → ( 𝐼 × { ( 1r ‘ 𝑅 ) } ) = ( 1r ‘ 𝑌 ) )
72 5 6 71 syl2anc ⊢ ( 𝜑 → ( 𝐼 × { ( 1r ‘ 𝑅 ) } ) = ( 1r ‘ 𝑌 ) )
73 72 fveq1d ⊢ ( 𝜑 → ( ( 𝐼 × { ( 1r ‘ 𝑅 ) } ) ‘ 𝐴 ) = ( ( 1r ‘ 𝑌 ) ‘ 𝐴 ) )
74 fvex ⊢ ( 1r ‘ 𝑅 ) ∈ V
75 74 fvconst2 ⊢ ( 𝐴 ∈ 𝐼 → ( ( 𝐼 × { ( 1r ‘ 𝑅 ) } ) ‘ 𝐴 ) = ( 1r ‘ 𝑅 ) )
76 7 75 syl ⊢ ( 𝜑 → ( ( 𝐼 × { ( 1r ‘ 𝑅 ) } ) ‘ 𝐴 ) = ( 1r ‘ 𝑅 ) )
77 70 73 76 3eqtr2d ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 ‘ 𝐴 ) ) ‘ ( 1r ‘ 𝑌 ) ) = ( 1r ‘ 𝑅 ) )
78 8 10 12 14 16 18 22 24 31 65 77 ismhmd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 ‘ 𝐴 ) ) ∈ ( 𝑀 MndHom 𝑇 ) )