unitgrp

Description: The group of units is a group under multiplication. (Contributed by Mario Carneiro, 2-Dec-2014)

	Ref	Expression
Hypotheses	unitmulcl.1	$⊢ U = Unit (R)$
	unitgrp.2	$⊢ G = {mulGrp}_{R} ↾_{𝑠} U$
Assertion	unitgrp	$⊢ R \in Ring \to G \in Grp$

Proof

Step	Hyp	Ref	Expression
1		unitmulcl.1	$⊢ U = Unit (R)$
2		unitgrp.2	$⊢ G = {mulGrp}_{R} ↾_{𝑠} U$
3	1 2	unitgrpbas	$⊢ U = {Base}_{G}$
4	3	a1i	$⊢ R \in Ring \to U = {Base}_{G}$
5	1	fvexi	$⊢ U \in V$
6		eqid	$⊢ {mulGrp}_{R} = {mulGrp}_{R}$
7		eqid	$⊢ \cdot_{R} = \cdot_{R}$
8	6 7	mgpplusg	$⊢ \cdot_{R} = +_{{mulGrp}_{R}}$
9	2 8	ressplusg	$⊢ U \in V \to \cdot_{R} = +_{G}$
10	5 9	mp1i	$⊢ R \in Ring \to \cdot_{R} = +_{G}$
11	1 7	unitmulcl	$⊢ (R \in Ring \land x \in U \land y \in U) \to x \cdot_{R} y \in U$
12		eqid	$⊢ {Base}_{R} = {Base}_{R}$
13	12 1	unitcl	$⊢ x \in U \to x \in {Base}_{R}$
14	12 1	unitcl	$⊢ y \in U \to y \in {Base}_{R}$
15	12 1	unitcl	$⊢ z \in U \to z \in {Base}_{R}$
16	13 14 15	3anim123i	$⊢ (x \in U \land y \in U \land z \in U) \to (x \in {Base}_{R} \land y \in {Base}_{R} \land z \in {Base}_{R})$
17	12 7	ringass	$⊢ (R \in Ring \land (x \in {Base}_{R} \land y \in {Base}_{R} \land z \in {Base}_{R})) \to (x \cdot_{R} y) \cdot_{R} z = x \cdot_{R} (y \cdot_{R} z)$
18	16 17	sylan2	$⊢ (R \in Ring \land (x \in U \land y \in U \land z \in U)) \to (x \cdot_{R} y) \cdot_{R} z = x \cdot_{R} (y \cdot_{R} z)$
19		eqid	$⊢ 1_{R} = 1_{R}$
20	1 19	1unit	$⊢ R \in Ring \to 1_{R} \in U$
21	12 7 19	ringlidm	$⊢ (R \in Ring \land x \in {Base}_{R}) \to 1_{R} \cdot_{R} x = x$
22	13 21	sylan2	$⊢ (R \in Ring \land x \in U) \to 1_{R} \cdot_{R} x = x$
23		eqid	$⊢ ∥_{r} (R) = ∥_{r} (R)$
24		eqid	$⊢ {opp}_{r} (R) = {opp}_{r} (R)$
25		eqid	$⊢ ∥_{r} ({opp}_{r} (R)) = ∥_{r} ({opp}_{r} (R))$
26	1 19 23 24 25	isunit	$⊢ x \in U \leftrightarrow (x ∥_{r} (R) 1_{R} \land x ∥_{r} ({opp}_{r} (R)) 1_{R})$
27	26	bilani	$⊢ (R \in Ring \land x \in U) \to (x ∥_{r} (R) 1_{R} \land x ∥_{r} ({opp}_{r} (R)) 1_{R})$
28	13	adantl	$⊢ (R \in Ring \land x \in U) \to x \in {Base}_{R}$
29	12 23 7	dvdsr2	$⊢ x \in {Base}_{R} \to (x ∥_{r} (R) 1_{R} \leftrightarrow \exists y \in {Base}_{R} y \cdot_{R} x = 1_{R})$
30	28 29	syl	$⊢ (R \in Ring \land x \in U) \to (x ∥_{r} (R) 1_{R} \leftrightarrow \exists y \in {Base}_{R} y \cdot_{R} x = 1_{R})$
31	24 12	opprbas	$⊢ {Base}_{R} = {Base}_{{opp}_{r} (R)}$
32		eqid	$⊢ \cdot_{{opp}_{r} (R)} = \cdot_{{opp}_{r} (R)}$
33	31 25 32	dvdsr2	$⊢ x \in {Base}_{R} \to (x ∥_{r} ({opp}_{r} (R)) 1_{R} \leftrightarrow \exists m \in {Base}_{R} m \cdot_{{opp}_{r} (R)} x = 1_{R})$
34	28 33	syl	$⊢ (R \in Ring \land x \in U) \to (x ∥_{r} ({opp}_{r} (R)) 1_{R} \leftrightarrow \exists m \in {Base}_{R} m \cdot_{{opp}_{r} (R)} x = 1_{R})$
35	30 34	anbi12d	$⊢ (R \in Ring \land x \in U) \to ((x ∥_{r} (R) 1_{R} \land x ∥_{r} ({opp}_{r} (R)) 1_{R}) \leftrightarrow (\exists y \in {Base}_{R} y \cdot_{R} x = 1_{R} \land \exists m \in {Base}_{R} m \cdot_{{opp}_{r} (R)} x = 1_{R}))$
36		reeanv	$⊢ \exists y \in {Base}_{R} \exists m \in {Base}_{R} (y \cdot_{R} x = 1_{R} \land m \cdot_{{opp}_{r} (R)} x = 1_{R}) \leftrightarrow (\exists y \in {Base}_{R} y \cdot_{R} x = 1_{R} \land \exists m \in {Base}_{R} m \cdot_{{opp}_{r} (R)} x = 1_{R})$
37		simprl	$⊢ (((R \in Ring \land x \in U) \land y \in {Base}_{R}) \land (m \in {Base}_{R} \land (y \cdot_{R} x = 1_{R} \land m \cdot_{{opp}_{r} (R)} x = 1_{R}))) \to m \in {Base}_{R}$
38	28	ad2antrr	$⊢ (((R \in Ring \land x \in U) \land y \in {Base}_{R}) \land (m \in {Base}_{R} \land (y \cdot_{R} x = 1_{R} \land m \cdot_{{opp}_{r} (R)} x = 1_{R}))) \to x \in {Base}_{R}$
39	12 23 7	dvdsrmul	$⊢ (m \in {Base}_{R} \land x \in {Base}_{R}) \to m ∥_{r} (R) (x \cdot_{R} m)$
40	37 38 39	syl2anc	$⊢ (((R \in Ring \land x \in U) \land y \in {Base}_{R}) \land (m \in {Base}_{R} \land (y \cdot_{R} x = 1_{R} \land m \cdot_{{opp}_{r} (R)} x = 1_{R}))) \to m ∥_{r} (R) (x \cdot_{R} m)$
41		simplll	$⊢ (((R \in Ring \land x \in U) \land y \in {Base}_{R}) \land (m \in {Base}_{R} \land (y \cdot_{R} x = 1_{R} \land m \cdot_{{opp}_{r} (R)} x = 1_{R}))) \to R \in Ring$
42		simplr	$⊢ (((R \in Ring \land x \in U) \land y \in {Base}_{R}) \land (m \in {Base}_{R} \land (y \cdot_{R} x = 1_{R} \land m \cdot_{{opp}_{r} (R)} x = 1_{R}))) \to y \in {Base}_{R}$
43	12 7	ringass	$⊢ (R \in Ring \land (y \in {Base}_{R} \land x \in {Base}_{R} \land m \in {Base}_{R})) \to (y \cdot_{R} x) \cdot_{R} m = y \cdot_{R} (x \cdot_{R} m)$
44	41 42 38 37 43	syl13anc	$⊢ (((R \in Ring \land x \in U) \land y \in {Base}_{R}) \land (m \in {Base}_{R} \land (y \cdot_{R} x = 1_{R} \land m \cdot_{{opp}_{r} (R)} x = 1_{R}))) \to (y \cdot_{R} x) \cdot_{R} m = y \cdot_{R} (x \cdot_{R} m)$
45		simprrl	$⊢ (((R \in Ring \land x \in U) \land y \in {Base}_{R}) \land (m \in {Base}_{R} \land (y \cdot_{R} x = 1_{R} \land m \cdot_{{opp}_{r} (R)} x = 1_{R}))) \to y \cdot_{R} x = 1_{R}$
46	45	oveq1d	$⊢ (((R \in Ring \land x \in U) \land y \in {Base}_{R}) \land (m \in {Base}_{R} \land (y \cdot_{R} x = 1_{R} \land m \cdot_{{opp}_{r} (R)} x = 1_{R}))) \to (y \cdot_{R} x) \cdot_{R} m = 1_{R} \cdot_{R} m$
47	12 7 24 32	opprmul	$⊢ m \cdot_{{opp}_{r} (R)} x = x \cdot_{R} m$
48		simprrr	$⊢ (((R \in Ring \land x \in U) \land y \in {Base}_{R}) \land (m \in {Base}_{R} \land (y \cdot_{R} x = 1_{R} \land m \cdot_{{opp}_{r} (R)} x = 1_{R}))) \to m \cdot_{{opp}_{r} (R)} x = 1_{R}$
49	47 48	eqtr3id	$⊢ (((R \in Ring \land x \in U) \land y \in {Base}_{R}) \land (m \in {Base}_{R} \land (y \cdot_{R} x = 1_{R} \land m \cdot_{{opp}_{r} (R)} x = 1_{R}))) \to x \cdot_{R} m = 1_{R}$
50	49	oveq2d	$⊢ (((R \in Ring \land x \in U) \land y \in {Base}_{R}) \land (m \in {Base}_{R} \land (y \cdot_{R} x = 1_{R} \land m \cdot_{{opp}_{r} (R)} x = 1_{R}))) \to y \cdot_{R} (x \cdot_{R} m) = y \cdot_{R} 1_{R}$
51	44 46 50	3eqtr3d	$⊢ (((R \in Ring \land x \in U) \land y \in {Base}_{R}) \land (m \in {Base}_{R} \land (y \cdot_{R} x = 1_{R} \land m \cdot_{{opp}_{r} (R)} x = 1_{R}))) \to 1_{R} \cdot_{R} m = y \cdot_{R} 1_{R}$
52	12 7 19	ringlidm	$⊢ (R \in Ring \land m \in {Base}_{R}) \to 1_{R} \cdot_{R} m = m$
53	41 37 52	syl2anc	$⊢ (((R \in Ring \land x \in U) \land y \in {Base}_{R}) \land (m \in {Base}_{R} \land (y \cdot_{R} x = 1_{R} \land m \cdot_{{opp}_{r} (R)} x = 1_{R}))) \to 1_{R} \cdot_{R} m = m$
54	12 7 19	ringridm	$⊢ (R \in Ring \land y \in {Base}_{R}) \to y \cdot_{R} 1_{R} = y$
55	41 42 54	syl2anc	$⊢ (((R \in Ring \land x \in U) \land y \in {Base}_{R}) \land (m \in {Base}_{R} \land (y \cdot_{R} x = 1_{R} \land m \cdot_{{opp}_{r} (R)} x = 1_{R}))) \to y \cdot_{R} 1_{R} = y$
56	51 53 55	3eqtr3d	$⊢ (((R \in Ring \land x \in U) \land y \in {Base}_{R}) \land (m \in {Base}_{R} \land (y \cdot_{R} x = 1_{R} \land m \cdot_{{opp}_{r} (R)} x = 1_{R}))) \to m = y$
57	40 56 49	3brtr3d	$⊢ (((R \in Ring \land x \in U) \land y \in {Base}_{R}) \land (m \in {Base}_{R} \land (y \cdot_{R} x = 1_{R} \land m \cdot_{{opp}_{r} (R)} x = 1_{R}))) \to y ∥_{r} (R) 1_{R}$
58	31 25 32	dvdsrmul	$⊢ (y \in {Base}_{R} \land x \in {Base}_{R}) \to y ∥_{r} ({opp}_{r} (R)) (x \cdot_{{opp}_{r} (R)} y)$
59	42 38 58	syl2anc	$⊢ (((R \in Ring \land x \in U) \land y \in {Base}_{R}) \land (m \in {Base}_{R} \land (y \cdot_{R} x = 1_{R} \land m \cdot_{{opp}_{r} (R)} x = 1_{R}))) \to y ∥_{r} ({opp}_{r} (R)) (x \cdot_{{opp}_{r} (R)} y)$
60	12 7 24 32	opprmul	$⊢ x \cdot_{{opp}_{r} (R)} y = y \cdot_{R} x$
61	60 45	eqtrid	$⊢ (((R \in Ring \land x \in U) \land y \in {Base}_{R}) \land (m \in {Base}_{R} \land (y \cdot_{R} x = 1_{R} \land m \cdot_{{opp}_{r} (R)} x = 1_{R}))) \to x \cdot_{{opp}_{r} (R)} y = 1_{R}$
62	59 61	breqtrd	$⊢ (((R \in Ring \land x \in U) \land y \in {Base}_{R}) \land (m \in {Base}_{R} \land (y \cdot_{R} x = 1_{R} \land m \cdot_{{opp}_{r} (R)} x = 1_{R}))) \to y ∥_{r} ({opp}_{r} (R)) 1_{R}$
63	1 19 23 24 25	isunit	$⊢ y \in U \leftrightarrow (y ∥_{r} (R) 1_{R} \land y ∥_{r} ({opp}_{r} (R)) 1_{R})$
64	57 62 63	sylanbrc	$⊢ (((R \in Ring \land x \in U) \land y \in {Base}_{R}) \land (m \in {Base}_{R} \land (y \cdot_{R} x = 1_{R} \land m \cdot_{{opp}_{r} (R)} x = 1_{R}))) \to y \in U$
65	64 45	jca	$⊢ (((R \in Ring \land x \in U) \land y \in {Base}_{R}) \land (m \in {Base}_{R} \land (y \cdot_{R} x = 1_{R} \land m \cdot_{{opp}_{r} (R)} x = 1_{R}))) \to (y \in U \land y \cdot_{R} x = 1_{R})$
66	65	rexlimdvaa	$⊢ ((R \in Ring \land x \in U) \land y \in {Base}_{R}) \to (\exists m \in {Base}_{R} (y \cdot_{R} x = 1_{R} \land m \cdot_{{opp}_{r} (R)} x = 1_{R}) \to (y \in U \land y \cdot_{R} x = 1_{R}))$
67	66	expimpd	$⊢ (R \in Ring \land x \in U) \to ((y \in {Base}_{R} \land \exists m \in {Base}_{R} (y \cdot_{R} x = 1_{R} \land m \cdot_{{opp}_{r} (R)} x = 1_{R})) \to (y \in U \land y \cdot_{R} x = 1_{R}))$
68	67	reximdv2	$⊢ (R \in Ring \land x \in U) \to (\exists y \in {Base}_{R} \exists m \in {Base}_{R} (y \cdot_{R} x = 1_{R} \land m \cdot_{{opp}_{r} (R)} x = 1_{R}) \to \exists y \in U y \cdot_{R} x = 1_{R})$
69	36 68	biimtrrid	$⊢ (R \in Ring \land x \in U) \to ((\exists y \in {Base}_{R} y \cdot_{R} x = 1_{R} \land \exists m \in {Base}_{R} m \cdot_{{opp}_{r} (R)} x = 1_{R}) \to \exists y \in U y \cdot_{R} x = 1_{R})$
70	35 69	sylbid	$⊢ (R \in Ring \land x \in U) \to ((x ∥_{r} (R) 1_{R} \land x ∥_{r} ({opp}_{r} (R)) 1_{R}) \to \exists y \in U y \cdot_{R} x = 1_{R})$
71	27 70	mpd	$⊢ (R \in Ring \land x \in U) \to \exists y \in U y \cdot_{R} x = 1_{R}$
72	4 10 11 18 20 22 71	isgrpde	$⊢ R \in Ring \to G \in Grp$

Metamath Proof Explorer

Theorem unitgrp

Proof