This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )