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	31 2	syl6reqr	⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → 1 = ( 1r ‘ 𝑆 ) )