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

Metamath Proof Explorer

Theorem subrg1

Description: A subring always has the same multiplicative identity. (Contributed by Stefan O'Rear, 27-Nov-2014)

Ref Expression
Hypotheses subrg1.1 ⊢ 𝑆 = ( 𝑅 ↾s 𝐴 )
subrg1.2 ⊢ 1 = ( 1r ‘ 𝑅 )
Assertion subrg1 ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → 1 = ( 1r ‘ 𝑆 ) )

Proof

Step Hyp Ref Expression
1 subrg1.1 ⊢ 𝑆 = ( 𝑅 ↾s 𝐴 )
2 subrg1.2 ⊢ 1 = ( 1r ‘ 𝑅 )
3 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
4 3 subrg1cl ⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → ( 1r ‘ 𝑅 ) ∈ 𝐴 )
5 1 subrgbas ⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → 𝐴 = ( Base ‘ 𝑆 ) )
6 4 5 eleqtrd ⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑆 ) )
7 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
8 7 subrgss ⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → 𝐴 ⊆ ( Base ‘ 𝑅 ) )
9 5 8 eqsstrrd ⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → ( Base ‘ 𝑆 ) ⊆ ( Base ‘ 𝑅 ) )
10 9 sselda ⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ) → 𝑥 ∈ ( Base ‘ 𝑅 ) )
11 subrgrcl ⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → 𝑅 ∈ Ring )
12 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
13 7 12 3 ringidmlem ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) → ( ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) = 𝑥 ) )
14 11 13 sylan ⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) → ( ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) = 𝑥 ) )
15 1 12 ressmulr ⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → ( .r ‘ 𝑅 ) = ( .r ‘ 𝑆 ) )
16 15 oveqd ⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) 𝑥 ) = ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑆 ) 𝑥 ) )
17 16 eqeq1d ⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → ( ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) 𝑥 ) = 𝑥 ↔ ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑆 ) 𝑥 ) = 𝑥 ) )
18 15 oveqd ⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → ( 𝑥 ( .r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) = ( 𝑥 ( .r ‘ 𝑆 ) ( 1r ‘ 𝑅 ) ) )
19 18 eqeq1d ⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → ( ( 𝑥 ( .r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) = 𝑥 ↔ ( 𝑥 ( .r ‘ 𝑆 ) ( 1r ‘ 𝑅 ) ) = 𝑥 ) )
20 17 19 anbi12d ⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → ( ( ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) = 𝑥 ) ↔ ( ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑆 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r ‘ 𝑆 ) ( 1r ‘ 𝑅 ) ) = 𝑥 ) ) )
21 20 biimpa ⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ ( ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) = 𝑥 ) ) → ( ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑆 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r ‘ 𝑆 ) ( 1r ‘ 𝑅 ) ) = 𝑥 ) )
22 14 21 syldan ⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) → ( ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑆 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r ‘ 𝑆 ) ( 1r ‘ 𝑅 ) ) = 𝑥 ) )
23 10 22 syldan ⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ) → ( ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑆 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r ‘ 𝑆 ) ( 1r ‘ 𝑅 ) ) = 𝑥 ) )
24 23 ralrimiva ⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → ∀ 𝑥 ∈ ( Base ‘ 𝑆 ) ( ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑆 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r ‘ 𝑆 ) ( 1r ‘ 𝑅 ) ) = 𝑥 ) )
25 1 subrgring ⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → 𝑆 ∈ Ring )
26 eqid ⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
27 eqid ⊢ ( .r ‘ 𝑆 ) = ( .r ‘ 𝑆 )
28 eqid ⊢ ( 1r ‘ 𝑆 ) = ( 1r ‘ 𝑆 )
29 26 27 28 isringid ⊢ ( 𝑆 ∈ Ring → ( ( ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑆 ) ( ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑆 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r ‘ 𝑆 ) ( 1r ‘ 𝑅 ) ) = 𝑥 ) ) ↔ ( 1r ‘ 𝑆 ) = ( 1r ‘ 𝑅 ) ) )
30 25 29 syl ⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → ( ( ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑆 ) ( ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑆 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r ‘ 𝑆 ) ( 1r ‘ 𝑅 ) ) = 𝑥 ) ) ↔ ( 1r ‘ 𝑆 ) = ( 1r ‘ 𝑅 ) ) )
31 6 24 30 mpbi2and ⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → ( 1r ‘ 𝑆 ) = ( 1r ‘ 𝑅 ) )
32 2 31 eqtr4id ⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → 1 = ( 1r ‘ 𝑆 ) )