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		simpr	$⊢ (R \in Ring \land x \in U) \to x \in U$
24		eqid	$⊢ ∥_{r} (R) = ∥_{r} (R)$
25		eqid	$⊢ {opp}_{r} (R) = {opp}_{r} (R)$
26		eqid	$⊢ ∥_{r} ({opp}_{r} (R)) = ∥_{r} ({opp}_{r} (R))$
27	1 19 24 25 26	isunit	$⊢ x \in U \leftrightarrow (x ∥_{r} (R) 1_{R} \land x ∥_{r} ({opp}_{r} (R)) 1_{R})$
28	23 27	sylib	$⊢ (R \in Ring \land x \in U) \to (x ∥_{r} (R) 1_{R} \land x ∥_{r} ({opp}_{r} (R)) 1_{R})$
29	13	adantl	$⊢ (R \in Ring \land x \in U) \to x \in {Base}_{R}$
30	12 24 7	dvdsr2	$⊢ x \in {Base}_{R} \to (x ∥_{r} (R) 1_{R} \leftrightarrow \exists y \in {Base}_{R} y \cdot_{R} x = 1_{R})$
31	29 30	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})$
32	25 12	opprbas	$⊢ {Base}_{R} = {Base}_{{opp}_{r} (R)}$
33		eqid	$⊢ \cdot_{{opp}_{r} (R)} = \cdot_{{opp}_{r} (R)}$
34	32 26 33	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})$
35	29 34	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})$
36	31 35	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}))$
37		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})$
38		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}$
39	29	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}$
40	12 24 7	dvdsrmul	$⊢ (m \in {Base}_{R} \land x \in {Base}_{R}) \to m ∥_{r} (R) (x \cdot_{R} m)$
41	38 39 40	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)$
42		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$
43		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}$
44	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)$
45	42 43 39 38 44	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)$
46		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}$
47	46	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$
48	12 7 25 33	opprmul	$⊢ m \cdot_{{opp}_{r} (R)} x = x \cdot_{R} m$
49		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}$
50	48 49	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}$
51	50	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}$
52	45 47 51	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}$
53	12 7 19	ringlidm	$⊢ (R \in Ring \land m \in {Base}_{R}) \to 1_{R} \cdot_{R} m = m$
54	42 38 53	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$
55	12 7 19	ringridm	$⊢ (R \in Ring \land y \in {Base}_{R}) \to y \cdot_{R} 1_{R} = y$
56	42 43 55	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$
57	52 54 56	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$
58	41 57 50	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}$
59	32 26 33	dvdsrmul	$⊢ (y \in {Base}_{R} \land x \in {Base}_{R}) \to y ∥_{r} ({opp}_{r} (R)) (x \cdot_{{opp}_{r} (R)} y)$
60	43 39 59	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)$
61	12 7 25 33	opprmul	$⊢ x \cdot_{{opp}_{r} (R)} y = y \cdot_{R} x$
62	61 46	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}$
63	60 62	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}$
64	1 19 24 25 26	isunit	$⊢ y \in U \leftrightarrow (y ∥_{r} (R) 1_{R} \land y ∥_{r} ({opp}_{r} (R)) 1_{R})$
65	58 63 64	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$
66	65 46	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})$
67	66	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}))$
68	67	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}))$
69	68	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})$
70	37 69	syl5bir	$⊢ (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})$
71	36 70	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})$
72	28 71	mpd	$⊢ (R \in Ring \land x \in U) \to \exists y \in U y \cdot_{R} x = 1_{R}$
73	4 10 11 18 20 22 72	isgrpde	$⊢ R \in Ring \to G \in Grp$

Metamath Proof Explorer

Theorem unitgrp

Proof