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