rsp1

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

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

Metamath Proof Explorer