Step |
Hyp |
Ref |
Expression |
1 |
|
isprrng.1 |
⊢ 𝐺 = ( 1st ‘ 𝑅 ) |
2 |
|
isprrng.2 |
⊢ 𝑍 = ( GId ‘ 𝐺 ) |
3 |
|
fveq2 |
⊢ ( 𝑟 = 𝑅 → ( 1st ‘ 𝑟 ) = ( 1st ‘ 𝑅 ) ) |
4 |
3 1
|
eqtr4di |
⊢ ( 𝑟 = 𝑅 → ( 1st ‘ 𝑟 ) = 𝐺 ) |
5 |
4
|
fveq2d |
⊢ ( 𝑟 = 𝑅 → ( GId ‘ ( 1st ‘ 𝑟 ) ) = ( GId ‘ 𝐺 ) ) |
6 |
5 2
|
eqtr4di |
⊢ ( 𝑟 = 𝑅 → ( GId ‘ ( 1st ‘ 𝑟 ) ) = 𝑍 ) |
7 |
6
|
sneqd |
⊢ ( 𝑟 = 𝑅 → { ( GId ‘ ( 1st ‘ 𝑟 ) ) } = { 𝑍 } ) |
8 |
|
fveq2 |
⊢ ( 𝑟 = 𝑅 → ( PrIdl ‘ 𝑟 ) = ( PrIdl ‘ 𝑅 ) ) |
9 |
7 8
|
eleq12d |
⊢ ( 𝑟 = 𝑅 → ( { ( GId ‘ ( 1st ‘ 𝑟 ) ) } ∈ ( PrIdl ‘ 𝑟 ) ↔ { 𝑍 } ∈ ( PrIdl ‘ 𝑅 ) ) ) |
10 |
|
df-prrngo |
⊢ PrRing = { 𝑟 ∈ RingOps ∣ { ( GId ‘ ( 1st ‘ 𝑟 ) ) } ∈ ( PrIdl ‘ 𝑟 ) } |
11 |
9 10
|
elrab2 |
⊢ ( 𝑅 ∈ PrRing ↔ ( 𝑅 ∈ RingOps ∧ { 𝑍 } ∈ ( PrIdl ‘ 𝑅 ) ) ) |