Step |
Hyp |
Ref |
Expression |
1 |
|
mulgaddcom.b |
โข ๐ต = ( Base โ ๐บ ) |
2 |
|
mulgaddcom.t |
โข ยท = ( .g โ ๐บ ) |
3 |
|
mulgaddcom.p |
โข + = ( +g โ ๐บ ) |
4 |
|
simp1 |
โข ( ( ๐บ โ Grp โง ๐ฆ โ โค โง ๐ โ ๐ต ) โ ๐บ โ Grp ) |
5 |
4
|
adantr |
โข ( ( ( ๐บ โ Grp โง ๐ฆ โ โค โง ๐ โ ๐ต ) โง ( ( ๐ฆ ยท ๐ ) + ๐ ) = ( ๐ + ( ๐ฆ ยท ๐ ) ) ) โ ๐บ โ Grp ) |
6 |
|
simp3 |
โข ( ( ๐บ โ Grp โง ๐ฆ โ โค โง ๐ โ ๐ต ) โ ๐ โ ๐ต ) |
7 |
6
|
adantr |
โข ( ( ( ๐บ โ Grp โง ๐ฆ โ โค โง ๐ โ ๐ต ) โง ( ( ๐ฆ ยท ๐ ) + ๐ ) = ( ๐ + ( ๐ฆ ยท ๐ ) ) ) โ ๐ โ ๐ต ) |
8 |
|
znegcl |
โข ( ๐ฆ โ โค โ - ๐ฆ โ โค ) |
9 |
1 2
|
mulgcl |
โข ( ( ๐บ โ Grp โง - ๐ฆ โ โค โง ๐ โ ๐ต ) โ ( - ๐ฆ ยท ๐ ) โ ๐ต ) |
10 |
8 9
|
syl3an2 |
โข ( ( ๐บ โ Grp โง ๐ฆ โ โค โง ๐ โ ๐ต ) โ ( - ๐ฆ ยท ๐ ) โ ๐ต ) |
11 |
10
|
adantr |
โข ( ( ( ๐บ โ Grp โง ๐ฆ โ โค โง ๐ โ ๐ต ) โง ( ( ๐ฆ ยท ๐ ) + ๐ ) = ( ๐ + ( ๐ฆ ยท ๐ ) ) ) โ ( - ๐ฆ ยท ๐ ) โ ๐ต ) |
12 |
|
eqid |
โข ( invg โ ๐บ ) = ( invg โ ๐บ ) |
13 |
1 12
|
grpinvcl |
โข ( ( ๐บ โ Grp โง ๐ โ ๐ต ) โ ( ( invg โ ๐บ ) โ ๐ ) โ ๐ต ) |
14 |
13
|
3adant2 |
โข ( ( ๐บ โ Grp โง ๐ฆ โ โค โง ๐ โ ๐ต ) โ ( ( invg โ ๐บ ) โ ๐ ) โ ๐ต ) |
15 |
14
|
adantr |
โข ( ( ( ๐บ โ Grp โง ๐ฆ โ โค โง ๐ โ ๐ต ) โง ( ( ๐ฆ ยท ๐ ) + ๐ ) = ( ๐ + ( ๐ฆ ยท ๐ ) ) ) โ ( ( invg โ ๐บ ) โ ๐ ) โ ๐ต ) |
16 |
1 3
|
grpass |
โข ( ( ๐บ โ Grp โง ( ๐ โ ๐ต โง ( - ๐ฆ ยท ๐ ) โ ๐ต โง ( ( invg โ ๐บ ) โ ๐ ) โ ๐ต ) ) โ ( ( ๐ + ( - ๐ฆ ยท ๐ ) ) + ( ( invg โ ๐บ ) โ ๐ ) ) = ( ๐ + ( ( - ๐ฆ ยท ๐ ) + ( ( invg โ ๐บ ) โ ๐ ) ) ) ) |
17 |
5 7 11 15 16
|
syl13anc |
โข ( ( ( ๐บ โ Grp โง ๐ฆ โ โค โง ๐ โ ๐ต ) โง ( ( ๐ฆ ยท ๐ ) + ๐ ) = ( ๐ + ( ๐ฆ ยท ๐ ) ) ) โ ( ( ๐ + ( - ๐ฆ ยท ๐ ) ) + ( ( invg โ ๐บ ) โ ๐ ) ) = ( ๐ + ( ( - ๐ฆ ยท ๐ ) + ( ( invg โ ๐บ ) โ ๐ ) ) ) ) |
18 |
1 2 12
|
mulgneg |
โข ( ( ๐บ โ Grp โง ๐ฆ โ โค โง ๐ โ ๐ต ) โ ( - ๐ฆ ยท ๐ ) = ( ( invg โ ๐บ ) โ ( ๐ฆ ยท ๐ ) ) ) |
19 |
18
|
adantr |
โข ( ( ( ๐บ โ Grp โง ๐ฆ โ โค โง ๐ โ ๐ต ) โง ( ( ๐ฆ ยท ๐ ) + ๐ ) = ( ๐ + ( ๐ฆ ยท ๐ ) ) ) โ ( - ๐ฆ ยท ๐ ) = ( ( invg โ ๐บ ) โ ( ๐ฆ ยท ๐ ) ) ) |
20 |
19
|
oveq1d |
โข ( ( ( ๐บ โ Grp โง ๐ฆ โ โค โง ๐ โ ๐ต ) โง ( ( ๐ฆ ยท ๐ ) + ๐ ) = ( ๐ + ( ๐ฆ ยท ๐ ) ) ) โ ( ( - ๐ฆ ยท ๐ ) + ( ( invg โ ๐บ ) โ ๐ ) ) = ( ( ( invg โ ๐บ ) โ ( ๐ฆ ยท ๐ ) ) + ( ( invg โ ๐บ ) โ ๐ ) ) ) |
21 |
1 2
|
mulgcl |
โข ( ( ๐บ โ Grp โง ๐ฆ โ โค โง ๐ โ ๐ต ) โ ( ๐ฆ ยท ๐ ) โ ๐ต ) |
22 |
21
|
adantr |
โข ( ( ( ๐บ โ Grp โง ๐ฆ โ โค โง ๐ โ ๐ต ) โง ( ( ๐ฆ ยท ๐ ) + ๐ ) = ( ๐ + ( ๐ฆ ยท ๐ ) ) ) โ ( ๐ฆ ยท ๐ ) โ ๐ต ) |
23 |
1 3 12
|
grpinvadd |
โข ( ( ๐บ โ Grp โง ๐ โ ๐ต โง ( ๐ฆ ยท ๐ ) โ ๐ต ) โ ( ( invg โ ๐บ ) โ ( ๐ + ( ๐ฆ ยท ๐ ) ) ) = ( ( ( invg โ ๐บ ) โ ( ๐ฆ ยท ๐ ) ) + ( ( invg โ ๐บ ) โ ๐ ) ) ) |
24 |
5 7 22 23
|
syl3anc |
โข ( ( ( ๐บ โ Grp โง ๐ฆ โ โค โง ๐ โ ๐ต ) โง ( ( ๐ฆ ยท ๐ ) + ๐ ) = ( ๐ + ( ๐ฆ ยท ๐ ) ) ) โ ( ( invg โ ๐บ ) โ ( ๐ + ( ๐ฆ ยท ๐ ) ) ) = ( ( ( invg โ ๐บ ) โ ( ๐ฆ ยท ๐ ) ) + ( ( invg โ ๐บ ) โ ๐ ) ) ) |
25 |
19
|
oveq2d |
โข ( ( ( ๐บ โ Grp โง ๐ฆ โ โค โง ๐ โ ๐ต ) โง ( ( ๐ฆ ยท ๐ ) + ๐ ) = ( ๐ + ( ๐ฆ ยท ๐ ) ) ) โ ( ( ( invg โ ๐บ ) โ ๐ ) + ( - ๐ฆ ยท ๐ ) ) = ( ( ( invg โ ๐บ ) โ ๐ ) + ( ( invg โ ๐บ ) โ ( ๐ฆ ยท ๐ ) ) ) ) |
26 |
1 3 12
|
grpinvadd |
โข ( ( ๐บ โ Grp โง ( ๐ฆ ยท ๐ ) โ ๐ต โง ๐ โ ๐ต ) โ ( ( invg โ ๐บ ) โ ( ( ๐ฆ ยท ๐ ) + ๐ ) ) = ( ( ( invg โ ๐บ ) โ ๐ ) + ( ( invg โ ๐บ ) โ ( ๐ฆ ยท ๐ ) ) ) ) |
27 |
5 22 7 26
|
syl3anc |
โข ( ( ( ๐บ โ Grp โง ๐ฆ โ โค โง ๐ โ ๐ต ) โง ( ( ๐ฆ ยท ๐ ) + ๐ ) = ( ๐ + ( ๐ฆ ยท ๐ ) ) ) โ ( ( invg โ ๐บ ) โ ( ( ๐ฆ ยท ๐ ) + ๐ ) ) = ( ( ( invg โ ๐บ ) โ ๐ ) + ( ( invg โ ๐บ ) โ ( ๐ฆ ยท ๐ ) ) ) ) |
28 |
|
fveq2 |
โข ( ( ( ๐ฆ ยท ๐ ) + ๐ ) = ( ๐ + ( ๐ฆ ยท ๐ ) ) โ ( ( invg โ ๐บ ) โ ( ( ๐ฆ ยท ๐ ) + ๐ ) ) = ( ( invg โ ๐บ ) โ ( ๐ + ( ๐ฆ ยท ๐ ) ) ) ) |
29 |
28
|
adantl |
โข ( ( ( ๐บ โ Grp โง ๐ฆ โ โค โง ๐ โ ๐ต ) โง ( ( ๐ฆ ยท ๐ ) + ๐ ) = ( ๐ + ( ๐ฆ ยท ๐ ) ) ) โ ( ( invg โ ๐บ ) โ ( ( ๐ฆ ยท ๐ ) + ๐ ) ) = ( ( invg โ ๐บ ) โ ( ๐ + ( ๐ฆ ยท ๐ ) ) ) ) |
30 |
25 27 29
|
3eqtr2rd |
โข ( ( ( ๐บ โ Grp โง ๐ฆ โ โค โง ๐ โ ๐ต ) โง ( ( ๐ฆ ยท ๐ ) + ๐ ) = ( ๐ + ( ๐ฆ ยท ๐ ) ) ) โ ( ( invg โ ๐บ ) โ ( ๐ + ( ๐ฆ ยท ๐ ) ) ) = ( ( ( invg โ ๐บ ) โ ๐ ) + ( - ๐ฆ ยท ๐ ) ) ) |
31 |
20 24 30
|
3eqtr2d |
โข ( ( ( ๐บ โ Grp โง ๐ฆ โ โค โง ๐ โ ๐ต ) โง ( ( ๐ฆ ยท ๐ ) + ๐ ) = ( ๐ + ( ๐ฆ ยท ๐ ) ) ) โ ( ( - ๐ฆ ยท ๐ ) + ( ( invg โ ๐บ ) โ ๐ ) ) = ( ( ( invg โ ๐บ ) โ ๐ ) + ( - ๐ฆ ยท ๐ ) ) ) |
32 |
31
|
oveq2d |
โข ( ( ( ๐บ โ Grp โง ๐ฆ โ โค โง ๐ โ ๐ต ) โง ( ( ๐ฆ ยท ๐ ) + ๐ ) = ( ๐ + ( ๐ฆ ยท ๐ ) ) ) โ ( ๐ + ( ( - ๐ฆ ยท ๐ ) + ( ( invg โ ๐บ ) โ ๐ ) ) ) = ( ๐ + ( ( ( invg โ ๐บ ) โ ๐ ) + ( - ๐ฆ ยท ๐ ) ) ) ) |
33 |
1 3 12
|
grpasscan1 |
โข ( ( ๐บ โ Grp โง ๐ โ ๐ต โง ( - ๐ฆ ยท ๐ ) โ ๐ต ) โ ( ๐ + ( ( ( invg โ ๐บ ) โ ๐ ) + ( - ๐ฆ ยท ๐ ) ) ) = ( - ๐ฆ ยท ๐ ) ) |
34 |
5 7 11 33
|
syl3anc |
โข ( ( ( ๐บ โ Grp โง ๐ฆ โ โค โง ๐ โ ๐ต ) โง ( ( ๐ฆ ยท ๐ ) + ๐ ) = ( ๐ + ( ๐ฆ ยท ๐ ) ) ) โ ( ๐ + ( ( ( invg โ ๐บ ) โ ๐ ) + ( - ๐ฆ ยท ๐ ) ) ) = ( - ๐ฆ ยท ๐ ) ) |
35 |
17 32 34
|
3eqtrd |
โข ( ( ( ๐บ โ Grp โง ๐ฆ โ โค โง ๐ โ ๐ต ) โง ( ( ๐ฆ ยท ๐ ) + ๐ ) = ( ๐ + ( ๐ฆ ยท ๐ ) ) ) โ ( ( ๐ + ( - ๐ฆ ยท ๐ ) ) + ( ( invg โ ๐บ ) โ ๐ ) ) = ( - ๐ฆ ยท ๐ ) ) |
36 |
35
|
oveq1d |
โข ( ( ( ๐บ โ Grp โง ๐ฆ โ โค โง ๐ โ ๐ต ) โง ( ( ๐ฆ ยท ๐ ) + ๐ ) = ( ๐ + ( ๐ฆ ยท ๐ ) ) ) โ ( ( ( ๐ + ( - ๐ฆ ยท ๐ ) ) + ( ( invg โ ๐บ ) โ ๐ ) ) + ๐ ) = ( ( - ๐ฆ ยท ๐ ) + ๐ ) ) |
37 |
1 3
|
grpcl |
โข ( ( ๐บ โ Grp โง ๐ โ ๐ต โง ( - ๐ฆ ยท ๐ ) โ ๐ต ) โ ( ๐ + ( - ๐ฆ ยท ๐ ) ) โ ๐ต ) |
38 |
4 6 10 37
|
syl3anc |
โข ( ( ๐บ โ Grp โง ๐ฆ โ โค โง ๐ โ ๐ต ) โ ( ๐ + ( - ๐ฆ ยท ๐ ) ) โ ๐ต ) |
39 |
38
|
adantr |
โข ( ( ( ๐บ โ Grp โง ๐ฆ โ โค โง ๐ โ ๐ต ) โง ( ( ๐ฆ ยท ๐ ) + ๐ ) = ( ๐ + ( ๐ฆ ยท ๐ ) ) ) โ ( ๐ + ( - ๐ฆ ยท ๐ ) ) โ ๐ต ) |
40 |
1 3 12
|
grpasscan2 |
โข ( ( ๐บ โ Grp โง ( ๐ + ( - ๐ฆ ยท ๐ ) ) โ ๐ต โง ๐ โ ๐ต ) โ ( ( ( ๐ + ( - ๐ฆ ยท ๐ ) ) + ( ( invg โ ๐บ ) โ ๐ ) ) + ๐ ) = ( ๐ + ( - ๐ฆ ยท ๐ ) ) ) |
41 |
5 39 7 40
|
syl3anc |
โข ( ( ( ๐บ โ Grp โง ๐ฆ โ โค โง ๐ โ ๐ต ) โง ( ( ๐ฆ ยท ๐ ) + ๐ ) = ( ๐ + ( ๐ฆ ยท ๐ ) ) ) โ ( ( ( ๐ + ( - ๐ฆ ยท ๐ ) ) + ( ( invg โ ๐บ ) โ ๐ ) ) + ๐ ) = ( ๐ + ( - ๐ฆ ยท ๐ ) ) ) |
42 |
36 41
|
eqtr3d |
โข ( ( ( ๐บ โ Grp โง ๐ฆ โ โค โง ๐ โ ๐ต ) โง ( ( ๐ฆ ยท ๐ ) + ๐ ) = ( ๐ + ( ๐ฆ ยท ๐ ) ) ) โ ( ( - ๐ฆ ยท ๐ ) + ๐ ) = ( ๐ + ( - ๐ฆ ยท ๐ ) ) ) |