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

Metamath Proof Explorer

Theorem ress1r

Description: 1r is unaffected by restriction. This is a bit more generic than subrg1 . (Contributed by Thierry Arnoux, 6-Sep-2018)

Ref Expression
Hypotheses ress1r.s ⊢ 𝑆 = ( 𝑅 ↾s 𝐴 )
ress1r.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
ress1r.1 ⊢ 1 = ( 1r ‘ 𝑅 )
Assertion ress1r ( ( 𝑅 ∈ Ring ∧ 1 ∈ 𝐴 ∧ 𝐴 ⊆ 𝐵 ) → 1 = ( 1r ‘ 𝑆 ) )

Proof

Step Hyp Ref Expression
1 ress1r.s ⊢ 𝑆 = ( 𝑅 ↾s 𝐴 )
2 ress1r.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
3 ress1r.1 ⊢ 1 = ( 1r ‘ 𝑅 )
4 1 2 ressbas2 ⊢ ( 𝐴 ⊆ 𝐵 → 𝐴 = ( Base ‘ 𝑆 ) )
5 4 3ad2ant3 ⊢ ( ( 𝑅 ∈ Ring ∧ 1 ∈ 𝐴 ∧ 𝐴 ⊆ 𝐵 ) → 𝐴 = ( Base ‘ 𝑆 ) )
6 simp3 ⊢ ( ( 𝑅 ∈ Ring ∧ 1 ∈ 𝐴 ∧ 𝐴 ⊆ 𝐵 ) → 𝐴 ⊆ 𝐵 )
7 2 fvexi ⊢ 𝐵 ∈ V
8 ssexg ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ V ) → 𝐴 ∈ V )
9 6 7 8 sylancl ⊢ ( ( 𝑅 ∈ Ring ∧ 1 ∈ 𝐴 ∧ 𝐴 ⊆ 𝐵 ) → 𝐴 ∈ V )
10 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
11 1 10 ressmulr ⊢ ( 𝐴 ∈ V → ( .r ‘ 𝑅 ) = ( .r ‘ 𝑆 ) )
12 9 11 syl ⊢ ( ( 𝑅 ∈ Ring ∧ 1 ∈ 𝐴 ∧ 𝐴 ⊆ 𝐵 ) → ( .r ‘ 𝑅 ) = ( .r ‘ 𝑆 ) )
13 simp2 ⊢ ( ( 𝑅 ∈ Ring ∧ 1 ∈ 𝐴 ∧ 𝐴 ⊆ 𝐵 ) → 1 ∈ 𝐴 )
14 simpl1 ⊢ ( ( ( 𝑅 ∈ Ring ∧ 1 ∈ 𝐴 ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → 𝑅 ∈ Ring )
15 6 sselda ⊢ ( ( ( 𝑅 ∈ Ring ∧ 1 ∈ 𝐴 ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐵 )
16 2 10 3 ringlidm ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐵 ) → ( 1 ( .r ‘ 𝑅 ) 𝑥 ) = 𝑥 )
17 14 15 16 syl2anc ⊢ ( ( ( 𝑅 ∈ Ring ∧ 1 ∈ 𝐴 ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → ( 1 ( .r ‘ 𝑅 ) 𝑥 ) = 𝑥 )
18 2 10 3 ringridm ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 ( .r ‘ 𝑅 ) 1 ) = 𝑥 )
19 14 15 18 syl2anc ⊢ ( ( ( 𝑅 ∈ Ring ∧ 1 ∈ 𝐴 ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 ( .r ‘ 𝑅 ) 1 ) = 𝑥 )
20 5 12 13 17 19 ringurd ⊢ ( ( 𝑅 ∈ Ring ∧ 1 ∈ 𝐴 ∧ 𝐴 ⊆ 𝐵 ) → 1 = ( 1r ‘ 𝑆 ) )