Theorem lpival

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

	Ref	Expression
Hypotheses	lpival.p	$$⊢P=\mathrm{LPIdeal}\left(R\right)$$
	lpival.k	$$⊢K=\mathrm{RSpan}\left(R\right)$$
	lpival.b	$$⊢B={\mathrm{Base}}_R$$
Assertion	lpival	$$⊢R\in \mathrm{Ring}\to P=\bigcup _{g\in B}\left\{K\left(\left\{g\right\}\right)\right\}$$

Proof

Step	Hyp	Ref	Expression
1		lpival.p	$$⊢P=\mathrm{LPIdeal}\left(R\right)$$
2		lpival.k	$$⊢K=\mathrm{RSpan}\left(R\right)$$
3		lpival.b	$$⊢B={\mathrm{Base}}_R$$
4		fveq2	$$⊢r=R\to {\mathrm{Base}}_r={\mathrm{Base}}_R$$
5		fveq2	$$⊢r=R\to \mathrm{RSpan}\left(r\right)=\mathrm{RSpan}\left(R\right)$$
6	5	fveq1d	$$⊢r=R\to \mathrm{RSpan}\left(r\right)\left(\left\{g\right\}\right)=\mathrm{RSpan}\left(R\right)\left(\left\{g\right\}\right)$$
7	6	sneqd	$$⊢r=R\to \left\{\mathrm{RSpan}\left(r\right)\left(\left\{g\right\}\right)\right\}=\left\{\mathrm{RSpan}\left(R\right)\left(\left\{g\right\}\right)\right\}$$
8	4 7	iuneq12d	$$⊢r=R\to \bigcup _{g\in {\mathrm{Base}}_r}\left\{\mathrm{RSpan}\left(r\right)\left(\left\{g\right\}\right)\right\}=\bigcup _{g\in {\mathrm{Base}}_R}\left\{\mathrm{RSpan}\left(R\right)\left(\left\{g\right\}\right)\right\}$$
9		df-lpidl	$$⊢\mathrm{LPIdeal}=\left(r\in \mathrm{Ring}⟼\bigcup _{g\in {\mathrm{Base}}_r}\left\{\mathrm{RSpan}\left(r\right)\left(\left\{g\right\}\right)\right\}\right)$$
10		fvex	$$⊢\mathrm{RSpan}\left(R\right)\in \mathrm{V}$$
11	10	rnex	$$⊢\mathrm{ran}\mathrm{RSpan}\left(R\right)\in \mathrm{V}$$
12		p0ex	$$⊢\left\{\varnothing \right\}\in \mathrm{V}$$
13	11 12	unex	$$⊢\mathrm{ran}\mathrm{RSpan}\left(R\right)\cup \left\{\varnothing \right\}\in \mathrm{V}$$
14		iunss	$$⊢\bigcup _{g\in {\mathrm{Base}}_R}\left\{\mathrm{RSpan}\left(R\right)\left(\left\{g\right\}\right)\right\}\subseteq \mathrm{ran}\mathrm{RSpan}\left(R\right)\cup \left\{\varnothing \right\}\leftrightarrow \forall g\in {\mathrm{Base}}_R\left\{\mathrm{RSpan}\left(R\right)\left(\left\{g\right\}\right)\right\}\subseteq \mathrm{ran}\mathrm{RSpan}\left(R\right)\cup \left\{\varnothing \right\}$$
15		fvrn0	$$⊢\mathrm{RSpan}\left(R\right)\left(\left\{g\right\}\right)\in \left(\mathrm{ran}\mathrm{RSpan}\left(R\right)\cup \left\{\varnothing \right\}\right)$$
16		snssi	$$⊢\mathrm{RSpan}\left(R\right)\left(\left\{g\right\}\right)\in \left(\mathrm{ran}\mathrm{RSpan}\left(R\right)\cup \left\{\varnothing \right\}\right)\to \left\{\mathrm{RSpan}\left(R\right)\left(\left\{g\right\}\right)\right\}\subseteq \mathrm{ran}\mathrm{RSpan}\left(R\right)\cup \left\{\varnothing \right\}$$
17	15 16	ax-mp	$$⊢\left\{\mathrm{RSpan}\left(R\right)\left(\left\{g\right\}\right)\right\}\subseteq \mathrm{ran}\mathrm{RSpan}\left(R\right)\cup \left\{\varnothing \right\}$$
18	17	a1i	$$⊢g\in {\mathrm{Base}}_R\to \left\{\mathrm{RSpan}\left(R\right)\left(\left\{g\right\}\right)\right\}\subseteq \mathrm{ran}\mathrm{RSpan}\left(R\right)\cup \left\{\varnothing \right\}$$
19	14 18	mprgbir	$$⊢\bigcup _{g\in {\mathrm{Base}}_R}\left\{\mathrm{RSpan}\left(R\right)\left(\left\{g\right\}\right)\right\}\subseteq \mathrm{ran}\mathrm{RSpan}\left(R\right)\cup \left\{\varnothing \right\}$$
20	13 19	ssexi	$$⊢\bigcup _{g\in {\mathrm{Base}}_R}\left\{\mathrm{RSpan}\left(R\right)\left(\left\{g\right\}\right)\right\}\in \mathrm{V}$$
21	8 9 20	fvmpt	$$⊢R\in \mathrm{Ring}\to \mathrm{LPIdeal}\left(R\right)=\bigcup _{g\in {\mathrm{Base}}_R}\left\{\mathrm{RSpan}\left(R\right)\left(\left\{g\right\}\right)\right\}$$
22		iuneq1	$$⊢B={\mathrm{Base}}_R\to \bigcup _{g\in B}\left\{K\left(\left\{g\right\}\right)\right\}=\bigcup _{g\in {\mathrm{Base}}_R}\left\{K\left(\left\{g\right\}\right)\right\}$$
23	3 22	ax-mp	$$⊢\bigcup _{g\in B}\left\{K\left(\left\{g\right\}\right)\right\}=\bigcup _{g\in {\mathrm{Base}}_R}\left\{K\left(\left\{g\right\}\right)\right\}$$
24	2	fveq1i	$$⊢K\left(\left\{g\right\}\right)=\mathrm{RSpan}\left(R\right)\left(\left\{g\right\}\right)$$
25	24	sneqi	$$⊢\left\{K\left(\left\{g\right\}\right)\right\}=\left\{\mathrm{RSpan}\left(R\right)\left(\left\{g\right\}\right)\right\}$$
26	25	a1i	$$⊢g\in {\mathrm{Base}}_R\to \left\{K\left(\left\{g\right\}\right)\right\}=\left\{\mathrm{RSpan}\left(R\right)\left(\left\{g\right\}\right)\right\}$$
27	26	iuneq2i	$$⊢\bigcup _{g\in {\mathrm{Base}}_R}\left\{K\left(\left\{g\right\}\right)\right\}=\bigcup _{g\in {\mathrm{Base}}_R}\left\{\mathrm{RSpan}\left(R\right)\left(\left\{g\right\}\right)\right\}$$
28	23 27	eqtri	$$⊢\bigcup _{g\in B}\left\{K\left(\left\{g\right\}\right)\right\}=\bigcup _{g\in {\mathrm{Base}}_R}\left\{\mathrm{RSpan}\left(R\right)\left(\left\{g\right\}\right)\right\}$$
29	21 1 28	3eqtr4g	$$⊢R\in \mathrm{Ring}\to P=\bigcup _{g\in B}\left\{K\left(\left\{g\right\}\right)\right\}$$