Step |
Hyp |
Ref |
Expression |
1 |
|
rngneglmul.b |
|- B = ( Base ` R ) |
2 |
|
rngneglmul.t |
|- .x. = ( .r ` R ) |
3 |
|
rngneglmul.n |
|- N = ( invg ` R ) |
4 |
|
rngneglmul.r |
|- ( ph -> R e. Rng ) |
5 |
|
rngneglmul.x |
|- ( ph -> X e. B ) |
6 |
|
rngneglmul.y |
|- ( ph -> Y e. B ) |
7 |
|
eqid |
|- ( +g ` R ) = ( +g ` R ) |
8 |
|
eqid |
|- ( 0g ` R ) = ( 0g ` R ) |
9 |
|
rnggrp |
|- ( R e. Rng -> R e. Grp ) |
10 |
4 9
|
syl |
|- ( ph -> R e. Grp ) |
11 |
1 7 8 3 10 5
|
grprinvd |
|- ( ph -> ( X ( +g ` R ) ( N ` X ) ) = ( 0g ` R ) ) |
12 |
11
|
oveq1d |
|- ( ph -> ( ( X ( +g ` R ) ( N ` X ) ) .x. Y ) = ( ( 0g ` R ) .x. Y ) ) |
13 |
1 2 8
|
rnglz |
|- ( ( R e. Rng /\ Y e. B ) -> ( ( 0g ` R ) .x. Y ) = ( 0g ` R ) ) |
14 |
4 6 13
|
syl2anc |
|- ( ph -> ( ( 0g ` R ) .x. Y ) = ( 0g ` R ) ) |
15 |
12 14
|
eqtrd |
|- ( ph -> ( ( X ( +g ` R ) ( N ` X ) ) .x. Y ) = ( 0g ` R ) ) |
16 |
1 2
|
rngcl |
|- ( ( R e. Rng /\ X e. B /\ Y e. B ) -> ( X .x. Y ) e. B ) |
17 |
4 5 6 16
|
syl3anc |
|- ( ph -> ( X .x. Y ) e. B ) |
18 |
1 3 10 5
|
grpinvcld |
|- ( ph -> ( N ` X ) e. B ) |
19 |
1 2
|
rngcl |
|- ( ( R e. Rng /\ ( N ` X ) e. B /\ Y e. B ) -> ( ( N ` X ) .x. Y ) e. B ) |
20 |
4 18 6 19
|
syl3anc |
|- ( ph -> ( ( N ` X ) .x. Y ) e. B ) |
21 |
1 7 8 3
|
grpinvid1 |
|- ( ( R e. Grp /\ ( X .x. Y ) e. B /\ ( ( N ` X ) .x. Y ) e. B ) -> ( ( N ` ( X .x. Y ) ) = ( ( N ` X ) .x. Y ) <-> ( ( X .x. Y ) ( +g ` R ) ( ( N ` X ) .x. Y ) ) = ( 0g ` R ) ) ) |
22 |
10 17 20 21
|
syl3anc |
|- ( ph -> ( ( N ` ( X .x. Y ) ) = ( ( N ` X ) .x. Y ) <-> ( ( X .x. Y ) ( +g ` R ) ( ( N ` X ) .x. Y ) ) = ( 0g ` R ) ) ) |
23 |
1 7 2
|
rngdir |
|- ( ( R e. Rng /\ ( X e. B /\ ( N ` X ) e. B /\ Y e. B ) ) -> ( ( X ( +g ` R ) ( N ` X ) ) .x. Y ) = ( ( X .x. Y ) ( +g ` R ) ( ( N ` X ) .x. Y ) ) ) |
24 |
23
|
eqcomd |
|- ( ( R e. Rng /\ ( X e. B /\ ( N ` X ) e. B /\ Y e. B ) ) -> ( ( X .x. Y ) ( +g ` R ) ( ( N ` X ) .x. Y ) ) = ( ( X ( +g ` R ) ( N ` X ) ) .x. Y ) ) |
25 |
4 5 18 6 24
|
syl13anc |
|- ( ph -> ( ( X .x. Y ) ( +g ` R ) ( ( N ` X ) .x. Y ) ) = ( ( X ( +g ` R ) ( N ` X ) ) .x. Y ) ) |
26 |
25
|
eqeq1d |
|- ( ph -> ( ( ( X .x. Y ) ( +g ` R ) ( ( N ` X ) .x. Y ) ) = ( 0g ` R ) <-> ( ( X ( +g ` R ) ( N ` X ) ) .x. Y ) = ( 0g ` R ) ) ) |
27 |
22 26
|
bitrd |
|- ( ph -> ( ( N ` ( X .x. Y ) ) = ( ( N ` X ) .x. Y ) <-> ( ( X ( +g ` R ) ( N ` X ) ) .x. Y ) = ( 0g ` R ) ) ) |
28 |
15 27
|
mpbird |
|- ( ph -> ( N ` ( X .x. Y ) ) = ( ( N ` X ) .x. Y ) ) |
29 |
28
|
eqcomd |
|- ( ph -> ( ( N ` X ) .x. Y ) = ( N ` ( X .x. Y ) ) ) |