Metamath Proof Explorer


Theorem lpival

Description: Value of the set of principal ideals. (Contributed by Stefan O'Rear, 3-Jan-2015)

Ref Expression
Hypotheses lpival.p P = LPIdeal R
lpival.k K = RSpan R
lpival.b B = Base R
Assertion lpival R Ring P = g B K g

Proof

Step Hyp Ref Expression
1 lpival.p P = LPIdeal R
2 lpival.k K = RSpan R
3 lpival.b B = Base R
4 fveq2 r = R Base r = Base R
5 fveq2 r = R RSpan r = RSpan R
6 5 fveq1d r = R RSpan r g = RSpan R g
7 6 sneqd r = R RSpan r g = RSpan R g
8 4 7 iuneq12d r = R g Base r RSpan r g = g Base R RSpan R g
9 df-lpidl LPIdeal = r Ring g Base r RSpan r g
10 fvex RSpan R V
11 10 rnex ran RSpan R V
12 p0ex V
13 11 12 unex ran RSpan R V
14 iunss g Base R RSpan R g ran RSpan R g Base R RSpan R g ran RSpan R
15 fvrn0 RSpan R g ran RSpan R
16 snssi RSpan R g ran RSpan R RSpan R g ran RSpan R
17 15 16 ax-mp RSpan R g ran RSpan R
18 17 a1i g Base R RSpan R g ran RSpan R
19 14 18 mprgbir g Base R RSpan R g ran RSpan R
20 13 19 ssexi g Base R RSpan R g V
21 8 9 20 fvmpt R Ring LPIdeal R = g Base R RSpan R g
22 iuneq1 B = Base R g B K g = g Base R K g
23 3 22 ax-mp g B K g = g Base R K g
24 2 fveq1i K g = RSpan R g
25 24 sneqi K g = RSpan R g
26 25 a1i g Base R K g = RSpan R g
27 26 iuneq2i g Base R K g = g Base R RSpan R g
28 23 27 eqtri g B K g = g Base R RSpan R g
29 21 1 28 3eqtr4g R Ring P = g B K g