subrg1

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

	Ref	Expression
Hypotheses	subrg1.1	$⊢ S = R ↾_{𝑠} A$
	subrg1.2	$⊢ \underset{˙}{1} = 1_{R}$
Assertion	subrg1	$⊢ A \in SubRing (R) \to \underset{˙}{1} = 1_{S}$

Proof

Step	Hyp	Ref	Expression
1		subrg1.1	$⊢ S = R ↾_{𝑠} A$
2		subrg1.2	$⊢ \underset{˙}{1} = 1_{R}$
3		eqid	$⊢ 1_{R} = 1_{R}$
4	3	subrg1cl	$⊢ A \in SubRing (R) \to 1_{R} \in A$
5	1	subrgbas	$⊢ A \in SubRing (R) \to A = {Base}_{S}$
6	4 5	eleqtrd	$⊢ A \in SubRing (R) \to 1_{R} \in {Base}_{S}$
7		eqid	$⊢ {Base}_{R} = {Base}_{R}$
8	7	subrgss	$⊢ A \in SubRing (R) \to A \subseteq {Base}_{R}$
9	5 8	eqsstrrd	$⊢ A \in SubRing (R) \to {Base}_{S} \subseteq {Base}_{R}$
10	9	sselda	$⊢ (A \in SubRing (R) \land x \in {Base}_{S}) \to x \in {Base}_{R}$
11		subrgrcl	$⊢ A \in SubRing (R) \to R \in Ring$
12		eqid	$⊢ \cdot_{R} = \cdot_{R}$
13	7 12 3	ringidmlem	$⊢ (R \in Ring \land x \in {Base}_{R}) \to (1_{R} \cdot_{R} x = x \land x \cdot_{R} 1_{R} = x)$
14	11 13	sylan	$⊢ (A \in SubRing (R) \land x \in {Base}_{R}) \to (1_{R} \cdot_{R} x = x \land x \cdot_{R} 1_{R} = x)$
15	1 12	ressmulr	$⊢ A \in SubRing (R) \to \cdot_{R} = \cdot_{S}$
16	15	oveqd	$⊢ A \in SubRing (R) \to 1_{R} \cdot_{R} x = 1_{R} \cdot_{S} x$
17	16	eqeq1d	$⊢ A \in SubRing (R) \to (1_{R} \cdot_{R} x = x \leftrightarrow 1_{R} \cdot_{S} x = x)$
18	15	oveqd	$⊢ A \in SubRing (R) \to x \cdot_{R} 1_{R} = x \cdot_{S} 1_{R}$
19	18	eqeq1d	$⊢ A \in SubRing (R) \to (x \cdot_{R} 1_{R} = x \leftrightarrow x \cdot_{S} 1_{R} = x)$
20	17 19	anbi12d	$⊢ A \in SubRing (R) \to ((1_{R} \cdot_{R} x = x \land x \cdot_{R} 1_{R} = x) \leftrightarrow (1_{R} \cdot_{S} x = x \land x \cdot_{S} 1_{R} = x))$
21	20	biimpa	$⊢ (A \in SubRing (R) \land (1_{R} \cdot_{R} x = x \land x \cdot_{R} 1_{R} = x)) \to (1_{R} \cdot_{S} x = x \land x \cdot_{S} 1_{R} = x)$
22	14 21	syldan	$⊢ (A \in SubRing (R) \land x \in {Base}_{R}) \to (1_{R} \cdot_{S} x = x \land x \cdot_{S} 1_{R} = x)$
23	10 22	syldan	$⊢ (A \in SubRing (R) \land x \in {Base}_{S}) \to (1_{R} \cdot_{S} x = x \land x \cdot_{S} 1_{R} = x)$
24	23	ralrimiva	$⊢ A \in SubRing (R) \to \forall x \in {Base}_{S} (1_{R} \cdot_{S} x = x \land x \cdot_{S} 1_{R} = x)$
25	1	subrgring	$⊢ A \in SubRing (R) \to S \in Ring$
26		eqid	$⊢ {Base}_{S} = {Base}_{S}$
27		eqid	$⊢ \cdot_{S} = \cdot_{S}$
28		eqid	$⊢ 1_{S} = 1_{S}$
29	26 27 28	isringid	$⊢ S \in Ring \to ((1_{R} \in {Base}_{S} \land \forall x \in {Base}_{S} (1_{R} \cdot_{S} x = x \land x \cdot_{S} 1_{R} = x)) \leftrightarrow 1_{S} = 1_{R})$
30	25 29	syl	$⊢ A \in SubRing (R) \to ((1_{R} \in {Base}_{S} \land \forall x \in {Base}_{S} (1_{R} \cdot_{S} x = x \land x \cdot_{S} 1_{R} = x)) \leftrightarrow 1_{S} = 1_{R})$
31	6 24 30	mpbi2and	$⊢ A \in SubRing (R) \to 1_{S} = 1_{R}$
32	2 31	eqtr4id	$⊢ A \in SubRing (R) \to \underset{˙}{1} = 1_{S}$

Metamath Proof Explorer

Theorem subrg1

Proof