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 = opp r R
2idlval.j J = LIdeal O
2idlval.t T = 2Ideal R
Assertion 2idlval T = I J

Proof

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 LIdeal r = LIdeal R
6 5 1 eqtr4di r = R LIdeal r = I
7 fveq2 r = R opp r r = opp r R
8 7 2 eqtr4di r = R opp r r = O
9 8 fveq2d r = R LIdeal opp r r = LIdeal O
10 9 3 eqtr4di r = R LIdeal opp r r = J
11 6 10 ineq12d r = R LIdeal r LIdeal opp r r = I J
12 df-2idl 2Ideal = r V LIdeal r LIdeal opp r r
13 1 fvexi I V
14 13 inex1 I J V
15 11 12 14 fvmpt R V 2Ideal R = I J
16 fvprc ¬ R V 2Ideal R =
17 inss1 I J I
18 fvprc ¬ R V LIdeal R =
19 1 18 syl5eq ¬ R V I =
20 sseq0 I J I I = I J =
21 17 19 20 sylancr ¬ R V I J =
22 16 21 eqtr4d ¬ R V 2Ideal R = I J
23 15 22 pm2.61i 2Ideal R = I J
24 4 23 eqtri T = I J