isidl

Description: The predicate "is an ideal of the ring R ". (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	isidl	$⊢ R \in RingOps \to (I \in Idl (R) \leftrightarrow (I \subseteq X \land 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	1 2 3 4	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)))\}$
6	5	eleq2d	$⊢ R \in RingOps \to (I \in Idl (R) \leftrightarrow I \in \{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)))\})$
7	1	fvexi	$⊢ G \in V$
8	7	rnex	$⊢ ran G \in V$
9	3 8	eqeltri	$⊢ X \in V$
10	9	elpw2	$⊢ I \in 𝒫 X \leftrightarrow I \subseteq X$
11	10	anbi1i	$⊢ (I \in 𝒫 X \land (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)))) \leftrightarrow (I \subseteq X \land (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))))$
12		eleq2	$⊢ i = I \to (Z \in i \leftrightarrow Z \in I)$
13		eleq2	$⊢ i = I \to (x G y \in i \leftrightarrow x G y \in I)$
14	13	raleqbi1dv	$⊢ i = I \to (\forall y \in i x G y \in i \leftrightarrow \forall y \in I x G y \in I)$
15		eleq2	$⊢ i = I \to (z H x \in i \leftrightarrow z H x \in I)$
16		eleq2	$⊢ i = I \to (x H z \in i \leftrightarrow x H z \in I)$
17	15 16	anbi12d	$⊢ i = I \to ((z H x \in i \land x H z \in i) \leftrightarrow (z H x \in I \land x H z \in I))$
18	17	ralbidv	$⊢ i = I \to (\forall z \in X (z H x \in i \land x H z \in i) \leftrightarrow \forall z \in X (z H x \in I \land x H z \in I))$
19	14 18	anbi12d	$⊢ i = I \to ((\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)) \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)))$
20	19	raleqbi1dv	$⊢ i = I \to (\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)) \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)))$
21	12 20	anbi12d	$⊢ i = I \to ((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))) \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))))$
22	21	elrab	$⊢ I \in \{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)))\} \leftrightarrow (I \in 𝒫 X \land (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))))$
23		3anass	$⊢ (I \subseteq X \land 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))) \leftrightarrow (I \subseteq X \land (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))))$
24	11 22 23	3bitr4i	$⊢ I \in \{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)))\} \leftrightarrow (I \subseteq X \land 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)))$
25	6 24	bitrdi	$⊢ R \in RingOps \to (I \in Idl (R) \leftrightarrow (I \subseteq X \land 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 isidl

Proof