subrgugrp

Description: The units of a subring form a subgroup of the unit group of the original ring. (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)$
	subrgugrp.4	$⊢ G = {mulGrp}_{R} ↾_{𝑠} U$
Assertion	subrgugrp	$⊢ A \in SubRing (R) \to V \in SubGrp (G)$

Proof

Step	Hyp	Ref	Expression
1		subrgugrp.1	$⊢ S = R ↾_{𝑠} A$
2		subrgugrp.2	$⊢ U = Unit (R)$
3		subrgugrp.3	$⊢ V = Unit (S)$
4		subrgugrp.4	$⊢ G = {mulGrp}_{R} ↾_{𝑠} U$
5	1 2 3	subrguss	$⊢ A \in SubRing (R) \to V \subseteq U$
6	1	subrgring	$⊢ A \in SubRing (R) \to S \in Ring$
7		eqid	$⊢ 1_{S} = 1_{S}$
8	3 7	1unit	$⊢ S \in Ring \to 1_{S} \in V$
9		ne0i	$⊢ 1_{S} \in V \to V \neq \emptyset$
10	6 8 9	3syl	$⊢ A \in SubRing (R) \to V \neq \emptyset$
11		eqid	$⊢ \cdot_{R} = \cdot_{R}$
12	1 11	ressmulr	$⊢ A \in SubRing (R) \to \cdot_{R} = \cdot_{S}$
13	12	3ad2ant1	$⊢ (A \in SubRing (R) \land x \in V \land y \in V) \to \cdot_{R} = \cdot_{S}$
14	13	oveqd	$⊢ (A \in SubRing (R) \land x \in V \land y \in V) \to x \cdot_{R} y = x \cdot_{S} y$
15		eqid	$⊢ \cdot_{S} = \cdot_{S}$
16	3 15	unitmulcl	$⊢ (S \in Ring \land x \in V \land y \in V) \to x \cdot_{S} y \in V$
17	6 16	syl3an1	$⊢ (A \in SubRing (R) \land x \in V \land y \in V) \to x \cdot_{S} y \in V$
18	14 17	eqeltrd	$⊢ (A \in SubRing (R) \land x \in V \land y \in V) \to x \cdot_{R} y \in V$
19	18	3expa	$⊢ ((A \in SubRing (R) \land x \in V) \land y \in V) \to x \cdot_{R} y \in V$
20	19	ralrimiva	$⊢ (A \in SubRing (R) \land x \in V) \to \forall y \in V x \cdot_{R} y \in V$
21		eqid	$⊢ {inv}_{r} (R) = {inv}_{r} (R)$
22		eqid	$⊢ {inv}_{r} (S) = {inv}_{r} (S)$
23	1 21 3 22	subrginv	$⊢ (A \in SubRing (R) \land x \in V) \to {inv}_{r} (R) (x) = {inv}_{r} (S) (x)$
24	3 22	unitinvcl	$⊢ (S \in Ring \land x \in V) \to {inv}_{r} (S) (x) \in V$
25	6 24	sylan	$⊢ (A \in SubRing (R) \land x \in V) \to {inv}_{r} (S) (x) \in V$
26	23 25	eqeltrd	$⊢ (A \in SubRing (R) \land x \in V) \to {inv}_{r} (R) (x) \in V$
27	20 26	jca	$⊢ (A \in SubRing (R) \land x \in V) \to (\forall y \in V x \cdot_{R} y \in V \land {inv}_{r} (R) (x) \in V)$
28	27	ralrimiva	$⊢ A \in SubRing (R) \to \forall x \in V (\forall y \in V x \cdot_{R} y \in V \land {inv}_{r} (R) (x) \in V)$
29		subrgrcl	$⊢ A \in SubRing (R) \to R \in Ring$
30	2 4	unitgrp	$⊢ R \in Ring \to G \in Grp$
31	2 4	unitgrpbas	$⊢ U = {Base}_{G}$
32	2	fvexi	$⊢ U \in V$
33		eqid	$⊢ {mulGrp}_{R} = {mulGrp}_{R}$
34	33 11	mgpplusg	$⊢ \cdot_{R} = +_{{mulGrp}_{R}}$
35	4 34	ressplusg	$⊢ U \in V \to \cdot_{R} = +_{G}$
36	32 35	ax-mp	$⊢ \cdot_{R} = +_{G}$
37	2 4 21	invrfval	$⊢ {inv}_{r} (R) = {inv}_{g} (G)$
38	31 36 37	issubg2	$⊢ G \in Grp \to (V \in SubGrp (G) \leftrightarrow (V \subseteq U \land V \neq \emptyset \land \forall x \in V (\forall y \in V x \cdot_{R} y \in V \land {inv}_{r} (R) (x) \in V)))$
39	29 30 38	3syl	$⊢ A \in SubRing (R) \to (V \in SubGrp (G) \leftrightarrow (V \subseteq U \land V \neq \emptyset \land \forall x \in V (\forall y \in V x \cdot_{R} y \in V \land {inv}_{r} (R) (x) \in V)))$
40	5 10 28 39	mpbir3and	$⊢ A \in SubRing (R) \to V \in SubGrp (G)$

Metamath Proof Explorer

Theorem subrgugrp

Proof