Description: Lemma for mulgaddcom . (Contributed by Paul Chapman, 17-Apr-2009) (Revised by AV, 31-Aug-2021)
Ref | Expression | ||
---|---|---|---|
Hypotheses | mulgaddcom.b | |
|
mulgaddcom.t | |
||
mulgaddcom.p | |
||
Assertion | mulgaddcomlem | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mulgaddcom.b | |
|
2 | mulgaddcom.t | |
|
3 | mulgaddcom.p | |
|
4 | simp1 | |
|
5 | 4 | adantr | |
6 | simp3 | |
|
7 | 6 | adantr | |
8 | znegcl | |
|
9 | 1 2 | mulgcl | |
10 | 8 9 | syl3an2 | |
11 | 10 | adantr | |
12 | eqid | |
|
13 | 1 12 | grpinvcl | |
14 | 13 | 3adant2 | |
15 | 14 | adantr | |
16 | 1 3 | grpass | |
17 | 5 7 11 15 16 | syl13anc | |
18 | 1 2 12 | mulgneg | |
19 | 18 | adantr | |
20 | 19 | oveq1d | |
21 | 1 2 | mulgcl | |
22 | 21 | adantr | |
23 | 1 3 12 | grpinvadd | |
24 | 5 7 22 23 | syl3anc | |
25 | 19 | oveq2d | |
26 | 1 3 12 | grpinvadd | |
27 | 5 22 7 26 | syl3anc | |
28 | fveq2 | |
|
29 | 28 | adantl | |
30 | 25 27 29 | 3eqtr2rd | |
31 | 20 24 30 | 3eqtr2d | |
32 | 31 | oveq2d | |
33 | 1 3 12 | grpasscan1 | |
34 | 5 7 11 33 | syl3anc | |
35 | 17 32 34 | 3eqtrd | |
36 | 35 | oveq1d | |
37 | 1 3 | grpcl | |
38 | 4 6 10 37 | syl3anc | |
39 | 38 | adantr | |
40 | 1 3 12 | grpasscan2 | |
41 | 5 39 7 40 | syl3anc | |
42 | 36 41 | eqtr3d | |