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 = ( RSpan ` R )
	rspcl.b	|- B = ( Base ` R )
	rsp1.o	|- .1. = ( 1r ` R )
Assertion	rsp1	|- ( R e. Ring -> ( K ` { .1. } ) = B )

Proof

Step	Hyp	Ref	Expression
1		rspcl.k	|- K = ( RSpan ` R )
2		rspcl.b	|- B = ( Base ` R )
3		rsp1.o	|- .1. = ( 1r ` R )
4	2 3	ringidcl	|- ( R e. Ring -> .1. e. B )
5	4	snssd	|- ( R e. Ring -> { .1. } C_ B )
6	1 2	rspssid	|- ( ( R e. Ring /\ { .1. } C_ B ) -> { .1. } C_ ( K ` { .1. } ) )
7	5 6	mpdan	|- ( R e. Ring -> { .1. } C_ ( K ` { .1. } ) )
8	3	fvexi	|- .1. e. _V
9	8	snss	|- ( .1. e. ( K ` { .1. } ) <-> { .1. } C_ ( K ` { .1. } ) )
10	7 9	sylibr	|- ( R e. Ring -> .1. e. ( K ` { .1. } ) )
11		eqid	|- ( LIdeal ` R ) = ( LIdeal ` R )
12	1 2 11	rspcl	|- ( ( R e. Ring /\ { .1. } C_ B ) -> ( K ` { .1. } ) e. ( LIdeal ` R ) )
13	5 12	mpdan	|- ( R e. Ring -> ( K ` { .1. } ) e. ( LIdeal ` R ) )
14	11 2 3	lidl1el	|- ( ( R e. Ring /\ ( K ` { .1. } ) e. ( LIdeal ` R ) ) -> ( .1. e. ( K ` { .1. } ) <-> ( K ` { .1. } ) = B ) )
15	13 14	mpdan	|- ( R e. Ring -> ( .1. e. ( K ` { .1. } ) <-> ( K ` { .1. } ) = B ) )
16	10 15	mpbid	|- ( R e. Ring -> ( K ` { .1. } ) = B )