Metamath Proof Explorer

Theorem 2idlval

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

Ref Expression
Hypotheses 2idlval.i 
|- I = ( LIdeal ` R )
2idlval.o 
|- O = ( oppR ` R )
2idlval.j 
|- J = ( LIdeal ` O )
2idlval.t 
|- T = ( 2Ideal ` R )
Assertion 2idlval 
|- T = ( I i^i J )

Proof

Step Hyp Ref Expression
1 2idlval.i 
 |-  I = ( LIdeal ` R )
2 2idlval.o 
 |-  O = ( oppR ` R )
3 2idlval.j 
 |-  J = ( LIdeal ` O )
4 2idlval.t 
 |-  T = ( 2Ideal ` R )
5 fveq2 
 |-  ( r = R -> ( LIdeal ` r ) = ( LIdeal ` R ) )
6 5 1 eqtr4di 
 |-  ( r = R -> ( LIdeal ` r ) = I )
7 fveq2 
 |-  ( r = R -> ( oppR ` r ) = ( oppR ` R ) )
8 7 2 eqtr4di 
 |-  ( r = R -> ( oppR ` r ) = O )
9 8 fveq2d 
 |-  ( r = R -> ( LIdeal ` ( oppR ` r ) ) = ( LIdeal ` O ) )
10 9 3 eqtr4di 
 |-  ( r = R -> ( LIdeal ` ( oppR ` r ) ) = J )
11 6 10 ineq12d 
 |-  ( r = R -> ( ( LIdeal ` r ) i^i ( LIdeal ` ( oppR ` r ) ) ) = ( I i^i J ) )
12 df-2idl 
 |-  2Ideal = ( r e. _V |-> ( ( LIdeal ` r ) i^i ( LIdeal ` ( oppR ` r ) ) ) )
13 1 fvexi 
 |-  I e. _V
14 13 inex1 
 |-  ( I i^i J ) e. _V
15 11 12 14 fvmpt 
 |-  ( R e. _V -> ( 2Ideal ` R ) = ( I i^i J ) )
16 fvprc 
 |-  ( -. R e. _V -> ( 2Ideal ` R ) = (/) )
17 inss1 
 |-  ( I i^i J ) C_ I
18 fvprc 
 |-  ( -. R e. _V -> ( LIdeal ` R ) = (/) )
19 1 18 syl5eq 
 |-  ( -. R e. _V -> I = (/) )
20 sseq0 
 |-  ( ( ( I i^i J ) C_ I /\ I = (/) ) -> ( I i^i J ) = (/) )
21 17 19 20 sylancr 
 |-  ( -. R e. _V -> ( I i^i J ) = (/) )
22 16 21 eqtr4d 
 |-  ( -. R e. _V -> ( 2Ideal ` R ) = ( I i^i J ) )
23 15 22 pm2.61i 
 |-  ( 2Ideal ` R ) = ( I i^i J )
24 4 23 eqtri 
 |-  T = ( I i^i J )