Theorem zarclssn

Description: The closed points of Zariski topology are the maximal ideals. (Contributed by Thierry Arnoux, 16-Jun-2024)

	Ref	Expression
Hypotheses	zarclsx.1	No typesetting found for |- V = ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | i C_ j } ) with typecode |-
	zarclssn.1	$$⊢B=\mathrm{LIdeal}\left(R\right)$$
Assertion	zarclssn	Could not format assertion : No typesetting found for |- ( ( R e. CRing /\ M e. B ) -> ( { M } = ( V ` M ) <-> M e. ( MaxIdeal ` R ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		zarclsx.1	Could not format V = ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | i C_ j } ) : No typesetting found for |- V = ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | i C_ j } ) with typecode |-
2		zarclssn.1	$$⊢B=\mathrm{LIdeal}\left(R\right)$$
3		crngring	$$⊢R\in \mathrm{CRing}\to R\in \mathrm{Ring}$$
4	3	ad2antrr	$$⊢\left(\left(R\in \mathrm{CRing}\wedge M\in B\right)\wedge \left\{M\right\}=V\left(M\right)\right)\to R\in \mathrm{Ring}$$
5		simplr	$$⊢\left(\left(R\in \mathrm{CRing}\wedge M\in B\right)\wedge \left\{M\right\}=V\left(M\right)\right)\to M\in B$$
6	5 2	eleqtrdi	$$⊢\left(\left(R\in \mathrm{CRing}\wedge M\in B\right)\wedge \left\{M\right\}=V\left(M\right)\right)\to M\in \mathrm{LIdeal}\left(R\right)$$
7		simpr	$$⊢\left(\left(R\in \mathrm{CRing}\wedge M\in B\right)\wedge \left\{M\right\}=V\left(M\right)\right)\to \left\{M\right\}=V\left(M\right)$$
8	5	snn0d	$$⊢\left(\left(R\in \mathrm{CRing}\wedge M\in B\right)\wedge \left\{M\right\}=V\left(M\right)\right)\to \left\{M\right\}\ne \varnothing$$
9	7 8	eqnetrrd	$$⊢\left(\left(R\in \mathrm{CRing}\wedge M\in B\right)\wedge \left\{M\right\}=V\left(M\right)\right)\to V\left(M\right)\ne \varnothing$$
10		simpll	$$⊢\left(\left(R\in \mathrm{CRing}\wedge M\in B\right)\wedge \left\{M\right\}=V\left(M\right)\right)\to R\in \mathrm{CRing}$$
11		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
12	1 11	zarcls1	$$⊢\left(R\in \mathrm{CRing}\wedge M\in \mathrm{LIdeal}\left(R\right)\right)\to \left(V\left(M\right)=\varnothing \leftrightarrow M={\mathrm{Base}}_R\right)$$
13	12	necon3bid	$$⊢\left(R\in \mathrm{CRing}\wedge M\in \mathrm{LIdeal}\left(R\right)\right)\to \left(V\left(M\right)\ne \varnothing \leftrightarrow M\ne {\mathrm{Base}}_R\right)$$
14	10 6 13	syl2anc	$$⊢\left(\left(R\in \mathrm{CRing}\wedge M\in B\right)\wedge \left\{M\right\}=V\left(M\right)\right)\to \left(V\left(M\right)\ne \varnothing \leftrightarrow M\ne {\mathrm{Base}}_R\right)$$
15	9 14	mpbid	$$⊢\left(\left(R\in \mathrm{CRing}\wedge M\in B\right)\wedge \left\{M\right\}=V\left(M\right)\right)\to M\ne {\mathrm{Base}}_R$$
16		simpr	Could not format ( ( ( ( ( ( ( ( R e. CRing /\ M e. B ) /\ { M } = ( V ` M ) ) /\ j e. ( LIdeal ` R ) ) /\ M C_ j ) /\ -. j = ( Base ` R ) ) /\ m e. ( MaxIdeal ` R ) ) /\ j C_ m ) -> j C_ m ) : No typesetting found for |- ( ( ( ( ( ( ( ( R e. CRing /\ M e. B ) /\ { M } = ( V ` M ) ) /\ j e. ( LIdeal ` R ) ) /\ M C_ j ) /\ -. j = ( Base ` R ) ) /\ m e. ( MaxIdeal ` R ) ) /\ j C_ m ) -> j C_ m ) with typecode |-
17	10	ad5antr	Could not format ( ( ( ( ( ( ( ( R e. CRing /\ M e. B ) /\ { M } = ( V ` M ) ) /\ j e. ( LIdeal ` R ) ) /\ M C_ j ) /\ -. j = ( Base ` R ) ) /\ m e. ( MaxIdeal ` R ) ) /\ j C_ m ) -> R e. CRing ) : No typesetting found for |- ( ( ( ( ( ( ( ( R e. CRing /\ M e. B ) /\ { M } = ( V ` M ) ) /\ j e. ( LIdeal ` R ) ) /\ M C_ j ) /\ -. j = ( Base ` R ) ) /\ m e. ( MaxIdeal ` R ) ) /\ j C_ m ) -> R e. CRing ) with typecode |-
18		simplr	Could not format ( ( ( ( ( ( ( ( R e. CRing /\ M e. B ) /\ { M } = ( V ` M ) ) /\ j e. ( LIdeal ` R ) ) /\ M C_ j ) /\ -. j = ( Base ` R ) ) /\ m e. ( MaxIdeal ` R ) ) /\ j C_ m ) -> m e. ( MaxIdeal ` R ) ) : No typesetting found for |- ( ( ( ( ( ( ( ( R e. CRing /\ M e. B ) /\ { M } = ( V ` M ) ) /\ j e. ( LIdeal ` R ) ) /\ M C_ j ) /\ -. j = ( Base ` R ) ) /\ m e. ( MaxIdeal ` R ) ) /\ j C_ m ) -> m e. ( MaxIdeal ` R ) ) with typecode |-
19		eqid	$$⊢\mathrm{LSSum}\left({\mathrm{mulGrp}}_R\right)=\mathrm{LSSum}\left({\mathrm{mulGrp}}_R\right)$$
20	19	mxidlprm	Could not format ( ( R e. CRing /\ m e. ( MaxIdeal ` R ) ) -> m e. ( PrmIdeal ` R ) ) : No typesetting found for |- ( ( R e. CRing /\ m e. ( MaxIdeal ` R ) ) -> m e. ( PrmIdeal ` R ) ) with typecode |-
21	17 18 20	syl2anc	Could not format ( ( ( ( ( ( ( ( R e. CRing /\ M e. B ) /\ { M } = ( V ` M ) ) /\ j e. ( LIdeal ` R ) ) /\ M C_ j ) /\ -. j = ( Base ` R ) ) /\ m e. ( MaxIdeal ` R ) ) /\ j C_ m ) -> m e. ( PrmIdeal ` R ) ) : No typesetting found for |- ( ( ( ( ( ( ( ( R e. CRing /\ M e. B ) /\ { M } = ( V ` M ) ) /\ j e. ( LIdeal ` R ) ) /\ M C_ j ) /\ -. j = ( Base ` R ) ) /\ m e. ( MaxIdeal ` R ) ) /\ j C_ m ) -> m e. ( PrmIdeal ` R ) ) with typecode |-
22		simp-4r	Could not format ( ( ( ( ( ( ( ( R e. CRing /\ M e. B ) /\ { M } = ( V ` M ) ) /\ j e. ( LIdeal ` R ) ) /\ M C_ j ) /\ -. j = ( Base ` R ) ) /\ m e. ( MaxIdeal ` R ) ) /\ j C_ m ) -> M C_ j ) : No typesetting found for |- ( ( ( ( ( ( ( ( R e. CRing /\ M e. B ) /\ { M } = ( V ` M ) ) /\ j e. ( LIdeal ` R ) ) /\ M C_ j ) /\ -. j = ( Base ` R ) ) /\ m e. ( MaxIdeal ` R ) ) /\ j C_ m ) -> M C_ j ) with typecode |-
23	22 16	sstrd	Could not format ( ( ( ( ( ( ( ( R e. CRing /\ M e. B ) /\ { M } = ( V ` M ) ) /\ j e. ( LIdeal ` R ) ) /\ M C_ j ) /\ -. j = ( Base ` R ) ) /\ m e. ( MaxIdeal ` R ) ) /\ j C_ m ) -> M C_ m ) : No typesetting found for |- ( ( ( ( ( ( ( ( R e. CRing /\ M e. B ) /\ { M } = ( V ` M ) ) /\ j e. ( LIdeal ` R ) ) /\ M C_ j ) /\ -. j = ( Base ` R ) ) /\ m e. ( MaxIdeal ` R ) ) /\ j C_ m ) -> M C_ m ) with typecode |-
24	1	a1i	Could not format ( ( ( R e. CRing /\ M e. B ) /\ { M } = ( V ` M ) ) -> V = ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | i C_ j } ) ) : No typesetting found for |- ( ( ( R e. CRing /\ M e. B ) /\ { M } = ( V ` M ) ) -> V = ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | i C_ j } ) ) with typecode |-
25		sseq1	$$⊢i=M\to \left(i\subseteq j\leftrightarrow M\subseteq j\right)$$
26	25	rabbidv	Could not format ( i = M -> { j e. ( PrmIdeal ` R ) | i C_ j } = { j e. ( PrmIdeal ` R ) | M C_ j } ) : No typesetting found for |- ( i = M -> { j e. ( PrmIdeal ` R ) | i C_ j } = { j e. ( PrmIdeal ` R ) | M C_ j } ) with typecode |-
27	26	adantl	Could not format ( ( ( ( R e. CRing /\ M e. B ) /\ { M } = ( V ` M ) ) /\ i = M ) -> { j e. ( PrmIdeal ` R ) | i C_ j } = { j e. ( PrmIdeal ` R ) | M C_ j } ) : No typesetting found for |- ( ( ( ( R e. CRing /\ M e. B ) /\ { M } = ( V ` M ) ) /\ i = M ) -> { j e. ( PrmIdeal ` R ) | i C_ j } = { j e. ( PrmIdeal ` R ) | M C_ j } ) with typecode |-
28		fvex	Could not format ( PrmIdeal ` R ) e. _V : No typesetting found for |- ( PrmIdeal ` R ) e. _V with typecode |-
29	28	rabex	Could not format { j e. ( PrmIdeal ` R ) | M C_ j } e. _V : No typesetting found for |- { j e. ( PrmIdeal ` R ) | M C_ j } e. _V with typecode |-
30	29	a1i	Could not format ( ( ( R e. CRing /\ M e. B ) /\ { M } = ( V ` M ) ) -> { j e. ( PrmIdeal ` R ) | M C_ j } e. _V ) : No typesetting found for |- ( ( ( R e. CRing /\ M e. B ) /\ { M } = ( V ` M ) ) -> { j e. ( PrmIdeal ` R ) | M C_ j } e. _V ) with typecode |-
31	24 27 6 30	fvmptd	Could not format ( ( ( R e. CRing /\ M e. B ) /\ { M } = ( V ` M ) ) -> ( V ` M ) = { j e. ( PrmIdeal ` R ) | M C_ j } ) : No typesetting found for |- ( ( ( R e. CRing /\ M e. B ) /\ { M } = ( V ` M ) ) -> ( V ` M ) = { j e. ( PrmIdeal ` R ) | M C_ j } ) with typecode |-
32	7 31	eqtr2d	Could not format ( ( ( R e. CRing /\ M e. B ) /\ { M } = ( V ` M ) ) -> { j e. ( PrmIdeal ` R ) | M C_ j } = { M } ) : No typesetting found for |- ( ( ( R e. CRing /\ M e. B ) /\ { M } = ( V ` M ) ) -> { j e. ( PrmIdeal ` R ) | M C_ j } = { M } ) with typecode |-
33		rabeqsn	Could not format ( { j e. ( PrmIdeal ` R ) | M C_ j } = { M } <-> A. j ( ( j e. ( PrmIdeal ` R ) /\ M C_ j ) <-> j = M ) ) : No typesetting found for |- ( { j e. ( PrmIdeal ` R ) | M C_ j } = { M } <-> A. j ( ( j e. ( PrmIdeal ` R ) /\ M C_ j ) <-> j = M ) ) with typecode |-
34	32 33	sylib	Could not format ( ( ( R e. CRing /\ M e. B ) /\ { M } = ( V ` M ) ) -> A. j ( ( j e. ( PrmIdeal ` R ) /\ M C_ j ) <-> j = M ) ) : No typesetting found for |- ( ( ( R e. CRing /\ M e. B ) /\ { M } = ( V ` M ) ) -> A. j ( ( j e. ( PrmIdeal ` R ) /\ M C_ j ) <-> j = M ) ) with typecode |-
35	34	ad5antr	Could not format ( ( ( ( ( ( ( ( R e. CRing /\ M e. B ) /\ { M } = ( V ` M ) ) /\ j e. ( LIdeal ` R ) ) /\ M C_ j ) /\ -. j = ( Base ` R ) ) /\ m e. ( MaxIdeal ` R ) ) /\ j C_ m ) -> A. j ( ( j e. ( PrmIdeal ` R ) /\ M C_ j ) <-> j = M ) ) : No typesetting found for |- ( ( ( ( ( ( ( ( R e. CRing /\ M e. B ) /\ { M } = ( V ` M ) ) /\ j e. ( LIdeal ` R ) ) /\ M C_ j ) /\ -. j = ( Base ` R ) ) /\ m e. ( MaxIdeal ` R ) ) /\ j C_ m ) -> A. j ( ( j e. ( PrmIdeal ` R ) /\ M C_ j ) <-> j = M ) ) with typecode |-
36		vex	$$⊢m\in \mathrm{V}$$
37		eleq1w	Could not format ( j = m -> ( j e. ( PrmIdeal ` R ) <-> m e. ( PrmIdeal ` R ) ) ) : No typesetting found for |- ( j = m -> ( j e. ( PrmIdeal ` R ) <-> m e. ( PrmIdeal ` R ) ) ) with typecode |-
38		sseq2	$$⊢j=m\to \left(M\subseteq j\leftrightarrow M\subseteq m\right)$$
39	37 38	anbi12d	Could not format ( j = m -> ( ( j e. ( PrmIdeal ` R ) /\ M C_ j ) <-> ( m e. ( PrmIdeal ` R ) /\ M C_ m ) ) ) : No typesetting found for |- ( j = m -> ( ( j e. ( PrmIdeal ` R ) /\ M C_ j ) <-> ( m e. ( PrmIdeal ` R ) /\ M C_ m ) ) ) with typecode |-
40		eqeq1	$$⊢j=m\to \left(j=M\leftrightarrow m=M\right)$$
41	39 40	bibi12d	Could not format ( j = m -> ( ( ( j e. ( PrmIdeal ` R ) /\ M C_ j ) <-> j = M ) <-> ( ( m e. ( PrmIdeal ` R ) /\ M C_ m ) <-> m = M ) ) ) : No typesetting found for |- ( j = m -> ( ( ( j e. ( PrmIdeal ` R ) /\ M C_ j ) <-> j = M ) <-> ( ( m e. ( PrmIdeal ` R ) /\ M C_ m ) <-> m = M ) ) ) with typecode |-
42	36 41	spcv	Could not format ( A. j ( ( j e. ( PrmIdeal ` R ) /\ M C_ j ) <-> j = M ) -> ( ( m e. ( PrmIdeal ` R ) /\ M C_ m ) <-> m = M ) ) : No typesetting found for |- ( A. j ( ( j e. ( PrmIdeal ` R ) /\ M C_ j ) <-> j = M ) -> ( ( m e. ( PrmIdeal ` R ) /\ M C_ m ) <-> m = M ) ) with typecode |-
43	35 42	syl	Could not format ( ( ( ( ( ( ( ( R e. CRing /\ M e. B ) /\ { M } = ( V ` M ) ) /\ j e. ( LIdeal ` R ) ) /\ M C_ j ) /\ -. j = ( Base ` R ) ) /\ m e. ( MaxIdeal ` R ) ) /\ j C_ m ) -> ( ( m e. ( PrmIdeal ` R ) /\ M C_ m ) <-> m = M ) ) : No typesetting found for |- ( ( ( ( ( ( ( ( R e. CRing /\ M e. B ) /\ { M } = ( V ` M ) ) /\ j e. ( LIdeal ` R ) ) /\ M C_ j ) /\ -. j = ( Base ` R ) ) /\ m e. ( MaxIdeal ` R ) ) /\ j C_ m ) -> ( ( m e. ( PrmIdeal ` R ) /\ M C_ m ) <-> m = M ) ) with typecode |-
44	21 23 43	mpbi2and	Could not format ( ( ( ( ( ( ( ( R e. CRing /\ M e. B ) /\ { M } = ( V ` M ) ) /\ j e. ( LIdeal ` R ) ) /\ M C_ j ) /\ -. j = ( Base ` R ) ) /\ m e. ( MaxIdeal ` R ) ) /\ j C_ m ) -> m = M ) : No typesetting found for |- ( ( ( ( ( ( ( ( R e. CRing /\ M e. B ) /\ { M } = ( V ` M ) ) /\ j e. ( LIdeal ` R ) ) /\ M C_ j ) /\ -. j = ( Base ` R ) ) /\ m e. ( MaxIdeal ` R ) ) /\ j C_ m ) -> m = M ) with typecode |-
45	16 44	sseqtrd	Could not format ( ( ( ( ( ( ( ( R e. CRing /\ M e. B ) /\ { M } = ( V ` M ) ) /\ j e. ( LIdeal ` R ) ) /\ M C_ j ) /\ -. j = ( Base ` R ) ) /\ m e. ( MaxIdeal ` R ) ) /\ j C_ m ) -> j C_ M ) : No typesetting found for |- ( ( ( ( ( ( ( ( R e. CRing /\ M e. B ) /\ { M } = ( V ` M ) ) /\ j e. ( LIdeal ` R ) ) /\ M C_ j ) /\ -. j = ( Base ` R ) ) /\ m e. ( MaxIdeal ` R ) ) /\ j C_ m ) -> j C_ M ) with typecode |-
46	45 22	eqssd	Could not format ( ( ( ( ( ( ( ( R e. CRing /\ M e. B ) /\ { M } = ( V ` M ) ) /\ j e. ( LIdeal ` R ) ) /\ M C_ j ) /\ -. j = ( Base ` R ) ) /\ m e. ( MaxIdeal ` R ) ) /\ j C_ m ) -> j = M ) : No typesetting found for |- ( ( ( ( ( ( ( ( R e. CRing /\ M e. B ) /\ { M } = ( V ` M ) ) /\ j e. ( LIdeal ` R ) ) /\ M C_ j ) /\ -. j = ( Base ` R ) ) /\ m e. ( MaxIdeal ` R ) ) /\ j C_ m ) -> j = M ) with typecode |-
47	3	ad5antr	$$⊢\left(\left(\left(\left(\left(R\in \mathrm{CRing}\wedge M\in B\right)\wedge \left\{M\right\}=V\left(M\right)\right)\wedge j\in \mathrm{LIdeal}\left(R\right)\right)\wedge M\subseteq j\right)\wedge \neg j={\mathrm{Base}}_R\right)\to R\in \mathrm{Ring}$$
48		simpllr	$$⊢\left(\left(\left(\left(\left(R\in \mathrm{CRing}\wedge M\in B\right)\wedge \left\{M\right\}=V\left(M\right)\right)\wedge j\in \mathrm{LIdeal}\left(R\right)\right)\wedge M\subseteq j\right)\wedge \neg j={\mathrm{Base}}_R\right)\to j\in \mathrm{LIdeal}\left(R\right)$$
49		simpr	$$⊢\left(\left(\left(\left(\left(R\in \mathrm{CRing}\wedge M\in B\right)\wedge \left\{M\right\}=V\left(M\right)\right)\wedge j\in \mathrm{LIdeal}\left(R\right)\right)\wedge M\subseteq j\right)\wedge \neg j={\mathrm{Base}}_R\right)\to \neg j={\mathrm{Base}}_R$$
50	49	neqned	$$⊢\left(\left(\left(\left(\left(R\in \mathrm{CRing}\wedge M\in B\right)\wedge \left\{M\right\}=V\left(M\right)\right)\wedge j\in \mathrm{LIdeal}\left(R\right)\right)\wedge M\subseteq j\right)\wedge \neg j={\mathrm{Base}}_R\right)\to j\ne {\mathrm{Base}}_R$$
51	11	ssmxidl	Could not format ( ( R e. Ring /\ j e. ( LIdeal ` R ) /\ j =/= ( Base ` R ) ) -> E. m e. ( MaxIdeal ` R ) j C_ m ) : No typesetting found for |- ( ( R e. Ring /\ j e. ( LIdeal ` R ) /\ j =/= ( Base ` R ) ) -> E. m e. ( MaxIdeal ` R ) j C_ m ) with typecode |-
52	47 48 50 51	syl3anc	Could not format ( ( ( ( ( ( R e. CRing /\ M e. B ) /\ { M } = ( V ` M ) ) /\ j e. ( LIdeal ` R ) ) /\ M C_ j ) /\ -. j = ( Base ` R ) ) -> E. m e. ( MaxIdeal ` R ) j C_ m ) : No typesetting found for |- ( ( ( ( ( ( R e. CRing /\ M e. B ) /\ { M } = ( V ` M ) ) /\ j e. ( LIdeal ` R ) ) /\ M C_ j ) /\ -. j = ( Base ` R ) ) -> E. m e. ( MaxIdeal ` R ) j C_ m ) with typecode |-
53	46 52	r19.29a	$$⊢\left(\left(\left(\left(\left(R\in \mathrm{CRing}\wedge M\in B\right)\wedge \left\{M\right\}=V\left(M\right)\right)\wedge j\in \mathrm{LIdeal}\left(R\right)\right)\wedge M\subseteq j\right)\wedge \neg j={\mathrm{Base}}_R\right)\to j=M$$
54	53	ex	$$⊢\left(\left(\left(\left(R\in \mathrm{CRing}\wedge M\in B\right)\wedge \left\{M\right\}=V\left(M\right)\right)\wedge j\in \mathrm{LIdeal}\left(R\right)\right)\wedge M\subseteq j\right)\to \left(\neg j={\mathrm{Base}}_R\to j=M\right)$$
55	54	orrd	$$⊢\left(\left(\left(\left(R\in \mathrm{CRing}\wedge M\in B\right)\wedge \left\{M\right\}=V\left(M\right)\right)\wedge j\in \mathrm{LIdeal}\left(R\right)\right)\wedge M\subseteq j\right)\to \left(j={\mathrm{Base}}_R\vee j=M\right)$$
56	55	orcomd	$$⊢\left(\left(\left(\left(R\in \mathrm{CRing}\wedge M\in B\right)\wedge \left\{M\right\}=V\left(M\right)\right)\wedge j\in \mathrm{LIdeal}\left(R\right)\right)\wedge M\subseteq j\right)\to \left(j=M\vee j={\mathrm{Base}}_R\right)$$
57	56	ex	$$⊢\left(\left(\left(R\in \mathrm{CRing}\wedge M\in B\right)\wedge \left\{M\right\}=V\left(M\right)\right)\wedge j\in \mathrm{LIdeal}\left(R\right)\right)\to \left(M\subseteq j\to \left(j=M\vee j={\mathrm{Base}}_R\right)\right)$$
58	57	ralrimiva	$$⊢\left(\left(R\in \mathrm{CRing}\wedge M\in B\right)\wedge \left\{M\right\}=V\left(M\right)\right)\to \forall j\in \mathrm{LIdeal}\left(R\right)\left(M\subseteq j\to \left(j=M\vee j={\mathrm{Base}}_R\right)\right)$$
59	6 15 58	3jca	$$⊢\left(\left(R\in \mathrm{CRing}\wedge M\in B\right)\wedge \left\{M\right\}=V\left(M\right)\right)\to \left(M\in \mathrm{LIdeal}\left(R\right)\wedge M\ne {\mathrm{Base}}_R\wedge \forall j\in \mathrm{LIdeal}\left(R\right)\left(M\subseteq j\to \left(j=M\vee j={\mathrm{Base}}_R\right)\right)\right)$$
60	11	ismxidl	Could not format ( R e. Ring -> ( M e. ( MaxIdeal ` R ) <-> ( M e. ( LIdeal ` R ) /\ M =/= ( Base ` R ) /\ A. j e. ( LIdeal ` R ) ( M C_ j -> ( j = M \/ j = ( Base ` R ) ) ) ) ) ) : No typesetting found for |- ( R e. Ring -> ( M e. ( MaxIdeal ` R ) <-> ( M e. ( LIdeal ` R ) /\ M =/= ( Base ` R ) /\ A. j e. ( LIdeal ` R ) ( M C_ j -> ( j = M \/ j = ( Base ` R ) ) ) ) ) ) with typecode |-
61	60	biimpar	Could not format ( ( R e. Ring /\ ( M e. ( LIdeal ` R ) /\ M =/= ( Base ` R ) /\ A. j e. ( LIdeal ` R ) ( M C_ j -> ( j = M \/ j = ( Base ` R ) ) ) ) ) -> M e. ( MaxIdeal ` R ) ) : No typesetting found for |- ( ( R e. Ring /\ ( M e. ( LIdeal ` R ) /\ M =/= ( Base ` R ) /\ A. j e. ( LIdeal ` R ) ( M C_ j -> ( j = M \/ j = ( Base ` R ) ) ) ) ) -> M e. ( MaxIdeal ` R ) ) with typecode |-
62	4 59 61	syl2anc	Could not format ( ( ( R e. CRing /\ M e. B ) /\ { M } = ( V ` M ) ) -> M e. ( MaxIdeal ` R ) ) : No typesetting found for |- ( ( ( R e. CRing /\ M e. B ) /\ { M } = ( V ` M ) ) -> M e. ( MaxIdeal ` R ) ) with typecode |-
63	1	a1i	Could not format ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) -> V = ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | i C_ j } ) ) : No typesetting found for |- ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) -> V = ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | i C_ j } ) ) with typecode |-
64	26	adantl	Could not format ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ i = M ) -> { j e. ( PrmIdeal ` R ) | i C_ j } = { j e. ( PrmIdeal ` R ) | M C_ j } ) : No typesetting found for |- ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ i = M ) -> { j e. ( PrmIdeal ` R ) | i C_ j } = { j e. ( PrmIdeal ` R ) | M C_ j } ) with typecode |-
65	11	mxidlidl	Could not format ( ( R e. Ring /\ M e. ( MaxIdeal ` R ) ) -> M e. ( LIdeal ` R ) ) : No typesetting found for |- ( ( R e. Ring /\ M e. ( MaxIdeal ` R ) ) -> M e. ( LIdeal ` R ) ) with typecode |-
66	3 65	sylan	Could not format ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) -> M e. ( LIdeal ` R ) ) : No typesetting found for |- ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) -> M e. ( LIdeal ` R ) ) with typecode |-
67	29	a1i	Could not format ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) -> { j e. ( PrmIdeal ` R ) | M C_ j } e. _V ) : No typesetting found for |- ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) -> { j e. ( PrmIdeal ` R ) | M C_ j } e. _V ) with typecode |-
68	63 64 66 67	fvmptd	Could not format ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) -> ( V ` M ) = { j e. ( PrmIdeal ` R ) | M C_ j } ) : No typesetting found for |- ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) -> ( V ` M ) = { j e. ( PrmIdeal ` R ) | M C_ j } ) with typecode |-
69	3	ad2antrr	Could not format ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ ( j e. ( PrmIdeal ` R ) /\ M C_ j ) ) -> R e. Ring ) : No typesetting found for |- ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ ( j e. ( PrmIdeal ` R ) /\ M C_ j ) ) -> R e. Ring ) with typecode |-
70		simplr	Could not format ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ ( j e. ( PrmIdeal ` R ) /\ M C_ j ) ) -> M e. ( MaxIdeal ` R ) ) : No typesetting found for |- ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ ( j e. ( PrmIdeal ` R ) /\ M C_ j ) ) -> M e. ( MaxIdeal ` R ) ) with typecode |-
71		simprl	Could not format ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ ( j e. ( PrmIdeal ` R ) /\ M C_ j ) ) -> j e. ( PrmIdeal ` R ) ) : No typesetting found for |- ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ ( j e. ( PrmIdeal ` R ) /\ M C_ j ) ) -> j e. ( PrmIdeal ` R ) ) with typecode |-
72		prmidlidl	Could not format ( ( R e. Ring /\ j e. ( PrmIdeal ` R ) ) -> j e. ( LIdeal ` R ) ) : No typesetting found for |- ( ( R e. Ring /\ j e. ( PrmIdeal ` R ) ) -> j e. ( LIdeal ` R ) ) with typecode |-
73	69 71 72	syl2anc	Could not format ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ ( j e. ( PrmIdeal ` R ) /\ M C_ j ) ) -> j e. ( LIdeal ` R ) ) : No typesetting found for |- ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ ( j e. ( PrmIdeal ` R ) /\ M C_ j ) ) -> j e. ( LIdeal ` R ) ) with typecode |-
74		simprr	Could not format ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ ( j e. ( PrmIdeal ` R ) /\ M C_ j ) ) -> M C_ j ) : No typesetting found for |- ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ ( j e. ( PrmIdeal ` R ) /\ M C_ j ) ) -> M C_ j ) with typecode |-
75	73 74	jca	Could not format ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ ( j e. ( PrmIdeal ` R ) /\ M C_ j ) ) -> ( j e. ( LIdeal ` R ) /\ M C_ j ) ) : No typesetting found for |- ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ ( j e. ( PrmIdeal ` R ) /\ M C_ j ) ) -> ( j e. ( LIdeal ` R ) /\ M C_ j ) ) with typecode |-
76	11	mxidlmax	Could not format ( ( ( R e. Ring /\ M e. ( MaxIdeal ` R ) ) /\ ( j e. ( LIdeal ` R ) /\ M C_ j ) ) -> ( j = M \/ j = ( Base ` R ) ) ) : No typesetting found for |- ( ( ( R e. Ring /\ M e. ( MaxIdeal ` R ) ) /\ ( j e. ( LIdeal ` R ) /\ M C_ j ) ) -> ( j = M \/ j = ( Base ` R ) ) ) with typecode |-
77	69 70 75 76	syl21anc	Could not format ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ ( j e. ( PrmIdeal ` R ) /\ M C_ j ) ) -> ( j = M \/ j = ( Base ` R ) ) ) : No typesetting found for |- ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ ( j e. ( PrmIdeal ` R ) /\ M C_ j ) ) -> ( j = M \/ j = ( Base ` R ) ) ) with typecode |-
78		eqid	$$⊢{\cdot }_R={\cdot }_R$$
79	11 78	prmidlnr	Could not format ( ( R e. Ring /\ j e. ( PrmIdeal ` R ) ) -> j =/= ( Base ` R ) ) : No typesetting found for |- ( ( R e. Ring /\ j e. ( PrmIdeal ` R ) ) -> j =/= ( Base ` R ) ) with typecode |-
80	69 71 79	syl2anc	Could not format ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ ( j e. ( PrmIdeal ` R ) /\ M C_ j ) ) -> j =/= ( Base ` R ) ) : No typesetting found for |- ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ ( j e. ( PrmIdeal ` R ) /\ M C_ j ) ) -> j =/= ( Base ` R ) ) with typecode |-
81	80	neneqd	Could not format ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ ( j e. ( PrmIdeal ` R ) /\ M C_ j ) ) -> -. j = ( Base ` R ) ) : No typesetting found for |- ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ ( j e. ( PrmIdeal ` R ) /\ M C_ j ) ) -> -. j = ( Base ` R ) ) with typecode |-
82	77 81	olcnd	Could not format ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ ( j e. ( PrmIdeal ` R ) /\ M C_ j ) ) -> j = M ) : No typesetting found for |- ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ ( j e. ( PrmIdeal ` R ) /\ M C_ j ) ) -> j = M ) with typecode |-
83		simpr	Could not format ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ j = M ) -> j = M ) : No typesetting found for |- ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ j = M ) -> j = M ) with typecode |-
84	19	mxidlprm	Could not format ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) -> M e. ( PrmIdeal ` R ) ) : No typesetting found for |- ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) -> M e. ( PrmIdeal ` R ) ) with typecode |-
85	84	adantr	Could not format ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ j = M ) -> M e. ( PrmIdeal ` R ) ) : No typesetting found for |- ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ j = M ) -> M e. ( PrmIdeal ` R ) ) with typecode |-
86	83 85	eqeltrd	Could not format ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ j = M ) -> j e. ( PrmIdeal ` R ) ) : No typesetting found for |- ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ j = M ) -> j e. ( PrmIdeal ` R ) ) with typecode |-
87		ssidd	Could not format ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ j = M ) -> j C_ j ) : No typesetting found for |- ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ j = M ) -> j C_ j ) with typecode |-
88	83 87	eqsstrrd	Could not format ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ j = M ) -> M C_ j ) : No typesetting found for |- ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ j = M ) -> M C_ j ) with typecode |-
89	86 88	jca	Could not format ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ j = M ) -> ( j e. ( PrmIdeal ` R ) /\ M C_ j ) ) : No typesetting found for |- ( ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) /\ j = M ) -> ( j e. ( PrmIdeal ` R ) /\ M C_ j ) ) with typecode |-
90	82 89	impbida	Could not format ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) -> ( ( j e. ( PrmIdeal ` R ) /\ M C_ j ) <-> j = M ) ) : No typesetting found for |- ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) -> ( ( j e. ( PrmIdeal ` R ) /\ M C_ j ) <-> j = M ) ) with typecode |-
91	90	alrimiv	Could not format ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) -> A. j ( ( j e. ( PrmIdeal ` R ) /\ M C_ j ) <-> j = M ) ) : No typesetting found for |- ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) -> A. j ( ( j e. ( PrmIdeal ` R ) /\ M C_ j ) <-> j = M ) ) with typecode |-
92	91 33	sylibr	Could not format ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) -> { j e. ( PrmIdeal ` R ) | M C_ j } = { M } ) : No typesetting found for |- ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) -> { j e. ( PrmIdeal ` R ) | M C_ j } = { M } ) with typecode |-
93	68 92	eqtr2d	Could not format ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) -> { M } = ( V ` M ) ) : No typesetting found for |- ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) ) -> { M } = ( V ` M ) ) with typecode |-
94	93	adantlr	Could not format ( ( ( R e. CRing /\ M e. B ) /\ M e. ( MaxIdeal ` R ) ) -> { M } = ( V ` M ) ) : No typesetting found for |- ( ( ( R e. CRing /\ M e. B ) /\ M e. ( MaxIdeal ` R ) ) -> { M } = ( V ` M ) ) with typecode |-
95	62 94	impbida	Could not format ( ( R e. CRing /\ M e. B ) -> ( { M } = ( V ` M ) <-> M e. ( MaxIdeal ` R ) ) ) : No typesetting found for |- ( ( R e. CRing /\ M e. B ) -> ( { M } = ( V ` M ) <-> M e. ( MaxIdeal ` R ) ) ) with typecode |-