idlval

Description: The class of ideals of a ring. (Contributed by Jeff Madsen, 10-Jun-2010)

	Ref	Expression
Hypotheses	idlval.1	$⊢ G = 1^{st} (R)$
	idlval.2	$⊢ H = 2^{nd} (R)$
	idlval.3	$⊢ X = ran G$
	idlval.4	$⊢ Z = GId (G)$
Assertion	idlval	$⊢ R \in RingOps \to Idl (R) = \{i \in 𝒫 X \| (Z \in i \land \forall x \in i (\forall y \in i x G y \in i \land \forall z \in X (z H x \in i \land x H z \in i)))\}$

Proof

Step	Hyp	Ref	Expression
1		idlval.1	$⊢ G = 1^{st} (R)$
2		idlval.2	$⊢ H = 2^{nd} (R)$
3		idlval.3	$⊢ X = ran G$
4		idlval.4	$⊢ Z = GId (G)$
5		fveq2	$⊢ r = R \to 1^{st} (r) = 1^{st} (R)$
6	5 1	eqtr4di	$⊢ r = R \to 1^{st} (r) = G$
7	6	rneqd	$⊢ r = R \to ran 1^{st} (r) = ran G$
8	7 3	eqtr4di	$⊢ r = R \to ran 1^{st} (r) = X$
9	8	pweqd	$⊢ r = R \to 𝒫 ran 1^{st} (r) = 𝒫 X$
10	6	fveq2d	$⊢ r = R \to GId (1^{st} (r)) = GId (G)$
11	10 4	eqtr4di	$⊢ r = R \to GId (1^{st} (r)) = Z$
12	11	eleq1d	$⊢ r = R \to (GId (1^{st} (r)) \in i \leftrightarrow Z \in i)$
13	6	oveqd	$⊢ r = R \to x 1^{st} (r) y = x G y$
14	13	eleq1d	$⊢ r = R \to (x 1^{st} (r) y \in i \leftrightarrow x G y \in i)$
15	14	ralbidv	$⊢ r = R \to (\forall y \in i x 1^{st} (r) y \in i \leftrightarrow \forall y \in i x G y \in i)$
16		fveq2	$⊢ r = R \to 2^{nd} (r) = 2^{nd} (R)$
17	16 2	eqtr4di	$⊢ r = R \to 2^{nd} (r) = H$
18	17	oveqd	$⊢ r = R \to z 2^{nd} (r) x = z H x$
19	18	eleq1d	$⊢ r = R \to (z 2^{nd} (r) x \in i \leftrightarrow z H x \in i)$
20	17	oveqd	$⊢ r = R \to x 2^{nd} (r) z = x H z$
21	20	eleq1d	$⊢ r = R \to (x 2^{nd} (r) z \in i \leftrightarrow x H z \in i)$
22	19 21	anbi12d	$⊢ r = R \to ((z 2^{nd} (r) x \in i \land x 2^{nd} (r) z \in i) \leftrightarrow (z H x \in i \land x H z \in i))$
23	8 22	raleqbidv	$⊢ r = R \to (\forall z \in ran 1^{st} (r) (z 2^{nd} (r) x \in i \land x 2^{nd} (r) z \in i) \leftrightarrow \forall z \in X (z H x \in i \land x H z \in i))$
24	15 23	anbi12d	$⊢ r = R \to ((\forall y \in i x 1^{st} (r) y \in i \land \forall z \in ran 1^{st} (r) (z 2^{nd} (r) x \in i \land x 2^{nd} (r) z \in i)) \leftrightarrow (\forall y \in i x G y \in i \land \forall z \in X (z H x \in i \land x H z \in i)))$
25	24	ralbidv	$⊢ r = R \to (\forall x \in i (\forall y \in i x 1^{st} (r) y \in i \land \forall z \in ran 1^{st} (r) (z 2^{nd} (r) x \in i \land x 2^{nd} (r) z \in i)) \leftrightarrow \forall x \in i (\forall y \in i x G y \in i \land \forall z \in X (z H x \in i \land x H z \in i)))$
26	12 25	anbi12d	$⊢ r = R \to ((GId (1^{st} (r)) \in i \land \forall x \in i (\forall y \in i x 1^{st} (r) y \in i \land \forall z \in ran 1^{st} (r) (z 2^{nd} (r) x \in i \land x 2^{nd} (r) z \in i))) \leftrightarrow (Z \in i \land \forall x \in i (\forall y \in i x G y \in i \land \forall z \in X (z H x \in i \land x H z \in i))))$
27	9 26	rabeqbidv	$⊢ r = R \to \{i \in 𝒫 ran 1^{st} (r) \| (GId (1^{st} (r)) \in i \land \forall x \in i (\forall y \in i x 1^{st} (r) y \in i \land \forall z \in ran 1^{st} (r) (z 2^{nd} (r) x \in i \land x 2^{nd} (r) z \in i)))\} = \{i \in 𝒫 X \| (Z \in i \land \forall x \in i (\forall y \in i x G y \in i \land \forall z \in X (z H x \in i \land x H z \in i)))\}$
28		df-idl	$⊢ Idl = (r \in RingOps ⟼ \{i \in 𝒫 ran 1^{st} (r) \| (GId (1^{st} (r)) \in i \land \forall x \in i (\forall y \in i x 1^{st} (r) y \in i \land \forall z \in ran 1^{st} (r) (z 2^{nd} (r) x \in i \land x 2^{nd} (r) z \in i)))\})$
29	1	fvexi	$⊢ G \in V$
30	29	rnex	$⊢ ran G \in V$
31	3 30	eqeltri	$⊢ X \in V$
32	31	pwex	$⊢ 𝒫 X \in V$
33	32	rabex	$⊢ \{i \in 𝒫 X \| (Z \in i \land \forall x \in i (\forall y \in i x G y \in i \land \forall z \in X (z H x \in i \land x H z \in i)))\} \in V$
34	27 28 33	fvmpt	$⊢ R \in RingOps \to Idl (R) = \{i \in 𝒫 X \| (Z \in i \land \forall x \in i (\forall y \in i x G y \in i \land \forall z \in X (z H x \in i \land x H z \in i)))\}$

Metamath Proof Explorer

Theorem idlval

Proof