Theorem lpi0

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

	Ref	Expression
Hypotheses	lpival.p	$$⊢P=\mathrm{LPIdeal}\left(R\right)$$
	lpi0.z	$$⊢\underset{\dot{}}{0}=0_R$$
Assertion	lpi0	$$⊢R\in \mathrm{Ring}\to \left\{\underset{\dot{}}{0}\right\}\in P$$

Proof

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