Theorem lpi1

Description: The unit ideal is always principal. (Contributed by Stefan O'Rear, 3-Jan-2015)

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

Proof

Step	Hyp	Ref	Expression
1		lpival.p	$$⊢P=\mathrm{LPIdeal}\left(R\right)$$
2		lpi1.b	$$⊢B={\mathrm{Base}}_R$$
3		eqid	$$⊢1_R=1_R$$
4	2 3	ringidcl	$$⊢R\in \mathrm{Ring}\to 1_R\in B$$
5		eqid	$$⊢\mathrm{RSpan}\left(R\right)=\mathrm{RSpan}\left(R\right)$$
6	5 2 3	rsp1	$$⊢R\in \mathrm{Ring}\to \mathrm{RSpan}\left(R\right)\left(\left\{1_R\right\}\right)=B$$
7	6	eqcomd	$$⊢R\in \mathrm{Ring}\to B=\mathrm{RSpan}\left(R\right)\left(\left\{1_R\right\}\right)$$
8		sneq	$$⊢g=1_R\to \left\{g\right\}=\left\{1_R\right\}$$
9	8	fveq2d	$$⊢g=1_R\to \mathrm{RSpan}\left(R\right)\left(\left\{g\right\}\right)=\mathrm{RSpan}\left(R\right)\left(\left\{1_R\right\}\right)$$
10	9	rspceeqv	$$⊢\left(1_R\in B\wedge B=\mathrm{RSpan}\left(R\right)\left(\left\{1_R\right\}\right)\right)\to \exists g\in BB=\mathrm{RSpan}\left(R\right)\left(\left\{g\right\}\right)$$
11	4 7 10	syl2anc	$$⊢R\in \mathrm{Ring}\to \exists g\in BB=\mathrm{RSpan}\left(R\right)\left(\left\{g\right\}\right)$$
12	1 5 2	islpidl	$$⊢R\in \mathrm{Ring}\to \left(B\in P\leftrightarrow \exists g\in BB=\mathrm{RSpan}\left(R\right)\left(\left\{g\right\}\right)\right)$$
13	11 12	mpbird	$$⊢R\in \mathrm{Ring}\to B\in P$$