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 ) ) |