Metamath Proof Explorer


Theorem isidl

Description: The predicate "is an ideal of the ring R ". (Contributed by Jeff Madsen, 10-Jun-2010)

Ref Expression
Hypotheses idlval.1 G = 1 st R
idlval.2 H = 2 nd R
idlval.3 X = ran G
idlval.4 Z = GId G
Assertion isidl R RingOps I Idl R I X Z I x I y I x G y I z X z H x I x H z I

Proof

Step Hyp Ref Expression
1 idlval.1 G = 1 st R
2 idlval.2 H = 2 nd R
3 idlval.3 X = ran G
4 idlval.4 Z = GId G
5 1 2 3 4 idlval R RingOps Idl R = i 𝒫 X | Z i x i y i x G y i z X z H x i x H z i
6 5 eleq2d R RingOps I Idl R I i 𝒫 X | Z i x i y i x G y i z X z H x i x H z i
7 1 fvexi G V
8 7 rnex ran G V
9 3 8 eqeltri X V
10 9 elpw2 I 𝒫 X I X
11 10 anbi1i I 𝒫 X Z I x I y I x G y I z X z H x I x H z I I X Z I x I y I x G y I z X z H x I x H z I
12 eleq2 i = I Z i Z I
13 eleq2 i = I x G y i x G y I
14 13 raleqbi1dv i = I y i x G y i y I x G y I
15 eleq2 i = I z H x i z H x I
16 eleq2 i = I x H z i x H z I
17 15 16 anbi12d i = I z H x i x H z i z H x I x H z I
18 17 ralbidv i = I z X z H x i x H z i z X z H x I x H z I
19 14 18 anbi12d i = I y i x G y i z X z H x i x H z i y I x G y I z X z H x I x H z I
20 19 raleqbi1dv i = I x i y i x G y i z X z H x i x H z i x I y I x G y I z X z H x I x H z I
21 12 20 anbi12d i = I Z i x i y i x G y i z X z H x i x H z i Z I x I y I x G y I z X z H x I x H z I
22 21 elrab I i 𝒫 X | Z i x i y i x G y i z X z H x i x H z i I 𝒫 X Z I x I y I x G y I z X z H x I x H z I
23 3anass I X Z I x I y I x G y I z X z H x I x H z I I X Z I x I y I x G y I z X z H x I x H z I
24 11 22 23 3bitr4i I i 𝒫 X | Z i x i y i x G y i z X z H x i x H z i I X Z I x I y I x G y I z X z H x I x H z I
25 6 24 bitrdi R RingOps I Idl R I X Z I x I y I x G y I z X z H x I x H z I