Step |
Hyp |
Ref |
Expression |
1 |
|
nzrring |
⊢ ( 𝑅 ∈ NzRing → 𝑅 ∈ Ring ) |
2 |
|
eqid |
⊢ ( LIdeal ‘ 𝑅 ) = ( LIdeal ‘ 𝑅 ) |
3 |
|
eqid |
⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 ) |
4 |
2 3
|
lidl0 |
⊢ ( 𝑅 ∈ Ring → { ( 0g ‘ 𝑅 ) } ∈ ( LIdeal ‘ 𝑅 ) ) |
5 |
1 4
|
syl |
⊢ ( 𝑅 ∈ NzRing → { ( 0g ‘ 𝑅 ) } ∈ ( LIdeal ‘ 𝑅 ) ) |
6 |
|
fvex |
⊢ ( 0g ‘ 𝑅 ) ∈ V |
7 |
|
hashsng |
⊢ ( ( 0g ‘ 𝑅 ) ∈ V → ( ♯ ‘ { ( 0g ‘ 𝑅 ) } ) = 1 ) |
8 |
6 7
|
ax-mp |
⊢ ( ♯ ‘ { ( 0g ‘ 𝑅 ) } ) = 1 |
9 |
|
simpr |
⊢ ( ( 𝑅 ∈ NzRing ∧ { ( 0g ‘ 𝑅 ) } = ( Base ‘ 𝑅 ) ) → { ( 0g ‘ 𝑅 ) } = ( Base ‘ 𝑅 ) ) |
10 |
9
|
fveq2d |
⊢ ( ( 𝑅 ∈ NzRing ∧ { ( 0g ‘ 𝑅 ) } = ( Base ‘ 𝑅 ) ) → ( ♯ ‘ { ( 0g ‘ 𝑅 ) } ) = ( ♯ ‘ ( Base ‘ 𝑅 ) ) ) |
11 |
8 10
|
eqtr3id |
⊢ ( ( 𝑅 ∈ NzRing ∧ { ( 0g ‘ 𝑅 ) } = ( Base ‘ 𝑅 ) ) → 1 = ( ♯ ‘ ( Base ‘ 𝑅 ) ) ) |
12 |
|
1red |
⊢ ( ( 𝑅 ∈ NzRing ∧ { ( 0g ‘ 𝑅 ) } = ( Base ‘ 𝑅 ) ) → 1 ∈ ℝ ) |
13 |
|
eqid |
⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 ) |
14 |
13
|
isnzr2hash |
⊢ ( 𝑅 ∈ NzRing ↔ ( 𝑅 ∈ Ring ∧ 1 < ( ♯ ‘ ( Base ‘ 𝑅 ) ) ) ) |
15 |
14
|
simprbi |
⊢ ( 𝑅 ∈ NzRing → 1 < ( ♯ ‘ ( Base ‘ 𝑅 ) ) ) |
16 |
15
|
adantr |
⊢ ( ( 𝑅 ∈ NzRing ∧ { ( 0g ‘ 𝑅 ) } = ( Base ‘ 𝑅 ) ) → 1 < ( ♯ ‘ ( Base ‘ 𝑅 ) ) ) |
17 |
12 16
|
ltned |
⊢ ( ( 𝑅 ∈ NzRing ∧ { ( 0g ‘ 𝑅 ) } = ( Base ‘ 𝑅 ) ) → 1 ≠ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ) |
18 |
17
|
neneqd |
⊢ ( ( 𝑅 ∈ NzRing ∧ { ( 0g ‘ 𝑅 ) } = ( Base ‘ 𝑅 ) ) → ¬ 1 = ( ♯ ‘ ( Base ‘ 𝑅 ) ) ) |
19 |
11 18
|
pm2.65da |
⊢ ( 𝑅 ∈ NzRing → ¬ { ( 0g ‘ 𝑅 ) } = ( Base ‘ 𝑅 ) ) |
20 |
19
|
neqned |
⊢ ( 𝑅 ∈ NzRing → { ( 0g ‘ 𝑅 ) } ≠ ( Base ‘ 𝑅 ) ) |
21 |
13
|
ssmxidl |
⊢ ( ( 𝑅 ∈ Ring ∧ { ( 0g ‘ 𝑅 ) } ∈ ( LIdeal ‘ 𝑅 ) ∧ { ( 0g ‘ 𝑅 ) } ≠ ( Base ‘ 𝑅 ) ) → ∃ 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) { ( 0g ‘ 𝑅 ) } ⊆ 𝑚 ) |
22 |
1 5 20 21
|
syl3anc |
⊢ ( 𝑅 ∈ NzRing → ∃ 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) { ( 0g ‘ 𝑅 ) } ⊆ 𝑚 ) |
23 |
|
df-rex |
⊢ ( ∃ 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) { ( 0g ‘ 𝑅 ) } ⊆ 𝑚 ↔ ∃ 𝑚 ( 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) ∧ { ( 0g ‘ 𝑅 ) } ⊆ 𝑚 ) ) |
24 |
|
exsimpl |
⊢ ( ∃ 𝑚 ( 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) ∧ { ( 0g ‘ 𝑅 ) } ⊆ 𝑚 ) → ∃ 𝑚 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) ) |
25 |
23 24
|
sylbi |
⊢ ( ∃ 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) { ( 0g ‘ 𝑅 ) } ⊆ 𝑚 → ∃ 𝑚 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) ) |
26 |
22 25
|
syl |
⊢ ( 𝑅 ∈ NzRing → ∃ 𝑚 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) ) |