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

Metamath Proof Explorer

Theorem ress1r

Description: 1r is unaffected by restriction. This is a bit more generic than subrg1 . (Contributed by Thierry Arnoux, 6-Sep-2018)

Ref Expression
Hypotheses ress1r.s 
|- S = ( R |`s A )
ress1r.b 
|- B = ( Base ` R )
ress1r.1 
|- .1. = ( 1r ` R )
Assertion ress1r 
|- ( ( R e. Ring /\ .1. e. A /\ A C_ B ) -> .1. = ( 1r ` S ) )

Proof

Step Hyp Ref Expression
1 ress1r.s 
 |-  S = ( R |`s A )
2 ress1r.b 
 |-  B = ( Base ` R )
3 ress1r.1 
 |-  .1. = ( 1r ` R )
4 1 2 ressbas2 
 |-  ( A C_ B -> A = ( Base ` S ) )
5 4 3ad2ant3 
 |-  ( ( R e. Ring /\ .1. e. A /\ A C_ B ) -> A = ( Base ` S ) )
6 simp3 
 |-  ( ( R e. Ring /\ .1. e. A /\ A C_ B ) -> A C_ B )
7 2 fvexi 
 |-  B e. _V
8 ssexg 
 |-  ( ( A C_ B /\ B e. _V ) -> A e. _V )
9 6 7 8 sylancl 
 |-  ( ( R e. Ring /\ .1. e. A /\ A C_ B ) -> A e. _V )
10 eqid 
 |-  ( .r ` R ) = ( .r ` R )
11 1 10 ressmulr 
 |-  ( A e. _V -> ( .r ` R ) = ( .r ` S ) )
12 9 11 syl 
 |-  ( ( R e. Ring /\ .1. e. A /\ A C_ B ) -> ( .r ` R ) = ( .r ` S ) )
13 simp2 
 |-  ( ( R e. Ring /\ .1. e. A /\ A C_ B ) -> .1. e. A )
14 simpl1 
 |-  ( ( ( R e. Ring /\ .1. e. A /\ A C_ B ) /\ x e. A ) -> R e. Ring )
15 6 sselda 
 |-  ( ( ( R e. Ring /\ .1. e. A /\ A C_ B ) /\ x e. A ) -> x e. B )
16 2 10 3 ringlidm 
 |-  ( ( R e. Ring /\ x e. B ) -> ( .1. ( .r ` R ) x ) = x )
17 14 15 16 syl2anc 
 |-  ( ( ( R e. Ring /\ .1. e. A /\ A C_ B ) /\ x e. A ) -> ( .1. ( .r ` R ) x ) = x )
18 2 10 3 ringridm 
 |-  ( ( R e. Ring /\ x e. B ) -> ( x ( .r ` R ) .1. ) = x )
19 14 15 18 syl2anc 
 |-  ( ( ( R e. Ring /\ .1. e. A /\ A C_ B ) /\ x e. A ) -> ( x ( .r ` R ) .1. ) = x )
20 5 12 13 17 19 ringurd 
 |-  ( ( R e. Ring /\ .1. e. A /\ A C_ B ) -> .1. = ( 1r ` S ) )