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 
|- Y = ( R ^s I )
pwspjmhmmgpd.b 
|- B = ( Base ` Y )
pwspjmhmmgpd.m 
|- M = ( mulGrp ` Y )
pwspjmhmmgpd.t 
|- T = ( mulGrp ` R )
pwspjmhmmgpd.r 
|- ( ph -> R e. Ring )
pwspjmhmmgpd.i 
|- ( ph -> I e. V )
pwspjmhmmgpd.a 
|- ( ph -> A e. I )
Assertion pwspjmhmmgpd 
|- ( ph -> ( x e. B |-> ( x ` A ) ) e. ( M MndHom T ) )

Proof

Step Hyp Ref Expression
1 pwspjmhmmgpd.y 
 |-  Y = ( R ^s I )
2 pwspjmhmmgpd.b 
 |-  B = ( Base ` Y )
3 pwspjmhmmgpd.m 
 |-  M = ( mulGrp ` Y )
4 pwspjmhmmgpd.t 
 |-  T = ( mulGrp ` R )
5 pwspjmhmmgpd.r 
 |-  ( ph -> R e. Ring )
6 pwspjmhmmgpd.i 
 |-  ( ph -> I e. V )
7 pwspjmhmmgpd.a 
 |-  ( ph -> A e. I )
8 3 2 mgpbas 
 |-  B = ( Base ` M )
9 eqid 
 |-  ( Base ` R ) = ( Base ` R )
10 4 9 mgpbas 
 |-  ( Base ` R ) = ( Base ` T )
11 eqid 
 |-  ( .r ` Y ) = ( .r ` Y )
12 3 11 mgpplusg 
 |-  ( .r ` Y ) = ( +g ` M )
13 eqid 
 |-  ( .r ` R ) = ( .r ` R )
14 4 13 mgpplusg 
 |-  ( .r ` R ) = ( +g ` T )
15 eqid 
 |-  ( 1r ` Y ) = ( 1r ` Y )
16 3 15 ringidval 
 |-  ( 1r ` Y ) = ( 0g ` M )
17 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
18 4 17 ringidval 
 |-  ( 1r ` R ) = ( 0g ` T )
19 1 pwsring 
 |-  ( ( R e. Ring /\ I e. V ) -> Y e. Ring )
20 5 6 19 syl2anc 
 |-  ( ph -> Y e. Ring )
21 3 ringmgp 
 |-  ( Y e. Ring -> M e. Mnd )
22 20 21 syl 
 |-  ( ph -> M e. Mnd )
23 4 ringmgp 
 |-  ( R e. Ring -> T e. Mnd )
24 5 23 syl 
 |-  ( ph -> T e. Mnd )
25 5 adantr 
 |-  ( ( ph /\ x e. B ) -> R e. Ring )
26 6 adantr 
 |-  ( ( ph /\ x e. B ) -> I e. V )
27 simpr 
 |-  ( ( ph /\ x e. B ) -> x e. B )
28 1 9 2 25 26 27 pwselbas 
 |-  ( ( ph /\ x e. B ) -> x : I --> ( Base ` R ) )
29 7 adantr 
 |-  ( ( ph /\ x e. B ) -> A e. I )
30 28 29 ffvelrnd 
 |-  ( ( ph /\ x e. B ) -> ( x ` A ) e. ( Base ` R ) )
31 30 fmpttd 
 |-  ( ph -> ( x e. B |-> ( x ` A ) ) : B --> ( Base ` R ) )
32 5 adantr 
 |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> R e. Ring )
33 6 adantr 
 |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> I e. V )
34 simprl 
 |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> a e. B )
35 simprr 
 |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> b e. B )
36 1 2 32 33 34 35 13 11 pwsmulrval 
 |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> ( a ( .r ` Y ) b ) = ( a oF ( .r ` R ) b ) )
37 36 fveq1d 
 |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> ( ( a ( .r ` Y ) b ) ` A ) = ( ( a oF ( .r ` R ) b ) ` A ) )
38 1 9 2 32 33 34 pwselbas 
 |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> a : I --> ( Base ` R ) )
39 38 ffnd 
 |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> a Fn I )
40 1 9 2 32 33 35 pwselbas 
 |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> b : I --> ( Base ` R ) )
41 40 ffnd 
 |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> b Fn I )
42 inidm 
 |-  ( I i^i I ) = I
43 eqidd 
 |-  ( ( ( ph /\ ( a e. B /\ b e. B ) ) /\ A e. I ) -> ( a ` A ) = ( a ` A ) )
44 eqidd 
 |-  ( ( ( ph /\ ( a e. B /\ b e. B ) ) /\ A e. I ) -> ( b ` A ) = ( b ` A ) )
45 39 41 33 33 42 43 44 ofval 
 |-  ( ( ( ph /\ ( a e. B /\ b e. B ) ) /\ A e. I ) -> ( ( a oF ( .r ` R ) b ) ` A ) = ( ( a ` A ) ( .r ` R ) ( b ` A ) ) )
46 7 45 mpidan 
 |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> ( ( a oF ( .r ` R ) b ) ` A ) = ( ( a ` A ) ( .r ` R ) ( b ` A ) ) )
47 37 46 eqtrd 
 |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> ( ( a ( .r ` Y ) b ) ` A ) = ( ( a ` A ) ( .r ` R ) ( b ` A ) ) )
48 2 11 ringcl 
 |-  ( ( Y e. Ring /\ a e. B /\ b e. B ) -> ( a ( .r ` Y ) b ) e. B )
49 20 48 syl3an1 
 |-  ( ( ph /\ a e. B /\ b e. B ) -> ( a ( .r ` Y ) b ) e. B )
50 49 3expb 
 |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> ( a ( .r ` Y ) b ) e. B )
51 fveq1 
 |-  ( x = ( a ( .r ` Y ) b ) -> ( x ` A ) = ( ( a ( .r ` Y ) b ) ` A ) )
52 eqid 
 |-  ( x e. B |-> ( x ` A ) ) = ( x e. B |-> ( x ` A ) )
53 fvex 
 |-  ( ( a ( .r ` Y ) b ) ` A ) e. _V
54 51 52 53 fvmpt 
 |-  ( ( a ( .r ` Y ) b ) e. B -> ( ( x e. B |-> ( x ` A ) ) ` ( a ( .r ` Y ) b ) ) = ( ( a ( .r ` Y ) b ) ` A ) )
55 50 54 syl 
 |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> ( ( x e. B |-> ( x ` A ) ) ` ( a ( .r ` Y ) b ) ) = ( ( a ( .r ` Y ) b ) ` A ) )
56 fveq1 
 |-  ( x = a -> ( x ` A ) = ( a ` A ) )
57 fvex 
 |-  ( a ` A ) e. _V
58 56 52 57 fvmpt 
 |-  ( a e. B -> ( ( x e. B |-> ( x ` A ) ) ` a ) = ( a ` A ) )
59 34 58 syl 
 |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> ( ( x e. B |-> ( x ` A ) ) ` a ) = ( a ` A ) )
60 fveq1 
 |-  ( x = b -> ( x ` A ) = ( b ` A ) )
61 fvex 
 |-  ( b ` A ) e. _V
62 60 52 61 fvmpt 
 |-  ( b e. B -> ( ( x e. B |-> ( x ` A ) ) ` b ) = ( b ` A ) )
63 35 62 syl 
 |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> ( ( x e. B |-> ( x ` A ) ) ` b ) = ( b ` A ) )
64 59 63 oveq12d 
 |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> ( ( ( x e. B |-> ( x ` A ) ) ` a ) ( .r ` R ) ( ( x e. B |-> ( x ` A ) ) ` b ) ) = ( ( a ` A ) ( .r ` R ) ( b ` A ) ) )
65 47 55 64 3eqtr4d 
 |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> ( ( x e. B |-> ( x ` A ) ) ` ( a ( .r ` Y ) b ) ) = ( ( ( x e. B |-> ( x ` A ) ) ` a ) ( .r ` R ) ( ( x e. B |-> ( x ` A ) ) ` b ) ) )
66 2 15 ringidcl 
 |-  ( Y e. Ring -> ( 1r ` Y ) e. B )
67 fveq1 
 |-  ( x = ( 1r ` Y ) -> ( x ` A ) = ( ( 1r ` Y ) ` A ) )
68 fvex 
 |-  ( ( 1r ` Y ) ` A ) e. _V
69 67 52 68 fvmpt 
 |-  ( ( 1r ` Y ) e. B -> ( ( x e. B |-> ( x ` A ) ) ` ( 1r ` Y ) ) = ( ( 1r ` Y ) ` A ) )
70 20 66 69 3syl 
 |-  ( ph -> ( ( x e. B |-> ( x ` A ) ) ` ( 1r ` Y ) ) = ( ( 1r ` Y ) ` A ) )
71 1 17 pws1 
 |-  ( ( R e. Ring /\ I e. V ) -> ( I X. { ( 1r ` R ) } ) = ( 1r ` Y ) )
72 5 6 71 syl2anc 
 |-  ( ph -> ( I X. { ( 1r ` R ) } ) = ( 1r ` Y ) )
73 72 fveq1d 
 |-  ( ph -> ( ( I X. { ( 1r ` R ) } ) ` A ) = ( ( 1r ` Y ) ` A ) )
74 fvex 
 |-  ( 1r ` R ) e. _V
75 74 fvconst2 
 |-  ( A e. I -> ( ( I X. { ( 1r ` R ) } ) ` A ) = ( 1r ` R ) )
76 7 75 syl 
 |-  ( ph -> ( ( I X. { ( 1r ` R ) } ) ` A ) = ( 1r ` R ) )
77 70 73 76 3eqtr2d 
 |-  ( ph -> ( ( x e. B |-> ( x ` A ) ) ` ( 1r ` Y ) ) = ( 1r ` R ) )
78 8 10 12 14 16 18 22 24 31 65 77 ismhmd 
 |-  ( ph -> ( x e. B |-> ( x ` A ) ) e. ( M MndHom T ) )