Theorem 2idlval

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

	Ref	Expression
Hypotheses	2idlval.i	$$⊢I=\mathrm{LIdeal}\left(R\right)$$
	2idlval.o	$$⊢O={opp}_r\left(R\right)$$
	2idlval.j	$$⊢J=\mathrm{LIdeal}\left(O\right)$$
	2idlval.t	$$⊢T=\mathrm{2Ideal}\left(R\right)$$
Assertion	2idlval	$$⊢T=I\cap J$$

Proof

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