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

Metamath Proof Explorer

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