Theorem 0ringufd

Description: A zero ring is a unique factorization domain. (Contributed by Thierry Arnoux, 18-May-2025)

	Ref	Expression
Hypotheses	0ringufd.1	⊢ 𝐵 = ( Base ‘ 𝑅 )
	0ringufd.2	⊢ ( 𝜑 → 𝑅 ∈ Ring )
	0ringufd.3	⊢ ( 𝜑 → ( ♯ ‘ 𝐵 ) = 1 )
Assertion	0ringufd	⊢ ( 𝜑 → 𝑅 ∈ UFD )

Proof

Step	Hyp	Ref	Expression
1		0ringufd.1	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		0ringufd.2	⊢ ( 𝜑 → 𝑅 ∈ Ring )
3		0ringufd.3	⊢ ( 𝜑 → ( ♯ ‘ 𝐵 ) = 1 )
4	1 2 3	0ringcring	⊢ ( 𝜑 → 𝑅 ∈ CRing )
5		eqid	⊢ ( AbsVal ‘ 𝑅 ) = ( AbsVal ‘ 𝑅 )
6		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
7		eqid	⊢ ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 = ( 0g ‘ 𝑅 ) , 0 , 1 ) ) = ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 = ( 0g ‘ 𝑅 ) , 0 , 1 ) )
8		eqid	⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
9		simprl	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑎 ≠ ( 0g ‘ 𝑅 ) ) ) → 𝑎 ∈ 𝐵 )
10	1	fveq2i	⊢ ( ♯ ‘ 𝐵 ) = ( ♯ ‘ ( Base ‘ 𝑅 ) )
11	10 3	eqtr3id	⊢ ( 𝜑 → ( ♯ ‘ ( Base ‘ 𝑅 ) ) = 1 )
12		0ringnnzr	⊢ ( 𝑅 ∈ Ring → ( ( ♯ ‘ ( Base ‘ 𝑅 ) ) = 1 ↔ ¬ 𝑅 ∈ NzRing ) )
13	12	biimpa	⊢ ( ( 𝑅 ∈ Ring ∧ ( ♯ ‘ ( Base ‘ 𝑅 ) ) = 1 ) → ¬ 𝑅 ∈ NzRing )
14	2 11 13	syl2anc	⊢ ( 𝜑 → ¬ 𝑅 ∈ NzRing )
15	2 14	eldifd	⊢ ( 𝜑 → 𝑅 ∈ ( Ring ∖ NzRing ) )
16	1 6	0ringbas	⊢ ( 𝑅 ∈ ( Ring ∖ NzRing ) → 𝐵 = { ( 0g ‘ 𝑅 ) } )
17	15 16	syl	⊢ ( 𝜑 → 𝐵 = { ( 0g ‘ 𝑅 ) } )
18	17	adantr	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑎 ≠ ( 0g ‘ 𝑅 ) ) ) → 𝐵 = { ( 0g ‘ 𝑅 ) } )
19	9 18	eleqtrd	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑎 ≠ ( 0g ‘ 𝑅 ) ) ) → 𝑎 ∈ { ( 0g ‘ 𝑅 ) } )
20		elsni	⊢ ( 𝑎 ∈ { ( 0g ‘ 𝑅 ) } → 𝑎 = ( 0g ‘ 𝑅 ) )
21	19 20	syl	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑎 ≠ ( 0g ‘ 𝑅 ) ) ) → 𝑎 = ( 0g ‘ 𝑅 ) )
22		simprr	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑎 ≠ ( 0g ‘ 𝑅 ) ) ) → 𝑎 ≠ ( 0g ‘ 𝑅 ) )
23	21 22	pm2.21ddne	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑎 ≠ ( 0g ‘ 𝑅 ) ) ) → ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ≠ ( 0g ‘ 𝑅 ) )
24	23	3adant3	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑎 ≠ ( 0g ‘ 𝑅 ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑏 ≠ ( 0g ‘ 𝑅 ) ) ) → ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ≠ ( 0g ‘ 𝑅 ) )
25	5 1 6 7 8 2 24	abvtrivd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 = ( 0g ‘ 𝑅 ) , 0 , 1 ) ) ∈ ( AbsVal ‘ 𝑅 ) )
26	25	ne0d	⊢ ( 𝜑 → ( AbsVal ‘ 𝑅 ) ≠ ∅ )
27		ral0	⊢ ∀ 𝑖 ∈ ∅ ( 𝑖 ∩ ( RPrime ‘ 𝑅 ) ) ≠ ∅
28		prmidlssidl	⊢ ( 𝑅 ∈ Ring → ( PrmIdeal ‘ 𝑅 ) ⊆ ( LIdeal ‘ 𝑅 ) )
29	2 28	syl	⊢ ( 𝜑 → ( PrmIdeal ‘ 𝑅 ) ⊆ ( LIdeal ‘ 𝑅 ) )
30	1 6	0ringidl	⊢ ( ( 𝑅 ∈ Ring ∧ ( ♯ ‘ 𝐵 ) = 1 ) → ( LIdeal ‘ 𝑅 ) = { { ( 0g ‘ 𝑅 ) } } )
31	2 3 30	syl2anc	⊢ ( 𝜑 → ( LIdeal ‘ 𝑅 ) = { { ( 0g ‘ 𝑅 ) } } )
32	29 31	sseqtrd	⊢ ( 𝜑 → ( PrmIdeal ‘ 𝑅 ) ⊆ { { ( 0g ‘ 𝑅 ) } } )
33		ssdif0	⊢ ( ( PrmIdeal ‘ 𝑅 ) ⊆ { { ( 0g ‘ 𝑅 ) } } ↔ ( ( PrmIdeal ‘ 𝑅 ) ∖ { { ( 0g ‘ 𝑅 ) } } ) = ∅ )
34	32 33	sylib	⊢ ( 𝜑 → ( ( PrmIdeal ‘ 𝑅 ) ∖ { { ( 0g ‘ 𝑅 ) } } ) = ∅ )
35	34	raleqdv	⊢ ( 𝜑 → ( ∀ 𝑖 ∈ ( ( PrmIdeal ‘ 𝑅 ) ∖ { { ( 0g ‘ 𝑅 ) } } ) ( 𝑖 ∩ ( RPrime ‘ 𝑅 ) ) ≠ ∅ ↔ ∀ 𝑖 ∈ ∅ ( 𝑖 ∩ ( RPrime ‘ 𝑅 ) ) ≠ ∅ ) )
36	27 35	mpbiri	⊢ ( 𝜑 → ∀ 𝑖 ∈ ( ( PrmIdeal ‘ 𝑅 ) ∖ { { ( 0g ‘ 𝑅 ) } } ) ( 𝑖 ∩ ( RPrime ‘ 𝑅 ) ) ≠ ∅ )
37	26 36	jca	⊢ ( 𝜑 → ( ( AbsVal ‘ 𝑅 ) ≠ ∅ ∧ ∀ 𝑖 ∈ ( ( PrmIdeal ‘ 𝑅 ) ∖ { { ( 0g ‘ 𝑅 ) } } ) ( 𝑖 ∩ ( RPrime ‘ 𝑅 ) ) ≠ ∅ ) )
38		eqid	⊢ ( PrmIdeal ‘ 𝑅 ) = ( PrmIdeal ‘ 𝑅 )
39		eqid	⊢ ( RPrime ‘ 𝑅 ) = ( RPrime ‘ 𝑅 )
40	5 38 39 6	isufd	⊢ ( 𝑅 ∈ UFD ↔ ( 𝑅 ∈ CRing ∧ ( ( AbsVal ‘ 𝑅 ) ≠ ∅ ∧ ∀ 𝑖 ∈ ( ( PrmIdeal ‘ 𝑅 ) ∖ { { ( 0g ‘ 𝑅 ) } } ) ( 𝑖 ∩ ( RPrime ‘ 𝑅 ) ) ≠ ∅ ) ) )
41	4 37 40	sylanbrc	⊢ ( 𝜑 → 𝑅 ∈ UFD )