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 𝐴 )
	ress0g.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	ress0g.0	⊢ 0 = ( 0g ‘ 𝑅 )
Assertion	ress0g	⊢ ( ( 𝑅 ∈ Mnd ∧ 0 ∈ 𝐴 ∧ 𝐴 ⊆ 𝐵 ) → 0 = ( 0g ‘ 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		ress0g.s	⊢ 𝑆 = ( 𝑅 ↾s 𝐴 )
2		ress0g.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
3		ress0g.0	⊢ 0 = ( 0g ‘ 𝑅 )
4		eqid	⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
5	2 4	mndid	⊢ ( 𝑅 ∈ Mnd → ∃ 𝑢 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑢 ( +g ‘ 𝑅 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g ‘ 𝑅 ) 𝑢 ) = 𝑥 ) )
6	5	3ad2ant1	⊢ ( ( 𝑅 ∈ Mnd ∧ 0 ∈ 𝐴 ∧ 𝐴 ⊆ 𝐵 ) → ∃ 𝑢 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑢 ( +g ‘ 𝑅 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g ‘ 𝑅 ) 𝑢 ) = 𝑥 ) )
7		simp3	⊢ ( ( 𝑅 ∈ Mnd ∧ 0 ∈ 𝐴 ∧ 𝐴 ⊆ 𝐵 ) → 𝐴 ⊆ 𝐵 )
8		simp2	⊢ ( ( 𝑅 ∈ Mnd ∧ 0 ∈ 𝐴 ∧ 𝐴 ⊆ 𝐵 ) → 0 ∈ 𝐴 )
9	2 4 3 6 1 7 8	idressid	⊢ ( ( 𝑅 ∈ Mnd ∧ 0 ∈ 𝐴 ∧ 𝐴 ⊆ 𝐵 ) → ( 0g ‘ 𝑆 ) = 0 )
10	9	eqcomd	⊢ ( ( 𝑅 ∈ Mnd ∧ 0 ∈ 𝐴 ∧ 𝐴 ⊆ 𝐵 ) → 0 = ( 0g ‘ 𝑆 ) )