Theorem ress0g

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

	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		eqid	|- ( +g ` R ) = ( +g ` R )
5	2 4	mndid	|- ( R e. Mnd -> E. u e. B A. x e. B ( ( u ( +g ` R ) x ) = x /\ ( x ( +g ` R ) u ) = x ) )
6	5	3ad2ant1	|- ( ( R e. Mnd /\ .0. e. A /\ A C_ B ) -> E. u e. B A. x e. B ( ( u ( +g ` R ) x ) = x /\ ( x ( +g ` R ) u ) = x ) )
7		simp3	|- ( ( R e. Mnd /\ .0. e. A /\ A C_ B ) -> A C_ B )
8		simp2	|- ( ( R e. Mnd /\ .0. e. A /\ A C_ B ) -> .0. e. A )
9	2 4 3 6 1 7 8	idressid	|- ( ( R e. Mnd /\ .0. e. A /\ A C_ B ) -> ( 0g ` S ) = .0. )
10	9	eqcomd	|- ( ( R e. Mnd /\ .0. e. A /\ A C_ B ) -> .0. = ( 0g ` S ) )