ispridlc

Description: The predicate "is a prime ideal". Alternate definition for commutative rings. (Contributed by Jeff Madsen, 19-Jun-2010)

	Ref	Expression
Hypotheses	ispridlc.1	$⊢ G = 1^{st} (R)$
	ispridlc.2	$⊢ H = 2^{nd} (R)$
	ispridlc.3	$⊢ X = ran G$
Assertion	ispridlc	$⊢ R \in CRingOps \to (P \in PrIdl (R) \leftrightarrow (P \in Idl (R) \land P \neq X \land \forall a \in X \forall b \in X (a H b \in P \to (a \in P \lor b \in P))))$

Proof

Step	Hyp	Ref	Expression
1		ispridlc.1	$⊢ G = 1^{st} (R)$
2		ispridlc.2	$⊢ H = 2^{nd} (R)$
3		ispridlc.3	$⊢ X = ran G$
4		crngorngo	$⊢ R \in CRingOps \to R \in RingOps$
5	1 2 3	ispridl	$⊢ R \in RingOps \to (P \in PrIdl (R) \leftrightarrow (P \in Idl (R) \land P \neq X \land \forall r \in Idl (R) \forall s \in Idl (R) (\forall x \in r \forall y \in s x H y \in P \to (r \subseteq P \lor s \subseteq P))))$
6	4 5	syl	$⊢ R \in CRingOps \to (P \in PrIdl (R) \leftrightarrow (P \in Idl (R) \land P \neq X \land \forall r \in Idl (R) \forall s \in Idl (R) (\forall x \in r \forall y \in s x H y \in P \to (r \subseteq P \lor s \subseteq P))))$
7		snssi	$⊢ a \in X \to \{a\} \subseteq X$
8	1 3	igenidl	$⊢ (R \in RingOps \land \{a\} \subseteq X) \to R IdlGen \{a\} \in Idl (R)$
9	4 7 8	syl2an	$⊢ (R \in CRingOps \land a \in X) \to R IdlGen \{a\} \in Idl (R)$
10	9	adantrr	$⊢ (R \in CRingOps \land (a \in X \land b \in X)) \to R IdlGen \{a\} \in Idl (R)$
11		snssi	$⊢ b \in X \to \{b\} \subseteq X$
12	1 3	igenidl	$⊢ (R \in RingOps \land \{b\} \subseteq X) \to R IdlGen \{b\} \in Idl (R)$
13	4 11 12	syl2an	$⊢ (R \in CRingOps \land b \in X) \to R IdlGen \{b\} \in Idl (R)$
14	13	adantrl	$⊢ (R \in CRingOps \land (a \in X \land b \in X)) \to R IdlGen \{b\} \in Idl (R)$
15		raleq	$⊢ r = R IdlGen \{a\} \to (\forall x \in r \forall y \in s x H y \in P \leftrightarrow \forall x \in (R IdlGen \{a\}) \forall y \in s x H y \in P)$
16		sseq1	$⊢ r = R IdlGen \{a\} \to (r \subseteq P \leftrightarrow R IdlGen \{a\} \subseteq P)$
17	16	orbi1d	$⊢ r = R IdlGen \{a\} \to ((r \subseteq P \lor s \subseteq P) \leftrightarrow (R IdlGen \{a\} \subseteq P \lor s \subseteq P))$
18	15 17	imbi12d	$⊢ r = R IdlGen \{a\} \to ((\forall x \in r \forall y \in s x H y \in P \to (r \subseteq P \lor s \subseteq P)) \leftrightarrow (\forall x \in (R IdlGen \{a\}) \forall y \in s x H y \in P \to (R IdlGen \{a\} \subseteq P \lor s \subseteq P)))$
19		raleq	$⊢ s = R IdlGen \{b\} \to (\forall y \in s x H y \in P \leftrightarrow \forall y \in (R IdlGen \{b\}) x H y \in P)$
20	19	ralbidv	$⊢ s = R IdlGen \{b\} \to (\forall x \in (R IdlGen \{a\}) \forall y \in s x H y \in P \leftrightarrow \forall x \in (R IdlGen \{a\}) \forall y \in (R IdlGen \{b\}) x H y \in P)$
21		sseq1	$⊢ s = R IdlGen \{b\} \to (s \subseteq P \leftrightarrow R IdlGen \{b\} \subseteq P)$
22	21	orbi2d	$⊢ s = R IdlGen \{b\} \to ((R IdlGen \{a\} \subseteq P \lor s \subseteq P) \leftrightarrow (R IdlGen \{a\} \subseteq P \lor R IdlGen \{b\} \subseteq P))$
23	20 22	imbi12d	$⊢ s = R IdlGen \{b\} \to ((\forall x \in (R IdlGen \{a\}) \forall y \in s x H y \in P \to (R IdlGen \{a\} \subseteq P \lor s \subseteq P)) \leftrightarrow (\forall x \in (R IdlGen \{a\}) \forall y \in (R IdlGen \{b\}) x H y \in P \to (R IdlGen \{a\} \subseteq P \lor R IdlGen \{b\} \subseteq P)))$
24	18 23	rspc2v	$⊢ (R IdlGen \{a\} \in Idl (R) \land R IdlGen \{b\} \in Idl (R)) \to (\forall r \in Idl (R) \forall s \in Idl (R) (\forall x \in r \forall y \in s x H y \in P \to (r \subseteq P \lor s \subseteq P)) \to (\forall x \in (R IdlGen \{a\}) \forall y \in (R IdlGen \{b\}) x H y \in P \to (R IdlGen \{a\} \subseteq P \lor R IdlGen \{b\} \subseteq P)))$
25	10 14 24	syl2anc	$⊢ (R \in CRingOps \land (a \in X \land b \in X)) \to (\forall r \in Idl (R) \forall s \in Idl (R) (\forall x \in r \forall y \in s x H y \in P \to (r \subseteq P \lor s \subseteq P)) \to (\forall x \in (R IdlGen \{a\}) \forall y \in (R IdlGen \{b\}) x H y \in P \to (R IdlGen \{a\} \subseteq P \lor R IdlGen \{b\} \subseteq P)))$
26	25	adantlr	$⊢ ((R \in CRingOps \land P \in Idl (R)) \land (a \in X \land b \in X)) \to (\forall r \in Idl (R) \forall s \in Idl (R) (\forall x \in r \forall y \in s x H y \in P \to (r \subseteq P \lor s \subseteq P)) \to (\forall x \in (R IdlGen \{a\}) \forall y \in (R IdlGen \{b\}) x H y \in P \to (R IdlGen \{a\} \subseteq P \lor R IdlGen \{b\} \subseteq P)))$
27	1 2 3	prnc	$⊢ (R \in CRingOps \land a \in X) \to R IdlGen \{a\} = \{x \in X \| \exists r \in X x = r H a\}$
28		df-rab	$⊢ \{x \in X \| \exists r \in X x = r H a\} = \{x \| (x \in X \land \exists r \in X x = r H a)\}$
29	27 28	eqtrdi	$⊢ (R \in CRingOps \land a \in X) \to R IdlGen \{a\} = \{x \| (x \in X \land \exists r \in X x = r H a)\}$
30	29	eqabrd	$⊢ (R \in CRingOps \land a \in X) \to (x \in (R IdlGen \{a\}) \leftrightarrow (x \in X \land \exists r \in X x = r H a))$
31	30	adantrr	$⊢ (R \in CRingOps \land (a \in X \land b \in X)) \to (x \in (R IdlGen \{a\}) \leftrightarrow (x \in X \land \exists r \in X x = r H a))$
32	1 2 3	prnc	$⊢ (R \in CRingOps \land b \in X) \to R IdlGen \{b\} = \{y \in X \| \exists s \in X y = s H b\}$
33		df-rab	$⊢ \{y \in X \| \exists s \in X y = s H b\} = \{y \| (y \in X \land \exists s \in X y = s H b)\}$
34	32 33	eqtrdi	$⊢ (R \in CRingOps \land b \in X) \to R IdlGen \{b\} = \{y \| (y \in X \land \exists s \in X y = s H b)\}$
35	34	eqabrd	$⊢ (R \in CRingOps \land b \in X) \to (y \in (R IdlGen \{b\}) \leftrightarrow (y \in X \land \exists s \in X y = s H b))$
36	35	adantrl	$⊢ (R \in CRingOps \land (a \in X \land b \in X)) \to (y \in (R IdlGen \{b\}) \leftrightarrow (y \in X \land \exists s \in X y = s H b))$
37	31 36	anbi12d	$⊢ (R \in CRingOps \land (a \in X \land b \in X)) \to ((x \in (R IdlGen \{a\}) \land y \in (R IdlGen \{b\})) \leftrightarrow ((x \in X \land \exists r \in X x = r H a) \land (y \in X \land \exists s \in X y = s H b)))$
38	37	adantlr	$⊢ ((R \in CRingOps \land P \in Idl (R)) \land (a \in X \land b \in X)) \to ((x \in (R IdlGen \{a\}) \land y \in (R IdlGen \{b\})) \leftrightarrow ((x \in X \land \exists r \in X x = r H a) \land (y \in X \land \exists s \in X y = s H b)))$
39	38	adantr	$⊢ (((R \in CRingOps \land P \in Idl (R)) \land (a \in X \land b \in X)) \land a H b \in P) \to ((x \in (R IdlGen \{a\}) \land y \in (R IdlGen \{b\})) \leftrightarrow ((x \in X \land \exists r \in X x = r H a) \land (y \in X \land \exists s \in X y = s H b)))$
40		reeanv	$⊢ \exists r \in X \exists s \in X (x = r H a \land y = s H b) \leftrightarrow (\exists r \in X x = r H a \land \exists s \in X y = s H b)$
41	40	anbi2i	$⊢ ((x \in X \land y \in X) \land \exists r \in X \exists s \in X (x = r H a \land y = s H b)) \leftrightarrow ((x \in X \land y \in X) \land (\exists r \in X x = r H a \land \exists s \in X y = s H b))$
42		an4	$⊢ ((x \in X \land y \in X) \land (\exists r \in X x = r H a \land \exists s \in X y = s H b)) \leftrightarrow ((x \in X \land \exists r \in X x = r H a) \land (y \in X \land \exists s \in X y = s H b))$
43	41 42	bitri	$⊢ ((x \in X \land y \in X) \land \exists r \in X \exists s \in X (x = r H a \land y = s H b)) \leftrightarrow ((x \in X \land \exists r \in X x = r H a) \land (y \in X \land \exists s \in X y = s H b))$
44	1 2 3	crngm4	$⊢ (R \in CRingOps \land (r \in X \land s \in X) \land (a \in X \land b \in X)) \to (r H s) H (a H b) = (r H a) H (s H b)$
45	44	3com23	$⊢ (R \in CRingOps \land (a \in X \land b \in X) \land (r \in X \land s \in X)) \to (r H s) H (a H b) = (r H a) H (s H b)$
46	45	3expa	$⊢ ((R \in CRingOps \land (a \in X \land b \in X)) \land (r \in X \land s \in X)) \to (r H s) H (a H b) = (r H a) H (s H b)$
47	46	adantllr	$⊢ (((R \in CRingOps \land P \in Idl (R)) \land (a \in X \land b \in X)) \land (r \in X \land s \in X)) \to (r H s) H (a H b) = (r H a) H (s H b)$
48	47	adantlr	$⊢ ((((R \in CRingOps \land P \in Idl (R)) \land (a \in X \land b \in X)) \land a H b \in P) \land (r \in X \land s \in X)) \to (r H s) H (a H b) = (r H a) H (s H b)$
49	1 2 3	rngocl	$⊢ (R \in RingOps \land r \in X \land s \in X) \to r H s \in X$
50	4 49	syl3an1	$⊢ (R \in CRingOps \land r \in X \land s \in X) \to r H s \in X$
51	50	3expb	$⊢ (R \in CRingOps \land (r \in X \land s \in X)) \to r H s \in X$
52	51	adantlr	$⊢ ((R \in CRingOps \land P \in Idl (R)) \land (r \in X \land s \in X)) \to r H s \in X$
53	52	adantlr	$⊢ (((R \in CRingOps \land P \in Idl (R)) \land a H b \in P) \land (r \in X \land s \in X)) \to r H s \in X$
54	1 2 3	idllmulcl	$⊢ ((R \in RingOps \land P \in Idl (R)) \land (a H b \in P \land r H s \in X)) \to (r H s) H (a H b) \in P$
55	4 54	sylanl1	$⊢ ((R \in CRingOps \land P \in Idl (R)) \land (a H b \in P \land r H s \in X)) \to (r H s) H (a H b) \in P$
56	55	anassrs	$⊢ (((R \in CRingOps \land P \in Idl (R)) \land a H b \in P) \land r H s \in X) \to (r H s) H (a H b) \in P$
57	53 56	syldan	$⊢ (((R \in CRingOps \land P \in Idl (R)) \land a H b \in P) \land (r \in X \land s \in X)) \to (r H s) H (a H b) \in P$
58	57	adantllr	$⊢ ((((R \in CRingOps \land P \in Idl (R)) \land (a \in X \land b \in X)) \land a H b \in P) \land (r \in X \land s \in X)) \to (r H s) H (a H b) \in P$
59	48 58	eqeltrrd	$⊢ ((((R \in CRingOps \land P \in Idl (R)) \land (a \in X \land b \in X)) \land a H b \in P) \land (r \in X \land s \in X)) \to (r H a) H (s H b) \in P$
60		oveq12	$⊢ (x = r H a \land y = s H b) \to x H y = (r H a) H (s H b)$
61	60	eleq1d	$⊢ (x = r H a \land y = s H b) \to (x H y \in P \leftrightarrow (r H a) H (s H b) \in P)$
62	59 61	syl5ibrcom	$⊢ ((((R \in CRingOps \land P \in Idl (R)) \land (a \in X \land b \in X)) \land a H b \in P) \land (r \in X \land s \in X)) \to ((x = r H a \land y = s H b) \to x H y \in P)$
63	62	rexlimdvva	$⊢ (((R \in CRingOps \land P \in Idl (R)) \land (a \in X \land b \in X)) \land a H b \in P) \to (\exists r \in X \exists s \in X (x = r H a \land y = s H b) \to x H y \in P)$
64	63	adantld	$⊢ (((R \in CRingOps \land P \in Idl (R)) \land (a \in X \land b \in X)) \land a H b \in P) \to (((x \in X \land y \in X) \land \exists r \in X \exists s \in X (x = r H a \land y = s H b)) \to x H y \in P)$
65	43 64	biimtrrid	$⊢ (((R \in CRingOps \land P \in Idl (R)) \land (a \in X \land b \in X)) \land a H b \in P) \to (((x \in X \land \exists r \in X x = r H a) \land (y \in X \land \exists s \in X y = s H b)) \to x H y \in P)$
66	39 65	sylbid	$⊢ (((R \in CRingOps \land P \in Idl (R)) \land (a \in X \land b \in X)) \land a H b \in P) \to ((x \in (R IdlGen \{a\}) \land y \in (R IdlGen \{b\})) \to x H y \in P)$
67	66	ralrimivv	$⊢ (((R \in CRingOps \land P \in Idl (R)) \land (a \in X \land b \in X)) \land a H b \in P) \to \forall x \in (R IdlGen \{a\}) \forall y \in (R IdlGen \{b\}) x H y \in P$
68	67	ex	$⊢ ((R \in CRingOps \land P \in Idl (R)) \land (a \in X \land b \in X)) \to (a H b \in P \to \forall x \in (R IdlGen \{a\}) \forall y \in (R IdlGen \{b\}) x H y \in P)$
69	1 3	igenss	$⊢ (R \in RingOps \land \{a\} \subseteq X) \to \{a\} \subseteq R IdlGen \{a\}$
70	4 7 69	syl2an	$⊢ (R \in CRingOps \land a \in X) \to \{a\} \subseteq R IdlGen \{a\}$
71		vex	$⊢ a \in V$
72	71	snss	$⊢ a \in (R IdlGen \{a\}) \leftrightarrow \{a\} \subseteq R IdlGen \{a\}$
73	70 72	sylibr	$⊢ (R \in CRingOps \land a \in X) \to a \in (R IdlGen \{a\})$
74	73	adantrr	$⊢ (R \in CRingOps \land (a \in X \land b \in X)) \to a \in (R IdlGen \{a\})$
75		ssel	$⊢ R IdlGen \{a\} \subseteq P \to (a \in (R IdlGen \{a\}) \to a \in P)$
76	74 75	syl5com	$⊢ (R \in CRingOps \land (a \in X \land b \in X)) \to (R IdlGen \{a\} \subseteq P \to a \in P)$
77	1 3	igenss	$⊢ (R \in RingOps \land \{b\} \subseteq X) \to \{b\} \subseteq R IdlGen \{b\}$
78	4 11 77	syl2an	$⊢ (R \in CRingOps \land b \in X) \to \{b\} \subseteq R IdlGen \{b\}$
79		vex	$⊢ b \in V$
80	79	snss	$⊢ b \in (R IdlGen \{b\}) \leftrightarrow \{b\} \subseteq R IdlGen \{b\}$
81	78 80	sylibr	$⊢ (R \in CRingOps \land b \in X) \to b \in (R IdlGen \{b\})$
82	81	adantrl	$⊢ (R \in CRingOps \land (a \in X \land b \in X)) \to b \in (R IdlGen \{b\})$
83		ssel	$⊢ R IdlGen \{b\} \subseteq P \to (b \in (R IdlGen \{b\}) \to b \in P)$
84	82 83	syl5com	$⊢ (R \in CRingOps \land (a \in X \land b \in X)) \to (R IdlGen \{b\} \subseteq P \to b \in P)$
85	76 84	orim12d	$⊢ (R \in CRingOps \land (a \in X \land b \in X)) \to ((R IdlGen \{a\} \subseteq P \lor R IdlGen \{b\} \subseteq P) \to (a \in P \lor b \in P))$
86	85	adantlr	$⊢ ((R \in CRingOps \land P \in Idl (R)) \land (a \in X \land b \in X)) \to ((R IdlGen \{a\} \subseteq P \lor R IdlGen \{b\} \subseteq P) \to (a \in P \lor b \in P))$
87	68 86	imim12d	$⊢ ((R \in CRingOps \land P \in Idl (R)) \land (a \in X \land b \in X)) \to ((\forall x \in (R IdlGen \{a\}) \forall y \in (R IdlGen \{b\}) x H y \in P \to (R IdlGen \{a\} \subseteq P \lor R IdlGen \{b\} \subseteq P)) \to (a H b \in P \to (a \in P \lor b \in P)))$
88	26 87	syld	$⊢ ((R \in CRingOps \land P \in Idl (R)) \land (a \in X \land b \in X)) \to (\forall r \in Idl (R) \forall s \in Idl (R) (\forall x \in r \forall y \in s x H y \in P \to (r \subseteq P \lor s \subseteq P)) \to (a H b \in P \to (a \in P \lor b \in P)))$
89	88	ralrimdvva	$⊢ (R \in CRingOps \land P \in Idl (R)) \to (\forall r \in Idl (R) \forall s \in Idl (R) (\forall x \in r \forall y \in s x H y \in P \to (r \subseteq P \lor s \subseteq P)) \to \forall a \in X \forall b \in X (a H b \in P \to (a \in P \lor b \in P)))$
90	89	ex	$⊢ R \in CRingOps \to (P \in Idl (R) \to (\forall r \in Idl (R) \forall s \in Idl (R) (\forall x \in r \forall y \in s x H y \in P \to (r \subseteq P \lor s \subseteq P)) \to \forall a \in X \forall b \in X (a H b \in P \to (a \in P \lor b \in P))))$
91	90	adantrd	$⊢ R \in CRingOps \to ((P \in Idl (R) \land P \neq X) \to (\forall r \in Idl (R) \forall s \in Idl (R) (\forall x \in r \forall y \in s x H y \in P \to (r \subseteq P \lor s \subseteq P)) \to \forall a \in X \forall b \in X (a H b \in P \to (a \in P \lor b \in P))))$
92	91	imdistand	$⊢ R \in CRingOps \to (((P \in Idl (R) \land P \neq X) \land \forall r \in Idl (R) \forall s \in Idl (R) (\forall x \in r \forall y \in s x H y \in P \to (r \subseteq P \lor s \subseteq P))) \to ((P \in Idl (R) \land P \neq X) \land \forall a \in X \forall b \in X (a H b \in P \to (a \in P \lor b \in P))))$
93		df-3an	$⊢ (P \in Idl (R) \land P \neq X \land \forall r \in Idl (R) \forall s \in Idl (R) (\forall x \in r \forall y \in s x H y \in P \to (r \subseteq P \lor s \subseteq P))) \leftrightarrow ((P \in Idl (R) \land P \neq X) \land \forall r \in Idl (R) \forall s \in Idl (R) (\forall x \in r \forall y \in s x H y \in P \to (r \subseteq P \lor s \subseteq P)))$
94		df-3an	$⊢ (P \in Idl (R) \land P \neq X \land \forall a \in X \forall b \in X (a H b \in P \to (a \in P \lor b \in P))) \leftrightarrow ((P \in Idl (R) \land P \neq X) \land \forall a \in X \forall b \in X (a H b \in P \to (a \in P \lor b \in P)))$
95	92 93 94	3imtr4g	$⊢ R \in CRingOps \to ((P \in Idl (R) \land P \neq X \land \forall r \in Idl (R) \forall s \in Idl (R) (\forall x \in r \forall y \in s x H y \in P \to (r \subseteq P \lor s \subseteq P))) \to (P \in Idl (R) \land P \neq X \land \forall a \in X \forall b \in X (a H b \in P \to (a \in P \lor b \in P))))$
96	6 95	sylbid	$⊢ R \in CRingOps \to (P \in PrIdl (R) \to (P \in Idl (R) \land P \neq X \land \forall a \in X \forall b \in X (a H b \in P \to (a \in P \lor b \in P))))$
97	1 2 3	ispridl2	$⊢ (R \in RingOps \land (P \in Idl (R) \land P \neq X \land \forall a \in X \forall b \in X (a H b \in P \to (a \in P \lor b \in P)))) \to P \in PrIdl (R)$
98	97	ex	$⊢ R \in RingOps \to ((P \in Idl (R) \land P \neq X \land \forall a \in X \forall b \in X (a H b \in P \to (a \in P \lor b \in P))) \to P \in PrIdl (R))$
99	4 98	syl	$⊢ R \in CRingOps \to ((P \in Idl (R) \land P \neq X \land \forall a \in X \forall b \in X (a H b \in P \to (a \in P \lor b \in P))) \to P \in PrIdl (R))$
100	96 99	impbid	$⊢ R \in CRingOps \to (P \in PrIdl (R) \leftrightarrow (P \in Idl (R) \land P \neq X \land \forall a \in X \forall b \in X (a H b \in P \to (a \in P \lor b \in P))))$

Metamath Proof Explorer

Theorem ispridlc

Proof