Theorem rsp1

Description: The span of the identity element is the unit ideal. (Contributed by Stefan O'Rear, 3-Jan-2015)

	Ref	Expression
Hypotheses	rspcl.k	$$⊢K=\mathrm{RSpan}\left(R\right)$$
	rspcl.b	$$⊢B={\mathrm{Base}}_R$$
	rsp1.o	$$⊢\underset{\dot{}}{1}=1_R$$
Assertion	rsp1	$$⊢R\in \mathrm{Ring}\to K\left(\left\{\underset{\dot{}}{1}\right\}\right)=B$$

Proof

Step	Hyp	Ref	Expression
1		rspcl.k	$$⊢K=\mathrm{RSpan}\left(R\right)$$
2		rspcl.b	$$⊢B={\mathrm{Base}}_R$$
3		rsp1.o	$$⊢\underset{\dot{}}{1}=1_R$$
4	2 3	ringidcl	$$⊢R\in \mathrm{Ring}\to \underset{\dot{}}{1}\in B$$
5	4	snssd	$$⊢R\in \mathrm{Ring}\to \left\{\underset{\dot{}}{1}\right\}\subseteq B$$
6	1 2	rspssid	$$⊢\left(R\in \mathrm{Ring}\wedge \left\{\underset{\dot{}}{1}\right\}\subseteq B\right)\to \left\{\underset{\dot{}}{1}\right\}\subseteq K\left(\left\{\underset{\dot{}}{1}\right\}\right)$$
7	5 6	mpdan	$$⊢R\in \mathrm{Ring}\to \left\{\underset{\dot{}}{1}\right\}\subseteq K\left(\left\{\underset{\dot{}}{1}\right\}\right)$$
8	3	fvexi	$$⊢\underset{\dot{}}{1}\in \mathrm{V}$$
9	8	snss	$$⊢\underset{\dot{}}{1}\in K\left(\left\{\underset{\dot{}}{1}\right\}\right)\leftrightarrow \left\{\underset{\dot{}}{1}\right\}\subseteq K\left(\left\{\underset{\dot{}}{1}\right\}\right)$$
10	7 9	sylibr	$$⊢R\in \mathrm{Ring}\to \underset{\dot{}}{1}\in K\left(\left\{\underset{\dot{}}{1}\right\}\right)$$
11		eqid	$$⊢\mathrm{LIdeal}\left(R\right)=\mathrm{LIdeal}\left(R\right)$$
12	1 2 11	rspcl	$$⊢\left(R\in \mathrm{Ring}\wedge \left\{\underset{\dot{}}{1}\right\}\subseteq B\right)\to K\left(\left\{\underset{\dot{}}{1}\right\}\right)\in \mathrm{LIdeal}\left(R\right)$$
13	5 12	mpdan	$$⊢R\in \mathrm{Ring}\to K\left(\left\{\underset{\dot{}}{1}\right\}\right)\in \mathrm{LIdeal}\left(R\right)$$
14	11 2 3	lidl1el	$$⊢\left(R\in \mathrm{Ring}\wedge K\left(\left\{\underset{\dot{}}{1}\right\}\right)\in \mathrm{LIdeal}\left(R\right)\right)\to \left(\underset{\dot{}}{1}\in K\left(\left\{\underset{\dot{}}{1}\right\}\right)\leftrightarrow K\left(\left\{\underset{\dot{}}{1}\right\}\right)=B\right)$$
15	13 14	mpdan	$$⊢R\in \mathrm{Ring}\to \left(\underset{\dot{}}{1}\in K\left(\left\{\underset{\dot{}}{1}\right\}\right)\leftrightarrow K\left(\left\{\underset{\dot{}}{1}\right\}\right)=B\right)$$
16	10 15	mpbid	$$⊢R\in \mathrm{Ring}\to K\left(\left\{\underset{\dot{}}{1}\right\}\right)=B$$