This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ismhm

Description: Property of a monoid homomorphism. (Contributed by Mario Carneiro, 7-Mar-2015)

Ref Expression
Hypotheses ismhm.b 
|- B = ( Base ` S )
ismhm.c 
|- C = ( Base ` T )
ismhm.p 
|- .+ = ( +g ` S )
ismhm.q 
|- .+^ = ( +g ` T )
ismhm.z 
|- .0. = ( 0g ` S )
ismhm.y 
|- Y = ( 0g ` T )
Assertion ismhm 
|- ( F e. ( S MndHom T ) <-> ( ( S e. Mnd /\ T e. Mnd ) /\ ( F : B --> C /\ A. x e. B A. y e. B ( F ` ( x .+ y ) ) = ( ( F ` x ) .+^ ( F ` y ) ) /\ ( F ` .0. ) = Y ) ) )

Proof

Step Hyp Ref Expression
1 ismhm.b 
 |-  B = ( Base ` S )
2 ismhm.c 
 |-  C = ( Base ` T )
3 ismhm.p 
 |-  .+ = ( +g ` S )
4 ismhm.q 
 |-  .+^ = ( +g ` T )
5 ismhm.z 
 |-  .0. = ( 0g ` S )
6 ismhm.y 
 |-  Y = ( 0g ` T )
7 df-mhm 
 |-  MndHom = ( s e. Mnd , t e. Mnd |-> { f e. ( ( Base ` t ) ^m ( Base ` s ) ) | ( A. x e. ( Base ` s ) A. y e. ( Base ` s ) ( f ` ( x ( +g ` s ) y ) ) = ( ( f ` x ) ( +g ` t ) ( f ` y ) ) /\ ( f ` ( 0g ` s ) ) = ( 0g ` t ) ) } )
8 7 elmpocl 
 |-  ( F e. ( S MndHom T ) -> ( S e. Mnd /\ T e. Mnd ) )
9 fveq2 
 |-  ( t = T -> ( Base ` t ) = ( Base ` T ) )
10 9 2 eqtr4di 
 |-  ( t = T -> ( Base ` t ) = C )
11 fveq2 
 |-  ( s = S -> ( Base ` s ) = ( Base ` S ) )
12 11 1 eqtr4di 
 |-  ( s = S -> ( Base ` s ) = B )
13 10 12 oveqan12rd 
 |-  ( ( s = S /\ t = T ) -> ( ( Base ` t ) ^m ( Base ` s ) ) = ( C ^m B ) )
14 12 adantr 
 |-  ( ( s = S /\ t = T ) -> ( Base ` s ) = B )
15 fveq2 
 |-  ( s = S -> ( +g ` s ) = ( +g ` S ) )
16 15 3 eqtr4di 
 |-  ( s = S -> ( +g ` s ) = .+ )
17 16 oveqd 
 |-  ( s = S -> ( x ( +g ` s ) y ) = ( x .+ y ) )
18 17 fveq2d 
 |-  ( s = S -> ( f ` ( x ( +g ` s ) y ) ) = ( f ` ( x .+ y ) ) )
19 fveq2 
 |-  ( t = T -> ( +g ` t ) = ( +g ` T ) )
20 19 4 eqtr4di 
 |-  ( t = T -> ( +g ` t ) = .+^ )
21 20 oveqd 
 |-  ( t = T -> ( ( f ` x ) ( +g ` t ) ( f ` y ) ) = ( ( f ` x ) .+^ ( f ` y ) ) )
22 18 21 eqeqan12d 
 |-  ( ( s = S /\ t = T ) -> ( ( f ` ( x ( +g ` s ) y ) ) = ( ( f ` x ) ( +g ` t ) ( f ` y ) ) <-> ( f ` ( x .+ y ) ) = ( ( f ` x ) .+^ ( f ` y ) ) ) )
23 14 22 raleqbidv 
 |-  ( ( s = S /\ t = T ) -> ( A. y e. ( Base ` s ) ( f ` ( x ( +g ` s ) y ) ) = ( ( f ` x ) ( +g ` t ) ( f ` y ) ) <-> A. y e. B ( f ` ( x .+ y ) ) = ( ( f ` x ) .+^ ( f ` y ) ) ) )
24 14 23 raleqbidv 
 |-  ( ( s = S /\ t = T ) -> ( A. x e. ( Base ` s ) A. y e. ( Base ` s ) ( f ` ( x ( +g ` s ) y ) ) = ( ( f ` x ) ( +g ` t ) ( f ` y ) ) <-> A. x e. B A. y e. B ( f ` ( x .+ y ) ) = ( ( f ` x ) .+^ ( f ` y ) ) ) )
25 fveq2 
 |-  ( s = S -> ( 0g ` s ) = ( 0g ` S ) )
26 25 5 eqtr4di 
 |-  ( s = S -> ( 0g ` s ) = .0. )
27 26 fveq2d 
 |-  ( s = S -> ( f ` ( 0g ` s ) ) = ( f ` .0. ) )
28 fveq2 
 |-  ( t = T -> ( 0g ` t ) = ( 0g ` T ) )
29 28 6 eqtr4di 
 |-  ( t = T -> ( 0g ` t ) = Y )
30 27 29 eqeqan12d 
 |-  ( ( s = S /\ t = T ) -> ( ( f ` ( 0g ` s ) ) = ( 0g ` t ) <-> ( f ` .0. ) = Y ) )
31 24 30 anbi12d 
 |-  ( ( s = S /\ t = T ) -> ( ( A. x e. ( Base ` s ) A. y e. ( Base ` s ) ( f ` ( x ( +g ` s ) y ) ) = ( ( f ` x ) ( +g ` t ) ( f ` y ) ) /\ ( f ` ( 0g ` s ) ) = ( 0g ` t ) ) <-> ( A. x e. B A. y e. B ( f ` ( x .+ y ) ) = ( ( f ` x ) .+^ ( f ` y ) ) /\ ( f ` .0. ) = Y ) ) )
32 13 31 rabeqbidv 
 |-  ( ( s = S /\ t = T ) -> { f e. ( ( Base ` t ) ^m ( Base ` s ) ) | ( A. x e. ( Base ` s ) A. y e. ( Base ` s ) ( f ` ( x ( +g ` s ) y ) ) = ( ( f ` x ) ( +g ` t ) ( f ` y ) ) /\ ( f ` ( 0g ` s ) ) = ( 0g ` t ) ) } = { f e. ( C ^m B ) | ( A. x e. B A. y e. B ( f ` ( x .+ y ) ) = ( ( f ` x ) .+^ ( f ` y ) ) /\ ( f ` .0. ) = Y ) } )
33 ovex 
 |-  ( C ^m B ) e. _V
34 33 rabex 
 |-  { f e. ( C ^m B ) | ( A. x e. B A. y e. B ( f ` ( x .+ y ) ) = ( ( f ` x ) .+^ ( f ` y ) ) /\ ( f ` .0. ) = Y ) } e. _V
35 32 7 34 ovmpoa 
 |-  ( ( S e. Mnd /\ T e. Mnd ) -> ( S MndHom T ) = { f e. ( C ^m B ) | ( A. x e. B A. y e. B ( f ` ( x .+ y ) ) = ( ( f ` x ) .+^ ( f ` y ) ) /\ ( f ` .0. ) = Y ) } )
36 35 eleq2d 
 |-  ( ( S e. Mnd /\ T e. Mnd ) -> ( F e. ( S MndHom T ) <-> F e. { f e. ( C ^m B ) | ( A. x e. B A. y e. B ( f ` ( x .+ y ) ) = ( ( f ` x ) .+^ ( f ` y ) ) /\ ( f ` .0. ) = Y ) } ) )
37 2 fvexi 
 |-  C e. _V
38 1 fvexi 
 |-  B e. _V
39 37 38 elmap 
 |-  ( F e. ( C ^m B ) <-> F : B --> C )
40 39 anbi1i 
 |-  ( ( F e. ( C ^m B ) /\ ( A. x e. B A. y e. B ( F ` ( x .+ y ) ) = ( ( F ` x ) .+^ ( F ` y ) ) /\ ( F ` .0. ) = Y ) ) <-> ( F : B --> C /\ ( A. x e. B A. y e. B ( F ` ( x .+ y ) ) = ( ( F ` x ) .+^ ( F ` y ) ) /\ ( F ` .0. ) = Y ) ) )
41 fveq1 
 |-  ( f = F -> ( f ` ( x .+ y ) ) = ( F ` ( x .+ y ) ) )
42 fveq1 
 |-  ( f = F -> ( f ` x ) = ( F ` x ) )
43 fveq1 
 |-  ( f = F -> ( f ` y ) = ( F ` y ) )
44 42 43 oveq12d 
 |-  ( f = F -> ( ( f ` x ) .+^ ( f ` y ) ) = ( ( F ` x ) .+^ ( F ` y ) ) )
45 41 44 eqeq12d 
 |-  ( f = F -> ( ( f ` ( x .+ y ) ) = ( ( f ` x ) .+^ ( f ` y ) ) <-> ( F ` ( x .+ y ) ) = ( ( F ` x ) .+^ ( F ` y ) ) ) )
46 45 2ralbidv 
 |-  ( f = F -> ( A. x e. B A. y e. B ( f ` ( x .+ y ) ) = ( ( f ` x ) .+^ ( f ` y ) ) <-> A. x e. B A. y e. B ( F ` ( x .+ y ) ) = ( ( F ` x ) .+^ ( F ` y ) ) ) )
47 fveq1 
 |-  ( f = F -> ( f ` .0. ) = ( F ` .0. ) )
48 47 eqeq1d 
 |-  ( f = F -> ( ( f ` .0. ) = Y <-> ( F ` .0. ) = Y ) )
49 46 48 anbi12d 
 |-  ( f = F -> ( ( A. x e. B A. y e. B ( f ` ( x .+ y ) ) = ( ( f ` x ) .+^ ( f ` y ) ) /\ ( f ` .0. ) = Y ) <-> ( A. x e. B A. y e. B ( F ` ( x .+ y ) ) = ( ( F ` x ) .+^ ( F ` y ) ) /\ ( F ` .0. ) = Y ) ) )
50 49 elrab 
 |-  ( F e. { f e. ( C ^m B ) | ( A. x e. B A. y e. B ( f ` ( x .+ y ) ) = ( ( f ` x ) .+^ ( f ` y ) ) /\ ( f ` .0. ) = Y ) } <-> ( F e. ( C ^m B ) /\ ( A. x e. B A. y e. B ( F ` ( x .+ y ) ) = ( ( F ` x ) .+^ ( F ` y ) ) /\ ( F ` .0. ) = Y ) ) )
51 3anass 
 |-  ( ( F : B --> C /\ A. x e. B A. y e. B ( F ` ( x .+ y ) ) = ( ( F ` x ) .+^ ( F ` y ) ) /\ ( F ` .0. ) = Y ) <-> ( F : B --> C /\ ( A. x e. B A. y e. B ( F ` ( x .+ y ) ) = ( ( F ` x ) .+^ ( F ` y ) ) /\ ( F ` .0. ) = Y ) ) )
52 40 50 51 3bitr4i 
 |-  ( F e. { f e. ( C ^m B ) | ( A. x e. B A. y e. B ( f ` ( x .+ y ) ) = ( ( f ` x ) .+^ ( f ` y ) ) /\ ( f ` .0. ) = Y ) } <-> ( F : B --> C /\ A. x e. B A. y e. B ( F ` ( x .+ y ) ) = ( ( F ` x ) .+^ ( F ` y ) ) /\ ( F ` .0. ) = Y ) )
53 36 52 bitrdi 
 |-  ( ( S e. Mnd /\ T e. Mnd ) -> ( F e. ( S MndHom T ) <-> ( F : B --> C /\ A. x e. B A. y e. B ( F ` ( x .+ y ) ) = ( ( F ` x ) .+^ ( F ` y ) ) /\ ( F ` .0. ) = Y ) ) )
54 8 53 biadanii 
 |-  ( F e. ( S MndHom T ) <-> ( ( S e. Mnd /\ T e. Mnd ) /\ ( F : B --> C /\ A. x e. B A. y e. B ( F ` ( x .+ y ) ) = ( ( F ` x ) .+^ ( F ` y ) ) /\ ( F ` .0. ) = Y ) ) )