Step |
Hyp |
Ref |
Expression |
1 |
|
nminvr.n |
⊢ 𝑁 = ( norm ‘ 𝑅 ) |
2 |
|
nminvr.u |
⊢ 𝑈 = ( Unit ‘ 𝑅 ) |
3 |
|
nrgngp |
⊢ ( 𝑅 ∈ NrmRing → 𝑅 ∈ NrmGrp ) |
4 |
3
|
3ad2ant1 |
⊢ ( ( 𝑅 ∈ NrmRing ∧ 𝑅 ∈ NzRing ∧ 𝐴 ∈ 𝑈 ) → 𝑅 ∈ NrmGrp ) |
5 |
|
eqid |
⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 ) |
6 |
5 2
|
unitcl |
⊢ ( 𝐴 ∈ 𝑈 → 𝐴 ∈ ( Base ‘ 𝑅 ) ) |
7 |
6
|
3ad2ant3 |
⊢ ( ( 𝑅 ∈ NrmRing ∧ 𝑅 ∈ NzRing ∧ 𝐴 ∈ 𝑈 ) → 𝐴 ∈ ( Base ‘ 𝑅 ) ) |
8 |
|
eqid |
⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 ) |
9 |
2 8
|
nzrunit |
⊢ ( ( 𝑅 ∈ NzRing ∧ 𝐴 ∈ 𝑈 ) → 𝐴 ≠ ( 0g ‘ 𝑅 ) ) |
10 |
9
|
3adant1 |
⊢ ( ( 𝑅 ∈ NrmRing ∧ 𝑅 ∈ NzRing ∧ 𝐴 ∈ 𝑈 ) → 𝐴 ≠ ( 0g ‘ 𝑅 ) ) |
11 |
5 1 8
|
nmne0 |
⊢ ( ( 𝑅 ∈ NrmGrp ∧ 𝐴 ∈ ( Base ‘ 𝑅 ) ∧ 𝐴 ≠ ( 0g ‘ 𝑅 ) ) → ( 𝑁 ‘ 𝐴 ) ≠ 0 ) |
12 |
4 7 10 11
|
syl3anc |
⊢ ( ( 𝑅 ∈ NrmRing ∧ 𝑅 ∈ NzRing ∧ 𝐴 ∈ 𝑈 ) → ( 𝑁 ‘ 𝐴 ) ≠ 0 ) |