subrginv

Description: A subring always has the same inversion function, for elements that are invertible. (Contributed by Mario Carneiro, 4-Dec-2014)

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

Proof

Step	Hyp	Ref	Expression
1		subrginv.1	$⊢ S = R ↾_{𝑠} A$
2		subrginv.2	$⊢ I = {inv}_{r} (R)$
3		subrginv.3	$⊢ U = Unit (S)$
4		subrginv.4	$⊢ J = {inv}_{r} (S)$
5		subrgrcl	$⊢ A \in SubRing (R) \to R \in Ring$
6	5	adantr	$⊢ (A \in SubRing (R) \land X \in U) \to R \in Ring$
7	1	subrgbas	$⊢ A \in SubRing (R) \to A = {Base}_{S}$
8		eqid	$⊢ {Base}_{R} = {Base}_{R}$
9	8	subrgss	$⊢ A \in SubRing (R) \to A \subseteq {Base}_{R}$
10	7 9	eqsstrrd	$⊢ A \in SubRing (R) \to {Base}_{S} \subseteq {Base}_{R}$
11	10	adantr	$⊢ (A \in SubRing (R) \land X \in U) \to {Base}_{S} \subseteq {Base}_{R}$
12	1	subrgring	$⊢ A \in SubRing (R) \to S \in Ring$
13		eqid	$⊢ {Base}_{S} = {Base}_{S}$
14	3 4 13	ringinvcl	$⊢ (S \in Ring \land X \in U) \to J (X) \in {Base}_{S}$
15	12 14	sylan	$⊢ (A \in SubRing (R) \land X \in U) \to J (X) \in {Base}_{S}$
16	11 15	sseldd	$⊢ (A \in SubRing (R) \land X \in U) \to J (X) \in {Base}_{R}$
17	13 3	unitcl	$⊢ X \in U \to X \in {Base}_{S}$
18	17	adantl	$⊢ (A \in SubRing (R) \land X \in U) \to X \in {Base}_{S}$
19	11 18	sseldd	$⊢ (A \in SubRing (R) \land X \in U) \to X \in {Base}_{R}$
20		eqid	$⊢ Unit (R) = Unit (R)$
21	1 20 3	subrguss	$⊢ A \in SubRing (R) \to U \subseteq Unit (R)$
22	21	sselda	$⊢ (A \in SubRing (R) \land X \in U) \to X \in Unit (R)$
23	20 2 8	ringinvcl	$⊢ (R \in Ring \land X \in Unit (R)) \to I (X) \in {Base}_{R}$
24	5 22 23	syl2an2r	$⊢ (A \in SubRing (R) \land X \in U) \to I (X) \in {Base}_{R}$
25		eqid	$⊢ \cdot_{R} = \cdot_{R}$
26	8 25	ringass	$⊢ (R \in Ring \land (J (X) \in {Base}_{R} \land X \in {Base}_{R} \land I (X) \in {Base}_{R})) \to (J (X) \cdot_{R} X) \cdot_{R} I (X) = J (X) \cdot_{R} (X \cdot_{R} I (X))$
27	6 16 19 24 26	syl13anc	$⊢ (A \in SubRing (R) \land X \in U) \to (J (X) \cdot_{R} X) \cdot_{R} I (X) = J (X) \cdot_{R} (X \cdot_{R} I (X))$
28		eqid	$⊢ \cdot_{S} = \cdot_{S}$
29		eqid	$⊢ 1_{S} = 1_{S}$
30	3 4 28 29	unitlinv	$⊢ (S \in Ring \land X \in U) \to J (X) \cdot_{S} X = 1_{S}$
31	12 30	sylan	$⊢ (A \in SubRing (R) \land X \in U) \to J (X) \cdot_{S} X = 1_{S}$
32	1 25	ressmulr	$⊢ A \in SubRing (R) \to \cdot_{R} = \cdot_{S}$
33	32	adantr	$⊢ (A \in SubRing (R) \land X \in U) \to \cdot_{R} = \cdot_{S}$
34	33	oveqd	$⊢ (A \in SubRing (R) \land X \in U) \to J (X) \cdot_{R} X = J (X) \cdot_{S} X$
35		eqid	$⊢ 1_{R} = 1_{R}$
36	1 35	subrg1	$⊢ A \in SubRing (R) \to 1_{R} = 1_{S}$
37	36	adantr	$⊢ (A \in SubRing (R) \land X \in U) \to 1_{R} = 1_{S}$
38	31 34 37	3eqtr4d	$⊢ (A \in SubRing (R) \land X \in U) \to J (X) \cdot_{R} X = 1_{R}$
39	38	oveq1d	$⊢ (A \in SubRing (R) \land X \in U) \to (J (X) \cdot_{R} X) \cdot_{R} I (X) = 1_{R} \cdot_{R} I (X)$
40	20 2 25 35	unitrinv	$⊢ (R \in Ring \land X \in Unit (R)) \to X \cdot_{R} I (X) = 1_{R}$
41	5 22 40	syl2an2r	$⊢ (A \in SubRing (R) \land X \in U) \to X \cdot_{R} I (X) = 1_{R}$
42	41	oveq2d	$⊢ (A \in SubRing (R) \land X \in U) \to J (X) \cdot_{R} (X \cdot_{R} I (X)) = J (X) \cdot_{R} 1_{R}$
43	27 39 42	3eqtr3d	$⊢ (A \in SubRing (R) \land X \in U) \to 1_{R} \cdot_{R} I (X) = J (X) \cdot_{R} 1_{R}$
44	8 25 35	ringlidm	$⊢ (R \in Ring \land I (X) \in {Base}_{R}) \to 1_{R} \cdot_{R} I (X) = I (X)$
45	5 24 44	syl2an2r	$⊢ (A \in SubRing (R) \land X \in U) \to 1_{R} \cdot_{R} I (X) = I (X)$
46	8 25 35	ringridm	$⊢ (R \in Ring \land J (X) \in {Base}_{R}) \to J (X) \cdot_{R} 1_{R} = J (X)$
47	5 16 46	syl2an2r	$⊢ (A \in SubRing (R) \land X \in U) \to J (X) \cdot_{R} 1_{R} = J (X)$
48	43 45 47	3eqtr3d	$⊢ (A \in SubRing (R) \land X \in U) \to I (X) = J (X)$

Metamath Proof Explorer

Theorem subrginv

Proof