Step |
Hyp |
Ref |
Expression |
1 |
|
nmdvr.x |
|- X = ( Base ` R ) |
2 |
|
nmdvr.n |
|- N = ( norm ` R ) |
3 |
|
nmdvr.u |
|- U = ( Unit ` R ) |
4 |
|
nmdvr.d |
|- ./ = ( /r ` R ) |
5 |
|
simpll |
|- ( ( ( R e. NrmRing /\ R e. NzRing ) /\ ( A e. X /\ B e. U ) ) -> R e. NrmRing ) |
6 |
|
simprl |
|- ( ( ( R e. NrmRing /\ R e. NzRing ) /\ ( A e. X /\ B e. U ) ) -> A e. X ) |
7 |
|
nrgring |
|- ( R e. NrmRing -> R e. Ring ) |
8 |
7
|
ad2antrr |
|- ( ( ( R e. NrmRing /\ R e. NzRing ) /\ ( A e. X /\ B e. U ) ) -> R e. Ring ) |
9 |
|
simprr |
|- ( ( ( R e. NrmRing /\ R e. NzRing ) /\ ( A e. X /\ B e. U ) ) -> B e. U ) |
10 |
|
eqid |
|- ( invr ` R ) = ( invr ` R ) |
11 |
3 10 1
|
ringinvcl |
|- ( ( R e. Ring /\ B e. U ) -> ( ( invr ` R ) ` B ) e. X ) |
12 |
8 9 11
|
syl2anc |
|- ( ( ( R e. NrmRing /\ R e. NzRing ) /\ ( A e. X /\ B e. U ) ) -> ( ( invr ` R ) ` B ) e. X ) |
13 |
|
eqid |
|- ( .r ` R ) = ( .r ` R ) |
14 |
1 2 13
|
nmmul |
|- ( ( R e. NrmRing /\ A e. X /\ ( ( invr ` R ) ` B ) e. X ) -> ( N ` ( A ( .r ` R ) ( ( invr ` R ) ` B ) ) ) = ( ( N ` A ) x. ( N ` ( ( invr ` R ) ` B ) ) ) ) |
15 |
5 6 12 14
|
syl3anc |
|- ( ( ( R e. NrmRing /\ R e. NzRing ) /\ ( A e. X /\ B e. U ) ) -> ( N ` ( A ( .r ` R ) ( ( invr ` R ) ` B ) ) ) = ( ( N ` A ) x. ( N ` ( ( invr ` R ) ` B ) ) ) ) |
16 |
|
simplr |
|- ( ( ( R e. NrmRing /\ R e. NzRing ) /\ ( A e. X /\ B e. U ) ) -> R e. NzRing ) |
17 |
2 3 10
|
nminvr |
|- ( ( R e. NrmRing /\ R e. NzRing /\ B e. U ) -> ( N ` ( ( invr ` R ) ` B ) ) = ( 1 / ( N ` B ) ) ) |
18 |
5 16 9 17
|
syl3anc |
|- ( ( ( R e. NrmRing /\ R e. NzRing ) /\ ( A e. X /\ B e. U ) ) -> ( N ` ( ( invr ` R ) ` B ) ) = ( 1 / ( N ` B ) ) ) |
19 |
18
|
oveq2d |
|- ( ( ( R e. NrmRing /\ R e. NzRing ) /\ ( A e. X /\ B e. U ) ) -> ( ( N ` A ) x. ( N ` ( ( invr ` R ) ` B ) ) ) = ( ( N ` A ) x. ( 1 / ( N ` B ) ) ) ) |
20 |
15 19
|
eqtrd |
|- ( ( ( R e. NrmRing /\ R e. NzRing ) /\ ( A e. X /\ B e. U ) ) -> ( N ` ( A ( .r ` R ) ( ( invr ` R ) ` B ) ) ) = ( ( N ` A ) x. ( 1 / ( N ` B ) ) ) ) |
21 |
1 13 3 10 4
|
dvrval |
|- ( ( A e. X /\ B e. U ) -> ( A ./ B ) = ( A ( .r ` R ) ( ( invr ` R ) ` B ) ) ) |
22 |
21
|
adantl |
|- ( ( ( R e. NrmRing /\ R e. NzRing ) /\ ( A e. X /\ B e. U ) ) -> ( A ./ B ) = ( A ( .r ` R ) ( ( invr ` R ) ` B ) ) ) |
23 |
22
|
fveq2d |
|- ( ( ( R e. NrmRing /\ R e. NzRing ) /\ ( A e. X /\ B e. U ) ) -> ( N ` ( A ./ B ) ) = ( N ` ( A ( .r ` R ) ( ( invr ` R ) ` B ) ) ) ) |
24 |
|
nrgngp |
|- ( R e. NrmRing -> R e. NrmGrp ) |
25 |
24
|
ad2antrr |
|- ( ( ( R e. NrmRing /\ R e. NzRing ) /\ ( A e. X /\ B e. U ) ) -> R e. NrmGrp ) |
26 |
1 2
|
nmcl |
|- ( ( R e. NrmGrp /\ A e. X ) -> ( N ` A ) e. RR ) |
27 |
25 6 26
|
syl2anc |
|- ( ( ( R e. NrmRing /\ R e. NzRing ) /\ ( A e. X /\ B e. U ) ) -> ( N ` A ) e. RR ) |
28 |
27
|
recnd |
|- ( ( ( R e. NrmRing /\ R e. NzRing ) /\ ( A e. X /\ B e. U ) ) -> ( N ` A ) e. CC ) |
29 |
1 3
|
unitss |
|- U C_ X |
30 |
29 9
|
sselid |
|- ( ( ( R e. NrmRing /\ R e. NzRing ) /\ ( A e. X /\ B e. U ) ) -> B e. X ) |
31 |
1 2
|
nmcl |
|- ( ( R e. NrmGrp /\ B e. X ) -> ( N ` B ) e. RR ) |
32 |
25 30 31
|
syl2anc |
|- ( ( ( R e. NrmRing /\ R e. NzRing ) /\ ( A e. X /\ B e. U ) ) -> ( N ` B ) e. RR ) |
33 |
32
|
recnd |
|- ( ( ( R e. NrmRing /\ R e. NzRing ) /\ ( A e. X /\ B e. U ) ) -> ( N ` B ) e. CC ) |
34 |
2 3
|
unitnmn0 |
|- ( ( R e. NrmRing /\ R e. NzRing /\ B e. U ) -> ( N ` B ) =/= 0 ) |
35 |
34
|
3expa |
|- ( ( ( R e. NrmRing /\ R e. NzRing ) /\ B e. U ) -> ( N ` B ) =/= 0 ) |
36 |
35
|
adantrl |
|- ( ( ( R e. NrmRing /\ R e. NzRing ) /\ ( A e. X /\ B e. U ) ) -> ( N ` B ) =/= 0 ) |
37 |
28 33 36
|
divrecd |
|- ( ( ( R e. NrmRing /\ R e. NzRing ) /\ ( A e. X /\ B e. U ) ) -> ( ( N ` A ) / ( N ` B ) ) = ( ( N ` A ) x. ( 1 / ( N ` B ) ) ) ) |
38 |
20 23 37
|
3eqtr4d |
|- ( ( ( R e. NrmRing /\ R e. NzRing ) /\ ( A e. X /\ B e. U ) ) -> ( N ` ( A ./ B ) ) = ( ( N ` A ) / ( N ` B ) ) ) |