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		snnzg	$$⊢M\in B\to \left\{M\right\}\ne \varnothing$$
9	5 8	syl	$$⊢\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$$
10	7 9	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$$
11		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}$$
12		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
13	1 12	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)$$
14	13	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)$$
15	11 6 14	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)$$
16	10 15	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$$
17		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 |-
18	11	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 |-
19		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 |-
20		eqid	$$⊢\mathrm{LSSum}\left({\mathrm{mulGrp}}_R\right)=\mathrm{LSSum}\left({\mathrm{mulGrp}}_R\right)$$
21	20	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 |-
22	18 19 21	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 |-
23		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 |-
24	23 17	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 |-
25	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 |-
26		sseq1	$$⊢i=M\to \left(i\subseteq j\leftrightarrow M\subseteq j\right)$$
27	26	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 |-
28	27	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 |-
29		fvex	Could not format ( PrmIdeal ` R ) e. _V : No typesetting found for |- ( PrmIdeal ` R ) e. _V with typecode |-
30	29	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 |-
31	30	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 |-
32	25 28 6 31	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 |-
33	7 32	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 |-
34		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 |-
35	33 34	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 |-
36	35	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 |-
37		vex	$$⊢m\in \mathrm{V}$$
38		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 |-
39		sseq2	$$⊢j=m\to \left(M\subseteq j\leftrightarrow M\subseteq m\right)$$
40	38 39	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 |-
41		eqeq1	$$⊢j=m\to \left(j=M\leftrightarrow m=M\right)$$
42	40 41	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 |-
43	37 42	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 |-
44	36 43	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 |-
45	22 24 44	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 |-
46	17 45	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 |-
47	46 23	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 |-
48	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}$$
49		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)$$
50		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$$
51	50	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$$
52	12	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 |-
53	48 49 51 52	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 |-
54	47 53	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$$
55	54	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)$$
56	55	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)$$
57	56	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)$$
58	57	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)$$
59	58	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)$$
60	6 16 59	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)$$
61	12	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 |-
62	61	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 |-
63	4 60 62	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 |-
64	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 |-
65	27	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 |-
66	12	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 |-
67	3 66	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 |-
68	30	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 |-
69	64 65 67 68	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 |-
70	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 |-
71		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 |-
72		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 |-
73		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 |-
74	70 72 73	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 |-
75		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 |-
76	74 75	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 |-
77	12	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 |-
78	70 71 76 77	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 |-
79		eqid	$$⊢{\cdot }_R={\cdot }_R$$
80	12 79	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 |-
81	70 72 80	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 |-
82	81	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 |-
83	78 82	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 |-
84		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 |-
85	20	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 |-
86	85	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 |-
87	84 86	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 |-
88		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 |-
89	84 88	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 |-
90	87 89	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 |-
91	83 90	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 |-
92	91	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 |-
93	92 34	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 |-
94	69 93	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 |-
95	94	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 |-
96	63 95	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 |-