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 → 𝑃 = ∪ 𝑔 ∈ 𝐵 { ( 𝐾 ‘ { 𝑔 } ) } )