Metamath Proof Explorer

Theorem prdspjmhm

Description: A projection from a product of monoids to one of the factors is a monoid homomorphism. (Contributed by Mario Carneiro, 6-May-2015)

Ref Expression
Hypotheses prdspjmhm.y 
|- Y = ( S Xs_ R )
prdspjmhm.b 
|- B = ( Base ` Y )
prdspjmhm.i 
|- ( ph -> I e. V )
prdspjmhm.s 
|- ( ph -> S e. X )
prdspjmhm.r 
|- ( ph -> R : I --> Mnd )
prdspjmhm.a 
|- ( ph -> A e. I )
Assertion prdspjmhm 
|- ( ph -> ( x e. B |-> ( x ` A ) ) e. ( Y MndHom ( R ` A ) ) )

Proof

Step Hyp Ref Expression
1 prdspjmhm.y 
 |-  Y = ( S Xs_ R )
2 prdspjmhm.b 
 |-  B = ( Base ` Y )
3 prdspjmhm.i 
 |-  ( ph -> I e. V )
4 prdspjmhm.s 
 |-  ( ph -> S e. X )
5 prdspjmhm.r 
 |-  ( ph -> R : I --> Mnd )
6 prdspjmhm.a 
 |-  ( ph -> A e. I )
7 1 3 4 5 prdsmndd 
 |-  ( ph -> Y e. Mnd )
8 5 6 ffvelrnd 
 |-  ( ph -> ( R ` A ) e. Mnd )
9 4 adantr 
 |-  ( ( ph /\ x e. B ) -> S e. X )
10 3 adantr 
 |-  ( ( ph /\ x e. B ) -> I e. V )
11 5 ffnd 
 |-  ( ph -> R Fn I )
12 11 adantr 
 |-  ( ( ph /\ x e. B ) -> R Fn I )
13 simpr 
 |-  ( ( ph /\ x e. B ) -> x e. B )
14 6 adantr 
 |-  ( ( ph /\ x e. B ) -> A e. I )
15 1 2 9 10 12 13 14 prdsbasprj 
 |-  ( ( ph /\ x e. B ) -> ( x ` A ) e. ( Base ` ( R ` A ) ) )
16 15 fmpttd 
 |-  ( ph -> ( x e. B |-> ( x ` A ) ) : B --> ( Base ` ( R ` A ) ) )
17 4 adantr 
 |-  ( ( ph /\ ( y e. B /\ z e. B ) ) -> S e. X )
18 3 adantr 
 |-  ( ( ph /\ ( y e. B /\ z e. B ) ) -> I e. V )
19 11 adantr 
 |-  ( ( ph /\ ( y e. B /\ z e. B ) ) -> R Fn I )
20 simprl 
 |-  ( ( ph /\ ( y e. B /\ z e. B ) ) -> y e. B )
21 simprr 
 |-  ( ( ph /\ ( y e. B /\ z e. B ) ) -> z e. B )
22 eqid 
 |-  ( +g ` Y ) = ( +g ` Y )
23 6 adantr 
 |-  ( ( ph /\ ( y e. B /\ z e. B ) ) -> A e. I )
24 1 2 17 18 19 20 21 22 23 prdsplusgfval 
 |-  ( ( ph /\ ( y e. B /\ z e. B ) ) -> ( ( y ( +g ` Y ) z ) ` A ) = ( ( y ` A ) ( +g ` ( R ` A ) ) ( z ` A ) ) )
25 2 22 mndcl 
 |-  ( ( Y e. Mnd /\ y e. B /\ z e. B ) -> ( y ( +g ` Y ) z ) e. B )
26 25 3expb 
 |-  ( ( Y e. Mnd /\ ( y e. B /\ z e. B ) ) -> ( y ( +g ` Y ) z ) e. B )
27 7 26 sylan 
 |-  ( ( ph /\ ( y e. B /\ z e. B ) ) -> ( y ( +g ` Y ) z ) e. B )
28 fveq1 
 |-  ( x = ( y ( +g ` Y ) z ) -> ( x ` A ) = ( ( y ( +g ` Y ) z ) ` A ) )
29 eqid 
 |-  ( x e. B |-> ( x ` A ) ) = ( x e. B |-> ( x ` A ) )
30 fvex 
 |-  ( ( y ( +g ` Y ) z ) ` A ) e. _V
31 28 29 30 fvmpt 
 |-  ( ( y ( +g ` Y ) z ) e. B -> ( ( x e. B |-> ( x ` A ) ) ` ( y ( +g ` Y ) z ) ) = ( ( y ( +g ` Y ) z ) ` A ) )
32 27 31 syl 
 |-  ( ( ph /\ ( y e. B /\ z e. B ) ) -> ( ( x e. B |-> ( x ` A ) ) ` ( y ( +g ` Y ) z ) ) = ( ( y ( +g ` Y ) z ) ` A ) )
33 fveq1 
 |-  ( x = y -> ( x ` A ) = ( y ` A ) )
34 fvex 
 |-  ( y ` A ) e. _V
35 33 29 34 fvmpt 
 |-  ( y e. B -> ( ( x e. B |-> ( x ` A ) ) ` y ) = ( y ` A ) )
36 fveq1 
 |-  ( x = z -> ( x ` A ) = ( z ` A ) )
37 fvex 
 |-  ( z ` A ) e. _V
38 36 29 37 fvmpt 
 |-  ( z e. B -> ( ( x e. B |-> ( x ` A ) ) ` z ) = ( z ` A ) )
39 35 38 oveqan12d 
 |-  ( ( y e. B /\ z e. B ) -> ( ( ( x e. B |-> ( x ` A ) ) ` y ) ( +g ` ( R ` A ) ) ( ( x e. B |-> ( x ` A ) ) ` z ) ) = ( ( y ` A ) ( +g ` ( R ` A ) ) ( z ` A ) ) )
40 39 adantl 
 |-  ( ( ph /\ ( y e. B /\ z e. B ) ) -> ( ( ( x e. B |-> ( x ` A ) ) ` y ) ( +g ` ( R ` A ) ) ( ( x e. B |-> ( x ` A ) ) ` z ) ) = ( ( y ` A ) ( +g ` ( R ` A ) ) ( z ` A ) ) )
41 24 32 40 3eqtr4d 
 |-  ( ( ph /\ ( y e. B /\ z e. B ) ) -> ( ( x e. B |-> ( x ` A ) ) ` ( y ( +g ` Y ) z ) ) = ( ( ( x e. B |-> ( x ` A ) ) ` y ) ( +g ` ( R ` A ) ) ( ( x e. B |-> ( x ` A ) ) ` z ) ) )
42 41 ralrimivva 
 |-  ( ph -> A. y e. B A. z e. B ( ( x e. B |-> ( x ` A ) ) ` ( y ( +g ` Y ) z ) ) = ( ( ( x e. B |-> ( x ` A ) ) ` y ) ( +g ` ( R ` A ) ) ( ( x e. B |-> ( x ` A ) ) ` z ) ) )
43 eqid 
 |-  ( 0g ` Y ) = ( 0g ` Y )
44 2 43 mndidcl 
 |-  ( Y e. Mnd -> ( 0g ` Y ) e. B )
45 fveq1 
 |-  ( x = ( 0g ` Y ) -> ( x ` A ) = ( ( 0g ` Y ) ` A ) )
46 fvex 
 |-  ( ( 0g ` Y ) ` A ) e. _V
47 45 29 46 fvmpt 
 |-  ( ( 0g ` Y ) e. B -> ( ( x e. B |-> ( x ` A ) ) ` ( 0g ` Y ) ) = ( ( 0g ` Y ) ` A ) )
48 7 44 47 3syl 
 |-  ( ph -> ( ( x e. B |-> ( x ` A ) ) ` ( 0g ` Y ) ) = ( ( 0g ` Y ) ` A ) )
49 1 3 4 5 prds0g 
 |-  ( ph -> ( 0g o. R ) = ( 0g ` Y ) )
50 49 fveq1d 
 |-  ( ph -> ( ( 0g o. R ) ` A ) = ( ( 0g ` Y ) ` A ) )
51 fvco3 
 |-  ( ( R : I --> Mnd /\ A e. I ) -> ( ( 0g o. R ) ` A ) = ( 0g ` ( R ` A ) ) )
52 5 6 51 syl2anc 
 |-  ( ph -> ( ( 0g o. R ) ` A ) = ( 0g ` ( R ` A ) ) )
53 48 50 52 3eqtr2d 
 |-  ( ph -> ( ( x e. B |-> ( x ` A ) ) ` ( 0g ` Y ) ) = ( 0g ` ( R ` A ) ) )
54 16 42 53 3jca 
 |-  ( ph -> ( ( x e. B |-> ( x ` A ) ) : B --> ( Base ` ( R ` A ) ) /\ A. y e. B A. z e. B ( ( x e. B |-> ( x ` A ) ) ` ( y ( +g ` Y ) z ) ) = ( ( ( x e. B |-> ( x ` A ) ) ` y ) ( +g ` ( R ` A ) ) ( ( x e. B |-> ( x ` A ) ) ` z ) ) /\ ( ( x e. B |-> ( x ` A ) ) ` ( 0g ` Y ) ) = ( 0g ` ( R ` A ) ) ) )
55 eqid 
 |-  ( Base ` ( R ` A ) ) = ( Base ` ( R ` A ) )
56 eqid 
 |-  ( +g ` ( R ` A ) ) = ( +g ` ( R ` A ) )
57 eqid 
 |-  ( 0g ` ( R ` A ) ) = ( 0g ` ( R ` A ) )
58 2 55 22 56 43 57 ismhm 
 |-  ( ( x e. B |-> ( x ` A ) ) e. ( Y MndHom ( R ` A ) ) <-> ( ( Y e. Mnd /\ ( R ` A ) e. Mnd ) /\ ( ( x e. B |-> ( x ` A ) ) : B --> ( Base ` ( R ` A ) ) /\ A. y e. B A. z e. B ( ( x e. B |-> ( x ` A ) ) ` ( y ( +g ` Y ) z ) ) = ( ( ( x e. B |-> ( x ` A ) ) ` y ) ( +g ` ( R ` A ) ) ( ( x e. B |-> ( x ` A ) ) ` z ) ) /\ ( ( x e. B |-> ( x ` A ) ) ` ( 0g ` Y ) ) = ( 0g ` ( R ` A ) ) ) ) )
59 7 8 54 58 syl21anbrc 
 |-  ( ph -> ( x e. B |-> ( x ` A ) ) e. ( Y MndHom ( R ` A ) ) )