Metamath Proof Explorer


Theorem mgmhmeql

Description: The equalizer of two magma homomorphisms is a submagma. (Contributed by AV, 27-Feb-2020)

Ref Expression
Assertion mgmhmeql F S MgmHom T G S MgmHom T dom F G SubMgm S

Proof

Step Hyp Ref Expression
1 eqid Base S = Base S
2 eqid Base T = Base T
3 1 2 mgmhmf F S MgmHom T F : Base S Base T
4 3 adantr F S MgmHom T G S MgmHom T F : Base S Base T
5 4 ffnd F S MgmHom T G S MgmHom T F Fn Base S
6 1 2 mgmhmf G S MgmHom T G : Base S Base T
7 6 adantl F S MgmHom T G S MgmHom T G : Base S Base T
8 7 ffnd F S MgmHom T G S MgmHom T G Fn Base S
9 fndmin F Fn Base S G Fn Base S dom F G = z Base S | F z = G z
10 5 8 9 syl2anc F S MgmHom T G S MgmHom T dom F G = z Base S | F z = G z
11 ssrab2 z Base S | F z = G z Base S
12 11 a1i F S MgmHom T G S MgmHom T z Base S | F z = G z Base S
13 mgmhmrcl F S MgmHom T S Mgm T Mgm
14 13 simpld F S MgmHom T S Mgm
15 14 adantr F S MgmHom T G S MgmHom T S Mgm
16 15 ad2antrr F S MgmHom T G S MgmHom T x Base S F x = G x y Base S F y = G y S Mgm
17 simplrl F S MgmHom T G S MgmHom T x Base S F x = G x y Base S F y = G y x Base S
18 simprl F S MgmHom T G S MgmHom T x Base S F x = G x y Base S F y = G y y Base S
19 eqid + S = + S
20 1 19 mgmcl S Mgm x Base S y Base S x + S y Base S
21 16 17 18 20 syl3anc F S MgmHom T G S MgmHom T x Base S F x = G x y Base S F y = G y x + S y Base S
22 simplrr F S MgmHom T G S MgmHom T x Base S F x = G x y Base S F y = G y F x = G x
23 simprr F S MgmHom T G S MgmHom T x Base S F x = G x y Base S F y = G y F y = G y
24 22 23 oveq12d F S MgmHom T G S MgmHom T x Base S F x = G x y Base S F y = G y F x + T F y = G x + T G y
25 simplll F S MgmHom T G S MgmHom T x Base S F x = G x y Base S F y = G y F S MgmHom T
26 eqid + T = + T
27 1 19 26 mgmhmlin F S MgmHom T x Base S y Base S F x + S y = F x + T F y
28 25 17 18 27 syl3anc F S MgmHom T G S MgmHom T x Base S F x = G x y Base S F y = G y F x + S y = F x + T F y
29 simpllr F S MgmHom T G S MgmHom T x Base S F x = G x y Base S F y = G y G S MgmHom T
30 1 19 26 mgmhmlin G S MgmHom T x Base S y Base S G x + S y = G x + T G y
31 29 17 18 30 syl3anc F S MgmHom T G S MgmHom T x Base S F x = G x y Base S F y = G y G x + S y = G x + T G y
32 24 28 31 3eqtr4d F S MgmHom T G S MgmHom T x Base S F x = G x y Base S F y = G y F x + S y = G x + S y
33 fveq2 z = x + S y F z = F x + S y
34 fveq2 z = x + S y G z = G x + S y
35 33 34 eqeq12d z = x + S y F z = G z F x + S y = G x + S y
36 35 elrab x + S y z Base S | F z = G z x + S y Base S F x + S y = G x + S y
37 21 32 36 sylanbrc F S MgmHom T G S MgmHom T x Base S F x = G x y Base S F y = G y x + S y z Base S | F z = G z
38 37 expr F S MgmHom T G S MgmHom T x Base S F x = G x y Base S F y = G y x + S y z Base S | F z = G z
39 38 ralrimiva F S MgmHom T G S MgmHom T x Base S F x = G x y Base S F y = G y x + S y z Base S | F z = G z
40 fveq2 z = y F z = F y
41 fveq2 z = y G z = G y
42 40 41 eqeq12d z = y F z = G z F y = G y
43 42 ralrab y z Base S | F z = G z x + S y z Base S | F z = G z y Base S F y = G y x + S y z Base S | F z = G z
44 39 43 sylibr F S MgmHom T G S MgmHom T x Base S F x = G x y z Base S | F z = G z x + S y z Base S | F z = G z
45 44 expr F S MgmHom T G S MgmHom T x Base S F x = G x y z Base S | F z = G z x + S y z Base S | F z = G z
46 45 ralrimiva F S MgmHom T G S MgmHom T x Base S F x = G x y z Base S | F z = G z x + S y z Base S | F z = G z
47 fveq2 z = x F z = F x
48 fveq2 z = x G z = G x
49 47 48 eqeq12d z = x F z = G z F x = G x
50 49 ralrab x z Base S | F z = G z y z Base S | F z = G z x + S y z Base S | F z = G z x Base S F x = G x y z Base S | F z = G z x + S y z Base S | F z = G z
51 46 50 sylibr F S MgmHom T G S MgmHom T x z Base S | F z = G z y z Base S | F z = G z x + S y z Base S | F z = G z
52 1 19 issubmgm S Mgm z Base S | F z = G z SubMgm S z Base S | F z = G z Base S x z Base S | F z = G z y z Base S | F z = G z x + S y z Base S | F z = G z
53 15 52 syl F S MgmHom T G S MgmHom T z Base S | F z = G z SubMgm S z Base S | F z = G z Base S x z Base S | F z = G z y z Base S | F z = G z x + S y z Base S | F z = G z
54 12 51 53 mpbir2and F S MgmHom T G S MgmHom T z Base S | F z = G z SubMgm S
55 10 54 eqeltrd F S MgmHom T G S MgmHom T dom F G SubMgm S