subrguss

Description: A unit of a subring is a unit of the parent ring. (Contributed by Mario Carneiro, 4-Dec-2014)

	Ref	Expression
Hypotheses	subrguss.1	$⊢ S = R ↾_{𝑠} A$
	subrguss.2	$⊢ U = Unit (R)$
	subrguss.3	$⊢ V = Unit (S)$
Assertion	subrguss	$⊢ A \in SubRing (R) \to V \subseteq U$

Proof

Step	Hyp	Ref	Expression
1		subrguss.1	$⊢ S = R ↾_{𝑠} A$
2		subrguss.2	$⊢ U = Unit (R)$
3		subrguss.3	$⊢ V = Unit (S)$
4		simpr	$⊢ (A \in SubRing (R) \land x \in V) \to x \in V$
5		eqid	$⊢ 1_{S} = 1_{S}$
6		eqid	$⊢ ∥_{r} (S) = ∥_{r} (S)$
7		eqid	$⊢ {opp}_{r} (S) = {opp}_{r} (S)$
8		eqid	$⊢ ∥_{r} ({opp}_{r} (S)) = ∥_{r} ({opp}_{r} (S))$
9	3 5 6 7 8	isunit	$⊢ x \in V \leftrightarrow (x ∥_{r} (S) 1_{S} \land x ∥_{r} ({opp}_{r} (S)) 1_{S})$
10	4 9	sylib	$⊢ (A \in SubRing (R) \land x \in V) \to (x ∥_{r} (S) 1_{S} \land x ∥_{r} ({opp}_{r} (S)) 1_{S})$
11	10	simpld	$⊢ (A \in SubRing (R) \land x \in V) \to x ∥_{r} (S) 1_{S}$
12		eqid	$⊢ 1_{R} = 1_{R}$
13	1 12	subrg1	$⊢ A \in SubRing (R) \to 1_{R} = 1_{S}$
14	13	adantr	$⊢ (A \in SubRing (R) \land x \in V) \to 1_{R} = 1_{S}$
15	11 14	breqtrrd	$⊢ (A \in SubRing (R) \land x \in V) \to x ∥_{r} (S) 1_{R}$
16		eqid	$⊢ ∥_{r} (R) = ∥_{r} (R)$
17	1 16 6	subrgdvds	$⊢ A \in SubRing (R) \to ∥_{r} (S) \subseteq ∥_{r} (R)$
18	17	adantr	$⊢ (A \in SubRing (R) \land x \in V) \to ∥_{r} (S) \subseteq ∥_{r} (R)$
19	18	ssbrd	$⊢ (A \in SubRing (R) \land x \in V) \to (x ∥_{r} (S) 1_{R} \to x ∥_{r} (R) 1_{R})$
20	15 19	mpd	$⊢ (A \in SubRing (R) \land x \in V) \to x ∥_{r} (R) 1_{R}$
21	1	subrgbas	$⊢ A \in SubRing (R) \to A = {Base}_{S}$
22	21	adantr	$⊢ (A \in SubRing (R) \land x \in V) \to A = {Base}_{S}$
23		eqid	$⊢ {Base}_{R} = {Base}_{R}$
24	23	subrgss	$⊢ A \in SubRing (R) \to A \subseteq {Base}_{R}$
25	24	adantr	$⊢ (A \in SubRing (R) \land x \in V) \to A \subseteq {Base}_{R}$
26	22 25	eqsstrrd	$⊢ (A \in SubRing (R) \land x \in V) \to {Base}_{S} \subseteq {Base}_{R}$
27		eqid	$⊢ {Base}_{S} = {Base}_{S}$
28	27 3	unitcl	$⊢ x \in V \to x \in {Base}_{S}$
29	28	adantl	$⊢ (A \in SubRing (R) \land x \in V) \to x \in {Base}_{S}$
30	26 29	sseldd	$⊢ (A \in SubRing (R) \land x \in V) \to x \in {Base}_{R}$
31	1	subrgring	$⊢ A \in SubRing (R) \to S \in Ring$
32		eqid	$⊢ {inv}_{r} (S) = {inv}_{r} (S)$
33	3 32 27	ringinvcl	$⊢ (S \in Ring \land x \in V) \to {inv}_{r} (S) (x) \in {Base}_{S}$
34	31 33	sylan	$⊢ (A \in SubRing (R) \land x \in V) \to {inv}_{r} (S) (x) \in {Base}_{S}$
35	26 34	sseldd	$⊢ (A \in SubRing (R) \land x \in V) \to {inv}_{r} (S) (x) \in {Base}_{R}$
36		eqid	$⊢ {opp}_{r} (R) = {opp}_{r} (R)$
37	36 23	opprbas	$⊢ {Base}_{R} = {Base}_{{opp}_{r} (R)}$
38		eqid	$⊢ ∥_{r} ({opp}_{r} (R)) = ∥_{r} ({opp}_{r} (R))$
39		eqid	$⊢ \cdot_{{opp}_{r} (R)} = \cdot_{{opp}_{r} (R)}$
40	37 38 39	dvdsrmul	$⊢ (x \in {Base}_{R} \land {inv}_{r} (S) (x) \in {Base}_{R}) \to x ∥_{r} ({opp}_{r} (R)) ({inv}_{r} (S) (x) \cdot_{{opp}_{r} (R)} x)$
41	30 35 40	syl2anc	$⊢ (A \in SubRing (R) \land x \in V) \to x ∥_{r} ({opp}_{r} (R)) ({inv}_{r} (S) (x) \cdot_{{opp}_{r} (R)} x)$
42		eqid	$⊢ \cdot_{R} = \cdot_{R}$
43	23 42 36 39	opprmul	$⊢ {inv}_{r} (S) (x) \cdot_{{opp}_{r} (R)} x = x \cdot_{R} {inv}_{r} (S) (x)$
44		eqid	$⊢ \cdot_{S} = \cdot_{S}$
45	3 32 44 5	unitrinv	$⊢ (S \in Ring \land x \in V) \to x \cdot_{S} {inv}_{r} (S) (x) = 1_{S}$
46	31 45	sylan	$⊢ (A \in SubRing (R) \land x \in V) \to x \cdot_{S} {inv}_{r} (S) (x) = 1_{S}$
47	1 42	ressmulr	$⊢ A \in SubRing (R) \to \cdot_{R} = \cdot_{S}$
48	47	adantr	$⊢ (A \in SubRing (R) \land x \in V) \to \cdot_{R} = \cdot_{S}$
49	48	oveqd	$⊢ (A \in SubRing (R) \land x \in V) \to x \cdot_{R} {inv}_{r} (S) (x) = x \cdot_{S} {inv}_{r} (S) (x)$
50	46 49 14	3eqtr4d	$⊢ (A \in SubRing (R) \land x \in V) \to x \cdot_{R} {inv}_{r} (S) (x) = 1_{R}$
51	43 50	syl5eq	$⊢ (A \in SubRing (R) \land x \in V) \to {inv}_{r} (S) (x) \cdot_{{opp}_{r} (R)} x = 1_{R}$
52	41 51	breqtrd	$⊢ (A \in SubRing (R) \land x \in V) \to x ∥_{r} ({opp}_{r} (R)) 1_{R}$
53	2 12 16 36 38	isunit	$⊢ x \in U \leftrightarrow (x ∥_{r} (R) 1_{R} \land x ∥_{r} ({opp}_{r} (R)) 1_{R})$
54	20 52 53	sylanbrc	$⊢ (A \in SubRing (R) \land x \in V) \to x \in U$
55	54	ex	$⊢ A \in SubRing (R) \to (x \in V \to x \in U)$
56	55	ssrdv	$⊢ A \in SubRing (R) \to V \subseteq U$

Metamath Proof Explorer

Theorem subrguss

Proof