Step |
Hyp |
Ref |
Expression |
1 |
|
nmdvr.x |
⊢ 𝑋 = ( Base ‘ 𝑅 ) |
2 |
|
nmdvr.n |
⊢ 𝑁 = ( norm ‘ 𝑅 ) |
3 |
|
nmdvr.u |
⊢ 𝑈 = ( Unit ‘ 𝑅 ) |
4 |
|
nmdvr.d |
⊢ / = ( /r ‘ 𝑅 ) |
5 |
|
simpll |
⊢ ( ( ( 𝑅 ∈ NrmRing ∧ 𝑅 ∈ NzRing ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑈 ) ) → 𝑅 ∈ NrmRing ) |
6 |
|
simprl |
⊢ ( ( ( 𝑅 ∈ NrmRing ∧ 𝑅 ∈ NzRing ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑈 ) ) → 𝐴 ∈ 𝑋 ) |
7 |
|
nrgring |
⊢ ( 𝑅 ∈ NrmRing → 𝑅 ∈ Ring ) |
8 |
7
|
ad2antrr |
⊢ ( ( ( 𝑅 ∈ NrmRing ∧ 𝑅 ∈ NzRing ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑈 ) ) → 𝑅 ∈ Ring ) |
9 |
|
simprr |
⊢ ( ( ( 𝑅 ∈ NrmRing ∧ 𝑅 ∈ NzRing ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑈 ) ) → 𝐵 ∈ 𝑈 ) |
10 |
|
eqid |
⊢ ( invr ‘ 𝑅 ) = ( invr ‘ 𝑅 ) |
11 |
3 10 1
|
ringinvcl |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝐵 ∈ 𝑈 ) → ( ( invr ‘ 𝑅 ) ‘ 𝐵 ) ∈ 𝑋 ) |
12 |
8 9 11
|
syl2anc |
⊢ ( ( ( 𝑅 ∈ NrmRing ∧ 𝑅 ∈ NzRing ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑈 ) ) → ( ( invr ‘ 𝑅 ) ‘ 𝐵 ) ∈ 𝑋 ) |
13 |
|
eqid |
⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 ) |
14 |
1 2 13
|
nmmul |
⊢ ( ( 𝑅 ∈ NrmRing ∧ 𝐴 ∈ 𝑋 ∧ ( ( invr ‘ 𝑅 ) ‘ 𝐵 ) ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝐴 ( .r ‘ 𝑅 ) ( ( invr ‘ 𝑅 ) ‘ 𝐵 ) ) ) = ( ( 𝑁 ‘ 𝐴 ) · ( 𝑁 ‘ ( ( invr ‘ 𝑅 ) ‘ 𝐵 ) ) ) ) |
15 |
5 6 12 14
|
syl3anc |
⊢ ( ( ( 𝑅 ∈ NrmRing ∧ 𝑅 ∈ NzRing ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑈 ) ) → ( 𝑁 ‘ ( 𝐴 ( .r ‘ 𝑅 ) ( ( invr ‘ 𝑅 ) ‘ 𝐵 ) ) ) = ( ( 𝑁 ‘ 𝐴 ) · ( 𝑁 ‘ ( ( invr ‘ 𝑅 ) ‘ 𝐵 ) ) ) ) |
16 |
|
simplr |
⊢ ( ( ( 𝑅 ∈ NrmRing ∧ 𝑅 ∈ NzRing ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑈 ) ) → 𝑅 ∈ NzRing ) |
17 |
2 3 10
|
nminvr |
⊢ ( ( 𝑅 ∈ NrmRing ∧ 𝑅 ∈ NzRing ∧ 𝐵 ∈ 𝑈 ) → ( 𝑁 ‘ ( ( invr ‘ 𝑅 ) ‘ 𝐵 ) ) = ( 1 / ( 𝑁 ‘ 𝐵 ) ) ) |
18 |
5 16 9 17
|
syl3anc |
⊢ ( ( ( 𝑅 ∈ NrmRing ∧ 𝑅 ∈ NzRing ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑈 ) ) → ( 𝑁 ‘ ( ( invr ‘ 𝑅 ) ‘ 𝐵 ) ) = ( 1 / ( 𝑁 ‘ 𝐵 ) ) ) |
19 |
18
|
oveq2d |
⊢ ( ( ( 𝑅 ∈ NrmRing ∧ 𝑅 ∈ NzRing ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑈 ) ) → ( ( 𝑁 ‘ 𝐴 ) · ( 𝑁 ‘ ( ( invr ‘ 𝑅 ) ‘ 𝐵 ) ) ) = ( ( 𝑁 ‘ 𝐴 ) · ( 1 / ( 𝑁 ‘ 𝐵 ) ) ) ) |
20 |
15 19
|
eqtrd |
⊢ ( ( ( 𝑅 ∈ NrmRing ∧ 𝑅 ∈ NzRing ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑈 ) ) → ( 𝑁 ‘ ( 𝐴 ( .r ‘ 𝑅 ) ( ( invr ‘ 𝑅 ) ‘ 𝐵 ) ) ) = ( ( 𝑁 ‘ 𝐴 ) · ( 1 / ( 𝑁 ‘ 𝐵 ) ) ) ) |
21 |
1 13 3 10 4
|
dvrval |
⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑈 ) → ( 𝐴 / 𝐵 ) = ( 𝐴 ( .r ‘ 𝑅 ) ( ( invr ‘ 𝑅 ) ‘ 𝐵 ) ) ) |
22 |
21
|
adantl |
⊢ ( ( ( 𝑅 ∈ NrmRing ∧ 𝑅 ∈ NzRing ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑈 ) ) → ( 𝐴 / 𝐵 ) = ( 𝐴 ( .r ‘ 𝑅 ) ( ( invr ‘ 𝑅 ) ‘ 𝐵 ) ) ) |
23 |
22
|
fveq2d |
⊢ ( ( ( 𝑅 ∈ NrmRing ∧ 𝑅 ∈ NzRing ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑈 ) ) → ( 𝑁 ‘ ( 𝐴 / 𝐵 ) ) = ( 𝑁 ‘ ( 𝐴 ( .r ‘ 𝑅 ) ( ( invr ‘ 𝑅 ) ‘ 𝐵 ) ) ) ) |
24 |
|
nrgngp |
⊢ ( 𝑅 ∈ NrmRing → 𝑅 ∈ NrmGrp ) |
25 |
24
|
ad2antrr |
⊢ ( ( ( 𝑅 ∈ NrmRing ∧ 𝑅 ∈ NzRing ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑈 ) ) → 𝑅 ∈ NrmGrp ) |
26 |
1 2
|
nmcl |
⊢ ( ( 𝑅 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ) → ( 𝑁 ‘ 𝐴 ) ∈ ℝ ) |
27 |
25 6 26
|
syl2anc |
⊢ ( ( ( 𝑅 ∈ NrmRing ∧ 𝑅 ∈ NzRing ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑈 ) ) → ( 𝑁 ‘ 𝐴 ) ∈ ℝ ) |
28 |
27
|
recnd |
⊢ ( ( ( 𝑅 ∈ NrmRing ∧ 𝑅 ∈ NzRing ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑈 ) ) → ( 𝑁 ‘ 𝐴 ) ∈ ℂ ) |
29 |
1 3
|
unitss |
⊢ 𝑈 ⊆ 𝑋 |
30 |
29 9
|
sselid |
⊢ ( ( ( 𝑅 ∈ NrmRing ∧ 𝑅 ∈ NzRing ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑈 ) ) → 𝐵 ∈ 𝑋 ) |
31 |
1 2
|
nmcl |
⊢ ( ( 𝑅 ∈ NrmGrp ∧ 𝐵 ∈ 𝑋 ) → ( 𝑁 ‘ 𝐵 ) ∈ ℝ ) |
32 |
25 30 31
|
syl2anc |
⊢ ( ( ( 𝑅 ∈ NrmRing ∧ 𝑅 ∈ NzRing ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑈 ) ) → ( 𝑁 ‘ 𝐵 ) ∈ ℝ ) |
33 |
32
|
recnd |
⊢ ( ( ( 𝑅 ∈ NrmRing ∧ 𝑅 ∈ NzRing ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑈 ) ) → ( 𝑁 ‘ 𝐵 ) ∈ ℂ ) |
34 |
2 3
|
unitnmn0 |
⊢ ( ( 𝑅 ∈ NrmRing ∧ 𝑅 ∈ NzRing ∧ 𝐵 ∈ 𝑈 ) → ( 𝑁 ‘ 𝐵 ) ≠ 0 ) |
35 |
34
|
3expa |
⊢ ( ( ( 𝑅 ∈ NrmRing ∧ 𝑅 ∈ NzRing ) ∧ 𝐵 ∈ 𝑈 ) → ( 𝑁 ‘ 𝐵 ) ≠ 0 ) |
36 |
35
|
adantrl |
⊢ ( ( ( 𝑅 ∈ NrmRing ∧ 𝑅 ∈ NzRing ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑈 ) ) → ( 𝑁 ‘ 𝐵 ) ≠ 0 ) |
37 |
28 33 36
|
divrecd |
⊢ ( ( ( 𝑅 ∈ NrmRing ∧ 𝑅 ∈ NzRing ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑈 ) ) → ( ( 𝑁 ‘ 𝐴 ) / ( 𝑁 ‘ 𝐵 ) ) = ( ( 𝑁 ‘ 𝐴 ) · ( 1 / ( 𝑁 ‘ 𝐵 ) ) ) ) |
38 |
20 23 37
|
3eqtr4d |
⊢ ( ( ( 𝑅 ∈ NrmRing ∧ 𝑅 ∈ NzRing ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑈 ) ) → ( 𝑁 ‘ ( 𝐴 / 𝐵 ) ) = ( ( 𝑁 ‘ 𝐴 ) / ( 𝑁 ‘ 𝐵 ) ) ) |