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 = R ↾_{𝑠} A$
	ress1r.b	$⊢ B = {Base}_{R}$
	ress1r.1	$⊢ \underset{˙}{1} = 1_{R}$
Assertion	ress1r	$⊢ (R \in Ring \land \underset{˙}{1} \in A \land A \subseteq B) \to \underset{˙}{1} = 1_{S}$

Proof

Step	Hyp	Ref	Expression
1		ress1r.s	$⊢ S = R ↾_{𝑠} A$
2		ress1r.b	$⊢ B = {Base}_{R}$
3		ress1r.1	$⊢ \underset{˙}{1} = 1_{R}$
4	1 2	ressbas2	$⊢ A \subseteq B \to A = {Base}_{S}$
5	4	3ad2ant3	$⊢ (R \in Ring \land \underset{˙}{1} \in A \land A \subseteq B) \to A = {Base}_{S}$
6		simp3	$⊢ (R \in Ring \land \underset{˙}{1} \in A \land A \subseteq B) \to A \subseteq B$
7	2	fvexi	$⊢ B \in V$
8		ssexg	$⊢ (A \subseteq B \land B \in V) \to A \in V$
9	6 7 8	sylancl	$⊢ (R \in Ring \land \underset{˙}{1} \in A \land A \subseteq B) \to A \in V$
10		eqid	$⊢ \cdot_{R} = \cdot_{R}$
11	1 10	ressmulr	$⊢ A \in V \to \cdot_{R} = \cdot_{S}$
12	9 11	syl	$⊢ (R \in Ring \land \underset{˙}{1} \in A \land A \subseteq B) \to \cdot_{R} = \cdot_{S}$
13		simp2	$⊢ (R \in Ring \land \underset{˙}{1} \in A \land A \subseteq B) \to \underset{˙}{1} \in A$
14		simpl1	$⊢ ((R \in Ring \land \underset{˙}{1} \in A \land A \subseteq B) \land x \in A) \to R \in Ring$
15	6	sselda	$⊢ ((R \in Ring \land \underset{˙}{1} \in A \land A \subseteq B) \land x \in A) \to x \in B$
16	2 10 3	ringlidm	$⊢ (R \in Ring \land x \in B) \to \underset{˙}{1} \cdot_{R} x = x$
17	14 15 16	syl2anc	$⊢ ((R \in Ring \land \underset{˙}{1} \in A \land A \subseteq B) \land x \in A) \to \underset{˙}{1} \cdot_{R} x = x$
18	2 10 3	ringridm	$⊢ (R \in Ring \land x \in B) \to x \cdot_{R} \underset{˙}{1} = x$
19	14 15 18	syl2anc	$⊢ ((R \in Ring \land \underset{˙}{1} \in A \land A \subseteq B) \land x \in A) \to x \cdot_{R} \underset{˙}{1} = x$
20	5 12 13 17 19	ringurd	$⊢ (R \in Ring \land \underset{˙}{1} \in A \land A \subseteq B) \to \underset{˙}{1} = 1_{S}$

Metamath Proof Explorer

Theorem ress1r

Proof