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