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 rngurd
 |-  ( ( R e. Ring /\ .1. e. A /\ A C_ B ) -> .1. = ( 1r ` S ) )