Theorem 2idlval

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

	Ref	Expression
Hypotheses	2idlval.i	⊢ 𝐼 = ( LIdeal ‘ 𝑅 )
	2idlval.o	⊢ 𝑂 = ( oppr ‘ 𝑅 )
	2idlval.j	⊢ 𝐽 = ( LIdeal ‘ 𝑂 )
	2idlval.t	⊢ 𝑇 = ( 2Ideal ‘ 𝑅 )
Assertion	2idlval	⊢ 𝑇 = ( 𝐼 ∩ 𝐽 )

Proof

Step	Hyp	Ref	Expression
1		2idlval.i	⊢ 𝐼 = ( LIdeal ‘ 𝑅 )
2		2idlval.o	⊢ 𝑂 = ( oppr ‘ 𝑅 )
3		2idlval.j	⊢ 𝐽 = ( LIdeal ‘ 𝑂 )
4		2idlval.t	⊢ 𝑇 = ( 2Ideal ‘ 𝑅 )
5		fveq2	⊢ ( 𝑟 = 𝑅 → ( LIdeal ‘ 𝑟 ) = ( LIdeal ‘ 𝑅 ) )
6	5 1	eqtr4di	⊢ ( 𝑟 = 𝑅 → ( LIdeal ‘ 𝑟 ) = 𝐼 )
7		fveq2	⊢ ( 𝑟 = 𝑅 → ( oppr ‘ 𝑟 ) = ( oppr ‘ 𝑅 ) )
8	7 2	eqtr4di	⊢ ( 𝑟 = 𝑅 → ( oppr ‘ 𝑟 ) = 𝑂 )
9	8	fveq2d	⊢ ( 𝑟 = 𝑅 → ( LIdeal ‘ ( oppr ‘ 𝑟 ) ) = ( LIdeal ‘ 𝑂 ) )
10	9 3	eqtr4di	⊢ ( 𝑟 = 𝑅 → ( LIdeal ‘ ( oppr ‘ 𝑟 ) ) = 𝐽 )
11	6 10	ineq12d	⊢ ( 𝑟 = 𝑅 → ( ( LIdeal ‘ 𝑟 ) ∩ ( LIdeal ‘ ( oppr ‘ 𝑟 ) ) ) = ( 𝐼 ∩ 𝐽 ) )
12		df-2idl	⊢ 2Ideal = ( 𝑟 ∈ V ↦ ( ( LIdeal ‘ 𝑟 ) ∩ ( LIdeal ‘ ( oppr ‘ 𝑟 ) ) ) )
13	1	fvexi	⊢ 𝐼 ∈ V
14	13	inex1	⊢ ( 𝐼 ∩ 𝐽 ) ∈ V
15	11 12 14	fvmpt	⊢ ( 𝑅 ∈ V → ( 2Ideal ‘ 𝑅 ) = ( 𝐼 ∩ 𝐽 ) )
16		fvprc	⊢ ( ¬ 𝑅 ∈ V → ( 2Ideal ‘ 𝑅 ) = ∅ )
17		inss1	⊢ ( 𝐼 ∩ 𝐽 ) ⊆ 𝐼
18		fvprc	⊢ ( ¬ 𝑅 ∈ V → ( LIdeal ‘ 𝑅 ) = ∅ )
19	1 18	syl5eq	⊢ ( ¬ 𝑅 ∈ V → 𝐼 = ∅ )
20		sseq0	⊢ ( ( ( 𝐼 ∩ 𝐽 ) ⊆ 𝐼 ∧ 𝐼 = ∅ ) → ( 𝐼 ∩ 𝐽 ) = ∅ )
21	17 19 20	sylancr	⊢ ( ¬ 𝑅 ∈ V → ( 𝐼 ∩ 𝐽 ) = ∅ )
22	16 21	eqtr4d	⊢ ( ¬ 𝑅 ∈ V → ( 2Ideal ‘ 𝑅 ) = ( 𝐼 ∩ 𝐽 ) )
23	15 22	pm2.61i	⊢ ( 2Ideal ‘ 𝑅 ) = ( 𝐼 ∩ 𝐽 )
24	4 23	eqtri	⊢ 𝑇 = ( 𝐼 ∩ 𝐽 )