Step |
Hyp |
Ref |
Expression |
1 |
|
mulgass3.b |
โข ๐ต = ( Base โ ๐
) |
2 |
|
mulgass3.m |
โข ยท = ( .g โ ๐
) |
3 |
|
mulgass3.t |
โข ร = ( .r โ ๐
) |
4 |
|
eqid |
โข ( oppr โ ๐
) = ( oppr โ ๐
) |
5 |
4
|
opprring |
โข ( ๐
โ Ring โ ( oppr โ ๐
) โ Ring ) |
6 |
5
|
adantr |
โข ( ( ๐
โ Ring โง ( ๐ โ โค โง ๐ โ ๐ต โง ๐ โ ๐ต ) ) โ ( oppr โ ๐
) โ Ring ) |
7 |
|
simpr1 |
โข ( ( ๐
โ Ring โง ( ๐ โ โค โง ๐ โ ๐ต โง ๐ โ ๐ต ) ) โ ๐ โ โค ) |
8 |
|
simpr3 |
โข ( ( ๐
โ Ring โง ( ๐ โ โค โง ๐ โ ๐ต โง ๐ โ ๐ต ) ) โ ๐ โ ๐ต ) |
9 |
|
simpr2 |
โข ( ( ๐
โ Ring โง ( ๐ โ โค โง ๐ โ ๐ต โง ๐ โ ๐ต ) ) โ ๐ โ ๐ต ) |
10 |
4 1
|
opprbas |
โข ๐ต = ( Base โ ( oppr โ ๐
) ) |
11 |
|
eqid |
โข ( .g โ ( oppr โ ๐
) ) = ( .g โ ( oppr โ ๐
) ) |
12 |
|
eqid |
โข ( .r โ ( oppr โ ๐
) ) = ( .r โ ( oppr โ ๐
) ) |
13 |
10 11 12
|
mulgass2 |
โข ( ( ( oppr โ ๐
) โ Ring โง ( ๐ โ โค โง ๐ โ ๐ต โง ๐ โ ๐ต ) ) โ ( ( ๐ ( .g โ ( oppr โ ๐
) ) ๐ ) ( .r โ ( oppr โ ๐
) ) ๐ ) = ( ๐ ( .g โ ( oppr โ ๐
) ) ( ๐ ( .r โ ( oppr โ ๐
) ) ๐ ) ) ) |
14 |
6 7 8 9 13
|
syl13anc |
โข ( ( ๐
โ Ring โง ( ๐ โ โค โง ๐ โ ๐ต โง ๐ โ ๐ต ) ) โ ( ( ๐ ( .g โ ( oppr โ ๐
) ) ๐ ) ( .r โ ( oppr โ ๐
) ) ๐ ) = ( ๐ ( .g โ ( oppr โ ๐
) ) ( ๐ ( .r โ ( oppr โ ๐
) ) ๐ ) ) ) |
15 |
1 3 4 12
|
opprmul |
โข ( ( ๐ ( .g โ ( oppr โ ๐
) ) ๐ ) ( .r โ ( oppr โ ๐
) ) ๐ ) = ( ๐ ร ( ๐ ( .g โ ( oppr โ ๐
) ) ๐ ) ) |
16 |
1 3 4 12
|
opprmul |
โข ( ๐ ( .r โ ( oppr โ ๐
) ) ๐ ) = ( ๐ ร ๐ ) |
17 |
16
|
oveq2i |
โข ( ๐ ( .g โ ( oppr โ ๐
) ) ( ๐ ( .r โ ( oppr โ ๐
) ) ๐ ) ) = ( ๐ ( .g โ ( oppr โ ๐
) ) ( ๐ ร ๐ ) ) |
18 |
14 15 17
|
3eqtr3g |
โข ( ( ๐
โ Ring โง ( ๐ โ โค โง ๐ โ ๐ต โง ๐ โ ๐ต ) ) โ ( ๐ ร ( ๐ ( .g โ ( oppr โ ๐
) ) ๐ ) ) = ( ๐ ( .g โ ( oppr โ ๐
) ) ( ๐ ร ๐ ) ) ) |
19 |
1
|
a1i |
โข ( ( ๐
โ Ring โง ( ๐ โ โค โง ๐ โ ๐ต โง ๐ โ ๐ต ) ) โ ๐ต = ( Base โ ๐
) ) |
20 |
10
|
a1i |
โข ( ( ๐
โ Ring โง ( ๐ โ โค โง ๐ โ ๐ต โง ๐ โ ๐ต ) ) โ ๐ต = ( Base โ ( oppr โ ๐
) ) ) |
21 |
|
ssv |
โข ๐ต โ V |
22 |
21
|
a1i |
โข ( ( ๐
โ Ring โง ( ๐ โ โค โง ๐ โ ๐ต โง ๐ โ ๐ต ) ) โ ๐ต โ V ) |
23 |
|
ovexd |
โข ( ( ( ๐
โ Ring โง ( ๐ โ โค โง ๐ โ ๐ต โง ๐ โ ๐ต ) ) โง ( ๐ฅ โ V โง ๐ฆ โ V ) ) โ ( ๐ฅ ( +g โ ๐
) ๐ฆ ) โ V ) |
24 |
|
eqid |
โข ( +g โ ๐
) = ( +g โ ๐
) |
25 |
4 24
|
oppradd |
โข ( +g โ ๐
) = ( +g โ ( oppr โ ๐
) ) |
26 |
25
|
oveqi |
โข ( ๐ฅ ( +g โ ๐
) ๐ฆ ) = ( ๐ฅ ( +g โ ( oppr โ ๐
) ) ๐ฆ ) |
27 |
26
|
a1i |
โข ( ( ( ๐
โ Ring โง ( ๐ โ โค โง ๐ โ ๐ต โง ๐ โ ๐ต ) ) โง ( ๐ฅ โ V โง ๐ฆ โ V ) ) โ ( ๐ฅ ( +g โ ๐
) ๐ฆ ) = ( ๐ฅ ( +g โ ( oppr โ ๐
) ) ๐ฆ ) ) |
28 |
2 11 19 20 22 23 27
|
mulgpropd |
โข ( ( ๐
โ Ring โง ( ๐ โ โค โง ๐ โ ๐ต โง ๐ โ ๐ต ) ) โ ยท = ( .g โ ( oppr โ ๐
) ) ) |
29 |
28
|
oveqd |
โข ( ( ๐
โ Ring โง ( ๐ โ โค โง ๐ โ ๐ต โง ๐ โ ๐ต ) ) โ ( ๐ ยท ๐ ) = ( ๐ ( .g โ ( oppr โ ๐
) ) ๐ ) ) |
30 |
29
|
oveq2d |
โข ( ( ๐
โ Ring โง ( ๐ โ โค โง ๐ โ ๐ต โง ๐ โ ๐ต ) ) โ ( ๐ ร ( ๐ ยท ๐ ) ) = ( ๐ ร ( ๐ ( .g โ ( oppr โ ๐
) ) ๐ ) ) ) |
31 |
28
|
oveqd |
โข ( ( ๐
โ Ring โง ( ๐ โ โค โง ๐ โ ๐ต โง ๐ โ ๐ต ) ) โ ( ๐ ยท ( ๐ ร ๐ ) ) = ( ๐ ( .g โ ( oppr โ ๐
) ) ( ๐ ร ๐ ) ) ) |
32 |
18 30 31
|
3eqtr4d |
โข ( ( ๐
โ Ring โง ( ๐ โ โค โง ๐ โ ๐ต โง ๐ โ ๐ต ) ) โ ( ๐ ร ( ๐ ยท ๐ ) ) = ( ๐ ยท ( ๐ ร ๐ ) ) ) |