Step |
Hyp |
Ref |
Expression |
1 |
|
nmmul.x |
⊢ 𝑋 = ( Base ‘ 𝑅 ) |
2 |
|
nmmul.n |
⊢ 𝑁 = ( norm ‘ 𝑅 ) |
3 |
|
nmmul.t |
⊢ · = ( .r ‘ 𝑅 ) |
4 |
|
nrgdsdi.d |
⊢ 𝐷 = ( dist ‘ 𝑅 ) |
5 |
|
simpl |
⊢ ( ( 𝑅 ∈ NrmRing ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → 𝑅 ∈ NrmRing ) |
6 |
|
nrgring |
⊢ ( 𝑅 ∈ NrmRing → 𝑅 ∈ Ring ) |
7 |
6
|
adantr |
⊢ ( ( 𝑅 ∈ NrmRing ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → 𝑅 ∈ Ring ) |
8 |
|
ringgrp |
⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Grp ) |
9 |
7 8
|
syl |
⊢ ( ( 𝑅 ∈ NrmRing ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → 𝑅 ∈ Grp ) |
10 |
|
simpr1 |
⊢ ( ( 𝑅 ∈ NrmRing ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → 𝐴 ∈ 𝑋 ) |
11 |
|
simpr2 |
⊢ ( ( 𝑅 ∈ NrmRing ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → 𝐵 ∈ 𝑋 ) |
12 |
|
eqid |
⊢ ( -g ‘ 𝑅 ) = ( -g ‘ 𝑅 ) |
13 |
1 12
|
grpsubcl |
⊢ ( ( 𝑅 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 ( -g ‘ 𝑅 ) 𝐵 ) ∈ 𝑋 ) |
14 |
9 10 11 13
|
syl3anc |
⊢ ( ( 𝑅 ∈ NrmRing ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝐴 ( -g ‘ 𝑅 ) 𝐵 ) ∈ 𝑋 ) |
15 |
|
simpr3 |
⊢ ( ( 𝑅 ∈ NrmRing ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → 𝐶 ∈ 𝑋 ) |
16 |
1 2 3
|
nmmul |
⊢ ( ( 𝑅 ∈ NrmRing ∧ ( 𝐴 ( -g ‘ 𝑅 ) 𝐵 ) ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) → ( 𝑁 ‘ ( ( 𝐴 ( -g ‘ 𝑅 ) 𝐵 ) · 𝐶 ) ) = ( ( 𝑁 ‘ ( 𝐴 ( -g ‘ 𝑅 ) 𝐵 ) ) · ( 𝑁 ‘ 𝐶 ) ) ) |
17 |
5 14 15 16
|
syl3anc |
⊢ ( ( 𝑅 ∈ NrmRing ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝑁 ‘ ( ( 𝐴 ( -g ‘ 𝑅 ) 𝐵 ) · 𝐶 ) ) = ( ( 𝑁 ‘ ( 𝐴 ( -g ‘ 𝑅 ) 𝐵 ) ) · ( 𝑁 ‘ 𝐶 ) ) ) |
18 |
1 3 12 7 10 11 15
|
rngsubdir |
⊢ ( ( 𝑅 ∈ NrmRing ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( 𝐴 ( -g ‘ 𝑅 ) 𝐵 ) · 𝐶 ) = ( ( 𝐴 · 𝐶 ) ( -g ‘ 𝑅 ) ( 𝐵 · 𝐶 ) ) ) |
19 |
18
|
fveq2d |
⊢ ( ( 𝑅 ∈ NrmRing ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝑁 ‘ ( ( 𝐴 ( -g ‘ 𝑅 ) 𝐵 ) · 𝐶 ) ) = ( 𝑁 ‘ ( ( 𝐴 · 𝐶 ) ( -g ‘ 𝑅 ) ( 𝐵 · 𝐶 ) ) ) ) |
20 |
17 19
|
eqtr3d |
⊢ ( ( 𝑅 ∈ NrmRing ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( 𝑁 ‘ ( 𝐴 ( -g ‘ 𝑅 ) 𝐵 ) ) · ( 𝑁 ‘ 𝐶 ) ) = ( 𝑁 ‘ ( ( 𝐴 · 𝐶 ) ( -g ‘ 𝑅 ) ( 𝐵 · 𝐶 ) ) ) ) |
21 |
|
nrgngp |
⊢ ( 𝑅 ∈ NrmRing → 𝑅 ∈ NrmGrp ) |
22 |
21
|
adantr |
⊢ ( ( 𝑅 ∈ NrmRing ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → 𝑅 ∈ NrmGrp ) |
23 |
2 1 12 4
|
ngpds |
⊢ ( ( 𝑅 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝐷 𝐵 ) = ( 𝑁 ‘ ( 𝐴 ( -g ‘ 𝑅 ) 𝐵 ) ) ) |
24 |
22 10 11 23
|
syl3anc |
⊢ ( ( 𝑅 ∈ NrmRing ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝐴 𝐷 𝐵 ) = ( 𝑁 ‘ ( 𝐴 ( -g ‘ 𝑅 ) 𝐵 ) ) ) |
25 |
24
|
oveq1d |
⊢ ( ( 𝑅 ∈ NrmRing ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( 𝐴 𝐷 𝐵 ) · ( 𝑁 ‘ 𝐶 ) ) = ( ( 𝑁 ‘ ( 𝐴 ( -g ‘ 𝑅 ) 𝐵 ) ) · ( 𝑁 ‘ 𝐶 ) ) ) |
26 |
1 3
|
ringcl |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) → ( 𝐴 · 𝐶 ) ∈ 𝑋 ) |
27 |
7 10 15 26
|
syl3anc |
⊢ ( ( 𝑅 ∈ NrmRing ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝐴 · 𝐶 ) ∈ 𝑋 ) |
28 |
1 3
|
ringcl |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) → ( 𝐵 · 𝐶 ) ∈ 𝑋 ) |
29 |
7 11 15 28
|
syl3anc |
⊢ ( ( 𝑅 ∈ NrmRing ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝐵 · 𝐶 ) ∈ 𝑋 ) |
30 |
2 1 12 4
|
ngpds |
⊢ ( ( 𝑅 ∈ NrmGrp ∧ ( 𝐴 · 𝐶 ) ∈ 𝑋 ∧ ( 𝐵 · 𝐶 ) ∈ 𝑋 ) → ( ( 𝐴 · 𝐶 ) 𝐷 ( 𝐵 · 𝐶 ) ) = ( 𝑁 ‘ ( ( 𝐴 · 𝐶 ) ( -g ‘ 𝑅 ) ( 𝐵 · 𝐶 ) ) ) ) |
31 |
22 27 29 30
|
syl3anc |
⊢ ( ( 𝑅 ∈ NrmRing ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( 𝐴 · 𝐶 ) 𝐷 ( 𝐵 · 𝐶 ) ) = ( 𝑁 ‘ ( ( 𝐴 · 𝐶 ) ( -g ‘ 𝑅 ) ( 𝐵 · 𝐶 ) ) ) ) |
32 |
20 25 31
|
3eqtr4d |
⊢ ( ( 𝑅 ∈ NrmRing ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( 𝐴 𝐷 𝐵 ) · ( 𝑁 ‘ 𝐶 ) ) = ( ( 𝐴 · 𝐶 ) 𝐷 ( 𝐵 · 𝐶 ) ) ) |