Description: Magma homomorphism depends only on the operation of structures. (Contributed by AV, 25-Feb-2020)
Ref | Expression | ||
---|---|---|---|
Hypotheses | mgmhmpropd.a | |
|
mgmhmpropd.b | |
||
mgmhmpropd.c | |
||
mgmhmpropd.d | |
||
mgmhmpropd.0 | |
||
mgmhmpropd.C | |
||
mgmhmpropd.e | |
||
mgmhmpropd.f | |
||
Assertion | mgmhmpropd | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mgmhmpropd.a | |
|
2 | mgmhmpropd.b | |
|
3 | mgmhmpropd.c | |
|
4 | mgmhmpropd.d | |
|
5 | mgmhmpropd.0 | |
|
6 | mgmhmpropd.C | |
|
7 | mgmhmpropd.e | |
|
8 | mgmhmpropd.f | |
|
9 | 7 | fveq2d | |
10 | 9 | adantlr | |
11 | ffvelcdm | |
|
12 | ffvelcdm | |
|
13 | 11 12 | anim12dan | |
14 | 8 | ralrimivva | |
15 | oveq1 | |
|
16 | oveq1 | |
|
17 | 15 16 | eqeq12d | |
18 | oveq2 | |
|
19 | oveq2 | |
|
20 | 18 19 | eqeq12d | |
21 | 17 20 | cbvral2vw | |
22 | 14 21 | sylib | |
23 | oveq1 | |
|
24 | oveq1 | |
|
25 | 23 24 | eqeq12d | |
26 | oveq2 | |
|
27 | oveq2 | |
|
28 | 26 27 | eqeq12d | |
29 | 25 28 | rspc2va | |
30 | 13 22 29 | syl2anr | |
31 | 30 | anassrs | |
32 | 10 31 | eqeq12d | |
33 | 32 | 2ralbidva | |
34 | 33 | adantrl | |
35 | raleq | |
|
36 | 35 | raleqbi1dv | |
37 | 1 36 | syl | |
38 | 37 | adantr | |
39 | raleq | |
|
40 | 39 | raleqbi1dv | |
41 | 3 40 | syl | |
42 | 41 | adantr | |
43 | 34 38 42 | 3bitr3d | |
44 | 43 | anassrs | |
45 | 44 | pm5.32da | |
46 | 1 2 | feq23d | |
47 | 46 | adantr | |
48 | 47 | anbi1d | |
49 | 3 4 | feq23d | |
50 | 49 | adantr | |
51 | 50 | anbi1d | |
52 | 45 48 51 | 3bitr3d | |
53 | 52 | pm5.32da | |
54 | 1 3 5 7 | mgmpropd | |
55 | 2 4 6 8 | mgmpropd | |
56 | 54 55 | anbi12d | |
57 | 56 | anbi1d | |
58 | 53 57 | bitrd | |
59 | eqid | |
|
60 | eqid | |
|
61 | eqid | |
|
62 | eqid | |
|
63 | 59 60 61 62 | ismgmhm | |
64 | eqid | |
|
65 | eqid | |
|
66 | eqid | |
|
67 | eqid | |
|
68 | 64 65 66 67 | ismgmhm | |
69 | 58 63 68 | 3bitr4g | |
70 | 69 | eqrdv | |