Theorem ress0g

Description: 0g is unaffected by restriction. This is a bit more generic than submnd0 . (Contributed by Thierry Arnoux, 23-Oct-2017)

	Ref	Expression
Hypotheses	ress0g.s	|- S = ( R |`s A )
	ress0g.b	|- B = ( Base ` R )
	ress0g.0	|- .0. = ( 0g ` R )
Assertion	ress0g	|- ( ( R e. Mnd /\ .0. e. A /\ A C_ B ) -> .0. = ( 0g ` S ) )

Proof

Step	Hyp	Ref	Expression
1		ress0g.s	|- S = ( R |`s A )
2		ress0g.b	|- B = ( Base ` R )
3		ress0g.0	|- .0. = ( 0g ` R )
4	1 2	ressbas2	|- ( A C_ B -> A = ( Base ` S ) )
5	4	3ad2ant3	|- ( ( R e. Mnd /\ .0. e. A /\ A C_ B ) -> A = ( Base ` S ) )
6		simp3	|- ( ( R e. Mnd /\ .0. 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. Mnd /\ .0. e. A /\ A C_ B ) -> A e. _V )
10		eqid	|- ( +g ` R ) = ( +g ` R )
11	1 10	ressplusg	|- ( A e. _V -> ( +g ` R ) = ( +g ` S ) )
12	9 11	syl	|- ( ( R e. Mnd /\ .0. e. A /\ A C_ B ) -> ( +g ` R ) = ( +g ` S ) )
13		simp2	|- ( ( R e. Mnd /\ .0. e. A /\ A C_ B ) -> .0. e. A )
14		simpl1	|- ( ( ( R e. Mnd /\ .0. e. A /\ A C_ B ) /\ x e. A ) -> R e. Mnd )
15	6	sselda	|- ( ( ( R e. Mnd /\ .0. e. A /\ A C_ B ) /\ x e. A ) -> x e. B )
16	2 10 3	mndlid	|- ( ( R e. Mnd /\ x e. B ) -> ( .0. ( +g ` R ) x ) = x )
17	14 15 16	syl2anc	|- ( ( ( R e. Mnd /\ .0. e. A /\ A C_ B ) /\ x e. A ) -> ( .0. ( +g ` R ) x ) = x )
18	2 10 3	mndrid	|- ( ( R e. Mnd /\ x e. B ) -> ( x ( +g ` R ) .0. ) = x )
19	14 15 18	syl2anc	|- ( ( ( R e. Mnd /\ .0. e. A /\ A C_ B ) /\ x e. A ) -> ( x ( +g ` R ) .0. ) = x )
20	5 12 13 17 19	grpidd	|- ( ( R e. Mnd /\ .0. e. A /\ A C_ B ) -> .0. = ( 0g ` S ) )