Theorem prmringnzring

Description: A prime ring is a nonzero ring. (Contributed by AV, 26-Jun-2026)

	Ref	Expression
Assertion	prmringnzring	⊢ ( 𝑅 ∈ PrmRing → 𝑅 ∈ NzRing )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
2		eqid	⊢ ( PrmIdeal ‘ 𝑅 ) = ( PrmIdeal ‘ 𝑅 )
3	1 2	isprmrng	⊢ ( 𝑅 ∈ PrmRing ↔ ( 𝑅 ∈ Ring ∧ { ( 0g ‘ 𝑅 ) } ∈ ( PrmIdeal ‘ 𝑅 ) ) )
4		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
5	4	0ringprmidl	⊢ ( ( 𝑅 ∈ Ring ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) = 1 ) → ( PrmIdeal ‘ 𝑅 ) = ∅ )
6		eleq2	⊢ ( ( PrmIdeal ‘ 𝑅 ) = ∅ → ( { ( 0g ‘ 𝑅 ) } ∈ ( PrmIdeal ‘ 𝑅 ) ↔ { ( 0g ‘ 𝑅 ) } ∈ ∅ ) )
7		noel	⊢ ¬ { ( 0g ‘ 𝑅 ) } ∈ ∅
8	7	pm2.21i	⊢ ( { ( 0g ‘ 𝑅 ) } ∈ ∅ → 𝑅 ∈ NzRing )
9	6 8	biimtrdi	⊢ ( ( PrmIdeal ‘ 𝑅 ) = ∅ → ( { ( 0g ‘ 𝑅 ) } ∈ ( PrmIdeal ‘ 𝑅 ) → 𝑅 ∈ NzRing ) )
10	5 9	syl	⊢ ( ( 𝑅 ∈ Ring ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) = 1 ) → ( { ( 0g ‘ 𝑅 ) } ∈ ( PrmIdeal ‘ 𝑅 ) → 𝑅 ∈ NzRing ) )
11	10	ex	⊢ ( 𝑅 ∈ Ring → ( ( ♯ ‘ ( Base ‘ 𝑅 ) ) = 1 → ( { ( 0g ‘ 𝑅 ) } ∈ ( PrmIdeal ‘ 𝑅 ) → 𝑅 ∈ NzRing ) ) )
12		0ringnnzr	⊢ ( 𝑅 ∈ Ring → ( ( ♯ ‘ ( Base ‘ 𝑅 ) ) = 1 ↔ ¬ 𝑅 ∈ NzRing ) )
13	12	bicomd	⊢ ( 𝑅 ∈ Ring → ( ¬ 𝑅 ∈ NzRing ↔ ( ♯ ‘ ( Base ‘ 𝑅 ) ) = 1 ) )
14	13	con1bid	⊢ ( 𝑅 ∈ Ring → ( ¬ ( ♯ ‘ ( Base ‘ 𝑅 ) ) = 1 ↔ 𝑅 ∈ NzRing ) )
15		ax1w	⊢ ( 𝑅 ∈ Ring → ( 𝑅 ∈ NzRing → ( { ( 0g ‘ 𝑅 ) } ∈ ( PrmIdeal ‘ 𝑅 ) → 𝑅 ∈ NzRing ) ) )
16	14 15	sylbid	⊢ ( 𝑅 ∈ Ring → ( ¬ ( ♯ ‘ ( Base ‘ 𝑅 ) ) = 1 → ( { ( 0g ‘ 𝑅 ) } ∈ ( PrmIdeal ‘ 𝑅 ) → 𝑅 ∈ NzRing ) ) )
17	11 16	pm2.61d	⊢ ( 𝑅 ∈ Ring → ( { ( 0g ‘ 𝑅 ) } ∈ ( PrmIdeal ‘ 𝑅 ) → 𝑅 ∈ NzRing ) )
18	17	imp	⊢ ( ( 𝑅 ∈ Ring ∧ { ( 0g ‘ 𝑅 ) } ∈ ( PrmIdeal ‘ 𝑅 ) ) → 𝑅 ∈ NzRing )
19	3 18	sylbi	⊢ ( 𝑅 ∈ PrmRing → 𝑅 ∈ NzRing )