Metamath Proof Explorer


Theorem pridlval

Description: The class of prime ideals of a ring R . (Contributed by Jeff Madsen, 10-Jun-2010)

Ref Expression
Hypotheses pridlval.1 G = 1 st R
pridlval.2 H = 2 nd R
pridlval.3 X = ran G
Assertion pridlval R RingOps PrIdl R = i Idl R | i X a Idl R b Idl R x a y b x H y i a i b i

Proof

Step Hyp Ref Expression
1 pridlval.1 G = 1 st R
2 pridlval.2 H = 2 nd R
3 pridlval.3 X = ran G
4 fveq2 r = R Idl r = Idl R
5 fveq2 r = R 1 st r = 1 st R
6 5 1 eqtr4di r = R 1 st r = G
7 6 rneqd r = R ran 1 st r = ran G
8 7 3 eqtr4di r = R ran 1 st r = X
9 8 neeq2d r = R i ran 1 st r i X
10 fveq2 r = R 2 nd r = 2 nd R
11 10 2 eqtr4di r = R 2 nd r = H
12 11 oveqd r = R x 2 nd r y = x H y
13 12 eleq1d r = R x 2 nd r y i x H y i
14 13 2ralbidv r = R x a y b x 2 nd r y i x a y b x H y i
15 14 imbi1d r = R x a y b x 2 nd r y i a i b i x a y b x H y i a i b i
16 4 15 raleqbidv r = R b Idl r x a y b x 2 nd r y i a i b i b Idl R x a y b x H y i a i b i
17 4 16 raleqbidv r = R a Idl r b Idl r x a y b x 2 nd r y i a i b i a Idl R b Idl R x a y b x H y i a i b i
18 9 17 anbi12d r = R i ran 1 st r a Idl r b Idl r x a y b x 2 nd r y i a i b i i X a Idl R b Idl R x a y b x H y i a i b i
19 4 18 rabeqbidv r = R i Idl r | i ran 1 st r a Idl r b Idl r x a y b x 2 nd r y i a i b i = i Idl R | i X a Idl R b Idl R x a y b x H y i a i b i
20 df-pridl PrIdl = r RingOps i Idl r | i ran 1 st r a Idl r b Idl r x a y b x 2 nd r y i a i b i
21 fvex Idl R V
22 21 rabex i Idl R | i X a Idl R b Idl R x a y b x H y i a i b i V
23 19 20 22 fvmpt R RingOps PrIdl R = i Idl R | i X a Idl R b Idl R x a y b x H y i a i b i