Description: Restriction of a magma homomorphism to a submagma is a homomorphism. (Contributed by AV, 26-Feb-2020)
Ref | Expression | ||
---|---|---|---|
Hypothesis | resmgmhm.u | |
|
Assertion | resmgmhm | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | resmgmhm.u | |
|
2 | mgmhmrcl | |
|
3 | 2 | simprd | |
4 | 1 | submgmmgm | |
5 | 3 4 | anim12ci | |
6 | eqid | |
|
7 | eqid | |
|
8 | 6 7 | mgmhmf | |
9 | 6 | submgmss | |
10 | fssres | |
|
11 | 8 9 10 | syl2an | |
12 | 9 | adantl | |
13 | 1 6 | ressbas2 | |
14 | 12 13 | syl | |
15 | 14 | feq2d | |
16 | 11 15 | mpbid | |
17 | simpll | |
|
18 | 9 | ad2antlr | |
19 | simprl | |
|
20 | 18 19 | sseldd | |
21 | simprr | |
|
22 | 18 21 | sseldd | |
23 | eqid | |
|
24 | eqid | |
|
25 | 6 23 24 | mgmhmlin | |
26 | 17 20 22 25 | syl3anc | |
27 | 23 | submgmcl | |
28 | 27 | 3expb | |
29 | 28 | adantll | |
30 | fvres | |
|
31 | 29 30 | syl | |
32 | fvres | |
|
33 | fvres | |
|
34 | 32 33 | oveqan12d | |
35 | 34 | adantl | |
36 | 26 31 35 | 3eqtr4d | |
37 | 36 | ralrimivva | |
38 | 1 23 | ressplusg | |
39 | 38 | adantl | |
40 | 39 | oveqd | |
41 | 40 | fveqeq2d | |
42 | 14 41 | raleqbidv | |
43 | 14 42 | raleqbidv | |
44 | 37 43 | mpbid | |
45 | 16 44 | jca | |
46 | eqid | |
|
47 | eqid | |
|
48 | 46 7 47 24 | ismgmhm | |
49 | 5 45 48 | sylanbrc | |