Metamath Proof Explorer

Theorem maxidlval

Description: The set of maximal ideals of a ring. (Contributed by Jeff Madsen, 5-Jan-2011)

		Ref	Expression
	Hypotheses	maxidlval.1	$⊢ G = 1^{st} (R)$
		maxidlval.2	$⊢ X = ran G$
	Assertion	maxidlval	$⊢ R \in RingOps \to MaxIdl (R) = \{i \in Idl (R) \| (i \neq X \land \forall j \in Idl (R) (i \subseteq j \to (j = i \lor j = X)))\}$

Proof

Step	Hyp	Ref	Expression
1		maxidlval.1	$⊢ G = 1^{st} (R)$
2		maxidlval.2	$⊢ X = ran G$
3		fveq2	$⊢ r = R \to Idl (r) = Idl (R)$
4		fveq2	$⊢ r = R \to 1^{st} (r) = 1^{st} (R)$
5	4 1	eqtr4di	$⊢ r = R \to 1^{st} (r) = G$
6	5	rneqd	$⊢ r = R \to ran 1^{st} (r) = ran G$
7	6 2	eqtr4di	$⊢ r = R \to ran 1^{st} (r) = X$
8	7	neeq2d	$⊢ r = R \to (i \neq ran 1^{st} (r) \leftrightarrow i \neq X)$
9	7	eqeq2d	$⊢ r = R \to (j = ran 1^{st} (r) \leftrightarrow j = X)$
10	9	orbi2d	$⊢ r = R \to ((j = i \lor j = ran 1^{st} (r)) \leftrightarrow (j = i \lor j = X))$
11	10	imbi2d	$⊢ r = R \to ((i \subseteq j \to (j = i \lor j = ran 1^{st} (r))) \leftrightarrow (i \subseteq j \to (j = i \lor j = X)))$
12	3 11	raleqbidv	$⊢ r = R \to (\forall j \in Idl (r) (i \subseteq j \to (j = i \lor j = ran 1^{st} (r))) \leftrightarrow \forall j \in Idl (R) (i \subseteq j \to (j = i \lor j = X)))$
13	8 12	anbi12d	$⊢ r = R \to ((i \neq ran 1^{st} (r) \land \forall j \in Idl (r) (i \subseteq j \to (j = i \lor j = ran 1^{st} (r)))) \leftrightarrow (i \neq X \land \forall j \in Idl (R) (i \subseteq j \to (j = i \lor j = X))))$
14	3 13	rabeqbidv	$⊢ r = R \to \{i \in Idl (r) \| (i \neq ran 1^{st} (r) \land \forall j \in Idl (r) (i \subseteq j \to (j = i \lor j = ran 1^{st} (r))))\} = \{i \in Idl (R) \| (i \neq X \land \forall j \in Idl (R) (i \subseteq j \to (j = i \lor j = X)))\}$
15		df-maxidl	$⊢ MaxIdl = (r \in RingOps ⟼ \{i \in Idl (r) \| (i \neq ran 1^{st} (r) \land \forall j \in Idl (r) (i \subseteq j \to (j = i \lor j = ran 1^{st} (r))))\})$
16		fvex	$⊢ Idl (R) \in V$
17	16	rabex	$⊢ \{i \in Idl (R) \| (i \neq X \land \forall j \in Idl (R) (i \subseteq j \to (j = i \lor j = X)))\} \in V$
18	14 15 17	fvmpt	$⊢ R \in RingOps \to MaxIdl (R) = \{i \in Idl (R) \| (i \neq X \land \forall j \in Idl (R) (i \subseteq j \to (j = i \lor j = X)))\}$