Step |
Hyp |
Ref |
Expression |
1 |
|
maxidln1.1 |
⊢ 𝐻 = ( 2nd ‘ 𝑅 ) |
2 |
|
maxidln1.2 |
⊢ 𝑈 = ( GId ‘ 𝐻 ) |
3 |
|
eqid |
⊢ ( 1st ‘ 𝑅 ) = ( 1st ‘ 𝑅 ) |
4 |
|
eqid |
⊢ ran ( 1st ‘ 𝑅 ) = ran ( 1st ‘ 𝑅 ) |
5 |
3 4
|
maxidlnr |
⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑀 ∈ ( MaxIdl ‘ 𝑅 ) ) → 𝑀 ≠ ran ( 1st ‘ 𝑅 ) ) |
6 |
|
maxidlidl |
⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑀 ∈ ( MaxIdl ‘ 𝑅 ) ) → 𝑀 ∈ ( Idl ‘ 𝑅 ) ) |
7 |
3 1 4 2
|
1idl |
⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑀 ∈ ( Idl ‘ 𝑅 ) ) → ( 𝑈 ∈ 𝑀 ↔ 𝑀 = ran ( 1st ‘ 𝑅 ) ) ) |
8 |
7
|
necon3bbid |
⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑀 ∈ ( Idl ‘ 𝑅 ) ) → ( ¬ 𝑈 ∈ 𝑀 ↔ 𝑀 ≠ ran ( 1st ‘ 𝑅 ) ) ) |
9 |
6 8
|
syldan |
⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑀 ∈ ( MaxIdl ‘ 𝑅 ) ) → ( ¬ 𝑈 ∈ 𝑀 ↔ 𝑀 ≠ ran ( 1st ‘ 𝑅 ) ) ) |
10 |
5 9
|
mpbird |
⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑀 ∈ ( MaxIdl ‘ 𝑅 ) ) → ¬ 𝑈 ∈ 𝑀 ) |