Metamath Proof Explorer

Theorem mgmhmpropd

Description: Magma homomorphism depends only on the operation of structures. (Contributed by AV, 25-Feb-2020)

Ref Expression
Hypotheses mgmhmpropd.a 
|- ( ph -> B = ( Base ` J ) )
mgmhmpropd.b 
|- ( ph -> C = ( Base ` K ) )
mgmhmpropd.c 
|- ( ph -> B = ( Base ` L ) )
mgmhmpropd.d 
|- ( ph -> C = ( Base ` M ) )
mgmhmpropd.0 
|- ( ph -> B =/= (/) )
mgmhmpropd.C 
|- ( ph -> C =/= (/) )
mgmhmpropd.e 
|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` J ) y ) = ( x ( +g ` L ) y ) )
mgmhmpropd.f 
|- ( ( ph /\ ( x e. C /\ y e. C ) ) -> ( x ( +g ` K ) y ) = ( x ( +g ` M ) y ) )
Assertion mgmhmpropd 
|- ( ph -> ( J MgmHom K ) = ( L MgmHom M ) )

Proof

Step Hyp Ref Expression
1 mgmhmpropd.a 
 |-  ( ph -> B = ( Base ` J ) )
2 mgmhmpropd.b 
 |-  ( ph -> C = ( Base ` K ) )
3 mgmhmpropd.c 
 |-  ( ph -> B = ( Base ` L ) )
4 mgmhmpropd.d 
 |-  ( ph -> C = ( Base ` M ) )
5 mgmhmpropd.0 
 |-  ( ph -> B =/= (/) )
6 mgmhmpropd.C 
 |-  ( ph -> C =/= (/) )
7 mgmhmpropd.e 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` J ) y ) = ( x ( +g ` L ) y ) )
8 mgmhmpropd.f 
 |-  ( ( ph /\ ( x e. C /\ y e. C ) ) -> ( x ( +g ` K ) y ) = ( x ( +g ` M ) y ) )
9 7 fveq2d 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( f ` ( x ( +g ` J ) y ) ) = ( f ` ( x ( +g ` L ) y ) ) )
10 9 adantlr 
 |-  ( ( ( ph /\ f : B --> C ) /\ ( x e. B /\ y e. B ) ) -> ( f ` ( x ( +g ` J ) y ) ) = ( f ` ( x ( +g ` L ) y ) ) )
11 ffvelrn 
 |-  ( ( f : B --> C /\ x e. B ) -> ( f ` x ) e. C )
12 ffvelrn 
 |-  ( ( f : B --> C /\ y e. B ) -> ( f ` y ) e. C )
13 11 12 anim12dan 
 |-  ( ( f : B --> C /\ ( x e. B /\ y e. B ) ) -> ( ( f ` x ) e. C /\ ( f ` y ) e. C ) )
14 8 ralrimivva 
 |-  ( ph -> A. x e. C A. y e. C ( x ( +g ` K ) y ) = ( x ( +g ` M ) y ) )
15 oveq1 
 |-  ( x = w -> ( x ( +g ` K ) y ) = ( w ( +g ` K ) y ) )
16 oveq1 
 |-  ( x = w -> ( x ( +g ` M ) y ) = ( w ( +g ` M ) y ) )
17 15 16 eqeq12d 
 |-  ( x = w -> ( ( x ( +g ` K ) y ) = ( x ( +g ` M ) y ) <-> ( w ( +g ` K ) y ) = ( w ( +g ` M ) y ) ) )
18 oveq2 
 |-  ( y = z -> ( w ( +g ` K ) y ) = ( w ( +g ` K ) z ) )
19 oveq2 
 |-  ( y = z -> ( w ( +g ` M ) y ) = ( w ( +g ` M ) z ) )
20 18 19 eqeq12d 
 |-  ( y = z -> ( ( w ( +g ` K ) y ) = ( w ( +g ` M ) y ) <-> ( w ( +g ` K ) z ) = ( w ( +g ` M ) z ) ) )
21 17 20 cbvral2vw 
 |-  ( A. x e. C A. y e. C ( x ( +g ` K ) y ) = ( x ( +g ` M ) y ) <-> A. w e. C A. z e. C ( w ( +g ` K ) z ) = ( w ( +g ` M ) z ) )
22 14 21 sylib 
 |-  ( ph -> A. w e. C A. z e. C ( w ( +g ` K ) z ) = ( w ( +g ` M ) z ) )
23 oveq1 
 |-  ( w = ( f ` x ) -> ( w ( +g ` K ) z ) = ( ( f ` x ) ( +g ` K ) z ) )
24 oveq1 
 |-  ( w = ( f ` x ) -> ( w ( +g ` M ) z ) = ( ( f ` x ) ( +g ` M ) z ) )
25 23 24 eqeq12d 
 |-  ( w = ( f ` x ) -> ( ( w ( +g ` K ) z ) = ( w ( +g ` M ) z ) <-> ( ( f ` x ) ( +g ` K ) z ) = ( ( f ` x ) ( +g ` M ) z ) ) )
26 oveq2 
 |-  ( z = ( f ` y ) -> ( ( f ` x ) ( +g ` K ) z ) = ( ( f ` x ) ( +g ` K ) ( f ` y ) ) )
27 oveq2 
 |-  ( z = ( f ` y ) -> ( ( f ` x ) ( +g ` M ) z ) = ( ( f ` x ) ( +g ` M ) ( f ` y ) ) )
28 26 27 eqeq12d 
 |-  ( z = ( f ` y ) -> ( ( ( f ` x ) ( +g ` K ) z ) = ( ( f ` x ) ( +g ` M ) z ) <-> ( ( f ` x ) ( +g ` K ) ( f ` y ) ) = ( ( f ` x ) ( +g ` M ) ( f ` y ) ) ) )
29 25 28 rspc2va 
 |-  ( ( ( ( f ` x ) e. C /\ ( f ` y ) e. C ) /\ A. w e. C A. z e. C ( w ( +g ` K ) z ) = ( w ( +g ` M ) z ) ) -> ( ( f ` x ) ( +g ` K ) ( f ` y ) ) = ( ( f ` x ) ( +g ` M ) ( f ` y ) ) )
30 13 22 29 syl2anr 
 |-  ( ( ph /\ ( f : B --> C /\ ( x e. B /\ y e. B ) ) ) -> ( ( f ` x ) ( +g ` K ) ( f ` y ) ) = ( ( f ` x ) ( +g ` M ) ( f ` y ) ) )
31 30 anassrs 
 |-  ( ( ( ph /\ f : B --> C ) /\ ( x e. B /\ y e. B ) ) -> ( ( f ` x ) ( +g ` K ) ( f ` y ) ) = ( ( f ` x ) ( +g ` M ) ( f ` y ) ) )
32 10 31 eqeq12d 
 |-  ( ( ( ph /\ f : B --> C ) /\ ( x e. B /\ y e. B ) ) -> ( ( f ` ( x ( +g ` J ) y ) ) = ( ( f ` x ) ( +g ` K ) ( f ` y ) ) <-> ( f ` ( x ( +g ` L ) y ) ) = ( ( f ` x ) ( +g ` M ) ( f ` y ) ) ) )
33 32 2ralbidva 
 |-  ( ( ph /\ f : B --> C ) -> ( A. x e. B A. y e. B ( f ` ( x ( +g ` J ) y ) ) = ( ( f ` x ) ( +g ` K ) ( f ` y ) ) <-> A. x e. B A. y e. B ( f ` ( x ( +g ` L ) y ) ) = ( ( f ` x ) ( +g ` M ) ( f ` y ) ) ) )
34 33 adantrl 
 |-  ( ( ph /\ ( ( J e. Mgm /\ K e. Mgm ) /\ f : B --> C ) ) -> ( A. x e. B A. y e. B ( f ` ( x ( +g ` J ) y ) ) = ( ( f ` x ) ( +g ` K ) ( f ` y ) ) <-> A. x e. B A. y e. B ( f ` ( x ( +g ` L ) y ) ) = ( ( f ` x ) ( +g ` M ) ( f ` y ) ) ) )
35 raleq 
 |-  ( B = ( Base ` J ) -> ( A. y e. B ( f ` ( x ( +g ` J ) y ) ) = ( ( f ` x ) ( +g ` K ) ( f ` y ) ) <-> A. y e. ( Base ` J ) ( f ` ( x ( +g ` J ) y ) ) = ( ( f ` x ) ( +g ` K ) ( f ` y ) ) ) )
36 35 raleqbi1dv 
 |-  ( B = ( Base ` J ) -> ( A. x e. B A. y e. B ( f ` ( x ( +g ` J ) y ) ) = ( ( f ` x ) ( +g ` K ) ( f ` y ) ) <-> A. x e. ( Base ` J ) A. y e. ( Base ` J ) ( f ` ( x ( +g ` J ) y ) ) = ( ( f ` x ) ( +g ` K ) ( f ` y ) ) ) )
37 1 36 syl 
 |-  ( ph -> ( A. x e. B A. y e. B ( f ` ( x ( +g ` J ) y ) ) = ( ( f ` x ) ( +g ` K ) ( f ` y ) ) <-> A. x e. ( Base ` J ) A. y e. ( Base ` J ) ( f ` ( x ( +g ` J ) y ) ) = ( ( f ` x ) ( +g ` K ) ( f ` y ) ) ) )
38 37 adantr 
 |-  ( ( ph /\ ( ( J e. Mgm /\ K e. Mgm ) /\ f : B --> C ) ) -> ( A. x e. B A. y e. B ( f ` ( x ( +g ` J ) y ) ) = ( ( f ` x ) ( +g ` K ) ( f ` y ) ) <-> A. x e. ( Base ` J ) A. y e. ( Base ` J ) ( f ` ( x ( +g ` J ) y ) ) = ( ( f ` x ) ( +g ` K ) ( f ` y ) ) ) )
39 raleq 
 |-  ( B = ( Base ` L ) -> ( A. y e. B ( f ` ( x ( +g ` L ) y ) ) = ( ( f ` x ) ( +g ` M ) ( f ` y ) ) <-> A. y e. ( Base ` L ) ( f ` ( x ( +g ` L ) y ) ) = ( ( f ` x ) ( +g ` M ) ( f ` y ) ) ) )
40 39 raleqbi1dv 
 |-  ( B = ( Base ` L ) -> ( A. x e. B A. y e. B ( f ` ( x ( +g ` L ) y ) ) = ( ( f ` x ) ( +g ` M ) ( f ` y ) ) <-> A. x e. ( Base ` L ) A. y e. ( Base ` L ) ( f ` ( x ( +g ` L ) y ) ) = ( ( f ` x ) ( +g ` M ) ( f ` y ) ) ) )
41 3 40 syl 
 |-  ( ph -> ( A. x e. B A. y e. B ( f ` ( x ( +g ` L ) y ) ) = ( ( f ` x ) ( +g ` M ) ( f ` y ) ) <-> A. x e. ( Base ` L ) A. y e. ( Base ` L ) ( f ` ( x ( +g ` L ) y ) ) = ( ( f ` x ) ( +g ` M ) ( f ` y ) ) ) )
42 41 adantr 
 |-  ( ( ph /\ ( ( J e. Mgm /\ K e. Mgm ) /\ f : B --> C ) ) -> ( A. x e. B A. y e. B ( f ` ( x ( +g ` L ) y ) ) = ( ( f ` x ) ( +g ` M ) ( f ` y ) ) <-> A. x e. ( Base ` L ) A. y e. ( Base ` L ) ( f ` ( x ( +g ` L ) y ) ) = ( ( f ` x ) ( +g ` M ) ( f ` y ) ) ) )
43 34 38 42 3bitr3d 
 |-  ( ( ph /\ ( ( J e. Mgm /\ K e. Mgm ) /\ f : B --> C ) ) -> ( A. x e. ( Base ` J ) A. y e. ( Base ` J ) ( f ` ( x ( +g ` J ) y ) ) = ( ( f ` x ) ( +g ` K ) ( f ` y ) ) <-> A. x e. ( Base ` L ) A. y e. ( Base ` L ) ( f ` ( x ( +g ` L ) y ) ) = ( ( f ` x ) ( +g ` M ) ( f ` y ) ) ) )
44 43 anassrs 
 |-  ( ( ( ph /\ ( J e. Mgm /\ K e. Mgm ) ) /\ f : B --> C ) -> ( A. x e. ( Base ` J ) A. y e. ( Base ` J ) ( f ` ( x ( +g ` J ) y ) ) = ( ( f ` x ) ( +g ` K ) ( f ` y ) ) <-> A. x e. ( Base ` L ) A. y e. ( Base ` L ) ( f ` ( x ( +g ` L ) y ) ) = ( ( f ` x ) ( +g ` M ) ( f ` y ) ) ) )
45 44 pm5.32da 
 |-  ( ( ph /\ ( J e. Mgm /\ K e. Mgm ) ) -> ( ( f : B --> C /\ A. x e. ( Base ` J ) A. y e. ( Base ` J ) ( f ` ( x ( +g ` J ) y ) ) = ( ( f ` x ) ( +g ` K ) ( f ` y ) ) ) <-> ( f : B --> C /\ A. x e. ( Base ` L ) A. y e. ( Base ` L ) ( f ` ( x ( +g ` L ) y ) ) = ( ( f ` x ) ( +g ` M ) ( f ` y ) ) ) ) )
46 1 2 feq23d 
 |-  ( ph -> ( f : B --> C <-> f : ( Base ` J ) --> ( Base ` K ) ) )
47 46 adantr 
 |-  ( ( ph /\ ( J e. Mgm /\ K e. Mgm ) ) -> ( f : B --> C <-> f : ( Base ` J ) --> ( Base ` K ) ) )
48 47 anbi1d 
 |-  ( ( ph /\ ( J e. Mgm /\ K e. Mgm ) ) -> ( ( f : B --> C /\ A. x e. ( Base ` J ) A. y e. ( Base ` J ) ( f ` ( x ( +g ` J ) y ) ) = ( ( f ` x ) ( +g ` K ) ( f ` y ) ) ) <-> ( f : ( Base ` J ) --> ( Base ` K ) /\ A. x e. ( Base ` J ) A. y e. ( Base ` J ) ( f ` ( x ( +g ` J ) y ) ) = ( ( f ` x ) ( +g ` K ) ( f ` y ) ) ) ) )
49 3 4 feq23d 
 |-  ( ph -> ( f : B --> C <-> f : ( Base ` L ) --> ( Base ` M ) ) )
50 49 adantr 
 |-  ( ( ph /\ ( J e. Mgm /\ K e. Mgm ) ) -> ( f : B --> C <-> f : ( Base ` L ) --> ( Base ` M ) ) )
51 50 anbi1d 
 |-  ( ( ph /\ ( J e. Mgm /\ K e. Mgm ) ) -> ( ( f : B --> C /\ A. x e. ( Base ` L ) A. y e. ( Base ` L ) ( f ` ( x ( +g ` L ) y ) ) = ( ( f ` x ) ( +g ` M ) ( f ` y ) ) ) <-> ( f : ( Base ` L ) --> ( Base ` M ) /\ A. x e. ( Base ` L ) A. y e. ( Base ` L ) ( f ` ( x ( +g ` L ) y ) ) = ( ( f ` x ) ( +g ` M ) ( f ` y ) ) ) ) )
52 45 48 51 3bitr3d 
 |-  ( ( ph /\ ( J e. Mgm /\ K e. Mgm ) ) -> ( ( f : ( Base ` J ) --> ( Base ` K ) /\ A. x e. ( Base ` J ) A. y e. ( Base ` J ) ( f ` ( x ( +g ` J ) y ) ) = ( ( f ` x ) ( +g ` K ) ( f ` y ) ) ) <-> ( f : ( Base ` L ) --> ( Base ` M ) /\ A. x e. ( Base ` L ) A. y e. ( Base ` L ) ( f ` ( x ( +g ` L ) y ) ) = ( ( f ` x ) ( +g ` M ) ( f ` y ) ) ) ) )
53 52 pm5.32da 
 |-  ( ph -> ( ( ( J e. Mgm /\ K e. Mgm ) /\ ( f : ( Base ` J ) --> ( Base ` K ) /\ A. x e. ( Base ` J ) A. y e. ( Base ` J ) ( f ` ( x ( +g ` J ) y ) ) = ( ( f ` x ) ( +g ` K ) ( f ` y ) ) ) ) <-> ( ( J e. Mgm /\ K e. Mgm ) /\ ( f : ( Base ` L ) --> ( Base ` M ) /\ A. x e. ( Base ` L ) A. y e. ( Base ` L ) ( f ` ( x ( +g ` L ) y ) ) = ( ( f ` x ) ( +g ` M ) ( f ` y ) ) ) ) ) )
54 1 3 5 7 mgmpropd 
 |-  ( ph -> ( J e. Mgm <-> L e. Mgm ) )
55 2 4 6 8 mgmpropd 
 |-  ( ph -> ( K e. Mgm <-> M e. Mgm ) )
56 54 55 anbi12d 
 |-  ( ph -> ( ( J e. Mgm /\ K e. Mgm ) <-> ( L e. Mgm /\ M e. Mgm ) ) )
57 56 anbi1d 
 |-  ( ph -> ( ( ( J e. Mgm /\ K e. Mgm ) /\ ( f : ( Base ` L ) --> ( Base ` M ) /\ A. x e. ( Base ` L ) A. y e. ( Base ` L ) ( f ` ( x ( +g ` L ) y ) ) = ( ( f ` x ) ( +g ` M ) ( f ` y ) ) ) ) <-> ( ( L e. Mgm /\ M e. Mgm ) /\ ( f : ( Base ` L ) --> ( Base ` M ) /\ A. x e. ( Base ` L ) A. y e. ( Base ` L ) ( f ` ( x ( +g ` L ) y ) ) = ( ( f ` x ) ( +g ` M ) ( f ` y ) ) ) ) ) )
58 53 57 bitrd 
 |-  ( ph -> ( ( ( J e. Mgm /\ K e. Mgm ) /\ ( f : ( Base ` J ) --> ( Base ` K ) /\ A. x e. ( Base ` J ) A. y e. ( Base ` J ) ( f ` ( x ( +g ` J ) y ) ) = ( ( f ` x ) ( +g ` K ) ( f ` y ) ) ) ) <-> ( ( L e. Mgm /\ M e. Mgm ) /\ ( f : ( Base ` L ) --> ( Base ` M ) /\ A. x e. ( Base ` L ) A. y e. ( Base ` L ) ( f ` ( x ( +g ` L ) y ) ) = ( ( f ` x ) ( +g ` M ) ( f ` y ) ) ) ) ) )
59 eqid 
 |-  ( Base ` J ) = ( Base ` J )
60 eqid 
 |-  ( Base ` K ) = ( Base ` K )
61 eqid 
 |-  ( +g ` J ) = ( +g ` J )
62 eqid 
 |-  ( +g ` K ) = ( +g ` K )
63 59 60 61 62 ismgmhm 
 |-  ( f e. ( J MgmHom K ) <-> ( ( J e. Mgm /\ K e. Mgm ) /\ ( f : ( Base ` J ) --> ( Base ` K ) /\ A. x e. ( Base ` J ) A. y e. ( Base ` J ) ( f ` ( x ( +g ` J ) y ) ) = ( ( f ` x ) ( +g ` K ) ( f ` y ) ) ) ) )
64 eqid 
 |-  ( Base ` L ) = ( Base ` L )
65 eqid 
 |-  ( Base ` M ) = ( Base ` M )
66 eqid 
 |-  ( +g ` L ) = ( +g ` L )
67 eqid 
 |-  ( +g ` M ) = ( +g ` M )
68 64 65 66 67 ismgmhm 
 |-  ( f e. ( L MgmHom M ) <-> ( ( L e. Mgm /\ M e. Mgm ) /\ ( f : ( Base ` L ) --> ( Base ` M ) /\ A. x e. ( Base ` L ) A. y e. ( Base ` L ) ( f ` ( x ( +g ` L ) y ) ) = ( ( f ` x ) ( +g ` M ) ( f ` y ) ) ) ) )
69 58 63 68 3bitr4g 
 |-  ( ph -> ( f e. ( J MgmHom K ) <-> f e. ( L MgmHom M ) ) )
70 69 eqrdv 
 |-  ( ph -> ( J MgmHom K ) = ( L MgmHom M ) )