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 e. Ring -> P = U_ g e. 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 -> U_ g e. ( Base ` r ) { ( ( RSpan ` r ) ` { g } ) } = U_ g e. ( Base ` R ) { ( ( RSpan ` R ) ` { g } ) } )
9 df-lpidl 
 |-  LPIdeal = ( r e. Ring |-> U_ g e. ( Base ` r ) { ( ( RSpan ` r ) ` { g } ) } )
10 fvex 
 |-  ( RSpan ` R ) e. _V
11 10 rnex 
 |-  ran ( RSpan ` R ) e. _V
12 p0ex 
 |-  { (/) } e. _V
13 11 12 unex 
 |-  ( ran ( RSpan ` R ) u. { (/) } ) e. _V
14 iunss 
 |-  ( U_ g e. ( Base ` R ) { ( ( RSpan ` R ) ` { g } ) } C_ ( ran ( RSpan ` R ) u. { (/) } ) <-> A. g e. ( Base ` R ) { ( ( RSpan ` R ) ` { g } ) } C_ ( ran ( RSpan ` R ) u. { (/) } ) )
15 fvrn0 
 |-  ( ( RSpan ` R ) ` { g } ) e. ( ran ( RSpan ` R ) u. { (/) } )
16 snssi 
 |-  ( ( ( RSpan ` R ) ` { g } ) e. ( ran ( RSpan ` R ) u. { (/) } ) -> { ( ( RSpan ` R ) ` { g } ) } C_ ( ran ( RSpan ` R ) u. { (/) } ) )
17 15 16 ax-mp 
 |-  { ( ( RSpan ` R ) ` { g } ) } C_ ( ran ( RSpan ` R ) u. { (/) } )
18 17 a1i 
 |-  ( g e. ( Base ` R ) -> { ( ( RSpan ` R ) ` { g } ) } C_ ( ran ( RSpan ` R ) u. { (/) } ) )
19 14 18 mprgbir 
 |-  U_ g e. ( Base ` R ) { ( ( RSpan ` R ) ` { g } ) } C_ ( ran ( RSpan ` R ) u. { (/) } )
20 13 19 ssexi 
 |-  U_ g e. ( Base ` R ) { ( ( RSpan ` R ) ` { g } ) } e. _V
21 8 9 20 fvmpt 
 |-  ( R e. Ring -> ( LPIdeal ` R ) = U_ g e. ( Base ` R ) { ( ( RSpan ` R ) ` { g } ) } )
22 iuneq1 
 |-  ( B = ( Base ` R ) -> U_ g e. B { ( K ` { g } ) } = U_ g e. ( Base ` R ) { ( K ` { g } ) } )
23 3 22 ax-mp 
 |-  U_ g e. B { ( K ` { g } ) } = U_ g e. ( Base ` R ) { ( K ` { g } ) }
24 2 fveq1i 
 |-  ( K ` { g } ) = ( ( RSpan ` R ) ` { g } )
25 24 sneqi 
 |-  { ( K ` { g } ) } = { ( ( RSpan ` R ) ` { g } ) }
26 25 a1i 
 |-  ( g e. ( Base ` R ) -> { ( K ` { g } ) } = { ( ( RSpan ` R ) ` { g } ) } )
27 26 iuneq2i 
 |-  U_ g e. ( Base ` R ) { ( K ` { g } ) } = U_ g e. ( Base ` R ) { ( ( RSpan ` R ) ` { g } ) }
28 23 27 eqtri 
 |-  U_ g e. B { ( K ` { g } ) } = U_ g e. ( Base ` R ) { ( ( RSpan ` R ) ` { g } ) }
29 21 1 28 3eqtr4g 
 |-  ( R e. Ring -> P = U_ g e. B { ( K ` { g } ) } )