subrgunit

Description: An element of a ring is a unit of a subring iff it is a unit of the parent ring and both it and its inverse are in the subring. (Contributed by Mario Carneiro, 4-Dec-2014)

	Ref	Expression
Hypotheses	subrgugrp.1	$⊢ S = R ↾_{𝑠} A$
	subrgugrp.2	$⊢ U = Unit (R)$
	subrgugrp.3	$⊢ V = Unit (S)$
	subrgunit.4	$⊢ I = {inv}_{r} (R)$
Assertion	subrgunit	$⊢ A \in SubRing (R) \to (X \in V \leftrightarrow (X \in U \land X \in A \land I (X) \in A))$

Proof

Step	Hyp	Ref	Expression
1		subrgugrp.1	$⊢ S = R ↾_{𝑠} A$
2		subrgugrp.2	$⊢ U = Unit (R)$
3		subrgugrp.3	$⊢ V = Unit (S)$
4		subrgunit.4	$⊢ I = {inv}_{r} (R)$
5	1 2 3	subrguss	$⊢ A \in SubRing (R) \to V \subseteq U$
6	5	sselda	$⊢ (A \in SubRing (R) \land X \in V) \to X \in U$
7		eqid	$⊢ {Base}_{S} = {Base}_{S}$
8	7 3	unitcl	$⊢ X \in V \to X \in {Base}_{S}$
9	8	adantl	$⊢ (A \in SubRing (R) \land X \in V) \to X \in {Base}_{S}$
10	1	subrgbas	$⊢ A \in SubRing (R) \to A = {Base}_{S}$
11	10	adantr	$⊢ (A \in SubRing (R) \land X \in V) \to A = {Base}_{S}$
12	9 11	eleqtrrd	$⊢ (A \in SubRing (R) \land X \in V) \to X \in A$
13	1	subrgring	$⊢ A \in SubRing (R) \to S \in Ring$
14		eqid	$⊢ {inv}_{r} (S) = {inv}_{r} (S)$
15	3 14 7	ringinvcl	$⊢ (S \in Ring \land X \in V) \to {inv}_{r} (S) (X) \in {Base}_{S}$
16	13 15	sylan	$⊢ (A \in SubRing (R) \land X \in V) \to {inv}_{r} (S) (X) \in {Base}_{S}$
17	1 4 3 14	subrginv	$⊢ (A \in SubRing (R) \land X \in V) \to I (X) = {inv}_{r} (S) (X)$
18	16 17 11	3eltr4d	$⊢ (A \in SubRing (R) \land X \in V) \to I (X) \in A$
19	6 12 18	3jca	$⊢ (A \in SubRing (R) \land X \in V) \to (X \in U \land X \in A \land I (X) \in A)$
20		simpr2	$⊢ (A \in SubRing (R) \land (X \in U \land X \in A \land I (X) \in A)) \to X \in A$
21	10	adantr	$⊢ (A \in SubRing (R) \land (X \in U \land X \in A \land I (X) \in A)) \to A = {Base}_{S}$
22	20 21	eleqtrd	$⊢ (A \in SubRing (R) \land (X \in U \land X \in A \land I (X) \in A)) \to X \in {Base}_{S}$
23		simpr3	$⊢ (A \in SubRing (R) \land (X \in U \land X \in A \land I (X) \in A)) \to I (X) \in A$
24	23 21	eleqtrd	$⊢ (A \in SubRing (R) \land (X \in U \land X \in A \land I (X) \in A)) \to I (X) \in {Base}_{S}$
25		eqid	$⊢ ∥_{r} (S) = ∥_{r} (S)$
26		eqid	$⊢ \cdot_{S} = \cdot_{S}$
27	7 25 26	dvdsrmul	$⊢ (X \in {Base}_{S} \land I (X) \in {Base}_{S}) \to X ∥_{r} (S) (I (X) \cdot_{S} X)$
28	22 24 27	syl2anc	$⊢ (A \in SubRing (R) \land (X \in U \land X \in A \land I (X) \in A)) \to X ∥_{r} (S) (I (X) \cdot_{S} X)$
29		subrgrcl	$⊢ A \in SubRing (R) \to R \in Ring$
30	29	adantr	$⊢ (A \in SubRing (R) \land (X \in U \land X \in A \land I (X) \in A)) \to R \in Ring$
31		simpr1	$⊢ (A \in SubRing (R) \land (X \in U \land X \in A \land I (X) \in A)) \to X \in U$
32		eqid	$⊢ \cdot_{R} = \cdot_{R}$
33		eqid	$⊢ 1_{R} = 1_{R}$
34	2 4 32 33	unitlinv	$⊢ (R \in Ring \land X \in U) \to I (X) \cdot_{R} X = 1_{R}$
35	30 31 34	syl2anc	$⊢ (A \in SubRing (R) \land (X \in U \land X \in A \land I (X) \in A)) \to I (X) \cdot_{R} X = 1_{R}$
36	1 32	ressmulr	$⊢ A \in SubRing (R) \to \cdot_{R} = \cdot_{S}$
37	36	adantr	$⊢ (A \in SubRing (R) \land (X \in U \land X \in A \land I (X) \in A)) \to \cdot_{R} = \cdot_{S}$
38	37	oveqd	$⊢ (A \in SubRing (R) \land (X \in U \land X \in A \land I (X) \in A)) \to I (X) \cdot_{R} X = I (X) \cdot_{S} X$
39	1 33	subrg1	$⊢ A \in SubRing (R) \to 1_{R} = 1_{S}$
40	39	adantr	$⊢ (A \in SubRing (R) \land (X \in U \land X \in A \land I (X) \in A)) \to 1_{R} = 1_{S}$
41	35 38 40	3eqtr3d	$⊢ (A \in SubRing (R) \land (X \in U \land X \in A \land I (X) \in A)) \to I (X) \cdot_{S} X = 1_{S}$
42	28 41	breqtrd	$⊢ (A \in SubRing (R) \land (X \in U \land X \in A \land I (X) \in A)) \to X ∥_{r} (S) 1_{S}$
43		eqid	$⊢ {opp}_{r} (S) = {opp}_{r} (S)$
44	43 7	opprbas	$⊢ {Base}_{S} = {Base}_{{opp}_{r} (S)}$
45		eqid	$⊢ ∥_{r} ({opp}_{r} (S)) = ∥_{r} ({opp}_{r} (S))$
46		eqid	$⊢ \cdot_{{opp}_{r} (S)} = \cdot_{{opp}_{r} (S)}$
47	44 45 46	dvdsrmul	$⊢ (X \in {Base}_{S} \land I (X) \in {Base}_{S}) \to X ∥_{r} ({opp}_{r} (S)) (I (X) \cdot_{{opp}_{r} (S)} X)$
48	22 24 47	syl2anc	$⊢ (A \in SubRing (R) \land (X \in U \land X \in A \land I (X) \in A)) \to X ∥_{r} ({opp}_{r} (S)) (I (X) \cdot_{{opp}_{r} (S)} X)$
49	7 26 43 46	opprmul	$⊢ I (X) \cdot_{{opp}_{r} (S)} X = X \cdot_{S} I (X)$
50	2 4 32 33	unitrinv	$⊢ (R \in Ring \land X \in U) \to X \cdot_{R} I (X) = 1_{R}$
51	30 31 50	syl2anc	$⊢ (A \in SubRing (R) \land (X \in U \land X \in A \land I (X) \in A)) \to X \cdot_{R} I (X) = 1_{R}$
52	37	oveqd	$⊢ (A \in SubRing (R) \land (X \in U \land X \in A \land I (X) \in A)) \to X \cdot_{R} I (X) = X \cdot_{S} I (X)$
53	51 52 40	3eqtr3d	$⊢ (A \in SubRing (R) \land (X \in U \land X \in A \land I (X) \in A)) \to X \cdot_{S} I (X) = 1_{S}$
54	49 53	syl5eq	$⊢ (A \in SubRing (R) \land (X \in U \land X \in A \land I (X) \in A)) \to I (X) \cdot_{{opp}_{r} (S)} X = 1_{S}$
55	48 54	breqtrd	$⊢ (A \in SubRing (R) \land (X \in U \land X \in A \land I (X) \in A)) \to X ∥_{r} ({opp}_{r} (S)) 1_{S}$
56		eqid	$⊢ 1_{S} = 1_{S}$
57	3 56 25 43 45	isunit	$⊢ X \in V \leftrightarrow (X ∥_{r} (S) 1_{S} \land X ∥_{r} ({opp}_{r} (S)) 1_{S})$
58	42 55 57	sylanbrc	$⊢ (A \in SubRing (R) \land (X \in U \land X \in A \land I (X) \in A)) \to X \in V$
59	19 58	impbida	$⊢ A \in SubRing (R) \to (X \in V \leftrightarrow (X \in U \land X \in A \land I (X) \in A))$

Metamath Proof Explorer

Theorem subrgunit

Proof