Theorem 0ringufd

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

	Ref	Expression
Hypotheses	0ringufd.1	$$⊢B={\mathrm{Base}}_R$$
	0ringufd.2	$$⊢\phi \to R\in \mathrm{Ring}$$
	0ringufd.3	$$⊢\phi \to \left|B\right|=1$$
Assertion	0ringufd	Could not format assertion : No typesetting found for |- ( ph -> R e. UFD ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		0ringufd.1	$$⊢B={\mathrm{Base}}_R$$
2		0ringufd.2	$$⊢\phi \to R\in \mathrm{Ring}$$
3		0ringufd.3	$$⊢\phi \to \left|B\right|=1$$
4	1 2 3	0ringcring	$$⊢\phi \to R\in \mathrm{CRing}$$
5		eqid	$$⊢\mathrm{AbsVal}\left(R\right)=\mathrm{AbsVal}\left(R\right)$$
6		eqid	$$⊢0_R=0_R$$
7		eqid	$$⊢\left(x\in B⟼if\left(x=0_R,0,1\right)\right)=\left(x\in B⟼if\left(x=0_R,0,1\right)\right)$$
8		eqid	$$⊢{\cdot }_R={\cdot }_R$$
9		simprl	$$⊢\left(\phi \wedge \left(a\in B\wedge a\ne 0_R\right)\right)\to a\in B$$
10	1	fveq2i	$$⊢\left|B\right|=\left|{\mathrm{Base}}_R\right|$$
11	10 3	eqtr3id	$$⊢\phi \to \left|{\mathrm{Base}}_R\right|=1$$
12		0ringnnzr	$$⊢R\in \mathrm{Ring}\to \left(\left|{\mathrm{Base}}_R\right|=1\leftrightarrow \neg R\in \mathrm{NzRing}\right)$$
13	12	biimpa	$$⊢\left(R\in \mathrm{Ring}\wedge \left|{\mathrm{Base}}_R\right|=1\right)\to \neg R\in \mathrm{NzRing}$$
14	2 11 13	syl2anc	$$⊢\phi \to \neg R\in \mathrm{NzRing}$$
15	2 14	eldifd	$$⊢\phi \to R\in \left(\mathrm{Ring}\setminus \mathrm{NzRing}\right)$$
16	1 6	0ringbas	$$⊢R\in \left(\mathrm{Ring}\setminus \mathrm{NzRing}\right)\to B=\left\{0_R\right\}$$
17	15 16	syl	$$⊢\phi \to B=\left\{0_R\right\}$$
18	17	adantr	$$⊢\left(\phi \wedge \left(a\in B\wedge a\ne 0_R\right)\right)\to B=\left\{0_R\right\}$$
19	9 18	eleqtrd	$$⊢\left(\phi \wedge \left(a\in B\wedge a\ne 0_R\right)\right)\to a\in \left\{0_R\right\}$$
20		elsni	$$⊢a\in \left\{0_R\right\}\to a=0_R$$
21	19 20	syl	$$⊢\left(\phi \wedge \left(a\in B\wedge a\ne 0_R\right)\right)\to a=0_R$$
22		simprr	$$⊢\left(\phi \wedge \left(a\in B\wedge a\ne 0_R\right)\right)\to a\ne 0_R$$
23	21 22	pm2.21ddne	$$⊢\left(\phi \wedge \left(a\in B\wedge a\ne 0_R\right)\right)\to a{\cdot }_{R}b\ne 0_R$$
24	23	3adant3	$$⊢\left(\phi \wedge \left(a\in B\wedge a\ne 0_R\right)\wedge \left(b\in B\wedge b\ne 0_R\right)\right)\to a{\cdot }_{R}b\ne 0_R$$
25	5 1 6 7 8 2 24	abvtrivd	$$⊢\phi \to \left(x\in B⟼if\left(x=0_R,0,1\right)\right)\in \mathrm{AbsVal}\left(R\right)$$
26	25	ne0d	$$⊢\phi \to \mathrm{AbsVal}\left(R\right)\ne \varnothing$$
27		ral0	$$⊢\forall i\in \varnothing i\cap \mathrm{RPrime}\left(R\right)\ne \varnothing$$
28		prmidlssidl	Could not format ( R e. Ring -> ( PrmIdeal ` R ) C_ ( LIdeal ` R ) ) : No typesetting found for |- ( R e. Ring -> ( PrmIdeal ` R ) C_ ( LIdeal ` R ) ) with typecode |-
29	2 28	syl	Could not format ( ph -> ( PrmIdeal ` R ) C_ ( LIdeal ` R ) ) : No typesetting found for |- ( ph -> ( PrmIdeal ` R ) C_ ( LIdeal ` R ) ) with typecode |-
30	1 6	0ringidl	$$⊢\left(R\in \mathrm{Ring}\wedge \left|B\right|=1\right)\to \mathrm{LIdeal}\left(R\right)=\left\{\left\{0_R\right\}\right\}$$
31	2 3 30	syl2anc	$$⊢\phi \to \mathrm{LIdeal}\left(R\right)=\left\{\left\{0_R\right\}\right\}$$
32	29 31	sseqtrd	Could not format ( ph -> ( PrmIdeal ` R ) C_ { { ( 0g ` R ) } } ) : No typesetting found for |- ( ph -> ( PrmIdeal ` R ) C_ { { ( 0g ` R ) } } ) with typecode |-
33		ssdif0	Could not format ( ( PrmIdeal ` R ) C_ { { ( 0g ` R ) } } <-> ( ( PrmIdeal ` R ) \ { { ( 0g ` R ) } } ) = (/) ) : No typesetting found for |- ( ( PrmIdeal ` R ) C_ { { ( 0g ` R ) } } <-> ( ( PrmIdeal ` R ) \ { { ( 0g ` R ) } } ) = (/) ) with typecode |-
34	32 33	sylib	Could not format ( ph -> ( ( PrmIdeal ` R ) \ { { ( 0g ` R ) } } ) = (/) ) : No typesetting found for |- ( ph -> ( ( PrmIdeal ` R ) \ { { ( 0g ` R ) } } ) = (/) ) with typecode |-
35	34	raleqdv	Could not format ( ph -> ( A. i e. ( ( PrmIdeal ` R ) \ { { ( 0g ` R ) } } ) ( i i^i ( RPrime ` R ) ) =/= (/) <-> A. i e. (/) ( i i^i ( RPrime ` R ) ) =/= (/) ) ) : No typesetting found for |- ( ph -> ( A. i e. ( ( PrmIdeal ` R ) \ { { ( 0g ` R ) } } ) ( i i^i ( RPrime ` R ) ) =/= (/) <-> A. i e. (/) ( i i^i ( RPrime ` R ) ) =/= (/) ) ) with typecode |-
36	27 35	mpbiri	Could not format ( ph -> A. i e. ( ( PrmIdeal ` R ) \ { { ( 0g ` R ) } } ) ( i i^i ( RPrime ` R ) ) =/= (/) ) : No typesetting found for |- ( ph -> A. i e. ( ( PrmIdeal ` R ) \ { { ( 0g ` R ) } } ) ( i i^i ( RPrime ` R ) ) =/= (/) ) with typecode |-
37	26 36	jca	Could not format ( ph -> ( ( AbsVal ` R ) =/= (/) /\ A. i e. ( ( PrmIdeal ` R ) \ { { ( 0g ` R ) } } ) ( i i^i ( RPrime ` R ) ) =/= (/) ) ) : No typesetting found for |- ( ph -> ( ( AbsVal ` R ) =/= (/) /\ A. i e. ( ( PrmIdeal ` R ) \ { { ( 0g ` R ) } } ) ( i i^i ( RPrime ` R ) ) =/= (/) ) ) with typecode |-
38		eqid	Could not format ( PrmIdeal ` R ) = ( PrmIdeal ` R ) : No typesetting found for |- ( PrmIdeal ` R ) = ( PrmIdeal ` R ) with typecode |-
39		eqid	$$⊢\mathrm{RPrime}\left(R\right)=\mathrm{RPrime}\left(R\right)$$
40	5 38 39 6	isufd	Could not format ( R e. UFD <-> ( R e. CRing /\ ( ( AbsVal ` R ) =/= (/) /\ A. i e. ( ( PrmIdeal ` R ) \ { { ( 0g ` R ) } } ) ( i i^i ( RPrime ` R ) ) =/= (/) ) ) ) : No typesetting found for |- ( R e. UFD <-> ( R e. CRing /\ ( ( AbsVal ` R ) =/= (/) /\ A. i e. ( ( PrmIdeal ` R ) \ { { ( 0g ` R ) } } ) ( i i^i ( RPrime ` R ) ) =/= (/) ) ) ) with typecode |-
41	4 37 40	sylanbrc	Could not format ( ph -> R e. UFD ) : No typesetting found for |- ( ph -> R e. UFD ) with typecode |-