Theorem mxidlirred

Description: In a principal ideal domain, maximal ideals are exactly the ideals generated by irreducible elements. (Contributed by Thierry Arnoux, 22-Mar-2025)

	Ref	Expression
Hypotheses	mxidlirred.b	$$⊢B={\mathrm{Base}}_R$$
	mxidlirred.k	$$⊢K=\mathrm{RSpan}\left(R\right)$$
	mxidlirred.0	$$⊢\underset{\dot{}}{0}=0_R$$
	mxidlirred.m	$$⊢M=K\left(\left\{X\right\}\right)$$
	mxidlirred.r	$$⊢\phi \to R\in \mathrm{PID}$$
	mxidlirred.x	$$⊢\phi \to X\in B$$
	mxidlirred.y	$$⊢\phi \to X\ne \underset{\dot{}}{0}$$
	mxidlirred.1	$$⊢\phi \to M\in \mathrm{LIdeal}\left(R\right)$$
Assertion	mxidlirred	Could not format assertion : No typesetting found for |- ( ph -> ( M e. ( MaxIdeal ` R ) <-> X e. ( Irred ` R ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		mxidlirred.b	$$⊢B={\mathrm{Base}}_R$$
2		mxidlirred.k	$$⊢K=\mathrm{RSpan}\left(R\right)$$
3		mxidlirred.0	$$⊢\underset{\dot{}}{0}=0_R$$
4		mxidlirred.m	$$⊢M=K\left(\left\{X\right\}\right)$$
5		mxidlirred.r	$$⊢\phi \to R\in \mathrm{PID}$$
6		mxidlirred.x	$$⊢\phi \to X\in B$$
7		mxidlirred.y	$$⊢\phi \to X\ne \underset{\dot{}}{0}$$
8		mxidlirred.1	$$⊢\phi \to M\in \mathrm{LIdeal}\left(R\right)$$
9		df-pid	$$⊢\mathrm{PID}=\mathrm{IDomn}\cap \mathrm{LPIR}$$
10	5 9	eleqtrdi	$$⊢\phi \to R\in \left(\mathrm{IDomn}\cap \mathrm{LPIR}\right)$$
11	10	elin1d	$$⊢\phi \to R\in \mathrm{IDomn}$$
12	11	adantr	Could not format ( ( ph /\ M e. ( MaxIdeal ` R ) ) -> R e. IDomn ) : No typesetting found for |- ( ( ph /\ M e. ( MaxIdeal ` R ) ) -> R e. IDomn ) with typecode |-
13	6	adantr	Could not format ( ( ph /\ M e. ( MaxIdeal ` R ) ) -> X e. B ) : No typesetting found for |- ( ( ph /\ M e. ( MaxIdeal ` R ) ) -> X e. B ) with typecode |-
14	7	adantr	Could not format ( ( ph /\ M e. ( MaxIdeal ` R ) ) -> X =/= .0. ) : No typesetting found for |- ( ( ph /\ M e. ( MaxIdeal ` R ) ) -> X =/= .0. ) with typecode |-
15		simpr	Could not format ( ( ph /\ M e. ( MaxIdeal ` R ) ) -> M e. ( MaxIdeal ` R ) ) : No typesetting found for |- ( ( ph /\ M e. ( MaxIdeal ` R ) ) -> M e. ( MaxIdeal ` R ) ) with typecode |-
16	1 2 3 4 12 13 14 15	mxidlirredi	Could not format ( ( ph /\ M e. ( MaxIdeal ` R ) ) -> X e. ( Irred ` R ) ) : No typesetting found for |- ( ( ph /\ M e. ( MaxIdeal ` R ) ) -> X e. ( Irred ` R ) ) with typecode |-
17		eqid	$$⊢{\parallel }_r\left(R\right)={\parallel }_r\left(R\right)$$
18		simplr	Could not format ( ( ( ( ( ( ( ph /\ X e. ( Irred ` R ) ) /\ -. M e. ( MaxIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ -. ( M C_ k -> ( k = M \/ k = B ) ) ) /\ x e. B ) /\ k = ( K ` { x } ) ) -> x e. B ) : No typesetting found for |- ( ( ( ( ( ( ( ph /\ X e. ( Irred ` R ) ) /\ -. M e. ( MaxIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ -. ( M C_ k -> ( k = M \/ k = B ) ) ) /\ x e. B ) /\ k = ( K ` { x } ) ) -> x e. B ) with typecode |-
19	18	ad2antrr	Could not format ( ( ( ( ( ( ( ( ( ph /\ X e. ( Irred ` R ) ) /\ -. M e. ( MaxIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ -. ( M C_ k -> ( k = M \/ k = B ) ) ) /\ x e. B ) /\ k = ( K ` { x } ) ) /\ t e. B ) /\ X = ( t ( .r ` R ) x ) ) -> x e. B ) : No typesetting found for |- ( ( ( ( ( ( ( ( ( ph /\ X e. ( Irred ` R ) ) /\ -. M e. ( MaxIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ -. ( M C_ k -> ( k = M \/ k = B ) ) ) /\ x e. B ) /\ k = ( K ` { x } ) ) /\ t e. B ) /\ X = ( t ( .r ` R ) x ) ) -> x e. B ) with typecode |-
20	6	ad8antr	Could not format ( ( ( ( ( ( ( ( ( ph /\ X e. ( Irred ` R ) ) /\ -. M e. ( MaxIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ -. ( M C_ k -> ( k = M \/ k = B ) ) ) /\ x e. B ) /\ k = ( K ` { x } ) ) /\ t e. B ) /\ X = ( t ( .r ` R ) x ) ) -> X e. B ) : No typesetting found for |- ( ( ( ( ( ( ( ( ( ph /\ X e. ( Irred ` R ) ) /\ -. M e. ( MaxIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ -. ( M C_ k -> ( k = M \/ k = B ) ) ) /\ x e. B ) /\ k = ( K ` { x } ) ) /\ t e. B ) /\ X = ( t ( .r ` R ) x ) ) -> X e. B ) with typecode |-
21		eqid	$$⊢\mathrm{Unit}\left(R\right)=\mathrm{Unit}\left(R\right)$$
22		eqid	$$⊢{\cdot }_R={\cdot }_R$$
23	11	idomringd	$$⊢\phi \to R\in \mathrm{Ring}$$
24	23	ad4antr	Could not format ( ( ( ( ( ph /\ X e. ( Irred ` R ) ) /\ -. M e. ( MaxIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ -. ( M C_ k -> ( k = M \/ k = B ) ) ) -> R e. Ring ) : No typesetting found for |- ( ( ( ( ( ph /\ X e. ( Irred ` R ) ) /\ -. M e. ( MaxIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ -. ( M C_ k -> ( k = M \/ k = B ) ) ) -> R e. Ring ) with typecode |-
25	24	ad2antrr	Could not format ( ( ( ( ( ( ( ph /\ X e. ( Irred ` R ) ) /\ -. M e. ( MaxIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ -. ( M C_ k -> ( k = M \/ k = B ) ) ) /\ x e. B ) /\ k = ( K ` { x } ) ) -> R e. Ring ) : No typesetting found for |- ( ( ( ( ( ( ( ph /\ X e. ( Irred ` R ) ) /\ -. M e. ( MaxIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ -. ( M C_ k -> ( k = M \/ k = B ) ) ) /\ x e. B ) /\ k = ( K ` { x } ) ) -> R e. Ring ) with typecode |-
26	25	ad2antrr	Could not format ( ( ( ( ( ( ( ( ( ph /\ X e. ( Irred ` R ) ) /\ -. M e. ( MaxIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ -. ( M C_ k -> ( k = M \/ k = B ) ) ) /\ x e. B ) /\ k = ( K ` { x } ) ) /\ t e. B ) /\ X = ( t ( .r ` R ) x ) ) -> R e. Ring ) : No typesetting found for |- ( ( ( ( ( ( ( ( ( ph /\ X e. ( Irred ` R ) ) /\ -. M e. ( MaxIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ -. ( M C_ k -> ( k = M \/ k = B ) ) ) /\ x e. B ) /\ k = ( K ` { x } ) ) /\ t e. B ) /\ X = ( t ( .r ` R ) x ) ) -> R e. Ring ) with typecode |-
27		simplr	Could not format ( ( ( ( ( ( ( ( ( ph /\ X e. ( Irred ` R ) ) /\ -. M e. ( MaxIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ -. ( M C_ k -> ( k = M \/ k = B ) ) ) /\ x e. B ) /\ k = ( K ` { x } ) ) /\ t e. B ) /\ X = ( t ( .r ` R ) x ) ) -> t e. B ) : No typesetting found for |- ( ( ( ( ( ( ( ( ( ph /\ X e. ( Irred ` R ) ) /\ -. M e. ( MaxIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ -. ( M C_ k -> ( k = M \/ k = B ) ) ) /\ x e. B ) /\ k = ( K ` { x } ) ) /\ t e. B ) /\ X = ( t ( .r ` R ) x ) ) -> t e. B ) with typecode |-
28		simpr	Could not format ( ( ( ( ( ( ( ( ( ph /\ X e. ( Irred ` R ) ) /\ -. M e. ( MaxIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ -. ( M C_ k -> ( k = M \/ k = B ) ) ) /\ x e. B ) /\ k = ( K ` { x } ) ) /\ t e. B ) /\ X = ( t ( .r ` R ) x ) ) -> X = ( t ( .r ` R ) x ) ) : No typesetting found for |- ( ( ( ( ( ( ( ( ( ph /\ X e. ( Irred ` R ) ) /\ -. M e. ( MaxIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ -. ( M C_ k -> ( k = M \/ k = B ) ) ) /\ x e. B ) /\ k = ( K ` { x } ) ) /\ t e. B ) /\ X = ( t ( .r ` R ) x ) ) -> X = ( t ( .r ` R ) x ) ) with typecode |-
29		simp-8r	Could not format ( ( ( ( ( ( ( ( ( ph /\ X e. ( Irred ` R ) ) /\ -. M e. ( MaxIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ -. ( M C_ k -> ( k = M \/ k = B ) ) ) /\ x e. B ) /\ k = ( K ` { x } ) ) /\ t e. B ) /\ X = ( t ( .r ` R ) x ) ) -> X e. ( Irred ` R ) ) : No typesetting found for |- ( ( ( ( ( ( ( ( ( ph /\ X e. ( Irred ` R ) ) /\ -. M e. ( MaxIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ -. ( M C_ k -> ( k = M \/ k = B ) ) ) /\ x e. B ) /\ k = ( K ` { x } ) ) /\ t e. B ) /\ X = ( t ( .r ` R ) x ) ) -> X e. ( Irred ` R ) ) with typecode |-
30	28 29	eqeltrrd	Could not format ( ( ( ( ( ( ( ( ( ph /\ X e. ( Irred ` R ) ) /\ -. M e. ( MaxIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ -. ( M C_ k -> ( k = M \/ k = B ) ) ) /\ x e. B ) /\ k = ( K ` { x } ) ) /\ t e. B ) /\ X = ( t ( .r ` R ) x ) ) -> ( t ( .r ` R ) x ) e. ( Irred ` R ) ) : No typesetting found for |- ( ( ( ( ( ( ( ( ( ph /\ X e. ( Irred ` R ) ) /\ -. M e. ( MaxIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ -. ( M C_ k -> ( k = M \/ k = B ) ) ) /\ x e. B ) /\ k = ( K ` { x } ) ) /\ t e. B ) /\ X = ( t ( .r ` R ) x ) ) -> ( t ( .r ` R ) x ) e. ( Irred ` R ) ) with typecode |-
31		eqid	$$⊢\mathrm{Irred}\left(R\right)=\mathrm{Irred}\left(R\right)$$
32	31 1 21 22	irredmul	$$⊢\left(t\in B\wedge x\in B\wedge t{\cdot }_{R}x\in \mathrm{Irred}\left(R\right)\right)\to \left(t\in \mathrm{Unit}\left(R\right)\vee x\in \mathrm{Unit}\left(R\right)\right)$$
33	27 19 30 32	syl3anc	Could not format ( ( ( ( ( ( ( ( ( ph /\ X e. ( Irred ` R ) ) /\ -. M e. ( MaxIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ -. ( M C_ k -> ( k = M \/ k = B ) ) ) /\ x e. B ) /\ k = ( K ` { x } ) ) /\ t e. B ) /\ X = ( t ( .r ` R ) x ) ) -> ( t e. ( Unit ` R ) \/ x e. ( Unit ` R ) ) ) : No typesetting found for |- ( ( ( ( ( ( ( ( ( ph /\ X e. ( Irred ` R ) ) /\ -. M e. ( MaxIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ -. ( M C_ k -> ( k = M \/ k = B ) ) ) /\ x e. B ) /\ k = ( K ` { x } ) ) /\ t e. B ) /\ X = ( t ( .r ` R ) x ) ) -> ( t e. ( Unit ` R ) \/ x e. ( Unit ` R ) ) ) with typecode |-
34		simpr	Could not format ( ( ( ( ( ( ( ph /\ X e. ( Irred ` R ) ) /\ -. M e. ( MaxIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ -. ( M C_ k -> ( k = M \/ k = B ) ) ) /\ x e. B ) /\ k = ( K ` { x } ) ) -> k = ( K ` { x } ) ) : No typesetting found for |- ( ( ( ( ( ( ( ph /\ X e. ( Irred ` R ) ) /\ -. M e. ( MaxIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ -. ( M C_ k -> ( k = M \/ k = B ) ) ) /\ x e. B ) /\ k = ( K ` { x } ) ) -> k = ( K ` { x } ) ) with typecode |-
35	34	ad2antrr	Could not format ( ( ( ( ( ( ( ( ( ph /\ X e. ( Irred ` R ) ) /\ -. M e. ( MaxIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ -. ( M C_ k -> ( k = M \/ k = B ) ) ) /\ x e. B ) /\ k = ( K ` { x } ) ) /\ t e. B ) /\ X = ( t ( .r ` R ) x ) ) -> k = ( K ` { x } ) ) : No typesetting found for |- ( ( ( ( ( ( ( ( ( ph /\ X e. ( Irred ` R ) ) /\ -. M e. ( MaxIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ -. ( M C_ k -> ( k = M \/ k = B ) ) ) /\ x e. B ) /\ k = ( K ` { x } ) ) /\ t e. B ) /\ X = ( t ( .r ` R ) x ) ) -> k = ( K ` { x } ) ) with typecode |-
36		simpr	Could not format ( ( ( ( ( ph /\ X e. ( Irred ` R ) ) /\ -. M e. ( MaxIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ -. ( M C_ k -> ( k = M \/ k = B ) ) ) -> -. ( M C_ k -> ( k = M \/ k = B ) ) ) : No typesetting found for |- ( ( ( ( ( ph /\ X e. ( Irred ` R ) ) /\ -. M e. ( MaxIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ -. ( M C_ k -> ( k = M \/ k = B ) ) ) -> -. ( M C_ k -> ( k = M \/ k = B ) ) ) with typecode |-
37		annim	$$⊢\left(M\subseteq k\wedge \neg \left(k=M\vee k=B\right)\right)\leftrightarrow \neg \left(M\subseteq k\to \left(k=M\vee k=B\right)\right)$$
38	36 37	sylibr	Could not format ( ( ( ( ( ph /\ X e. ( Irred ` R ) ) /\ -. M e. ( MaxIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ -. ( M C_ k -> ( k = M \/ k = B ) ) ) -> ( M C_ k /\ -. ( k = M \/ k = B ) ) ) : No typesetting found for |- ( ( ( ( ( ph /\ X e. ( Irred ` R ) ) /\ -. M e. ( MaxIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ -. ( M C_ k -> ( k = M \/ k = B ) ) ) -> ( M C_ k /\ -. ( k = M \/ k = B ) ) ) with typecode |-
39	38	simprd	Could not format ( ( ( ( ( ph /\ X e. ( Irred ` R ) ) /\ -. M e. ( MaxIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ -. ( M C_ k -> ( k = M \/ k = B ) ) ) -> -. ( k = M \/ k = B ) ) : No typesetting found for |- ( ( ( ( ( ph /\ X e. ( Irred ` R ) ) /\ -. M e. ( MaxIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ -. ( M C_ k -> ( k = M \/ k = B ) ) ) -> -. ( k = M \/ k = B ) ) with typecode |-
40		ioran	$$⊢\neg \left(k=M\vee k=B\right)\leftrightarrow \left(\neg k=M\wedge \neg k=B\right)$$
41	39 40	sylib	Could not format ( ( ( ( ( ph /\ X e. ( Irred ` R ) ) /\ -. M e. ( MaxIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ -. ( M C_ k -> ( k = M \/ k = B ) ) ) -> ( -. k = M /\ -. k = B ) ) : No typesetting found for |- ( ( ( ( ( ph /\ X e. ( Irred ` R ) ) /\ -. M e. ( MaxIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ -. ( M C_ k -> ( k = M \/ k = B ) ) ) -> ( -. k = M /\ -. k = B ) ) with typecode |-
42	41	simprd	Could not format ( ( ( ( ( ph /\ X e. ( Irred ` R ) ) /\ -. M e. ( MaxIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ -. ( M C_ k -> ( k = M \/ k = B ) ) ) -> -. k = B ) : No typesetting found for |- ( ( ( ( ( ph /\ X e. ( Irred ` R ) ) /\ -. M e. ( MaxIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ -. ( M C_ k -> ( k = M \/ k = B ) ) ) -> -. k = B ) with typecode |-
43	42	neqned	Could not format ( ( ( ( ( ph /\ X e. ( Irred ` R ) ) /\ -. M e. ( MaxIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ -. ( M C_ k -> ( k = M \/ k = B ) ) ) -> k =/= B ) : No typesetting found for |- ( ( ( ( ( ph /\ X e. ( Irred ` R ) ) /\ -. M e. ( MaxIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ -. ( M C_ k -> ( k = M \/ k = B ) ) ) -> k =/= B ) with typecode |-
44	43	ad4antr	Could not format ( ( ( ( ( ( ( ( ( ph /\ X e. ( Irred ` R ) ) /\ -. M e. ( MaxIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ -. ( M C_ k -> ( k = M \/ k = B ) ) ) /\ x e. B ) /\ k = ( K ` { x } ) ) /\ t e. B ) /\ X = ( t ( .r ` R ) x ) ) -> k =/= B ) : No typesetting found for |- ( ( ( ( ( ( ( ( ( ph /\ X e. ( Irred ` R ) ) /\ -. M e. ( MaxIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ -. ( M C_ k -> ( k = M \/ k = B ) ) ) /\ x e. B ) /\ k = ( K ` { x } ) ) /\ t e. B ) /\ X = ( t ( .r ` R ) x ) ) -> k =/= B ) with typecode |-
45	35 44	eqnetrrd	Could not format ( ( ( ( ( ( ( ( ( ph /\ X e. ( Irred ` R ) ) /\ -. M e. ( MaxIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ -. ( M C_ k -> ( k = M \/ k = B ) ) ) /\ x e. B ) /\ k = ( K ` { x } ) ) /\ t e. B ) /\ X = ( t ( .r ` R ) x ) ) -> ( K ` { x } ) =/= B ) : No typesetting found for |- ( ( ( ( ( ( ( ( ( ph /\ X e. ( Irred ` R ) ) /\ -. M e. ( MaxIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ -. ( M C_ k -> ( k = M \/ k = B ) ) ) /\ x e. B ) /\ k = ( K ` { x } ) ) /\ t e. B ) /\ X = ( t ( .r ` R ) x ) ) -> ( K ` { x } ) =/= B ) with typecode |-
46	45	neneqd	Could not format ( ( ( ( ( ( ( ( ( ph /\ X e. ( Irred ` R ) ) /\ -. M e. ( MaxIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ -. ( M C_ k -> ( k = M \/ k = B ) ) ) /\ x e. B ) /\ k = ( K ` { x } ) ) /\ t e. B ) /\ X = ( t ( .r ` R ) x ) ) -> -. ( K ` { x } ) = B ) : No typesetting found for |- ( ( ( ( ( ( ( ( ( ph /\ X e. ( Irred ` R ) ) /\ -. M e. ( MaxIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ -. ( M C_ k -> ( k = M \/ k = B ) ) ) /\ x e. B ) /\ k = ( K ` { x } ) ) /\ t e. B ) /\ X = ( t ( .r ` R ) x ) ) -> -. ( K ` { x } ) = B ) with typecode |-
47		eqid	$$⊢K\left(\left\{x\right\}\right)=K\left(\left\{x\right\}\right)$$
48	11	ad8antr	Could not format ( ( ( ( ( ( ( ( ( ph /\ X e. ( Irred ` R ) ) /\ -. M e. ( MaxIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ -. ( M C_ k -> ( k = M \/ k = B ) ) ) /\ x e. B ) /\ k = ( K ` { x } ) ) /\ t e. B ) /\ X = ( t ( .r ` R ) x ) ) -> R e. IDomn ) : No typesetting found for |- ( ( ( ( ( ( ( ( ( ph /\ X e. ( Irred ` R ) ) /\ -. M e. ( MaxIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ -. ( M C_ k -> ( k = M \/ k = B ) ) ) /\ x e. B ) /\ k = ( K ` { x } ) ) /\ t e. B ) /\ X = ( t ( .r ` R ) x ) ) -> R e. IDomn ) with typecode |-
49	21 2 47 1 19 48	unitpidl1	Could not format ( ( ( ( ( ( ( ( ( ph /\ X e. ( Irred ` R ) ) /\ -. M e. ( MaxIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ -. ( M C_ k -> ( k = M \/ k = B ) ) ) /\ x e. B ) /\ k = ( K ` { x } ) ) /\ t e. B ) /\ X = ( t ( .r ` R ) x ) ) -> ( ( K ` { x } ) = B <-> x e. ( Unit ` R ) ) ) : No typesetting found for |- ( ( ( ( ( ( ( ( ( ph /\ X e. ( Irred ` R ) ) /\ -. M e. ( MaxIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ -. ( M C_ k -> ( k = M \/ k = B ) ) ) /\ x e. B ) /\ k = ( K ` { x } ) ) /\ t e. B ) /\ X = ( t ( .r ` R ) x ) ) -> ( ( K ` { x } ) = B <-> x e. ( Unit ` R ) ) ) with typecode |-
50	46 49	mtbid	Could not format ( ( ( ( ( ( ( ( ( ph /\ X e. ( Irred ` R ) ) /\ -. M e. ( MaxIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ -. ( M C_ k -> ( k = M \/ k = B ) ) ) /\ x e. B ) /\ k = ( K ` { x } ) ) /\ t e. B ) /\ X = ( t ( .r ` R ) x ) ) -> -. x e. ( Unit ` R ) ) : No typesetting found for |- ( ( ( ( ( ( ( ( ( ph /\ X e. ( Irred ` R ) ) /\ -. M e. ( MaxIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ -. ( M C_ k -> ( k = M \/ k = B ) ) ) /\ x e. B ) /\ k = ( K ` { x } ) ) /\ t e. B ) /\ X = ( t ( .r ` R ) x ) ) -> -. x e. ( Unit ` R ) ) with typecode |-
51	33 50	olcnd	Could not format ( ( ( ( ( ( ( ( ( ph /\ X e. ( Irred ` R ) ) /\ -. M e. ( MaxIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ -. ( M C_ k -> ( k = M \/ k = B ) ) ) /\ x e. B ) /\ k = ( K ` { x } ) ) /\ t e. B ) /\ X = ( t ( .r ` R ) x ) ) -> t e. ( Unit ` R ) ) : No typesetting found for |- ( ( ( ( ( ( ( ( ( ph /\ X e. ( Irred ` R ) ) /\ -. M e. ( MaxIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ -. ( M C_ k -> ( k = M \/ k = B ) ) ) /\ x e. B ) /\ k = ( K ` { x } ) ) /\ t e. B ) /\ X = ( t ( .r ` R ) x ) ) -> t e. ( Unit ` R ) ) with typecode |-
52	28	eqcomd	Could not format ( ( ( ( ( ( ( ( ( ph /\ X e. ( Irred ` R ) ) /\ -. M e. ( MaxIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ -. ( M C_ k -> ( k = M \/ k = B ) ) ) /\ x e. B ) /\ k = ( K ` { x } ) ) /\ t e. B ) /\ X = ( t ( .r ` R ) x ) ) -> ( t ( .r ` R ) x ) = X ) : No typesetting found for |- ( ( ( ( ( ( ( ( ( ph /\ X e. ( Irred ` R ) ) /\ -. M e. ( MaxIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ -. ( M C_ k -> ( k = M \/ k = B ) ) ) /\ x e. B ) /\ k = ( K ` { x } ) ) /\ t e. B ) /\ X = ( t ( .r ` R ) x ) ) -> ( t ( .r ` R ) x ) = X ) with typecode |-
53	1 2 17 19 20 21 22 26 51 52	dvdsruassoi	Could not format ( ( ( ( ( ( ( ( ( ph /\ X e. ( Irred ` R ) ) /\ -. M e. ( MaxIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ -. ( M C_ k -> ( k = M \/ k = B ) ) ) /\ x e. B ) /\ k = ( K ` { x } ) ) /\ t e. B ) /\ X = ( t ( .r ` R ) x ) ) -> ( x ( ||r ` R ) X /\ X ( ||r ` R ) x ) ) : No typesetting found for |- ( ( ( ( ( ( ( ( ( ph /\ X e. ( Irred ` R ) ) /\ -. M e. ( MaxIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ -. ( M C_ k -> ( k = M \/ k = B ) ) ) /\ x e. B ) /\ k = ( K ` { x } ) ) /\ t e. B ) /\ X = ( t ( .r ` R ) x ) ) -> ( x ( ||r ` R ) X /\ X ( ||r ` R ) x ) ) with typecode |-
54	1 2 17 19 20 26	rspsnasso	Could not format ( ( ( ( ( ( ( ( ( ph /\ X e. ( Irred ` R ) ) /\ -. M e. ( MaxIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ -. ( M C_ k -> ( k = M \/ k = B ) ) ) /\ x e. B ) /\ k = ( K ` { x } ) ) /\ t e. B ) /\ X = ( t ( .r ` R ) x ) ) -> ( ( x ( ||r ` R ) X /\ X ( ||r ` R ) x ) <-> ( K ` { X } ) = ( K ` { x } ) ) ) : No typesetting found for |- ( ( ( ( ( ( ( ( ( ph /\ X e. ( Irred ` R ) ) /\ -. M e. ( MaxIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ -. ( M C_ k -> ( k = M \/ k = B ) ) ) /\ x e. B ) /\ k = ( K ` { x } ) ) /\ t e. B ) /\ X = ( t ( .r ` R ) x ) ) -> ( ( x ( ||r ` R ) X /\ X ( ||r ` R ) x ) <-> ( K ` { X } ) = ( K ` { x } ) ) ) with typecode |-
55	53 54	mpbid	Could not format ( ( ( ( ( ( ( ( ( ph /\ X e. ( Irred ` R ) ) /\ -. M e. ( MaxIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ -. ( M C_ k -> ( k = M \/ k = B ) ) ) /\ x e. B ) /\ k = ( K ` { x } ) ) /\ t e. B ) /\ X = ( t ( .r ` R ) x ) ) -> ( K ` { X } ) = ( K ` { x } ) ) : No typesetting found for |- ( ( ( ( ( ( ( ( ( ph /\ X e. ( Irred ` R ) ) /\ -. M e. ( MaxIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ -. ( M C_ k -> ( k = M \/ k = B ) ) ) /\ x e. B ) /\ k = ( K ` { x } ) ) /\ t e. B ) /\ X = ( t ( .r ` R ) x ) ) -> ( K ` { X } ) = ( K ` { x } ) ) with typecode |-
56	55 35	eqtr4d	Could not format ( ( ( ( ( ( ( ( ( ph /\ X e. ( Irred ` R ) ) /\ -. M e. ( MaxIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ -. ( M C_ k -> ( k = M \/ k = B ) ) ) /\ x e. B ) /\ k = ( K ` { x } ) ) /\ t e. B ) /\ X = ( t ( .r ` R ) x ) ) -> ( K ` { X } ) = k ) : No typesetting found for |- ( ( ( ( ( ( ( ( ( ph /\ X e. ( Irred ` R ) ) /\ -. M e. ( MaxIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ -. ( M C_ k -> ( k = M \/ k = B ) ) ) /\ x e. B ) /\ k = ( K ` { x } ) ) /\ t e. B ) /\ X = ( t ( .r ` R ) x ) ) -> ( K ` { X } ) = k ) with typecode |-
57	4 56	eqtr2id	Could not format ( ( ( ( ( ( ( ( ( ph /\ X e. ( Irred ` R ) ) /\ -. M e. ( MaxIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ -. ( M C_ k -> ( k = M \/ k = B ) ) ) /\ x e. B ) /\ k = ( K ` { x } ) ) /\ t e. B ) /\ X = ( t ( .r ` R ) x ) ) -> k = M ) : No typesetting found for |- ( ( ( ( ( ( ( ( ( ph /\ X e. ( Irred ` R ) ) /\ -. M e. ( MaxIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ -. ( M C_ k -> ( k = M \/ k = B ) ) ) /\ x e. B ) /\ k = ( K ` { x } ) ) /\ t e. B ) /\ X = ( t ( .r ` R ) x ) ) -> k = M ) with typecode |-
58	41	simpld	Could not format ( ( ( ( ( ph /\ X e. ( Irred ` R ) ) /\ -. M e. ( MaxIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ -. ( M C_ k -> ( k = M \/ k = B ) ) ) -> -. k = M ) : No typesetting found for |- ( ( ( ( ( ph /\ X e. ( Irred ` R ) ) /\ -. M e. ( MaxIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ -. ( M C_ k -> ( k = M \/ k = B ) ) ) -> -. k = M ) with typecode |-
59	58	ad4antr	Could not format ( ( ( ( ( ( ( ( ( ph /\ X e. ( Irred ` R ) ) /\ -. M e. ( MaxIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ -. ( M C_ k -> ( k = M \/ k = B ) ) ) /\ x e. B ) /\ k = ( K ` { x } ) ) /\ t e. B ) /\ X = ( t ( .r ` R ) x ) ) -> -. k = M ) : No typesetting found for |- ( ( ( ( ( ( ( ( ( ph /\ X e. ( Irred ` R ) ) /\ -. M e. ( MaxIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ -. ( M C_ k -> ( k = M \/ k = B ) ) ) /\ x e. B ) /\ k = ( K ` { x } ) ) /\ t e. B ) /\ X = ( t ( .r ` R ) x ) ) -> -. k = M ) with typecode |-
60	57 59	pm2.21dd	Could not format ( ( ( ( ( ( ( ( ( ph /\ X e. ( Irred ` R ) ) /\ -. M e. ( MaxIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ -. ( M C_ k -> ( k = M \/ k = B ) ) ) /\ x e. B ) /\ k = ( K ` { x } ) ) /\ t e. B ) /\ X = ( t ( .r ` R ) x ) ) -> M e. ( MaxIdeal ` R ) ) : No typesetting found for |- ( ( ( ( ( ( ( ( ( ph /\ X e. ( Irred ` R ) ) /\ -. M e. ( MaxIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ -. ( M C_ k -> ( k = M \/ k = B ) ) ) /\ x e. B ) /\ k = ( K ` { x } ) ) /\ t e. B ) /\ X = ( t ( .r ` R ) x ) ) -> M e. ( MaxIdeal ` R ) ) with typecode |-
61	38	simpld	Could not format ( ( ( ( ( ph /\ X e. ( Irred ` R ) ) /\ -. M e. ( MaxIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ -. ( M C_ k -> ( k = M \/ k = B ) ) ) -> M C_ k ) : No typesetting found for |- ( ( ( ( ( ph /\ X e. ( Irred ` R ) ) /\ -. M e. ( MaxIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ -. ( M C_ k -> ( k = M \/ k = B ) ) ) -> M C_ k ) with typecode |-
62	61	ad2antrr	Could not format ( ( ( ( ( ( ( ph /\ X e. ( Irred ` R ) ) /\ -. M e. ( MaxIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ -. ( M C_ k -> ( k = M \/ k = B ) ) ) /\ x e. B ) /\ k = ( K ` { x } ) ) -> M C_ k ) : No typesetting found for |- ( ( ( ( ( ( ( ph /\ X e. ( Irred ` R ) ) /\ -. M e. ( MaxIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ -. ( M C_ k -> ( k = M \/ k = B ) ) ) /\ x e. B ) /\ k = ( K ` { x } ) ) -> M C_ k ) with typecode |-
63	6	snssd	$$⊢\phi \to \left\{X\right\}\subseteq B$$
64	2 1	rspssid	$$⊢\left(R\in \mathrm{Ring}\wedge \left\{X\right\}\subseteq B\right)\to \left\{X\right\}\subseteq K\left(\left\{X\right\}\right)$$
65	23 63 64	syl2anc	$$⊢\phi \to \left\{X\right\}\subseteq K\left(\left\{X\right\}\right)$$
66	65 4	sseqtrrdi	$$⊢\phi \to \left\{X\right\}\subseteq M$$
67		snssg	$$⊢X\in B\to \left(X\in M\leftrightarrow \left\{X\right\}\subseteq M\right)$$
68	67	biimpar	$$⊢\left(X\in B\wedge \left\{X\right\}\subseteq M\right)\to X\in M$$
69	6 66 68	syl2anc	$$⊢\phi \to X\in M$$
70	69	ad6antr	Could not format ( ( ( ( ( ( ( ph /\ X e. ( Irred ` R ) ) /\ -. M e. ( MaxIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ -. ( M C_ k -> ( k = M \/ k = B ) ) ) /\ x e. B ) /\ k = ( K ` { x } ) ) -> X e. M ) : No typesetting found for |- ( ( ( ( ( ( ( ph /\ X e. ( Irred ` R ) ) /\ -. M e. ( MaxIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ -. ( M C_ k -> ( k = M \/ k = B ) ) ) /\ x e. B ) /\ k = ( K ` { x } ) ) -> X e. M ) with typecode |-
71	62 70	sseldd	Could not format ( ( ( ( ( ( ( ph /\ X e. ( Irred ` R ) ) /\ -. M e. ( MaxIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ -. ( M C_ k -> ( k = M \/ k = B ) ) ) /\ x e. B ) /\ k = ( K ` { x } ) ) -> X e. k ) : No typesetting found for |- ( ( ( ( ( ( ( ph /\ X e. ( Irred ` R ) ) /\ -. M e. ( MaxIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ -. ( M C_ k -> ( k = M \/ k = B ) ) ) /\ x e. B ) /\ k = ( K ` { x } ) ) -> X e. k ) with typecode |-
72	71 34	eleqtrd	Could not format ( ( ( ( ( ( ( ph /\ X e. ( Irred ` R ) ) /\ -. M e. ( MaxIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ -. ( M C_ k -> ( k = M \/ k = B ) ) ) /\ x e. B ) /\ k = ( K ` { x } ) ) -> X e. ( K ` { x } ) ) : No typesetting found for |- ( ( ( ( ( ( ( ph /\ X e. ( Irred ` R ) ) /\ -. M e. ( MaxIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ -. ( M C_ k -> ( k = M \/ k = B ) ) ) /\ x e. B ) /\ k = ( K ` { x } ) ) -> X e. ( K ` { x } ) ) with typecode |-
73	1 22 2	rspsnel	$$⊢\left(R\in \mathrm{Ring}\wedge x\in B\right)\to \left(X\in K\left(\left\{x\right\}\right)\leftrightarrow \exists t\in BX=t{\cdot }_{R}x\right)$$
74	73	biimpa	$$⊢\left(\left(R\in \mathrm{Ring}\wedge x\in B\right)\wedge X\in K\left(\left\{x\right\}\right)\right)\to \exists t\in BX=t{\cdot }_{R}x$$
75	25 18 72 74	syl21anc	Could not format ( ( ( ( ( ( ( ph /\ X e. ( Irred ` R ) ) /\ -. M e. ( MaxIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ -. ( M C_ k -> ( k = M \/ k = B ) ) ) /\ x e. B ) /\ k = ( K ` { x } ) ) -> E. t e. B X = ( t ( .r ` R ) x ) ) : No typesetting found for |- ( ( ( ( ( ( ( ph /\ X e. ( Irred ` R ) ) /\ -. M e. ( MaxIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ -. ( M C_ k -> ( k = M \/ k = B ) ) ) /\ x e. B ) /\ k = ( K ` { x } ) ) -> E. t e. B X = ( t ( .r ` R ) x ) ) with typecode |-
76	60 75	r19.29a	Could not format ( ( ( ( ( ( ( ph /\ X e. ( Irred ` R ) ) /\ -. M e. ( MaxIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ -. ( M C_ k -> ( k = M \/ k = B ) ) ) /\ x e. B ) /\ k = ( K ` { x } ) ) -> M e. ( MaxIdeal ` R ) ) : No typesetting found for |- ( ( ( ( ( ( ( ph /\ X e. ( Irred ` R ) ) /\ -. M e. ( MaxIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ -. ( M C_ k -> ( k = M \/ k = B ) ) ) /\ x e. B ) /\ k = ( K ` { x } ) ) -> M e. ( MaxIdeal ` R ) ) with typecode |-
77		simplr	Could not format ( ( ( ( ( ph /\ X e. ( Irred ` R ) ) /\ -. M e. ( MaxIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ -. ( M C_ k -> ( k = M \/ k = B ) ) ) -> k e. ( LIdeal ` R ) ) : No typesetting found for |- ( ( ( ( ( ph /\ X e. ( Irred ` R ) ) /\ -. M e. ( MaxIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ -. ( M C_ k -> ( k = M \/ k = B ) ) ) -> k e. ( LIdeal ` R ) ) with typecode |-
78	10	elin2d	$$⊢\phi \to R\in \mathrm{LPIR}$$
79		eqid	$$⊢\mathrm{LPIdeal}\left(R\right)=\mathrm{LPIdeal}\left(R\right)$$
80		eqid	$$⊢\mathrm{LIdeal}\left(R\right)=\mathrm{LIdeal}\left(R\right)$$
81	79 80	islpir	$$⊢R\in \mathrm{LPIR}\leftrightarrow \left(R\in \mathrm{Ring}\wedge \mathrm{LIdeal}\left(R\right)=\mathrm{LPIdeal}\left(R\right)\right)$$
82	81	simprbi	$$⊢R\in \mathrm{LPIR}\to \mathrm{LIdeal}\left(R\right)=\mathrm{LPIdeal}\left(R\right)$$
83	78 82	syl	$$⊢\phi \to \mathrm{LIdeal}\left(R\right)=\mathrm{LPIdeal}\left(R\right)$$
84	83	ad4antr	Could not format ( ( ( ( ( ph /\ X e. ( Irred ` R ) ) /\ -. M e. ( MaxIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ -. ( M C_ k -> ( k = M \/ k = B ) ) ) -> ( LIdeal ` R ) = ( LPIdeal ` R ) ) : No typesetting found for |- ( ( ( ( ( ph /\ X e. ( Irred ` R ) ) /\ -. M e. ( MaxIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ -. ( M C_ k -> ( k = M \/ k = B ) ) ) -> ( LIdeal ` R ) = ( LPIdeal ` R ) ) with typecode |-
85	77 84	eleqtrd	Could not format ( ( ( ( ( ph /\ X e. ( Irred ` R ) ) /\ -. M e. ( MaxIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ -. ( M C_ k -> ( k = M \/ k = B ) ) ) -> k e. ( LPIdeal ` R ) ) : No typesetting found for |- ( ( ( ( ( ph /\ X e. ( Irred ` R ) ) /\ -. M e. ( MaxIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ -. ( M C_ k -> ( k = M \/ k = B ) ) ) -> k e. ( LPIdeal ` R ) ) with typecode |-
86	79 2 1	islpidl	$$⊢R\in \mathrm{Ring}\to \left(k\in \mathrm{LPIdeal}\left(R\right)\leftrightarrow \exists x\in Bk=K\left(\left\{x\right\}\right)\right)$$
87	86	biimpa	$$⊢\left(R\in \mathrm{Ring}\wedge k\in \mathrm{LPIdeal}\left(R\right)\right)\to \exists x\in Bk=K\left(\left\{x\right\}\right)$$
88	24 85 87	syl2anc	Could not format ( ( ( ( ( ph /\ X e. ( Irred ` R ) ) /\ -. M e. ( MaxIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ -. ( M C_ k -> ( k = M \/ k = B ) ) ) -> E. x e. B k = ( K ` { x } ) ) : No typesetting found for |- ( ( ( ( ( ph /\ X e. ( Irred ` R ) ) /\ -. M e. ( MaxIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ -. ( M C_ k -> ( k = M \/ k = B ) ) ) -> E. x e. B k = ( K ` { x } ) ) with typecode |-
89	76 88	r19.29a	Could not format ( ( ( ( ( ph /\ X e. ( Irred ` R ) ) /\ -. M e. ( MaxIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ -. ( M C_ k -> ( k = M \/ k = B ) ) ) -> M e. ( MaxIdeal ` R ) ) : No typesetting found for |- ( ( ( ( ( ph /\ X e. ( Irred ` R ) ) /\ -. M e. ( MaxIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ -. ( M C_ k -> ( k = M \/ k = B ) ) ) -> M e. ( MaxIdeal ` R ) ) with typecode |-
90	8	ad2antrr	Could not format ( ( ( ph /\ X e. ( Irred ` R ) ) /\ -. M e. ( MaxIdeal ` R ) ) -> M e. ( LIdeal ` R ) ) : No typesetting found for |- ( ( ( ph /\ X e. ( Irred ` R ) ) /\ -. M e. ( MaxIdeal ` R ) ) -> M e. ( LIdeal ` R ) ) with typecode |-
91	31 21	irrednu	$$⊢X\in \mathrm{Irred}\left(R\right)\to \neg X\in \mathrm{Unit}\left(R\right)$$
92	91	adantl	$$⊢\left(\phi \wedge X\in \mathrm{Irred}\left(R\right)\right)\to \neg X\in \mathrm{Unit}\left(R\right)$$
93	21 2 4 1 6 11	unitpidl1	$$⊢\phi \to \left(M=B\leftrightarrow X\in \mathrm{Unit}\left(R\right)\right)$$
94	93	adantr	$$⊢\left(\phi \wedge X\in \mathrm{Irred}\left(R\right)\right)\to \left(M=B\leftrightarrow X\in \mathrm{Unit}\left(R\right)\right)$$
95	94	necon3abid	$$⊢\left(\phi \wedge X\in \mathrm{Irred}\left(R\right)\right)\to \left(M\ne B\leftrightarrow \neg X\in \mathrm{Unit}\left(R\right)\right)$$
96	92 95	mpbird	$$⊢\left(\phi \wedge X\in \mathrm{Irred}\left(R\right)\right)\to M\ne B$$
97	96	adantr	Could not format ( ( ( ph /\ X e. ( Irred ` R ) ) /\ -. M e. ( MaxIdeal ` R ) ) -> M =/= B ) : No typesetting found for |- ( ( ( ph /\ X e. ( Irred ` R ) ) /\ -. M e. ( MaxIdeal ` R ) ) -> M =/= B ) with typecode |-
98	90 97	jca	Could not format ( ( ( ph /\ X e. ( Irred ` R ) ) /\ -. M e. ( MaxIdeal ` R ) ) -> ( M e. ( LIdeal ` R ) /\ M =/= B ) ) : No typesetting found for |- ( ( ( ph /\ X e. ( Irred ` R ) ) /\ -. M e. ( MaxIdeal ` R ) ) -> ( M e. ( LIdeal ` R ) /\ M =/= B ) ) with typecode |-
99	1	ismxidl	Could not format ( R e. Ring -> ( M e. ( MaxIdeal ` R ) <-> ( M e. ( LIdeal ` R ) /\ M =/= B /\ A. k e. ( LIdeal ` R ) ( M C_ k -> ( k = M \/ k = B ) ) ) ) ) : No typesetting found for |- ( R e. Ring -> ( M e. ( MaxIdeal ` R ) <-> ( M e. ( LIdeal ` R ) /\ M =/= B /\ A. k e. ( LIdeal ` R ) ( M C_ k -> ( k = M \/ k = B ) ) ) ) ) with typecode |-
100	23 99	syl	Could not format ( ph -> ( M e. ( MaxIdeal ` R ) <-> ( M e. ( LIdeal ` R ) /\ M =/= B /\ A. k e. ( LIdeal ` R ) ( M C_ k -> ( k = M \/ k = B ) ) ) ) ) : No typesetting found for |- ( ph -> ( M e. ( MaxIdeal ` R ) <-> ( M e. ( LIdeal ` R ) /\ M =/= B /\ A. k e. ( LIdeal ` R ) ( M C_ k -> ( k = M \/ k = B ) ) ) ) ) with typecode |-
101		df-3an	$$⊢\left(M\in \mathrm{LIdeal}\left(R\right)\wedge M\ne B\wedge \forall k\in \mathrm{LIdeal}\left(R\right)\left(M\subseteq k\to \left(k=M\vee k=B\right)\right)\right)\leftrightarrow \left(\left(M\in \mathrm{LIdeal}\left(R\right)\wedge M\ne B\right)\wedge \forall k\in \mathrm{LIdeal}\left(R\right)\left(M\subseteq k\to \left(k=M\vee k=B\right)\right)\right)$$
102	100 101	bitrdi	Could not format ( ph -> ( M e. ( MaxIdeal ` R ) <-> ( ( M e. ( LIdeal ` R ) /\ M =/= B ) /\ A. k e. ( LIdeal ` R ) ( M C_ k -> ( k = M \/ k = B ) ) ) ) ) : No typesetting found for |- ( ph -> ( M e. ( MaxIdeal ` R ) <-> ( ( M e. ( LIdeal ` R ) /\ M =/= B ) /\ A. k e. ( LIdeal ` R ) ( M C_ k -> ( k = M \/ k = B ) ) ) ) ) with typecode |-
103	102	notbid	Could not format ( ph -> ( -. M e. ( MaxIdeal ` R ) <-> -. ( ( M e. ( LIdeal ` R ) /\ M =/= B ) /\ A. k e. ( LIdeal ` R ) ( M C_ k -> ( k = M \/ k = B ) ) ) ) ) : No typesetting found for |- ( ph -> ( -. M e. ( MaxIdeal ` R ) <-> -. ( ( M e. ( LIdeal ` R ) /\ M =/= B ) /\ A. k e. ( LIdeal ` R ) ( M C_ k -> ( k = M \/ k = B ) ) ) ) ) with typecode |-
104	103	biimpa	Could not format ( ( ph /\ -. M e. ( MaxIdeal ` R ) ) -> -. ( ( M e. ( LIdeal ` R ) /\ M =/= B ) /\ A. k e. ( LIdeal ` R ) ( M C_ k -> ( k = M \/ k = B ) ) ) ) : No typesetting found for |- ( ( ph /\ -. M e. ( MaxIdeal ` R ) ) -> -. ( ( M e. ( LIdeal ` R ) /\ M =/= B ) /\ A. k e. ( LIdeal ` R ) ( M C_ k -> ( k = M \/ k = B ) ) ) ) with typecode |-
105	104	adantlr	Could not format ( ( ( ph /\ X e. ( Irred ` R ) ) /\ -. M e. ( MaxIdeal ` R ) ) -> -. ( ( M e. ( LIdeal ` R ) /\ M =/= B ) /\ A. k e. ( LIdeal ` R ) ( M C_ k -> ( k = M \/ k = B ) ) ) ) : No typesetting found for |- ( ( ( ph /\ X e. ( Irred ` R ) ) /\ -. M e. ( MaxIdeal ` R ) ) -> -. ( ( M e. ( LIdeal ` R ) /\ M =/= B ) /\ A. k e. ( LIdeal ` R ) ( M C_ k -> ( k = M \/ k = B ) ) ) ) with typecode |-
106	98 105	mpnanrd	Could not format ( ( ( ph /\ X e. ( Irred ` R ) ) /\ -. M e. ( MaxIdeal ` R ) ) -> -. A. k e. ( LIdeal ` R ) ( M C_ k -> ( k = M \/ k = B ) ) ) : No typesetting found for |- ( ( ( ph /\ X e. ( Irred ` R ) ) /\ -. M e. ( MaxIdeal ` R ) ) -> -. A. k e. ( LIdeal ` R ) ( M C_ k -> ( k = M \/ k = B ) ) ) with typecode |-
107		rexnal	$$⊢\exists k\in \mathrm{LIdeal}\left(R\right)\neg \left(M\subseteq k\to \left(k=M\vee k=B\right)\right)\leftrightarrow \neg \forall k\in \mathrm{LIdeal}\left(R\right)\left(M\subseteq k\to \left(k=M\vee k=B\right)\right)$$
108	106 107	sylibr	Could not format ( ( ( ph /\ X e. ( Irred ` R ) ) /\ -. M e. ( MaxIdeal ` R ) ) -> E. k e. ( LIdeal ` R ) -. ( M C_ k -> ( k = M \/ k = B ) ) ) : No typesetting found for |- ( ( ( ph /\ X e. ( Irred ` R ) ) /\ -. M e. ( MaxIdeal ` R ) ) -> E. k e. ( LIdeal ` R ) -. ( M C_ k -> ( k = M \/ k = B ) ) ) with typecode |-
109	89 108	r19.29a	Could not format ( ( ( ph /\ X e. ( Irred ` R ) ) /\ -. M e. ( MaxIdeal ` R ) ) -> M e. ( MaxIdeal ` R ) ) : No typesetting found for |- ( ( ( ph /\ X e. ( Irred ` R ) ) /\ -. M e. ( MaxIdeal ` R ) ) -> M e. ( MaxIdeal ` R ) ) with typecode |-
110	109	pm2.18da	Could not format ( ( ph /\ X e. ( Irred ` R ) ) -> M e. ( MaxIdeal ` R ) ) : No typesetting found for |- ( ( ph /\ X e. ( Irred ` R ) ) -> M e. ( MaxIdeal ` R ) ) with typecode |-
111	16 110	impbida	Could not format ( ph -> ( M e. ( MaxIdeal ` R ) <-> X e. ( Irred ` R ) ) ) : No typesetting found for |- ( ph -> ( M e. ( MaxIdeal ` R ) <-> X e. ( Irred ` R ) ) ) with typecode |-