This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 eqtrid ⊢ ( ¬ 𝑅 ∈ 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 ⊢ 𝑇 = ( 𝐼 ∩ 𝐽 )