Theorem isprmidlc

Description: The predicate "is prime ideal" for commutative rings. Alternate definition for commutative rings. See definition in Lang p. 92. (Contributed by Jeff Madsen, 19-Jun-2010) (Revised by Thierry Arnoux, 12-Jan-2024)

	Ref	Expression
Hypotheses	isprmidlc.1	$$⊢B={\mathrm{Base}}_R$$
	isprmidlc.2	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
Assertion	isprmidlc	Could not format assertion : No typesetting found for |- ( R e. CRing -> ( P e. ( PrmIdeal ` R ) <-> ( P e. ( LIdeal ` R ) /\ P =/= B /\ A. x e. B A. y e. B ( ( x .x. y ) e. P -> ( x e. P \/ y e. P ) ) ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		isprmidlc.1	$$⊢B={\mathrm{Base}}_R$$
2		isprmidlc.2	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
3		crngring	$$⊢R\in \mathrm{CRing}\to R\in \mathrm{Ring}$$
4		prmidlidl	Could not format ( ( R e. Ring /\ P e. ( PrmIdeal ` R ) ) -> P e. ( LIdeal ` R ) ) : No typesetting found for |- ( ( R e. Ring /\ P e. ( PrmIdeal ` R ) ) -> P e. ( LIdeal ` R ) ) with typecode |-
5	3 4	sylan	Could not format ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) -> P e. ( LIdeal ` R ) ) : No typesetting found for |- ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) -> P e. ( LIdeal ` R ) ) with typecode |-
6	1 2	prmidlnr	Could not format ( ( R e. Ring /\ P e. ( PrmIdeal ` R ) ) -> P =/= B ) : No typesetting found for |- ( ( R e. Ring /\ P e. ( PrmIdeal ` R ) ) -> P =/= B ) with typecode |-
7	3 6	sylan	Could not format ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) -> P =/= B ) : No typesetting found for |- ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) -> P =/= B ) with typecode |-
8	3	ad4antr	Could not format ( ( ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ ( x .x. y ) e. P ) -> R e. Ring ) : No typesetting found for |- ( ( ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ ( x .x. y ) e. P ) -> R e. Ring ) with typecode |-
9		simp-4r	Could not format ( ( ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ ( x .x. y ) e. P ) -> P e. ( PrmIdeal ` R ) ) : No typesetting found for |- ( ( ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ ( x .x. y ) e. P ) -> P e. ( PrmIdeal ` R ) ) with typecode |-
10		simpllr	Could not format ( ( ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ ( x .x. y ) e. P ) -> x e. B ) : No typesetting found for |- ( ( ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ ( x .x. y ) e. P ) -> x e. B ) with typecode |-
11	10	snssd	Could not format ( ( ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ ( x .x. y ) e. P ) -> { x } C_ B ) : No typesetting found for |- ( ( ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ ( x .x. y ) e. P ) -> { x } C_ B ) with typecode |-
12		eqid	$$⊢\mathrm{RSpan}\left(R\right)=\mathrm{RSpan}\left(R\right)$$
13		eqid	$$⊢\mathrm{LIdeal}\left(R\right)=\mathrm{LIdeal}\left(R\right)$$
14	12 1 13	rspcl	$$⊢\left(R\in \mathrm{Ring}\wedge \left\{x\right\}\subseteq B\right)\to \mathrm{RSpan}\left(R\right)\left(\left\{x\right\}\right)\in \mathrm{LIdeal}\left(R\right)$$
15	8 11 14	syl2anc	Could not format ( ( ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ ( x .x. y ) e. P ) -> ( ( RSpan ` R ) ` { x } ) e. ( LIdeal ` R ) ) : No typesetting found for |- ( ( ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ ( x .x. y ) e. P ) -> ( ( RSpan ` R ) ` { x } ) e. ( LIdeal ` R ) ) with typecode |-
16		simplr	Could not format ( ( ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ ( x .x. y ) e. P ) -> y e. B ) : No typesetting found for |- ( ( ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ ( x .x. y ) e. P ) -> y e. B ) with typecode |-
17	16	snssd	Could not format ( ( ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ ( x .x. y ) e. P ) -> { y } C_ B ) : No typesetting found for |- ( ( ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ ( x .x. y ) e. P ) -> { y } C_ B ) with typecode |-
18	12 1 13	rspcl	$$⊢\left(R\in \mathrm{Ring}\wedge \left\{y\right\}\subseteq B\right)\to \mathrm{RSpan}\left(R\right)\left(\left\{y\right\}\right)\in \mathrm{LIdeal}\left(R\right)$$
19	8 17 18	syl2anc	Could not format ( ( ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ ( x .x. y ) e. P ) -> ( ( RSpan ` R ) ` { y } ) e. ( LIdeal ` R ) ) : No typesetting found for |- ( ( ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ ( x .x. y ) e. P ) -> ( ( RSpan ` R ) ` { y } ) e. ( LIdeal ` R ) ) with typecode |-
20	15 19	jca	Could not format ( ( ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ ( x .x. y ) e. P ) -> ( ( ( RSpan ` R ) ` { x } ) e. ( LIdeal ` R ) /\ ( ( RSpan ` R ) ` { y } ) e. ( LIdeal ` R ) ) ) : No typesetting found for |- ( ( ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ ( x .x. y ) e. P ) -> ( ( ( RSpan ` R ) ` { x } ) e. ( LIdeal ` R ) /\ ( ( RSpan ` R ) ` { y } ) e. ( LIdeal ` R ) ) ) with typecode |-
21		simpllr	Could not format ( ( ( ( ( ( ( ( ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ ( x .x. y ) e. P ) /\ r e. ( ( RSpan ` R ) ` { x } ) ) /\ s e. ( ( RSpan ` R ) ` { y } ) ) /\ m e. B ) /\ r = ( m .x. x ) ) /\ n e. B ) /\ s = ( n .x. y ) ) -> r = ( m .x. x ) ) : No typesetting found for |- ( ( ( ( ( ( ( ( ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ ( x .x. y ) e. P ) /\ r e. ( ( RSpan ` R ) ` { x } ) ) /\ s e. ( ( RSpan ` R ) ` { y } ) ) /\ m e. B ) /\ r = ( m .x. x ) ) /\ n e. B ) /\ s = ( n .x. y ) ) -> r = ( m .x. x ) ) with typecode |-
22		simpr	Could not format ( ( ( ( ( ( ( ( ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ ( x .x. y ) e. P ) /\ r e. ( ( RSpan ` R ) ` { x } ) ) /\ s e. ( ( RSpan ` R ) ` { y } ) ) /\ m e. B ) /\ r = ( m .x. x ) ) /\ n e. B ) /\ s = ( n .x. y ) ) -> s = ( n .x. y ) ) : No typesetting found for |- ( ( ( ( ( ( ( ( ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ ( x .x. y ) e. P ) /\ r e. ( ( RSpan ` R ) ` { x } ) ) /\ s e. ( ( RSpan ` R ) ` { y } ) ) /\ m e. B ) /\ r = ( m .x. x ) ) /\ n e. B ) /\ s = ( n .x. y ) ) -> s = ( n .x. y ) ) with typecode |-
23	21 22	oveq12d	Could not format ( ( ( ( ( ( ( ( ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ ( x .x. y ) e. P ) /\ r e. ( ( RSpan ` R ) ` { x } ) ) /\ s e. ( ( RSpan ` R ) ` { y } ) ) /\ m e. B ) /\ r = ( m .x. x ) ) /\ n e. B ) /\ s = ( n .x. y ) ) -> ( r .x. s ) = ( ( m .x. x ) .x. ( n .x. y ) ) ) : No typesetting found for |- ( ( ( ( ( ( ( ( ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ ( x .x. y ) e. P ) /\ r e. ( ( RSpan ` R ) ` { x } ) ) /\ s e. ( ( RSpan ` R ) ` { y } ) ) /\ m e. B ) /\ r = ( m .x. x ) ) /\ n e. B ) /\ s = ( n .x. y ) ) -> ( r .x. s ) = ( ( m .x. x ) .x. ( n .x. y ) ) ) with typecode |-
24		simp-10l	Could not format ( ( ( ( ( ( ( ( ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ ( x .x. y ) e. P ) /\ r e. ( ( RSpan ` R ) ` { x } ) ) /\ s e. ( ( RSpan ` R ) ` { y } ) ) /\ m e. B ) /\ r = ( m .x. x ) ) /\ n e. B ) /\ s = ( n .x. y ) ) -> R e. CRing ) : No typesetting found for |- ( ( ( ( ( ( ( ( ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ ( x .x. y ) e. P ) /\ r e. ( ( RSpan ` R ) ` { x } ) ) /\ s e. ( ( RSpan ` R ) ` { y } ) ) /\ m e. B ) /\ r = ( m .x. x ) ) /\ n e. B ) /\ s = ( n .x. y ) ) -> R e. CRing ) with typecode |-
25		simp-4r	Could not format ( ( ( ( ( ( ( ( ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ ( x .x. y ) e. P ) /\ r e. ( ( RSpan ` R ) ` { x } ) ) /\ s e. ( ( RSpan ` R ) ` { y } ) ) /\ m e. B ) /\ r = ( m .x. x ) ) /\ n e. B ) /\ s = ( n .x. y ) ) -> m e. B ) : No typesetting found for |- ( ( ( ( ( ( ( ( ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ ( x .x. y ) e. P ) /\ r e. ( ( RSpan ` R ) ` { x } ) ) /\ s e. ( ( RSpan ` R ) ` { y } ) ) /\ m e. B ) /\ r = ( m .x. x ) ) /\ n e. B ) /\ s = ( n .x. y ) ) -> m e. B ) with typecode |-
26	10	ad2antrr	Could not format ( ( ( ( ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ ( x .x. y ) e. P ) /\ r e. ( ( RSpan ` R ) ` { x } ) ) /\ s e. ( ( RSpan ` R ) ` { y } ) ) -> x e. B ) : No typesetting found for |- ( ( ( ( ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ ( x .x. y ) e. P ) /\ r e. ( ( RSpan ` R ) ` { x } ) ) /\ s e. ( ( RSpan ` R ) ` { y } ) ) -> x e. B ) with typecode |-
27	26	ad4antr	Could not format ( ( ( ( ( ( ( ( ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ ( x .x. y ) e. P ) /\ r e. ( ( RSpan ` R ) ` { x } ) ) /\ s e. ( ( RSpan ` R ) ` { y } ) ) /\ m e. B ) /\ r = ( m .x. x ) ) /\ n e. B ) /\ s = ( n .x. y ) ) -> x e. B ) : No typesetting found for |- ( ( ( ( ( ( ( ( ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ ( x .x. y ) e. P ) /\ r e. ( ( RSpan ` R ) ` { x } ) ) /\ s e. ( ( RSpan ` R ) ` { y } ) ) /\ m e. B ) /\ r = ( m .x. x ) ) /\ n e. B ) /\ s = ( n .x. y ) ) -> x e. B ) with typecode |-
28		simplr	Could not format ( ( ( ( ( ( ( ( ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ ( x .x. y ) e. P ) /\ r e. ( ( RSpan ` R ) ` { x } ) ) /\ s e. ( ( RSpan ` R ) ` { y } ) ) /\ m e. B ) /\ r = ( m .x. x ) ) /\ n e. B ) /\ s = ( n .x. y ) ) -> n e. B ) : No typesetting found for |- ( ( ( ( ( ( ( ( ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ ( x .x. y ) e. P ) /\ r e. ( ( RSpan ` R ) ` { x } ) ) /\ s e. ( ( RSpan ` R ) ` { y } ) ) /\ m e. B ) /\ r = ( m .x. x ) ) /\ n e. B ) /\ s = ( n .x. y ) ) -> n e. B ) with typecode |-
29	16	ad4antr	Could not format ( ( ( ( ( ( ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ ( x .x. y ) e. P ) /\ r e. ( ( RSpan ` R ) ` { x } ) ) /\ s e. ( ( RSpan ` R ) ` { y } ) ) /\ m e. B ) /\ r = ( m .x. x ) ) -> y e. B ) : No typesetting found for |- ( ( ( ( ( ( ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ ( x .x. y ) e. P ) /\ r e. ( ( RSpan ` R ) ` { x } ) ) /\ s e. ( ( RSpan ` R ) ` { y } ) ) /\ m e. B ) /\ r = ( m .x. x ) ) -> y e. B ) with typecode |-
30	29	ad2antrr	Could not format ( ( ( ( ( ( ( ( ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ ( x .x. y ) e. P ) /\ r e. ( ( RSpan ` R ) ` { x } ) ) /\ s e. ( ( RSpan ` R ) ` { y } ) ) /\ m e. B ) /\ r = ( m .x. x ) ) /\ n e. B ) /\ s = ( n .x. y ) ) -> y e. B ) : No typesetting found for |- ( ( ( ( ( ( ( ( ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ ( x .x. y ) e. P ) /\ r e. ( ( RSpan ` R ) ` { x } ) ) /\ s e. ( ( RSpan ` R ) ` { y } ) ) /\ m e. B ) /\ r = ( m .x. x ) ) /\ n e. B ) /\ s = ( n .x. y ) ) -> y e. B ) with typecode |-
31	1 2	cringm4	$$⊢\left(R\in \mathrm{CRing}\wedge \left(m\in B\wedge x\in B\right)\wedge \left(n\in B\wedge y\in B\right)\right)\to \left(m\underset{\dot{}}{·}x\right)\underset{\dot{}}{·}\left(n\underset{\dot{}}{·}y\right)=\left(m\underset{\dot{}}{·}n\right)\underset{\dot{}}{·}\left(x\underset{\dot{}}{·}y\right)$$
32	24 25 27 28 30 31	syl122anc	Could not format ( ( ( ( ( ( ( ( ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ ( x .x. y ) e. P ) /\ r e. ( ( RSpan ` R ) ` { x } ) ) /\ s e. ( ( RSpan ` R ) ` { y } ) ) /\ m e. B ) /\ r = ( m .x. x ) ) /\ n e. B ) /\ s = ( n .x. y ) ) -> ( ( m .x. x ) .x. ( n .x. y ) ) = ( ( m .x. n ) .x. ( x .x. y ) ) ) : No typesetting found for |- ( ( ( ( ( ( ( ( ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ ( x .x. y ) e. P ) /\ r e. ( ( RSpan ` R ) ` { x } ) ) /\ s e. ( ( RSpan ` R ) ` { y } ) ) /\ m e. B ) /\ r = ( m .x. x ) ) /\ n e. B ) /\ s = ( n .x. y ) ) -> ( ( m .x. x ) .x. ( n .x. y ) ) = ( ( m .x. n ) .x. ( x .x. y ) ) ) with typecode |-
33	24 3	syl	Could not format ( ( ( ( ( ( ( ( ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ ( x .x. y ) e. P ) /\ r e. ( ( RSpan ` R ) ` { x } ) ) /\ s e. ( ( RSpan ` R ) ` { y } ) ) /\ m e. B ) /\ r = ( m .x. x ) ) /\ n e. B ) /\ s = ( n .x. y ) ) -> R e. Ring ) : No typesetting found for |- ( ( ( ( ( ( ( ( ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ ( x .x. y ) e. P ) /\ r e. ( ( RSpan ` R ) ` { x } ) ) /\ s e. ( ( RSpan ` R ) ` { y } ) ) /\ m e. B ) /\ r = ( m .x. x ) ) /\ n e. B ) /\ s = ( n .x. y ) ) -> R e. Ring ) with typecode |-
34	5	ad9antr	Could not format ( ( ( ( ( ( ( ( ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ ( x .x. y ) e. P ) /\ r e. ( ( RSpan ` R ) ` { x } ) ) /\ s e. ( ( RSpan ` R ) ` { y } ) ) /\ m e. B ) /\ r = ( m .x. x ) ) /\ n e. B ) /\ s = ( n .x. y ) ) -> P e. ( LIdeal ` R ) ) : No typesetting found for |- ( ( ( ( ( ( ( ( ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ ( x .x. y ) e. P ) /\ r e. ( ( RSpan ` R ) ` { x } ) ) /\ s e. ( ( RSpan ` R ) ` { y } ) ) /\ m e. B ) /\ r = ( m .x. x ) ) /\ n e. B ) /\ s = ( n .x. y ) ) -> P e. ( LIdeal ` R ) ) with typecode |-
35	1 2	ringcl	$$⊢\left(R\in \mathrm{Ring}\wedge m\in B\wedge n\in B\right)\to m\underset{\dot{}}{·}n\in B$$
36	33 25 28 35	syl3anc	Could not format ( ( ( ( ( ( ( ( ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ ( x .x. y ) e. P ) /\ r e. ( ( RSpan ` R ) ` { x } ) ) /\ s e. ( ( RSpan ` R ) ` { y } ) ) /\ m e. B ) /\ r = ( m .x. x ) ) /\ n e. B ) /\ s = ( n .x. y ) ) -> ( m .x. n ) e. B ) : No typesetting found for |- ( ( ( ( ( ( ( ( ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ ( x .x. y ) e. P ) /\ r e. ( ( RSpan ` R ) ` { x } ) ) /\ s e. ( ( RSpan ` R ) ` { y } ) ) /\ m e. B ) /\ r = ( m .x. x ) ) /\ n e. B ) /\ s = ( n .x. y ) ) -> ( m .x. n ) e. B ) with typecode |-
37		simp-7r	Could not format ( ( ( ( ( ( ( ( ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ ( x .x. y ) e. P ) /\ r e. ( ( RSpan ` R ) ` { x } ) ) /\ s e. ( ( RSpan ` R ) ` { y } ) ) /\ m e. B ) /\ r = ( m .x. x ) ) /\ n e. B ) /\ s = ( n .x. y ) ) -> ( x .x. y ) e. P ) : No typesetting found for |- ( ( ( ( ( ( ( ( ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ ( x .x. y ) e. P ) /\ r e. ( ( RSpan ` R ) ` { x } ) ) /\ s e. ( ( RSpan ` R ) ` { y } ) ) /\ m e. B ) /\ r = ( m .x. x ) ) /\ n e. B ) /\ s = ( n .x. y ) ) -> ( x .x. y ) e. P ) with typecode |-
38	13 1 2	lidlmcl	$$⊢\left(\left(R\in \mathrm{Ring}\wedge P\in \mathrm{LIdeal}\left(R\right)\right)\wedge \left(m\underset{\dot{}}{·}n\in B\wedge x\underset{\dot{}}{·}y\in P\right)\right)\to \left(m\underset{\dot{}}{·}n\right)\underset{\dot{}}{·}\left(x\underset{\dot{}}{·}y\right)\in P$$
39	33 34 36 37 38	syl22anc	Could not format ( ( ( ( ( ( ( ( ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ ( x .x. y ) e. P ) /\ r e. ( ( RSpan ` R ) ` { x } ) ) /\ s e. ( ( RSpan ` R ) ` { y } ) ) /\ m e. B ) /\ r = ( m .x. x ) ) /\ n e. B ) /\ s = ( n .x. y ) ) -> ( ( m .x. n ) .x. ( x .x. y ) ) e. P ) : No typesetting found for |- ( ( ( ( ( ( ( ( ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ ( x .x. y ) e. P ) /\ r e. ( ( RSpan ` R ) ` { x } ) ) /\ s e. ( ( RSpan ` R ) ` { y } ) ) /\ m e. B ) /\ r = ( m .x. x ) ) /\ n e. B ) /\ s = ( n .x. y ) ) -> ( ( m .x. n ) .x. ( x .x. y ) ) e. P ) with typecode |-
40	32 39	eqeltrd	Could not format ( ( ( ( ( ( ( ( ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ ( x .x. y ) e. P ) /\ r e. ( ( RSpan ` R ) ` { x } ) ) /\ s e. ( ( RSpan ` R ) ` { y } ) ) /\ m e. B ) /\ r = ( m .x. x ) ) /\ n e. B ) /\ s = ( n .x. y ) ) -> ( ( m .x. x ) .x. ( n .x. y ) ) e. P ) : No typesetting found for |- ( ( ( ( ( ( ( ( ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ ( x .x. y ) e. P ) /\ r e. ( ( RSpan ` R ) ` { x } ) ) /\ s e. ( ( RSpan ` R ) ` { y } ) ) /\ m e. B ) /\ r = ( m .x. x ) ) /\ n e. B ) /\ s = ( n .x. y ) ) -> ( ( m .x. x ) .x. ( n .x. y ) ) e. P ) with typecode |-
41	23 40	eqeltrd	Could not format ( ( ( ( ( ( ( ( ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ ( x .x. y ) e. P ) /\ r e. ( ( RSpan ` R ) ` { x } ) ) /\ s e. ( ( RSpan ` R ) ` { y } ) ) /\ m e. B ) /\ r = ( m .x. x ) ) /\ n e. B ) /\ s = ( n .x. y ) ) -> ( r .x. s ) e. P ) : No typesetting found for |- ( ( ( ( ( ( ( ( ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ ( x .x. y ) e. P ) /\ r e. ( ( RSpan ` R ) ` { x } ) ) /\ s e. ( ( RSpan ` R ) ` { y } ) ) /\ m e. B ) /\ r = ( m .x. x ) ) /\ n e. B ) /\ s = ( n .x. y ) ) -> ( r .x. s ) e. P ) with typecode |-
42	8	ad2antrr	Could not format ( ( ( ( ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ ( x .x. y ) e. P ) /\ r e. ( ( RSpan ` R ) ` { x } ) ) /\ s e. ( ( RSpan ` R ) ` { y } ) ) -> R e. Ring ) : No typesetting found for |- ( ( ( ( ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ ( x .x. y ) e. P ) /\ r e. ( ( RSpan ` R ) ` { x } ) ) /\ s e. ( ( RSpan ` R ) ` { y } ) ) -> R e. Ring ) with typecode |-
43	42	ad2antrr	Could not format ( ( ( ( ( ( ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ ( x .x. y ) e. P ) /\ r e. ( ( RSpan ` R ) ` { x } ) ) /\ s e. ( ( RSpan ` R ) ` { y } ) ) /\ m e. B ) /\ r = ( m .x. x ) ) -> R e. Ring ) : No typesetting found for |- ( ( ( ( ( ( ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ ( x .x. y ) e. P ) /\ r e. ( ( RSpan ` R ) ` { x } ) ) /\ s e. ( ( RSpan ` R ) ` { y } ) ) /\ m e. B ) /\ r = ( m .x. x ) ) -> R e. Ring ) with typecode |-
44		simpllr	Could not format ( ( ( ( ( ( ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ ( x .x. y ) e. P ) /\ r e. ( ( RSpan ` R ) ` { x } ) ) /\ s e. ( ( RSpan ` R ) ` { y } ) ) /\ m e. B ) /\ r = ( m .x. x ) ) -> s e. ( ( RSpan ` R ) ` { y } ) ) : No typesetting found for |- ( ( ( ( ( ( ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ ( x .x. y ) e. P ) /\ r e. ( ( RSpan ` R ) ` { x } ) ) /\ s e. ( ( RSpan ` R ) ` { y } ) ) /\ m e. B ) /\ r = ( m .x. x ) ) -> s e. ( ( RSpan ` R ) ` { y } ) ) with typecode |-
45	1 2 12	rspsnel	$$⊢\left(R\in \mathrm{Ring}\wedge y\in B\right)\to \left(s\in \mathrm{RSpan}\left(R\right)\left(\left\{y\right\}\right)\leftrightarrow \exists n\in Bs=n\underset{\dot{}}{·}y\right)$$
46	45	biimpa	$$⊢\left(\left(R\in \mathrm{Ring}\wedge y\in B\right)\wedge s\in \mathrm{RSpan}\left(R\right)\left(\left\{y\right\}\right)\right)\to \exists n\in Bs=n\underset{\dot{}}{·}y$$
47	43 29 44 46	syl21anc	Could not format ( ( ( ( ( ( ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ ( x .x. y ) e. P ) /\ r e. ( ( RSpan ` R ) ` { x } ) ) /\ s e. ( ( RSpan ` R ) ` { y } ) ) /\ m e. B ) /\ r = ( m .x. x ) ) -> E. n e. B s = ( n .x. y ) ) : No typesetting found for |- ( ( ( ( ( ( ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ ( x .x. y ) e. P ) /\ r e. ( ( RSpan ` R ) ` { x } ) ) /\ s e. ( ( RSpan ` R ) ` { y } ) ) /\ m e. B ) /\ r = ( m .x. x ) ) -> E. n e. B s = ( n .x. y ) ) with typecode |-
48	41 47	r19.29a	Could not format ( ( ( ( ( ( ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ ( x .x. y ) e. P ) /\ r e. ( ( RSpan ` R ) ` { x } ) ) /\ s e. ( ( RSpan ` R ) ` { y } ) ) /\ m e. B ) /\ r = ( m .x. x ) ) -> ( r .x. s ) e. P ) : No typesetting found for |- ( ( ( ( ( ( ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ ( x .x. y ) e. P ) /\ r e. ( ( RSpan ` R ) ` { x } ) ) /\ s e. ( ( RSpan ` R ) ` { y } ) ) /\ m e. B ) /\ r = ( m .x. x ) ) -> ( r .x. s ) e. P ) with typecode |-
49		simplr	Could not format ( ( ( ( ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ ( x .x. y ) e. P ) /\ r e. ( ( RSpan ` R ) ` { x } ) ) /\ s e. ( ( RSpan ` R ) ` { y } ) ) -> r e. ( ( RSpan ` R ) ` { x } ) ) : No typesetting found for |- ( ( ( ( ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ ( x .x. y ) e. P ) /\ r e. ( ( RSpan ` R ) ` { x } ) ) /\ s e. ( ( RSpan ` R ) ` { y } ) ) -> r e. ( ( RSpan ` R ) ` { x } ) ) with typecode |-
50	1 2 12	rspsnel	$$⊢\left(R\in \mathrm{Ring}\wedge x\in B\right)\to \left(r\in \mathrm{RSpan}\left(R\right)\left(\left\{x\right\}\right)\leftrightarrow \exists m\in Br=m\underset{\dot{}}{·}x\right)$$
51	50	biimpa	$$⊢\left(\left(R\in \mathrm{Ring}\wedge x\in B\right)\wedge r\in \mathrm{RSpan}\left(R\right)\left(\left\{x\right\}\right)\right)\to \exists m\in Br=m\underset{\dot{}}{·}x$$
52	42 26 49 51	syl21anc	Could not format ( ( ( ( ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ ( x .x. y ) e. P ) /\ r e. ( ( RSpan ` R ) ` { x } ) ) /\ s e. ( ( RSpan ` R ) ` { y } ) ) -> E. m e. B r = ( m .x. x ) ) : No typesetting found for |- ( ( ( ( ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ ( x .x. y ) e. P ) /\ r e. ( ( RSpan ` R ) ` { x } ) ) /\ s e. ( ( RSpan ` R ) ` { y } ) ) -> E. m e. B r = ( m .x. x ) ) with typecode |-
53	48 52	r19.29a	Could not format ( ( ( ( ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ ( x .x. y ) e. P ) /\ r e. ( ( RSpan ` R ) ` { x } ) ) /\ s e. ( ( RSpan ` R ) ` { y } ) ) -> ( r .x. s ) e. P ) : No typesetting found for |- ( ( ( ( ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ ( x .x. y ) e. P ) /\ r e. ( ( RSpan ` R ) ` { x } ) ) /\ s e. ( ( RSpan ` R ) ` { y } ) ) -> ( r .x. s ) e. P ) with typecode |-
54	53	anasss	Could not format ( ( ( ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ ( x .x. y ) e. P ) /\ ( r e. ( ( RSpan ` R ) ` { x } ) /\ s e. ( ( RSpan ` R ) ` { y } ) ) ) -> ( r .x. s ) e. P ) : No typesetting found for |- ( ( ( ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ ( x .x. y ) e. P ) /\ ( r e. ( ( RSpan ` R ) ` { x } ) /\ s e. ( ( RSpan ` R ) ` { y } ) ) ) -> ( r .x. s ) e. P ) with typecode |-
55	54	ralrimivva	Could not format ( ( ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ ( x .x. y ) e. P ) -> A. r e. ( ( RSpan ` R ) ` { x } ) A. s e. ( ( RSpan ` R ) ` { y } ) ( r .x. s ) e. P ) : No typesetting found for |- ( ( ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ ( x .x. y ) e. P ) -> A. r e. ( ( RSpan ` R ) ` { x } ) A. s e. ( ( RSpan ` R ) ` { y } ) ( r .x. s ) e. P ) with typecode |-
56	1 2	prmidl	Could not format ( ( ( ( R e. Ring /\ P e. ( PrmIdeal ` R ) ) /\ ( ( ( RSpan ` R ) ` { x } ) e. ( LIdeal ` R ) /\ ( ( RSpan ` R ) ` { y } ) e. ( LIdeal ` R ) ) ) /\ A. r e. ( ( RSpan ` R ) ` { x } ) A. s e. ( ( RSpan ` R ) ` { y } ) ( r .x. s ) e. P ) -> ( ( ( RSpan ` R ) ` { x } ) C_ P \/ ( ( RSpan ` R ) ` { y } ) C_ P ) ) : No typesetting found for |- ( ( ( ( R e. Ring /\ P e. ( PrmIdeal ` R ) ) /\ ( ( ( RSpan ` R ) ` { x } ) e. ( LIdeal ` R ) /\ ( ( RSpan ` R ) ` { y } ) e. ( LIdeal ` R ) ) ) /\ A. r e. ( ( RSpan ` R ) ` { x } ) A. s e. ( ( RSpan ` R ) ` { y } ) ( r .x. s ) e. P ) -> ( ( ( RSpan ` R ) ` { x } ) C_ P \/ ( ( RSpan ` R ) ` { y } ) C_ P ) ) with typecode |-
57	8 9 20 55 56	syl1111anc	Could not format ( ( ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ ( x .x. y ) e. P ) -> ( ( ( RSpan ` R ) ` { x } ) C_ P \/ ( ( RSpan ` R ) ` { y } ) C_ P ) ) : No typesetting found for |- ( ( ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ ( x .x. y ) e. P ) -> ( ( ( RSpan ` R ) ` { x } ) C_ P \/ ( ( RSpan ` R ) ` { y } ) C_ P ) ) with typecode |-
58	1 12	rspsnid	$$⊢\left(R\in \mathrm{Ring}\wedge x\in B\right)\to x\in \mathrm{RSpan}\left(R\right)\left(\left\{x\right\}\right)$$
59	3 58	sylan	$$⊢\left(R\in \mathrm{CRing}\wedge x\in B\right)\to x\in \mathrm{RSpan}\left(R\right)\left(\left\{x\right\}\right)$$
60	59	adantr	$$⊢\left(\left(R\in \mathrm{CRing}\wedge x\in B\right)\wedge y\in B\right)\to x\in \mathrm{RSpan}\left(R\right)\left(\left\{x\right\}\right)$$
61		ssel	$$⊢\mathrm{RSpan}\left(R\right)\left(\left\{x\right\}\right)\subseteq P\to \left(x\in \mathrm{RSpan}\left(R\right)\left(\left\{x\right\}\right)\to x\in P\right)$$
62	60 61	syl5com	$$⊢\left(\left(R\in \mathrm{CRing}\wedge x\in B\right)\wedge y\in B\right)\to \left(\mathrm{RSpan}\left(R\right)\left(\left\{x\right\}\right)\subseteq P\to x\in P\right)$$
63	1 12	rspsnid	$$⊢\left(R\in \mathrm{Ring}\wedge y\in B\right)\to y\in \mathrm{RSpan}\left(R\right)\left(\left\{y\right\}\right)$$
64	3 63	sylan	$$⊢\left(R\in \mathrm{CRing}\wedge y\in B\right)\to y\in \mathrm{RSpan}\left(R\right)\left(\left\{y\right\}\right)$$
65	64	adantlr	$$⊢\left(\left(R\in \mathrm{CRing}\wedge x\in B\right)\wedge y\in B\right)\to y\in \mathrm{RSpan}\left(R\right)\left(\left\{y\right\}\right)$$
66		ssel	$$⊢\mathrm{RSpan}\left(R\right)\left(\left\{y\right\}\right)\subseteq P\to \left(y\in \mathrm{RSpan}\left(R\right)\left(\left\{y\right\}\right)\to y\in P\right)$$
67	65 66	syl5com	$$⊢\left(\left(R\in \mathrm{CRing}\wedge x\in B\right)\wedge y\in B\right)\to \left(\mathrm{RSpan}\left(R\right)\left(\left\{y\right\}\right)\subseteq P\to y\in P\right)$$
68	62 67	orim12d	$$⊢\left(\left(R\in \mathrm{CRing}\wedge x\in B\right)\wedge y\in B\right)\to \left(\left(\mathrm{RSpan}\left(R\right)\left(\left\{x\right\}\right)\subseteq P\vee \mathrm{RSpan}\left(R\right)\left(\left\{y\right\}\right)\subseteq P\right)\to \left(x\in P\vee y\in P\right)\right)$$
69	68	adantllr	Could not format ( ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) -> ( ( ( ( RSpan ` R ) ` { x } ) C_ P \/ ( ( RSpan ` R ) ` { y } ) C_ P ) -> ( x e. P \/ y e. P ) ) ) : No typesetting found for |- ( ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) -> ( ( ( ( RSpan ` R ) ` { x } ) C_ P \/ ( ( RSpan ` R ) ` { y } ) C_ P ) -> ( x e. P \/ y e. P ) ) ) with typecode |-
70	69	adantr	Could not format ( ( ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ ( x .x. y ) e. P ) -> ( ( ( ( RSpan ` R ) ` { x } ) C_ P \/ ( ( RSpan ` R ) ` { y } ) C_ P ) -> ( x e. P \/ y e. P ) ) ) : No typesetting found for |- ( ( ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ ( x .x. y ) e. P ) -> ( ( ( ( RSpan ` R ) ` { x } ) C_ P \/ ( ( RSpan ` R ) ` { y } ) C_ P ) -> ( x e. P \/ y e. P ) ) ) with typecode |-
71	57 70	mpd	Could not format ( ( ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ ( x .x. y ) e. P ) -> ( x e. P \/ y e. P ) ) : No typesetting found for |- ( ( ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ ( x .x. y ) e. P ) -> ( x e. P \/ y e. P ) ) with typecode |-
72	71	ex	Could not format ( ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) -> ( ( x .x. y ) e. P -> ( x e. P \/ y e. P ) ) ) : No typesetting found for |- ( ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) -> ( ( x .x. y ) e. P -> ( x e. P \/ y e. P ) ) ) with typecode |-
73	72	anasss	Could not format ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ ( x e. B /\ y e. B ) ) -> ( ( x .x. y ) e. P -> ( x e. P \/ y e. P ) ) ) : No typesetting found for |- ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ ( x e. B /\ y e. B ) ) -> ( ( x .x. y ) e. P -> ( x e. P \/ y e. P ) ) ) with typecode |-
74	73	ralrimivva	Could not format ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) -> A. x e. B A. y e. B ( ( x .x. y ) e. P -> ( x e. P \/ y e. P ) ) ) : No typesetting found for |- ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) -> A. x e. B A. y e. B ( ( x .x. y ) e. P -> ( x e. P \/ y e. P ) ) ) with typecode |-
75	5 7 74	3jca	Could not format ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) -> ( P e. ( LIdeal ` R ) /\ P =/= B /\ A. x e. B A. y e. B ( ( x .x. y ) e. P -> ( x e. P \/ y e. P ) ) ) ) : No typesetting found for |- ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) -> ( P e. ( LIdeal ` R ) /\ P =/= B /\ A. x e. B A. y e. B ( ( x .x. y ) e. P -> ( x e. P \/ y e. P ) ) ) ) with typecode |-
76		3anass	$$⊢\left(P\in \mathrm{LIdeal}\left(R\right)\wedge P\ne B\wedge \forall x\in B\forall y\in B\left(x\underset{\dot{}}{·}y\in P\to \left(x\in P\vee y\in P\right)\right)\right)\leftrightarrow \left(P\in \mathrm{LIdeal}\left(R\right)\wedge \left(P\ne B\wedge \forall x\in B\forall y\in B\left(x\underset{\dot{}}{·}y\in P\to \left(x\in P\vee y\in P\right)\right)\right)\right)$$
77	1 2	prmidl2	Could not format ( ( ( R e. Ring /\ P e. ( LIdeal ` R ) ) /\ ( P =/= B /\ A. x e. B A. y e. B ( ( x .x. y ) e. P -> ( x e. P \/ y e. P ) ) ) ) -> P e. ( PrmIdeal ` R ) ) : No typesetting found for |- ( ( ( R e. Ring /\ P e. ( LIdeal ` R ) ) /\ ( P =/= B /\ A. x e. B A. y e. B ( ( x .x. y ) e. P -> ( x e. P \/ y e. P ) ) ) ) -> P e. ( PrmIdeal ` R ) ) with typecode |-
78	77	anasss	Could not format ( ( R e. Ring /\ ( P e. ( LIdeal ` R ) /\ ( P =/= B /\ A. x e. B A. y e. B ( ( x .x. y ) e. P -> ( x e. P \/ y e. P ) ) ) ) ) -> P e. ( PrmIdeal ` R ) ) : No typesetting found for |- ( ( R e. Ring /\ ( P e. ( LIdeal ` R ) /\ ( P =/= B /\ A. x e. B A. y e. B ( ( x .x. y ) e. P -> ( x e. P \/ y e. P ) ) ) ) ) -> P e. ( PrmIdeal ` R ) ) with typecode |-
79	76 78	sylan2b	Could not format ( ( R e. Ring /\ ( P e. ( LIdeal ` R ) /\ P =/= B /\ A. x e. B A. y e. B ( ( x .x. y ) e. P -> ( x e. P \/ y e. P ) ) ) ) -> P e. ( PrmIdeal ` R ) ) : No typesetting found for |- ( ( R e. Ring /\ ( P e. ( LIdeal ` R ) /\ P =/= B /\ A. x e. B A. y e. B ( ( x .x. y ) e. P -> ( x e. P \/ y e. P ) ) ) ) -> P e. ( PrmIdeal ` R ) ) with typecode |-
80	3 79	sylan	Could not format ( ( R e. CRing /\ ( P e. ( LIdeal ` R ) /\ P =/= B /\ A. x e. B A. y e. B ( ( x .x. y ) e. P -> ( x e. P \/ y e. P ) ) ) ) -> P e. ( PrmIdeal ` R ) ) : No typesetting found for |- ( ( R e. CRing /\ ( P e. ( LIdeal ` R ) /\ P =/= B /\ A. x e. B A. y e. B ( ( x .x. y ) e. P -> ( x e. P \/ y e. P ) ) ) ) -> P e. ( PrmIdeal ` R ) ) with typecode |-
81	75 80	impbida	Could not format ( R e. CRing -> ( P e. ( PrmIdeal ` R ) <-> ( P e. ( LIdeal ` R ) /\ P =/= B /\ A. x e. B A. y e. B ( ( x .x. y ) e. P -> ( x e. P \/ y e. P ) ) ) ) ) : No typesetting found for |- ( R e. CRing -> ( P e. ( PrmIdeal ` R ) <-> ( P e. ( LIdeal ` R ) /\ P =/= B /\ A. x e. B A. y e. B ( ( x .x. y ) e. P -> ( x e. P \/ y e. P ) ) ) ) ) with typecode |-