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 𝐴 )
	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	1 2	ressbas2	⊢ ( 𝐴 ⊆ 𝐵 → 𝐴 = ( Base ‘ 𝑆 ) )
5	4	3ad2ant3	⊢ ( ( 𝑅 ∈ Mnd ∧ 0 ∈ 𝐴 ∧ 𝐴 ⊆ 𝐵 ) → 𝐴 = ( Base ‘ 𝑆 ) )
6		simp3	⊢ ( ( 𝑅 ∈ Mnd ∧ 0 ∈ 𝐴 ∧ 𝐴 ⊆ 𝐵 ) → 𝐴 ⊆ 𝐵 )
7	2	fvexi	⊢ 𝐵 ∈ V
8		ssexg	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ V ) → 𝐴 ∈ V )
9	6 7 8	sylancl	⊢ ( ( 𝑅 ∈ Mnd ∧ 0 ∈ 𝐴 ∧ 𝐴 ⊆ 𝐵 ) → 𝐴 ∈ V )
10		eqid	⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
11	1 10	ressplusg	⊢ ( 𝐴 ∈ V → ( +g ‘ 𝑅 ) = ( +g ‘ 𝑆 ) )
12	9 11	syl	⊢ ( ( 𝑅 ∈ Mnd ∧ 0 ∈ 𝐴 ∧ 𝐴 ⊆ 𝐵 ) → ( +g ‘ 𝑅 ) = ( +g ‘ 𝑆 ) )
13		simp2	⊢ ( ( 𝑅 ∈ Mnd ∧ 0 ∈ 𝐴 ∧ 𝐴 ⊆ 𝐵 ) → 0 ∈ 𝐴 )
14		simpl1	⊢ ( ( ( 𝑅 ∈ Mnd ∧ 0 ∈ 𝐴 ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → 𝑅 ∈ Mnd )
15	6	sselda	⊢ ( ( ( 𝑅 ∈ Mnd ∧ 0 ∈ 𝐴 ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐵 )
16	2 10 3	mndlid	⊢ ( ( 𝑅 ∈ Mnd ∧ 𝑥 ∈ 𝐵 ) → ( 0 ( +g ‘ 𝑅 ) 𝑥 ) = 𝑥 )
17	14 15 16	syl2anc	⊢ ( ( ( 𝑅 ∈ Mnd ∧ 0 ∈ 𝐴 ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → ( 0 ( +g ‘ 𝑅 ) 𝑥 ) = 𝑥 )
18	2 10 3	mndrid	⊢ ( ( 𝑅 ∈ Mnd ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 ( +g ‘ 𝑅 ) 0 ) = 𝑥 )
19	14 15 18	syl2anc	⊢ ( ( ( 𝑅 ∈ Mnd ∧ 0 ∈ 𝐴 ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 ( +g ‘ 𝑅 ) 0 ) = 𝑥 )
20	5 12 13 17 19	grpidd	⊢ ( ( 𝑅 ∈ Mnd ∧ 0 ∈ 𝐴 ∧ 𝐴 ⊆ 𝐵 ) → 0 = ( 0g ‘ 𝑆 ) )