This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑃 = ( LPIdeal ‘ 𝑅 )
lpival.k ⊢ 𝐾 = ( RSpan ‘ 𝑅 )
lpival.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
Assertion lpival ( 𝑅 ∈ Ring → 𝑃 = ∪ 𝑔 ∈ 𝐵 { ( 𝐾 ‘ { 𝑔 } ) } )

Proof

Step Hyp Ref Expression
1 lpival.p ⊢ 𝑃 = ( LPIdeal ‘ 𝑅 )
2 lpival.k ⊢ 𝐾 = ( RSpan ‘ 𝑅 )
3 lpival.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
4 fveq2 ⊢ ( 𝑟 = 𝑅 → ( Base ‘ 𝑟 ) = ( Base ‘ 𝑅 ) )
5 fveq2 ⊢ ( 𝑟 = 𝑅 → ( RSpan ‘ 𝑟 ) = ( RSpan ‘ 𝑅 ) )
6 5 fveq1d ⊢ ( 𝑟 = 𝑅 → ( ( RSpan ‘ 𝑟 ) ‘ { 𝑔 } ) = ( ( RSpan ‘ 𝑅 ) ‘ { 𝑔 } ) )
7 6 sneqd ⊢ ( 𝑟 = 𝑅 → { ( ( RSpan ‘ 𝑟 ) ‘ { 𝑔 } ) } = { ( ( RSpan ‘ 𝑅 ) ‘ { 𝑔 } ) } )
8 4 7 iuneq12d ⊢ ( 𝑟 = 𝑅 → ∪ 𝑔 ∈ ( Base ‘ 𝑟 ) { ( ( RSpan ‘ 𝑟 ) ‘ { 𝑔 } ) } = ∪ 𝑔 ∈ ( Base ‘ 𝑅 ) { ( ( RSpan ‘ 𝑅 ) ‘ { 𝑔 } ) } )
9 df-lpidl ⊢ LPIdeal = ( 𝑟 ∈ Ring ↦ ∪ 𝑔 ∈ ( Base ‘ 𝑟 ) { ( ( RSpan ‘ 𝑟 ) ‘ { 𝑔 } ) } )
10 fvex ⊢ ( RSpan ‘ 𝑅 ) ∈ V
11 10 rnex ⊢ ran ( RSpan ‘ 𝑅 ) ∈ V
12 p0ex ⊢ { ∅ } ∈ V
13 11 12 unex ⊢ ( ran ( RSpan ‘ 𝑅 ) ∪ { ∅ } ) ∈ V
14 iunss ⊢ ( ∪ 𝑔 ∈ ( Base ‘ 𝑅 ) { ( ( RSpan ‘ 𝑅 ) ‘ { 𝑔 } ) } ⊆ ( ran ( RSpan ‘ 𝑅 ) ∪ { ∅ } ) ↔ ∀ 𝑔 ∈ ( Base ‘ 𝑅 ) { ( ( RSpan ‘ 𝑅 ) ‘ { 𝑔 } ) } ⊆ ( ran ( RSpan ‘ 𝑅 ) ∪ { ∅ } ) )
15 fvrn0 ⊢ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑔 } ) ∈ ( ran ( RSpan ‘ 𝑅 ) ∪ { ∅ } )
16 snssi ⊢ ( ( ( RSpan ‘ 𝑅 ) ‘ { 𝑔 } ) ∈ ( ran ( RSpan ‘ 𝑅 ) ∪ { ∅ } ) → { ( ( RSpan ‘ 𝑅 ) ‘ { 𝑔 } ) } ⊆ ( ran ( RSpan ‘ 𝑅 ) ∪ { ∅ } ) )
17 15 16 ax-mp ⊢ { ( ( RSpan ‘ 𝑅 ) ‘ { 𝑔 } ) } ⊆ ( ran ( RSpan ‘ 𝑅 ) ∪ { ∅ } )
18 17 a1i ⊢ ( 𝑔 ∈ ( Base ‘ 𝑅 ) → { ( ( RSpan ‘ 𝑅 ) ‘ { 𝑔 } ) } ⊆ ( ran ( RSpan ‘ 𝑅 ) ∪ { ∅ } ) )
19 14 18 mprgbir ⊢ ∪ 𝑔 ∈ ( Base ‘ 𝑅 ) { ( ( RSpan ‘ 𝑅 ) ‘ { 𝑔 } ) } ⊆ ( ran ( RSpan ‘ 𝑅 ) ∪ { ∅ } )
20 13 19 ssexi ⊢ ∪ 𝑔 ∈ ( Base ‘ 𝑅 ) { ( ( RSpan ‘ 𝑅 ) ‘ { 𝑔 } ) } ∈ V
21 8 9 20 fvmpt ⊢ ( 𝑅 ∈ Ring → ( LPIdeal ‘ 𝑅 ) = ∪ 𝑔 ∈ ( Base ‘ 𝑅 ) { ( ( RSpan ‘ 𝑅 ) ‘ { 𝑔 } ) } )
22 iuneq1 ⊢ ( 𝐵 = ( Base ‘ 𝑅 ) → ∪ 𝑔 ∈ 𝐵 { ( 𝐾 ‘ { 𝑔 } ) } = ∪ 𝑔 ∈ ( Base ‘ 𝑅 ) { ( 𝐾 ‘ { 𝑔 } ) } )
23 3 22 ax-mp ⊢ ∪ 𝑔 ∈ 𝐵 { ( 𝐾 ‘ { 𝑔 } ) } = ∪ 𝑔 ∈ ( Base ‘ 𝑅 ) { ( 𝐾 ‘ { 𝑔 } ) }
24 2 fveq1i ⊢ ( 𝐾 ‘ { 𝑔 } ) = ( ( RSpan ‘ 𝑅 ) ‘ { 𝑔 } )
25 24 sneqi ⊢ { ( 𝐾 ‘ { 𝑔 } ) } = { ( ( RSpan ‘ 𝑅 ) ‘ { 𝑔 } ) }
26 25 a1i ⊢ ( 𝑔 ∈ ( Base ‘ 𝑅 ) → { ( 𝐾 ‘ { 𝑔 } ) } = { ( ( RSpan ‘ 𝑅 ) ‘ { 𝑔 } ) } )
27 26 iuneq2i ⊢ ∪ 𝑔 ∈ ( Base ‘ 𝑅 ) { ( 𝐾 ‘ { 𝑔 } ) } = ∪ 𝑔 ∈ ( Base ‘ 𝑅 ) { ( ( RSpan ‘ 𝑅 ) ‘ { 𝑔 } ) }
28 23 27 eqtri ⊢ ∪ 𝑔 ∈ 𝐵 { ( 𝐾 ‘ { 𝑔 } ) } = ∪ 𝑔 ∈ ( Base ‘ 𝑅 ) { ( ( RSpan ‘ 𝑅 ) ‘ { 𝑔 } ) }
29 21 1 28 3eqtr4g ⊢ ( 𝑅 ∈ Ring → 𝑃 = ∪ 𝑔 ∈ 𝐵 { ( 𝐾 ‘ { 𝑔 } ) } )