Step |
Hyp |
Ref |
Expression |
1 |
|
nmmul.x |
|- X = ( Base ` R ) |
2 |
|
nmmul.n |
|- N = ( norm ` R ) |
3 |
|
nmmul.t |
|- .x. = ( .r ` R ) |
4 |
|
nrgdsdi.d |
|- D = ( dist ` R ) |
5 |
|
simpl |
|- ( ( R e. NrmRing /\ ( A e. X /\ B e. X /\ C e. X ) ) -> R e. NrmRing ) |
6 |
|
nrgring |
|- ( R e. NrmRing -> R e. Ring ) |
7 |
6
|
adantr |
|- ( ( R e. NrmRing /\ ( A e. X /\ B e. X /\ C e. X ) ) -> R e. Ring ) |
8 |
|
ringgrp |
|- ( R e. Ring -> R e. Grp ) |
9 |
7 8
|
syl |
|- ( ( R e. NrmRing /\ ( A e. X /\ B e. X /\ C e. X ) ) -> R e. Grp ) |
10 |
|
simpr1 |
|- ( ( R e. NrmRing /\ ( A e. X /\ B e. X /\ C e. X ) ) -> A e. X ) |
11 |
|
simpr2 |
|- ( ( R e. NrmRing /\ ( A e. X /\ B e. X /\ C e. X ) ) -> B e. X ) |
12 |
|
eqid |
|- ( -g ` R ) = ( -g ` R ) |
13 |
1 12
|
grpsubcl |
|- ( ( R e. Grp /\ A e. X /\ B e. X ) -> ( A ( -g ` R ) B ) e. X ) |
14 |
9 10 11 13
|
syl3anc |
|- ( ( R e. NrmRing /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( A ( -g ` R ) B ) e. X ) |
15 |
|
simpr3 |
|- ( ( R e. NrmRing /\ ( A e. X /\ B e. X /\ C e. X ) ) -> C e. X ) |
16 |
1 2 3
|
nmmul |
|- ( ( R e. NrmRing /\ ( A ( -g ` R ) B ) e. X /\ C e. X ) -> ( N ` ( ( A ( -g ` R ) B ) .x. C ) ) = ( ( N ` ( A ( -g ` R ) B ) ) x. ( N ` C ) ) ) |
17 |
5 14 15 16
|
syl3anc |
|- ( ( R e. NrmRing /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( N ` ( ( A ( -g ` R ) B ) .x. C ) ) = ( ( N ` ( A ( -g ` R ) B ) ) x. ( N ` C ) ) ) |
18 |
1 3 12 7 10 11 15
|
rngsubdir |
|- ( ( R e. NrmRing /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A ( -g ` R ) B ) .x. C ) = ( ( A .x. C ) ( -g ` R ) ( B .x. C ) ) ) |
19 |
18
|
fveq2d |
|- ( ( R e. NrmRing /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( N ` ( ( A ( -g ` R ) B ) .x. C ) ) = ( N ` ( ( A .x. C ) ( -g ` R ) ( B .x. C ) ) ) ) |
20 |
17 19
|
eqtr3d |
|- ( ( R e. NrmRing /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( N ` ( A ( -g ` R ) B ) ) x. ( N ` C ) ) = ( N ` ( ( A .x. C ) ( -g ` R ) ( B .x. C ) ) ) ) |
21 |
|
nrgngp |
|- ( R e. NrmRing -> R e. NrmGrp ) |
22 |
21
|
adantr |
|- ( ( R e. NrmRing /\ ( A e. X /\ B e. X /\ C e. X ) ) -> R e. NrmGrp ) |
23 |
2 1 12 4
|
ngpds |
|- ( ( R e. NrmGrp /\ A e. X /\ B e. X ) -> ( A D B ) = ( N ` ( A ( -g ` R ) B ) ) ) |
24 |
22 10 11 23
|
syl3anc |
|- ( ( R e. NrmRing /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( A D B ) = ( N ` ( A ( -g ` R ) B ) ) ) |
25 |
24
|
oveq1d |
|- ( ( R e. NrmRing /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A D B ) x. ( N ` C ) ) = ( ( N ` ( A ( -g ` R ) B ) ) x. ( N ` C ) ) ) |
26 |
1 3
|
ringcl |
|- ( ( R e. Ring /\ A e. X /\ C e. X ) -> ( A .x. C ) e. X ) |
27 |
7 10 15 26
|
syl3anc |
|- ( ( R e. NrmRing /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( A .x. C ) e. X ) |
28 |
1 3
|
ringcl |
|- ( ( R e. Ring /\ B e. X /\ C e. X ) -> ( B .x. C ) e. X ) |
29 |
7 11 15 28
|
syl3anc |
|- ( ( R e. NrmRing /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( B .x. C ) e. X ) |
30 |
2 1 12 4
|
ngpds |
|- ( ( R e. NrmGrp /\ ( A .x. C ) e. X /\ ( B .x. C ) e. X ) -> ( ( A .x. C ) D ( B .x. C ) ) = ( N ` ( ( A .x. C ) ( -g ` R ) ( B .x. C ) ) ) ) |
31 |
22 27 29 30
|
syl3anc |
|- ( ( R e. NrmRing /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A .x. C ) D ( B .x. C ) ) = ( N ` ( ( A .x. C ) ( -g ` R ) ( B .x. C ) ) ) ) |
32 |
20 25 31
|
3eqtr4d |
|- ( ( R e. NrmRing /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A D B ) x. ( N ` C ) ) = ( ( A .x. C ) D ( B .x. C ) ) ) |