Metamath Proof Explorer

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 = ( Base ` R )
isprmidlc.2 
|- .x. = ( .r ` R )
Assertion isprmidlc 
|- ( 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 ) ) ) ) )

Proof

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