Step |
Hyp |
Ref |
Expression |
1 |
|
irredn0.i |
⊢ 𝐼 = ( Irred ‘ 𝑅 ) |
2 |
|
irredneg.n |
⊢ 𝑁 = ( invg ‘ 𝑅 ) |
3 |
|
irrednegb.b |
⊢ 𝐵 = ( Base ‘ 𝑅 ) |
4 |
1 2
|
irredneg |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐼 ) → ( 𝑁 ‘ 𝑋 ) ∈ 𝐼 ) |
5 |
4
|
adantlr |
⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑋 ∈ 𝐼 ) → ( 𝑁 ‘ 𝑋 ) ∈ 𝐼 ) |
6 |
|
ringgrp |
⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Grp ) |
7 |
3 2
|
grpinvinv |
⊢ ( ( 𝑅 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) → ( 𝑁 ‘ ( 𝑁 ‘ 𝑋 ) ) = 𝑋 ) |
8 |
6 7
|
sylan |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) → ( 𝑁 ‘ ( 𝑁 ‘ 𝑋 ) ) = 𝑋 ) |
9 |
8
|
adantr |
⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑁 ‘ 𝑋 ) ∈ 𝐼 ) → ( 𝑁 ‘ ( 𝑁 ‘ 𝑋 ) ) = 𝑋 ) |
10 |
1 2
|
irredneg |
⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑁 ‘ 𝑋 ) ∈ 𝐼 ) → ( 𝑁 ‘ ( 𝑁 ‘ 𝑋 ) ) ∈ 𝐼 ) |
11 |
10
|
adantlr |
⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑁 ‘ 𝑋 ) ∈ 𝐼 ) → ( 𝑁 ‘ ( 𝑁 ‘ 𝑋 ) ) ∈ 𝐼 ) |
12 |
9 11
|
eqeltrrd |
⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑁 ‘ 𝑋 ) ∈ 𝐼 ) → 𝑋 ∈ 𝐼 ) |
13 |
5 12
|
impbida |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 ∈ 𝐼 ↔ ( 𝑁 ‘ 𝑋 ) ∈ 𝐼 ) ) |