Theorem ispridlc 16218

Description: The predicate "is a prime ideal". Alternate definition for commutative rings.

Hypotheses

Ref	Expression
ispridlc.1	|- G = (1st` R)
ispridlc.2	|- H = (2nd` R)
ispridlc.3	|- X = ran G

Assertion

Ref	Expression
ispridlc	|- (R e. CRing -> (P e. (PrIdl` R) <-> (P e. (Idl` R) /\ P =/= X /\ A.a e. X A.b e. X ((aHb) e. P -> (a e. P \/ b e. P)))))

Distinct variable groups:   R,a,b   P,a,b   X,a,b   H,a,b

Proof of Theorem ispridlc

Step	Hyp	Ref	Expression
1		crngrng 16148	. . . 4 |- (R e. CRing -> R e. Ring)
2		ispridlc.1	. . . . 5 |- G = (1st` R)
3		ispridlc.2	. . . . 5 |- H = (2nd` R)
4		ispridlc.3	. . . . 5 |- X = ran G
5	2, 3, 4	ispridl 16182	. . . 4 |- (R e. Ring -> (P e. (PrIdl` R) <-> (P e. (Idl` R) /\ P =/= X /\ A.r e. (Idl` R)A.s e. (Idl` R)(A.x e. r A.y e. s (xHy) e. P -> (r C_ P \/ s C_ P)))))
6	1, 5	syl 12	. . 3 |- (R e. CRing -> (P e. (PrIdl` R) <-> (P e. (Idl` R) /\ P =/= X /\ A.r e. (Idl` R)A.s e. (Idl` R)(A.x e. r A.y e. s (xHy) e. P -> (r C_ P \/ s C_ P)))))
7	2, 4	igenidl 16211	. . . . . . . . . . . . 13 |- ((R e. Ring /\ {a} C_ X) -> (R IdlGen {a}) e. (Idl` R))
8		snssi 3129	. . . . . . . . . . . . 13 |- (a e. X -> {a} C_ X)
9	7, 1, 8	syl2an 503	. . . . . . . . . . . 12 |- ((R e. CRing /\ a e. X) -> (R IdlGen {a}) e. (Idl` R))
10	9	adantrr 431	. . . . . . . . . . 11 |- ((R e. CRing /\ (a e. X /\ b e. X)) -> (R IdlGen {a}) e. (Idl` R))
11	2, 4	igenidl 16211	. . . . . . . . . . . . 13 |- ((R e. Ring /\ {b} C_ X) -> (R IdlGen {b}) e. (Idl` R))
12		snssi 3129	. . . . . . . . . . . . 13 |- (b e. X -> {b} C_ X)
13	11, 1, 12	syl2an 503	. . . . . . . . . . . 12 |- ((R e. CRing /\ b e. X) -> (R IdlGen {b}) e. (Idl` R))
14	13	adantrl 430	. . . . . . . . . . 11 |- ((R e. CRing /\ (a e. X /\ b e. X)) -> (R IdlGen {b}) e. (Idl` R))
15		raleq 2266	. . . . . . . . . . . . 13 |- (r = (R IdlGen {a}) -> (A.x e. r A.y e. s (xHy) e. P <-> A.x e. (R IdlGen {a})A.y e. s (xHy) e. P))
16		sseq1 2637	. . . . . . . . . . . . . 14 |- (r = (R IdlGen {a}) -> (r C_ P <-> (R IdlGen {a}) C_ P))
17	16	orbi1d 677	. . . . . . . . . . . . 13 |- (r = (R IdlGen {a}) -> ((r C_ P \/ s C_ P) <-> ((R IdlGen {a}) C_ P \/ s C_ P)))
18	15, 17	imbi12d 688	. . . . . . . . . . . 12 |- (r = (R IdlGen {a}) -> ((A.x e. r A.y e. s (xHy) e. P -> (r C_ P \/ s C_ P)) <-> (A.x e. (R IdlGen {a})A.y e. s (xHy) e. P -> ((R IdlGen {a}) C_ P \/ s C_ P))))
19		raleq 2266	. . . . . . . . . . . . . 14 |- (s = (R IdlGen {b}) -> (A.y e. s (xHy) e. P <-> A.y e. (R IdlGen {b})(xHy) e. P))
20	19	ralbidv 2123	. . . . . . . . . . . . 13 |- (s = (R IdlGen {b}) -> (A.x e. (R IdlGen {a})A.y e. s (xHy) e. P <-> A.x e. (R IdlGen {a})A.y e. (R IdlGen {b})(xHy) e. P))
21		sseq1 2637	. . . . . . . . . . . . . 14 |- (s = (R IdlGen {b}) -> (s C_ P <-> (R IdlGen {b}) C_ P))
22	21	orbi2d 676	. . . . . . . . . . . . 13 |- (s = (R IdlGen {b}) -> (((R IdlGen {a}) C_ P \/ s C_ P) <-> ((R IdlGen {a}) C_ P \/ (R IdlGen {b}) C_ P)))
23	20, 22	imbi12d 688	. . . . . . . . . . . 12 |- (s = (R IdlGen {b}) -> ((A.x e. (R IdlGen {a})A.y e. s (xHy) e. P -> ((R IdlGen {a}) C_ P \/ s C_ P)) <-> (A.x e. (R IdlGen {a})A.y e. (R IdlGen {b})(xHy) e. P -> ((R IdlGen {a}) C_ P \/ (R IdlGen {b}) C_ P))))
24	18, 23	rcla42v 2384	. . . . . . . . . . 11 |- (((R IdlGen {a}) e. (Idl` R) /\ (R IdlGen {b}) e. (Idl` R)) -> (A.r e. (Idl` R)A.s e. (Idl` R)(A.x e. r A.y e. s (xHy) e. P -> (r C_ P \/ s C_ P)) -> (A.x e. (R IdlGen {a})A.y e. (R IdlGen {b})(xHy) e. P -> ((R IdlGen {a}) C_ P \/ (R IdlGen {b}) C_ P))))
25	10, 14, 24	syl11anc 524	. . . . . . . . . 10 |- ((R e. CRing /\ (a e. X /\ b e. X)) -> (A.r e. (Idl` R)A.s e. (Idl` R)(A.x e. r A.y e. s (xHy) e. P -> (r C_ P \/ s C_ P)) -> (A.x e. (R IdlGen {a})A.y e. (R IdlGen {b})(xHy) e. P -> ((R IdlGen {a}) C_ P \/ (R IdlGen {b}) C_ P))))
26	25	adantlr 429	. . . . . . . . 9 |- (((R e. CRing /\ P e. (Idl` R)) /\ (a e. X /\ b e. X)) -> (A.r e. (Idl` R)A.s e. (Idl` R)(A.x e. r A.y e. s (xHy) e. P -> (r C_ P \/ s C_ P)) -> (A.x e. (R IdlGen {a})A.y e. (R IdlGen {b})(xHy) e. P -> ((R IdlGen {a}) C_ P \/ (R IdlGen {b}) C_ P))))
27	2, 3, 4	prnc 16215	. . . . . . . . . . . . . . . . . . 19 |- ((R e. CRing /\ a e. X) -> (R IdlGen {a}) = {x e. X | E.r e. X x = (rHa)})
28		df-rab 2112	. . . . . . . . . . . . . . . . . . 19 |- {x e. X | E.r e. X x = (rHa)} = {x | (x e. X /\ E.r e. X x = (rHa))}
29	27, 28	syl6eq 1944	. . . . . . . . . . . . . . . . . 18 |- ((R e. CRing /\ a e. X) -> (R IdlGen {a}) = {x | (x e. X /\ E.r e. X x = (rHa))})
30	29	abeq2d 2003	. . . . . . . . . . . . . . . . 17 |- ((R e. CRing /\ a e. X) -> (x e. (R IdlGen {a}) <-> (x e. X /\ E.r e. X x = (rHa))))
31	30	adantrr 431	. . . . . . . . . . . . . . . 16 |- ((R e. CRing /\ (a e. X /\ b e. X)) -> (x e. (R IdlGen {a}) <-> (x e. X /\ E.r e. X x = (rHa))))
32	2, 3, 4	prnc 16215	. . . . . . . . . . . . . . . . . . 19 |- ((R e. CRing /\ b e. X) -> (R IdlGen {b}) = {y e. X | E.s e. X y = (sHb)})
33		df-rab 2112	. . . . . . . . . . . . . . . . . . 19 |- {y e. X | E.s e. X y = (sHb)} = {y | (y e. X /\ E.s e. X y = (sHb))}
34	32, 33	syl6eq 1944	. . . . . . . . . . . . . . . . . 18 |- ((R e. CRing /\ b e. X) -> (R IdlGen {b}) = {y | (y e. X /\ E.s e. X y = (sHb))})
35	34	abeq2d 2003	. . . . . . . . . . . . . . . . 17 |- ((R e. CRing /\ b e. X) -> (y e. (R IdlGen {b}) <-> (y e. X /\ E.s e. X y = (sHb))))
36	35	adantrl 430	. . . . . . . . . . . . . . . 16 |- ((R e. CRing /\ (a e. X /\ b e. X)) -> (y e. (R IdlGen {b}) <-> (y e. X /\ E.s e. X y = (sHb))))
37	31, 36	anbi12d 690	. . . . . . . . . . . . . . 15 |- ((R e. CRing /\ (a e. X /\ b e. X)) -> ((x e. (R IdlGen {a}) /\ y e. (R IdlGen {b})) <-> ((x e. X /\ E.r e. X x = (rHa)) /\ (y e. X /\ E.s e. X y = (sHb)))))
38	37	adantlr 429	. . . . . . . . . . . . . 14 |- (((R e. CRing /\ P e. (Idl` R)) /\ (a e. X /\ b e. X)) -> ((x e. (R IdlGen {a}) /\ y e. (R IdlGen {b})) <-> ((x e. X /\ E.r e. X x = (rHa)) /\ (y e. X /\ E.s e. X y = (sHb)))))
39	38	adantr 425	. . . . . . . . . . . . 13 |- ((((R e. CRing /\ P e. (Idl` R)) /\ (a e. X /\ b e. X)) /\ (aHb) e. P) -> ((x e. (R IdlGen {a}) /\ y e. (R IdlGen {b})) <-> ((x e. X /\ E.r e. X x = (rHa)) /\ (y e. X /\ E.s e. X y = (sHb)))))
40		opreq12 4891	. . . . . . . . . . . . . . . . . . 19 |- ((x = (rHa) /\ y = (sHb)) -> (xHy) = ((rHa)H(sHb)))
41	40	eleq1d 1963	. . . . . . . . . . . . . . . . . 18 |- ((x = (rHa) /\ y = (sHb)) -> ((xHy) e. P <-> ((rHa)H(sHb)) e. P))
42	2, 3, 4	crngm4 16151	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((R e. CRing /\ (r e. X /\ s e. X) /\ (a e. X /\ b e. X)) -> ((rHs)H(aHb)) = ((rHa)H(sHb)))
43	42	3com23 1074	. . . . . . . . . . . . . . . . . . . . . 22 |- ((R e. CRing /\ (a e. X /\ b e. X) /\ (r e. X /\ s e. X)) -> ((rHs)H(aHb)) = ((rHa)H(sHb)))
44	43	3expa 1067	. . . . . . . . . . . . . . . . . . . . 21 |- (((R e. CRing /\ (a e. X /\ b e. X)) /\ (r e. X /\ s e. X)) -> ((rHs)H(aHb)) = ((rHa)H(sHb)))
45	44	adantllr 433	. . . . . . . . . . . . . . . . . . . 20 |- ((((R e. CRing /\ P e. (Idl` R)) /\ (a e. X /\ b e. X)) /\ (r e. X /\ s e. X)) -> ((rHs)H(aHb)) = ((rHa)H(sHb)))
46	45	adantlr 429	. . . . . . . . . . . . . . . . . . 19 |- (((((R e. CRing /\ P e. (Idl` R)) /\ (a e. X /\ b e. X)) /\ (aHb) e. P) /\ (r e. X /\ s e. X)) -> ((rHs)H(aHb)) = ((rHa)H(sHb)))
47	2, 3, 4	ringcl 9468	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((R e. Ring /\ r e. X /\ s e. X) -> (rHs) e. X)
48	47, 1	syl3an1 1130	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((R e. CRing /\ r e. X /\ s e. X) -> (rHs) e. X)
49	48	3expb 1068	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((R e. CRing /\ (r e. X /\ s e. X)) -> (rHs) e. X)
50	49	adantlr 429	. . . . . . . . . . . . . . . . . . . . . 22 |- (((R e. CRing /\ P e. (Idl` R)) /\ (r e. X /\ s e. X)) -> (rHs) e. X)
51	50	adantlr 429	. . . . . . . . . . . . . . . . . . . . 21 |- ((((R e. CRing /\ P e. (Idl` R)) /\ (aHb) e. P) /\ (r e. X /\ s e. X)) -> (rHs) e. X)
52	2, 3, 4	idllmulcl 16168	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((R e. Ring /\ P e. (Idl` R)) /\ ((aHb) e. P /\ (rHs) e. X)) -> ((rHs)H(aHb)) e. P)
53	52, 1	sylanl1 509	. . . . . . . . . . . . . . . . . . . . . 22 |- (((R e. CRing /\ P e. (Idl` R)) /\ ((aHb) e. P /\ (rHs) e. X)) -> ((rHs)H(aHb)) e. P)
54	53	anassrs 489	. . . . . . . . . . . . . . . . . . . . 21 |- ((((R e. CRing /\ P e. (Idl` R)) /\ (aHb) e. P) /\ (rHs) e. X) -> ((rHs)H(aHb)) e. P)
55	51, 54	syldan 516	. . . . . . . . . . . . . . . . . . . 20 |- ((((R e. CRing /\ P e. (Idl` R)) /\ (aHb) e. P) /\ (r e. X /\ s e. X)) -> ((rHs)H(aHb)) e. P)
56	55	adantllr 433	. . . . . . . . . . . . . . . . . . 19 |- (((((R e. CRing /\ P e. (Idl` R)) /\ (a e. X /\ b e. X)) /\ (aHb) e. P) /\ (r e. X /\ s e. X)) -> ((rHs)H(aHb)) e. P)
57	46, 56	eqeltrrd 1972	. . . . . . . . . . . . . . . . . 18 |- (((((R e. CRing /\ P e. (Idl` R)) /\ (a e. X /\ b e. X)) /\ (aHb) e. P) /\ (r e. X /\ s e. X)) -> ((rHa)H(sHb)) e. P)
58	41, 57	syl5cbir 228	. . . . . . . . . . . . . . . . 17 |- (((((R e. CRing /\ P e. (Idl` R)) /\ (a e. X /\ b e. X)) /\ (aHb) e. P) /\ (r e. X /\ s e. X)) -> ((x = (rHa) /\ y = (sHb)) -> (xHy) e. P))
59	58	ex 402	. . . . . . . . . . . . . . . 16 |- ((((R e. CRing /\ P e. (Idl` R)) /\ (a e. X /\ b e. X)) /\ (aHb) e. P) -> ((r e. X /\ s e. X) -> ((x = (rHa) /\ y = (sHb)) -> (xHy) e. P)))
60	59	r19.23advv 2218	. . . . . . . . . . . . . . 15 |- ((((R e. CRing /\ P e. (Idl` R)) /\ (a e. X /\ b e. X)) /\ (aHb) e. P) -> (E.r e. X E.s e. X (x = (rHa) /\ y = (sHb)) -> (xHy) e. P))
61	60	adantld 426	. . . . . . . . . . . . . 14 |- ((((R e. CRing /\ P e. (Idl` R)) /\ (a e. X /\ b e. X)) /\ (aHb) e. P) -> (((x e. X /\ y e. X) /\ E.r e. X E.s e. X (x = (rHa) /\ y = (sHb))) -> (xHy) e. P))
62		reeanv 2249	. . . . . . . . . . . . . . . 16 |- (E.r e. X E.s e. X (x = (rHa) /\ y = (sHb)) <-> (E.r e. X x = (rHa) /\ E.s e. X y = (sHb)))
63	62	anbi2i 538	. . . . . . . . . . . . . . 15 |- (((x e. X /\ y e. X) /\ E.r e. X E.s e. X (x = (rHa) /\ y = (sHb))) <-> ((x e. X /\ y e. X) /\ (E.r e. X x = (rHa) /\ E.s e. X y = (sHb))))
64		an4 564	. . . . . . . . . . . . . . 15 |- (((x e. X /\ y e. X) /\ (E.r e. X x = (rHa) /\ E.s e. X y = (sHb))) <-> ((x e. X /\ E.r e. X x = (rHa)) /\ (y e. X /\ E.s e. X y = (sHb))))
65	63, 64	bitri 190	. . . . . . . . . . . . . 14 |- (((x e. X /\ y e. X) /\ E.r e. X E.s e. X (x = (rHa) /\ y = (sHb))) <-> ((x e. X /\ E.r e. X x = (rHa)) /\ (y e. X /\ E.s e. X y = (sHb))))
66	61, 65	syl5ibr 224	. . . . . . . . . . . . 13 |- ((((R e. CRing /\ P e. (Idl` R)) /\ (a e. X /\ b e. X)) /\ (aHb) e. P) -> (((x e. X /\ E.r e. X x = (rHa)) /\ (y e. X /\ E.s e. X y = (sHb))) -> (xHy) e. P))
67	39, 66	sylbid 220	. . . . . . . . . . . 12 |- ((((R e. CRing /\ P e. (Idl` R)) /\ (a e. X /\ b e. X)) /\ (aHb) e. P) -> ((x e. (R IdlGen {a}) /\ y e. (R IdlGen {b})) -> (xHy) e. P))
68	67	r19.21aivv 2183	. . . . . . . . . . 11 |- ((((R e. CRing /\ P e. (Idl` R)) /\ (a e. X /\ b e. X)) /\ (aHb) e. P) -> A.x e. (R IdlGen {a})A.y e. (R IdlGen {b})(xHy) e. P)
69	68	ex 402	. . . . . . . . . 10 |- (((R e. CRing /\ P e. (Idl` R)) /\ (a e. X /\ b e. X)) -> ((aHb) e. P -> A.x e. (R IdlGen {a})A.y e. (R IdlGen {b})(xHy) e. P))
70		ssel 2615	. . . . . . . . . . . . 13 |- ((R IdlGen {a}) C_ P -> (a e. (R IdlGen {a}) -> a e. P))
71	2, 4	igenss 16210	. . . . . . . . . . . . . . . 16 |- ((R e. Ring /\ {a} C_ X) -> {a} C_ (R IdlGen {a}))
72	71, 1, 8	syl2an 503	. . . . . . . . . . . . . . 15 |- ((R e. CRing /\ a e. X) -> {a} C_ (R IdlGen {a}))
73		visset 2295	. . . . . . . . . . . . . . . 16 |- a e. _V
74	73	snss 3122	. . . . . . . . . . . . . . 15 |- (a e. (R IdlGen {a}) <-> {a} C_ (R IdlGen {a}))
75	72, 74	sylibr 217	. . . . . . . . . . . . . 14 |- ((R e. CRing /\ a e. X) -> a e. (R IdlGen {a}))
76	75	adantrr 431	. . . . . . . . . . . . 13 |- ((R e. CRing /\ (a e. X /\ b e. X)) -> a e. (R IdlGen {a}))
77	70, 76	syl5com 63	. . . . . . . . . . . 12 |- ((R e. CRing /\ (a e. X /\ b e. X)) -> ((R IdlGen {a}) C_ P -> a e. P))
78		ssel 2615	. . . . . . . . . . . . 13 |- ((R IdlGen {b}) C_ P -> (b e. (R IdlGen {b}) -> b e. P))
79	2, 4	igenss 16210	. . . . . . . . . . . . . . . 16 |- ((R e. Ring /\ {b} C_ X) -> {b} C_ (R IdlGen {b}))
80	79, 1, 12	syl2an 503	. . . . . . . . . . . . . . 15 |- ((R e. CRing /\ b e. X) -> {b} C_ (R IdlGen {b}))
81		visset 2295	. . . . . . . . . . . . . . . 16 |- b e. _V
82	81	snss 3122	. . . . . . . . . . . . . . 15 |- (b e. (R IdlGen {b}) <-> {b} C_ (R IdlGen {b}))
83	80, 82	sylibr 217	. . . . . . . . . . . . . 14 |- ((R e. CRing /\ b e. X) -> b e. (R IdlGen {b}))
84	83	adantrl 430	. . . . . . . . . . . . 13 |- ((R e. CRing /\ (a e. X /\ b e. X)) -> b e. (R IdlGen {b}))
85	78, 84	syl5com 63	. . . . . . . . . . . 12 |- ((R e. CRing /\ (a e. X /\ b e. X)) -> ((R IdlGen {b}) C_ P -> b e. P))
86	77, 85	orim12d 624	. . . . . . . . . . 11 |- ((R e. CRing /\ (a e. X /\ b e. X)) -> (((R IdlGen {a}) C_ P \/ (R IdlGen {b}) C_ P) -> (a e. P \/ b e. P)))
87	86	adantlr 429	. . . . . . . . . 10 |- (((R e. CRing /\ P e. (Idl` R)) /\ (a e. X /\ b e. X)) -> (((R IdlGen {a}) C_ P \/ (R IdlGen {b}) C_ P) -> (a e. P \/ b e. P)))
88	69, 87	imim12d 69	. . . . . . . . 9 |- (((R e. CRing /\ P e. (Idl` R)) /\ (a e. X /\ b e. X)) -> ((A.x e. (R IdlGen {a})A.y e. (R IdlGen {b})(xHy) e. P -> ((R IdlGen {a}) C_ P \/ (R IdlGen {b}) C_ P)) -> ((aHb) e. P -> (a e. P \/ b e. P))))
89	26, 88	syld 30	. . . . . . . 8 |- (((R e. CRing /\ P e. (Idl` R)) /\ (a e. X /\ b e. X)) -> (A.r e. (Idl` R)A.s e. (Idl` R)(A.x e. r A.y e. s (xHy) e. P -> (r C_ P \/ s C_ P)) -> ((aHb) e. P -> (a e. P \/ b e. P))))
90	89	r19.21advva 2185	. . . . . . 7 |- ((R e. CRing /\ P e. (Idl` R)) -> (A.r e. (Idl` R)A.s e. (Idl` R)(A.x e. r A.y e. s (xHy) e. P -> (r C_ P \/ s C_ P)) -> A.a e. X A.b e. X ((aHb) e. P -> (a e. P \/ b e. P))))
91	90	ex 402	. . . . . 6 |- (R e. CRing -> (P e. (Idl` R) -> (A.r e. (Idl` R)A.s e. (Idl` R)(A.x e. r A.y e. s (xHy) e. P -> (r C_ P \/ s C_ P)) -> A.a e. X A.b e. X ((aHb) e. P -> (a e. P \/ b e. P)))))
92	91	adantrd 427	. . . . 5 |- (R e. CRing -> ((P e. (Idl` R) /\ P =/= X) -> (A.r e. (Idl` R)A.s e. (Idl` R)(A.x e. r A.y e. s (xHy) e. P -> (r C_ P \/ s C_ P)) -> A.a e. X A.b e. X ((aHb) e. P -> (a e. P \/ b e. P)))))
93	92	imdistand 493	. . . 4 |- (R e. CRing -> (((P e. (Idl` R) /\ P =/= X) /\ A.r e. (Idl` R)A.s e. (Idl` R)(A.x e. r A.y e. s (xHy) e. P -> (r C_ P \/ s C_ P))) -> ((P e. (Idl` R) /\ P =/= X) /\ A.a e. X A.b e. X ((aHb) e. P -> (a e. P \/ b e. P)))))
94		df-3an 860	. . . 4 |- ((P e. (Idl` R) /\ P =/= X /\ A.r e. (Idl` R)A.s e. (Idl` R)(A.x e. r A.y e. s (xHy) e. P -> (r C_ P \/ s C_ P))) <-> ((P e. (Idl` R) /\ P =/= X) /\ A.r e. (Idl` R)A.s e. (Idl` R)(A.x e. r A.y e. s (xHy) e. P -> (r C_ P \/ s C_ P))))
95		df-3an 860	. . . 4 |- ((P e. (Idl` R) /\ P =/= X /\ A.a e. X A.b e. X ((aHb) e. P -> (a e. P \/ b e. P))) <-> ((P e. (Idl` R) /\ P =/= X) /\ A.a e. X A.b e. X ((aHb) e. P -> (a e. P \/ b e. P))))
96	93, 94, 95	3imtr4g 612	. . 3 |- (R e. CRing -> ((P e. (Idl` R) /\ P =/= X /\ A.r e. (Idl` R)A.s e. (Idl` R)(A.x e. r A.y e. s (xHy) e. P -> (r C_ P \/ s C_ P))) -> (P e. (Idl` R) /\ P =/= X /\ A.a e. X A.b e. X ((aHb) e. P -> (a e. P \/ b e. P)))))
97	6, 96	sylbid 220	. 2 |- (R e. CRing -> (P e. (PrIdl` R) -> (P e. (Idl` R) /\ P =/= X /\ A.a e. X A.b e. X ((aHb) e. P -> (a e. P \/ b e. P)))))
98	2, 3, 4	ispridl2 16186	. . . 4 |- ((R e. Ring /\ (P e. (Idl` R) /\ P =/= X /\ A.a e. X A.b e. X ((aHb) e. P -> (a e. P \/ b e. P)))) -> P e. (PrIdl` R))
99	98	ex 402	. . 3 |- (R e. Ring -> ((P e. (Idl` R) /\ P =/= X /\ A.a e. X A.b e. X ((aHb) e. P -> (a e. P \/ b e. P))) -> P e. (PrIdl` R)))
100	1, 99	syl 12	. 2 |- (R e. CRing -> ((P e. (Idl` R) /\ P =/= X /\ A.a e. X A.b e. X ((aHb) e. P -> (a e. P \/ b e. P))) -> P e. (PrIdl` R)))
101	97, 100	impbid 574	1 |- (R e. CRing -> (P e. (PrIdl` R) <-> (P e. (Idl` R) /\ P =/= X /\ A.a e. X A.b e. X ((aHb) e. P -> (a e. P \/ b e. P)))))

Syntax hints:   -> wi 3   <-> wb 163   \/ wo 239   /\ wa 240   /\ w3a 858   = wceq 1298   e. wcel 1300  {cab 1871   =/= wne 2017  A.wral 2105  E.wrex 2106  {crab 2108   C_ wss 2593  {csn 3044  ran crn 3987  ` cfv 3998  (class class class)co 4884  1stc1st 5018  2ndc2nd 5019  Ringcring 9463  CRingccring 16143  Idlcidl 16155  PrIdlcpridl 16156   IdlGen cigen 16207

This theorem is referenced by:  pridlc 16219  isdmn3 16222

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-rep 3428  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3an 860  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-ral 2109  df-rex 2110  df-reu 2111  df-rab 2112  df-v 2294  df-sbc 2454  df-csb 2541  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-nul 2876  df-if 2983  df-pw 3035  df-sn 3049  df-pr 3050  df-op 3053  df-uni 3178  df-int 3215  df-br 3339  df-opab 3396  df-id 3586  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fn 4009  df-f 4010  df-f1 4011  df-fo 4012  df-f1o 4013  df-fv 4014  df-opr 4886  df-oprab 4887  df-1st 5020  df-2nd 5021  df-grp 9316  df-gid 9317  df-ginv 9318  df-abl 9408  df-ring 9464  df-ass 10360  df-exid 10362  df-mgm 10366  df-sgr 10378  df-mnd 10385  df-com2 10395  df-cring 16144  df-idl 16158  df-pridl 16159  df-igen 16208

Copyright terms: Public domain