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

Metamath Proof Explorer

Theorem subrguss

Proof