Metamath Proof Explorer

Theorem ismgmhm

Description: Property of a magma homomorphism. (Contributed by AV, 25-Feb-2020)

Ref Expression
Hypotheses ismgmhm.b 
|- B = ( Base ` S )
ismgmhm.c 
|- C = ( Base ` T )
ismgmhm.p 
|- .+ = ( +g ` S )
ismgmhm.q 
|- .+^ = ( +g ` T )
Assertion ismgmhm 
|- ( F e. ( S MgmHom T ) <-> ( ( S e. Mgm /\ T e. Mgm ) /\ ( F : B --> C /\ A. x e. B A. y e. B ( F ` ( x .+ y ) ) = ( ( F ` x ) .+^ ( F ` y ) ) ) ) )

Proof

Step Hyp Ref Expression
1 ismgmhm.b 
 |-  B = ( Base ` S )
2 ismgmhm.c 
 |-  C = ( Base ` T )
3 ismgmhm.p 
 |-  .+ = ( +g ` S )
4 ismgmhm.q 
 |-  .+^ = ( +g ` T )
5 mgmhmrcl 
 |-  ( F e. ( S MgmHom T ) -> ( S e. Mgm /\ T e. Mgm ) )
6 fveq2 
 |-  ( t = T -> ( Base ` t ) = ( Base ` T ) )
7 6 2 eqtr4di 
 |-  ( t = T -> ( Base ` t ) = C )
8 fveq2 
 |-  ( s = S -> ( Base ` s ) = ( Base ` S ) )
9 8 1 eqtr4di 
 |-  ( s = S -> ( Base ` s ) = B )
10 7 9 oveqan12rd 
 |-  ( ( s = S /\ t = T ) -> ( ( Base ` t ) ^m ( Base ` s ) ) = ( C ^m B ) )
11 9 adantr 
 |-  ( ( s = S /\ t = T ) -> ( Base ` s ) = B )
12 fveq2 
 |-  ( s = S -> ( +g ` s ) = ( +g ` S ) )
13 12 3 eqtr4di 
 |-  ( s = S -> ( +g ` s ) = .+ )
14 13 oveqd 
 |-  ( s = S -> ( x ( +g ` s ) y ) = ( x .+ y ) )
15 14 fveq2d 
 |-  ( s = S -> ( f ` ( x ( +g ` s ) y ) ) = ( f ` ( x .+ y ) ) )
16 fveq2 
 |-  ( t = T -> ( +g ` t ) = ( +g ` T ) )
17 16 4 eqtr4di 
 |-  ( t = T -> ( +g ` t ) = .+^ )
18 17 oveqd 
 |-  ( t = T -> ( ( f ` x ) ( +g ` t ) ( f ` y ) ) = ( ( f ` x ) .+^ ( f ` y ) ) )
19 15 18 eqeqan12d 
 |-  ( ( s = S /\ t = T ) -> ( ( f ` ( x ( +g ` s ) y ) ) = ( ( f ` x ) ( +g ` t ) ( f ` y ) ) <-> ( f ` ( x .+ y ) ) = ( ( f ` x ) .+^ ( f ` y ) ) ) )
20 11 19 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 ) ) ) )
21 11 20 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 ) ) ) )
22 10 21 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 e. ( C ^m B ) | A. x e. B A. y e. B ( f ` ( x .+ y ) ) = ( ( f ` x ) .+^ ( f ` y ) ) } )
23 df-mgmhm 
 |-  MgmHom = ( s e. Mgm , t e. Mgm |-> { 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 ) ) } )
24 ovex 
 |-  ( C ^m B ) e. _V
25 24 rabex 
 |-  { f e. ( C ^m B ) | A. x e. B A. y e. B ( f ` ( x .+ y ) ) = ( ( f ` x ) .+^ ( f ` y ) ) } e. _V
26 22 23 25 ovmpoa 
 |-  ( ( S e. Mgm /\ T e. Mgm ) -> ( S MgmHom T ) = { f e. ( C ^m B ) | A. x e. B A. y e. B ( f ` ( x .+ y ) ) = ( ( f ` x ) .+^ ( f ` y ) ) } )
27 26 eleq2d 
 |-  ( ( S e. Mgm /\ T e. Mgm ) -> ( F e. ( S MgmHom T ) <-> F e. { f e. ( C ^m B ) | A. x e. B A. y e. B ( f ` ( x .+ y ) ) = ( ( f ` x ) .+^ ( f ` y ) ) } ) )
28 fveq1 
 |-  ( f = F -> ( f ` ( x .+ y ) ) = ( F ` ( x .+ y ) ) )
29 fveq1 
 |-  ( f = F -> ( f ` x ) = ( F ` x ) )
30 fveq1 
 |-  ( f = F -> ( f ` y ) = ( F ` y ) )
31 29 30 oveq12d 
 |-  ( f = F -> ( ( f ` x ) .+^ ( f ` y ) ) = ( ( F ` x ) .+^ ( F ` y ) ) )
32 28 31 eqeq12d 
 |-  ( f = F -> ( ( f ` ( x .+ y ) ) = ( ( f ` x ) .+^ ( f ` y ) ) <-> ( F ` ( x .+ y ) ) = ( ( F ` x ) .+^ ( F ` y ) ) ) )
33 32 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 ) ) ) )
34 33 elrab 
 |-  ( F e. { f e. ( C ^m B ) | A. x e. B A. y e. B ( f ` ( x .+ y ) ) = ( ( f ` x ) .+^ ( f ` y ) ) } <-> ( F e. ( C ^m B ) /\ A. x e. B A. y e. B ( F ` ( x .+ y ) ) = ( ( F ` x ) .+^ ( F ` y ) ) ) )
35 2 fvexi 
 |-  C e. _V
36 1 fvexi 
 |-  B e. _V
37 35 36 elmap 
 |-  ( F e. ( C ^m B ) <-> F : B --> C )
38 37 anbi1i 
 |-  ( ( F e. ( C ^m B ) /\ A. x e. B A. y e. B ( F ` ( x .+ y ) ) = ( ( F ` x ) .+^ ( F ` y ) ) ) <-> ( F : B --> C /\ A. x e. B A. y e. B ( F ` ( x .+ y ) ) = ( ( F ` x ) .+^ ( F ` y ) ) ) )
39 34 38 bitri 
 |-  ( F e. { f e. ( C ^m B ) | A. x e. B A. y e. B ( f ` ( x .+ y ) ) = ( ( f ` x ) .+^ ( f ` y ) ) } <-> ( F : B --> C /\ A. x e. B A. y e. B ( F ` ( x .+ y ) ) = ( ( F ` x ) .+^ ( F ` y ) ) ) )
40 27 39 bitrdi 
 |-  ( ( S e. Mgm /\ T e. Mgm ) -> ( F e. ( S MgmHom T ) <-> ( F : B --> C /\ A. x e. B A. y e. B ( F ` ( x .+ y ) ) = ( ( F ` x ) .+^ ( F ` y ) ) ) ) )
41 5 40 biadanii 
 |-  ( F e. ( S MgmHom T ) <-> ( ( S e. Mgm /\ T e. Mgm ) /\ ( F : B --> C /\ A. x e. B A. y e. B ( F ` ( x .+ y ) ) = ( ( F ` x ) .+^ ( F ` y ) ) ) ) )