2idlval

Description: Definition of a two-sided ideal. (Contributed by Mario Carneiro, 14-Jun-2015)

Step	Hyp	Ref	Expression
1		2idlval.i	$⊢ I = LIdeal (R)$
2		2idlval.o	$⊢ O = {opp}_{r} (R)$
3		2idlval.j	$⊢ J = LIdeal (O)$
4		2idlval.t	$⊢ T = 2Ideal (R)$
5		fveq2	$⊢ r = R \to LIdeal (r) = LIdeal (R)$
6	5 1	eqtr4di	$⊢ r = R \to LIdeal (r) = I$
7		fveq2	$⊢ r = R \to {opp}_{r} (r) = {opp}_{r} (R)$
8	7 2	eqtr4di	$⊢ r = R \to {opp}_{r} (r) = O$
9	8	fveq2d	$⊢ r = R \to LIdeal ({opp}_{r} (r)) = LIdeal (O)$
10	9 3	eqtr4di	$⊢ r = R \to LIdeal ({opp}_{r} (r)) = J$
11	6 10	ineq12d	$⊢ r = R \to LIdeal (r) \cap LIdeal ({opp}_{r} (r)) = I \cap J$
12		df-2idl	$⊢ 2Ideal = (r \in V ⟼ LIdeal (r) \cap LIdeal ({opp}_{r} (r)))$
13	1	fvexi	$⊢ I \in V$
14	13	inex1	$⊢ I \cap J \in V$
15	11 12 14	fvmpt	$⊢ R \in V \to 2Ideal (R) = I \cap J$
16		fvprc	$⊢ \neg R \in V \to 2Ideal (R) = \emptyset$
17		inss1	$⊢ I \cap J \subseteq I$
18		fvprc	$⊢ \neg R \in V \to LIdeal (R) = \emptyset$
19	1 18	eqtrid	$⊢ \neg R \in V \to I = \emptyset$
20		sseq0	$⊢ (I \cap J \subseteq I \land I = \emptyset) \to I \cap J = \emptyset$
21	17 19 20	sylancr	$⊢ \neg R \in V \to I \cap J = \emptyset$
22	16 21	eqtr4d	$⊢ \neg R \in V \to 2Ideal (R) = I \cap J$
23	15 22	pm2.61i	$⊢ 2Ideal (R) = I \cap J$
24	4 23	eqtri	$⊢ T = I \cap J$

Metamath Proof Explorer