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 𝐴 )
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 ‘ 𝑆 ) )