Metamath Proof Explorer

Theorem mhmpropd

Description: Monoid homomorphism depends only on the monoidal attributes of structures. (Contributed by Mario Carneiro, 12-Mar-2015) (Revised by Mario Carneiro, 7-Nov-2015)

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

Proof

Step Hyp Ref Expression
1 mhmpropd.a 
 |-  ( ph -> B = ( Base ` J ) )
2 mhmpropd.b 
 |-  ( ph -> C = ( Base ` K ) )
3 mhmpropd.c 
 |-  ( ph -> B = ( Base ` L ) )
4 mhmpropd.d 
 |-  ( ph -> C = ( Base ` M ) )
5 mhmpropd.e 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` J ) y ) = ( x ( +g ` L ) y ) )
6 mhmpropd.f 
 |-  ( ( ph /\ ( x e. C /\ y e. C ) ) -> ( x ( +g ` K ) y ) = ( x ( +g ` M ) y ) )
7 5 fveq2d 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( f ` ( x ( +g ` J ) y ) ) = ( f ` ( x ( +g ` L ) y ) ) )
8 7 adantlr 
 |-  ( ( ( ph /\ f : B --> C ) /\ ( x e. B /\ y e. B ) ) -> ( f ` ( x ( +g ` J ) y ) ) = ( f ` ( x ( +g ` L ) y ) ) )
9 ffvelrn 
 |-  ( ( f : B --> C /\ x e. B ) -> ( f ` x ) e. C )
10 ffvelrn 
 |-  ( ( f : B --> C /\ y e. B ) -> ( f ` y ) e. C )
11 9 10 anim12dan 
 |-  ( ( f : B --> C /\ ( x e. B /\ y e. B ) ) -> ( ( f ` x ) e. C /\ ( f ` y ) e. C ) )
12 6 ralrimivva 
 |-  ( ph -> A. x e. C A. y e. C ( x ( +g ` K ) y ) = ( x ( +g ` M ) y ) )
13 oveq1 
 |-  ( x = w -> ( x ( +g ` K ) y ) = ( w ( +g ` K ) y ) )
14 oveq1 
 |-  ( x = w -> ( x ( +g ` M ) y ) = ( w ( +g ` M ) y ) )
15 13 14 eqeq12d 
 |-  ( x = w -> ( ( x ( +g ` K ) y ) = ( x ( +g ` M ) y ) <-> ( w ( +g ` K ) y ) = ( w ( +g ` M ) y ) ) )
16 oveq2 
 |-  ( y = z -> ( w ( +g ` K ) y ) = ( w ( +g ` K ) z ) )
17 oveq2 
 |-  ( y = z -> ( w ( +g ` M ) y ) = ( w ( +g ` M ) z ) )
18 16 17 eqeq12d 
 |-  ( y = z -> ( ( w ( +g ` K ) y ) = ( w ( +g ` M ) y ) <-> ( w ( +g ` K ) z ) = ( w ( +g ` M ) z ) ) )
19 15 18 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 ) )
20 12 19 sylib 
 |-  ( ph -> A. w e. C A. z e. C ( w ( +g ` K ) z ) = ( w ( +g ` M ) z ) )
21 oveq1 
 |-  ( w = ( f ` x ) -> ( w ( +g ` K ) z ) = ( ( f ` x ) ( +g ` K ) z ) )
22 oveq1 
 |-  ( w = ( f ` x ) -> ( w ( +g ` M ) z ) = ( ( f ` x ) ( +g ` M ) z ) )
23 21 22 eqeq12d 
 |-  ( w = ( f ` x ) -> ( ( w ( +g ` K ) z ) = ( w ( +g ` M ) z ) <-> ( ( f ` x ) ( +g ` K ) z ) = ( ( f ` x ) ( +g ` M ) z ) ) )
24 oveq2 
 |-  ( z = ( f ` y ) -> ( ( f ` x ) ( +g ` K ) z ) = ( ( f ` x ) ( +g ` K ) ( f ` y ) ) )
25 oveq2 
 |-  ( z = ( f ` y ) -> ( ( f ` x ) ( +g ` M ) z ) = ( ( f ` x ) ( +g ` M ) ( f ` y ) ) )
26 24 25 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 ) ) ) )
27 23 26 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 ) ) )
28 11 20 27 syl2anr 
 |-  ( ( ph /\ ( f : B --> C /\ ( x e. B /\ y e. B ) ) ) -> ( ( f ` x ) ( +g ` K ) ( f ` y ) ) = ( ( f ` x ) ( +g ` M ) ( f ` y ) ) )
29 28 anassrs 
 |-  ( ( ( ph /\ f : B --> C ) /\ ( x e. B /\ y e. B ) ) -> ( ( f ` x ) ( +g ` K ) ( f ` y ) ) = ( ( f ` x ) ( +g ` M ) ( f ` y ) ) )
30 8 29 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 ) ) ) )
31 30 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 ) ) ) )
32 31 adantrl 
 |-  ( ( ph /\ ( ( J e. Mnd /\ K e. Mnd ) /\ 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 ) ) ) )
33 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 ) ) ) )
34 33 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 ) ) ) )
35 1 34 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 ) ) ) )
36 35 adantr 
 |-  ( ( ph /\ ( ( J e. Mnd /\ K e. Mnd ) /\ 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 ) ) ) )
37 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 ) ) ) )
38 37 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 ) ) ) )
39 3 38 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 ) ) ) )
40 39 adantr 
 |-  ( ( ph /\ ( ( J e. Mnd /\ K e. Mnd ) /\ 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 ) ) ) )
41 32 36 40 3bitr3d 
 |-  ( ( ph /\ ( ( J e. Mnd /\ K e. Mnd ) /\ 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 ) ) ) )
42 1 adantr 
 |-  ( ( ph /\ ( ( J e. Mnd /\ K e. Mnd ) /\ f : B --> C ) ) -> B = ( Base ` J ) )
43 3 adantr 
 |-  ( ( ph /\ ( ( J e. Mnd /\ K e. Mnd ) /\ f : B --> C ) ) -> B = ( Base ` L ) )
44 5 adantlr 
 |-  ( ( ( ph /\ ( ( J e. Mnd /\ K e. Mnd ) /\ f : B --> C ) ) /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` J ) y ) = ( x ( +g ` L ) y ) )
45 42 43 44 grpidpropd 
 |-  ( ( ph /\ ( ( J e. Mnd /\ K e. Mnd ) /\ f : B --> C ) ) -> ( 0g ` J ) = ( 0g ` L ) )
46 45 fveq2d 
 |-  ( ( ph /\ ( ( J e. Mnd /\ K e. Mnd ) /\ f : B --> C ) ) -> ( f ` ( 0g ` J ) ) = ( f ` ( 0g ` L ) ) )
47 2 adantr 
 |-  ( ( ph /\ ( ( J e. Mnd /\ K e. Mnd ) /\ f : B --> C ) ) -> C = ( Base ` K ) )
48 4 adantr 
 |-  ( ( ph /\ ( ( J e. Mnd /\ K e. Mnd ) /\ f : B --> C ) ) -> C = ( Base ` M ) )
49 6 adantlr 
 |-  ( ( ( ph /\ ( ( J e. Mnd /\ K e. Mnd ) /\ f : B --> C ) ) /\ ( x e. C /\ y e. C ) ) -> ( x ( +g ` K ) y ) = ( x ( +g ` M ) y ) )
50 47 48 49 grpidpropd 
 |-  ( ( ph /\ ( ( J e. Mnd /\ K e. Mnd ) /\ f : B --> C ) ) -> ( 0g ` K ) = ( 0g ` M ) )
51 46 50 eqeq12d 
 |-  ( ( ph /\ ( ( J e. Mnd /\ K e. Mnd ) /\ f : B --> C ) ) -> ( ( f ` ( 0g ` J ) ) = ( 0g ` K ) <-> ( f ` ( 0g ` L ) ) = ( 0g ` M ) ) )
52 41 51 anbi12d 
 |-  ( ( ph /\ ( ( J e. Mnd /\ K e. Mnd ) /\ 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 ` ( 0g ` J ) ) = ( 0g ` K ) ) <-> ( A. x e. ( Base ` L ) A. y e. ( Base ` L ) ( f ` ( x ( +g ` L ) y ) ) = ( ( f ` x ) ( +g ` M ) ( f ` y ) ) /\ ( f ` ( 0g ` L ) ) = ( 0g ` M ) ) ) )
53 52 anassrs 
 |-  ( ( ( ph /\ ( J e. Mnd /\ K e. Mnd ) ) /\ 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 ` ( 0g ` J ) ) = ( 0g ` K ) ) <-> ( A. x e. ( Base ` L ) A. y e. ( Base ` L ) ( f ` ( x ( +g ` L ) y ) ) = ( ( f ` x ) ( +g ` M ) ( f ` y ) ) /\ ( f ` ( 0g ` L ) ) = ( 0g ` M ) ) ) )
54 53 pm5.32da 
 |-  ( ( ph /\ ( J e. Mnd /\ K e. Mnd ) ) -> ( ( 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 ` ( 0g ` J ) ) = ( 0g ` K ) ) ) <-> ( 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 ` ( 0g ` L ) ) = ( 0g ` M ) ) ) ) )
55 1 2 feq23d 
 |-  ( ph -> ( f : B --> C <-> f : ( Base ` J ) --> ( Base ` K ) ) )
56 55 adantr 
 |-  ( ( ph /\ ( J e. Mnd /\ K e. Mnd ) ) -> ( f : B --> C <-> f : ( Base ` J ) --> ( Base ` K ) ) )
57 56 anbi1d 
 |-  ( ( ph /\ ( J e. Mnd /\ K e. Mnd ) ) -> ( ( 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 ` ( 0g ` J ) ) = ( 0g ` K ) ) ) <-> ( 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 ` ( 0g ` J ) ) = ( 0g ` K ) ) ) ) )
58 3 4 feq23d 
 |-  ( ph -> ( f : B --> C <-> f : ( Base ` L ) --> ( Base ` M ) ) )
59 58 adantr 
 |-  ( ( ph /\ ( J e. Mnd /\ K e. Mnd ) ) -> ( f : B --> C <-> f : ( Base ` L ) --> ( Base ` M ) ) )
60 59 anbi1d 
 |-  ( ( ph /\ ( J e. Mnd /\ K e. Mnd ) ) -> ( ( 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 ` ( 0g ` L ) ) = ( 0g ` M ) ) ) <-> ( 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 ) ) /\ ( f ` ( 0g ` L ) ) = ( 0g ` M ) ) ) ) )
61 54 57 60 3bitr3d 
 |-  ( ( ph /\ ( J e. Mnd /\ K e. Mnd ) ) -> ( ( 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 ` ( 0g ` J ) ) = ( 0g ` K ) ) ) <-> ( 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 ) ) /\ ( f ` ( 0g ` L ) ) = ( 0g ` M ) ) ) ) )
62 3anass 
 |-  ( ( 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 ` ( 0g ` J ) ) = ( 0g ` K ) ) <-> ( 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 ` ( 0g ` J ) ) = ( 0g ` K ) ) ) )
63 3anass 
 |-  ( ( 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 ) ) /\ ( f ` ( 0g ` L ) ) = ( 0g ` M ) ) <-> ( 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 ) ) /\ ( f ` ( 0g ` L ) ) = ( 0g ` M ) ) ) )
64 61 62 63 3bitr4g 
 |-  ( ( ph /\ ( J e. Mnd /\ K e. Mnd ) ) -> ( ( 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 ` ( 0g ` J ) ) = ( 0g ` K ) ) <-> ( 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 ) ) /\ ( f ` ( 0g ` L ) ) = ( 0g ` M ) ) ) )
65 64 pm5.32da 
 |-  ( ph -> ( ( ( J e. Mnd /\ K e. Mnd ) /\ ( 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 ` ( 0g ` J ) ) = ( 0g ` K ) ) ) <-> ( ( J e. Mnd /\ K e. Mnd ) /\ ( 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 ) ) /\ ( f ` ( 0g ` L ) ) = ( 0g ` M ) ) ) ) )
66 1 3 5 mndpropd 
 |-  ( ph -> ( J e. Mnd <-> L e. Mnd ) )
67 2 4 6 mndpropd 
 |-  ( ph -> ( K e. Mnd <-> M e. Mnd ) )
68 66 67 anbi12d 
 |-  ( ph -> ( ( J e. Mnd /\ K e. Mnd ) <-> ( L e. Mnd /\ M e. Mnd ) ) )
69 68 anbi1d 
 |-  ( ph -> ( ( ( J e. Mnd /\ K e. Mnd ) /\ ( 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 ) ) /\ ( f ` ( 0g ` L ) ) = ( 0g ` M ) ) ) <-> ( ( L e. Mnd /\ M e. Mnd ) /\ ( 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 ) ) /\ ( f ` ( 0g ` L ) ) = ( 0g ` M ) ) ) ) )
70 65 69 bitrd 
 |-  ( ph -> ( ( ( J e. Mnd /\ K e. Mnd ) /\ ( 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 ` ( 0g ` J ) ) = ( 0g ` K ) ) ) <-> ( ( L e. Mnd /\ M e. Mnd ) /\ ( 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 ) ) /\ ( f ` ( 0g ` L ) ) = ( 0g ` M ) ) ) ) )
71 eqid 
 |-  ( Base ` J ) = ( Base ` J )
72 eqid 
 |-  ( Base ` K ) = ( Base ` K )
73 eqid 
 |-  ( +g ` J ) = ( +g ` J )
74 eqid 
 |-  ( +g ` K ) = ( +g ` K )
75 eqid 
 |-  ( 0g ` J ) = ( 0g ` J )
76 eqid 
 |-  ( 0g ` K ) = ( 0g ` K )
77 71 72 73 74 75 76 ismhm 
 |-  ( f e. ( J MndHom K ) <-> ( ( J e. Mnd /\ K e. Mnd ) /\ ( 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 ` ( 0g ` J ) ) = ( 0g ` K ) ) ) )
78 eqid 
 |-  ( Base ` L ) = ( Base ` L )
79 eqid 
 |-  ( Base ` M ) = ( Base ` M )
80 eqid 
 |-  ( +g ` L ) = ( +g ` L )
81 eqid 
 |-  ( +g ` M ) = ( +g ` M )
82 eqid 
 |-  ( 0g ` L ) = ( 0g ` L )
83 eqid 
 |-  ( 0g ` M ) = ( 0g ` M )
84 78 79 80 81 82 83 ismhm 
 |-  ( f e. ( L MndHom M ) <-> ( ( L e. Mnd /\ M e. Mnd ) /\ ( 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 ) ) /\ ( f ` ( 0g ` L ) ) = ( 0g ` M ) ) ) )
85 70 77 84 3bitr4g 
 |-  ( ph -> ( f e. ( J MndHom K ) <-> f e. ( L MndHom M ) ) )
86 85 eqrdv 
 |-  ( ph -> ( J MndHom K ) = ( L MndHom M ) )