unitgrp - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > unitgrp		Structured version Visualization version GIF version

Theorem unitgrp 20275

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

**Hypotheses**
Ref	Expression
unitmulcl.1	⊢ 𝑈 = (Unit‘𝑅)
unitgrp.2	⊢ 𝐺 = ((mulGrp‘𝑅) ↾_s 𝑈)

**Assertion**
Ref	Expression
unitgrp	⊢ (𝑅 ∈ Ring → 𝐺 ∈ Grp)

Proof of Theorem unitgrp Dummy variables 𝑥 𝑦 𝑧 𝑚 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		unitmulcl.1	. . . 4 ⊢ 𝑈 = (Unit‘𝑅)
2		unitgrp.2	. . . 4 ⊢ 𝐺 = ((mulGrp‘𝑅) ↾_s 𝑈)
3	1, 2	unitgrpbas 20274	. . 3 ⊢ 𝑈 = (Base‘𝐺)
4	3	a1i 11	. 2 ⊢ (𝑅 ∈ Ring → 𝑈 = (Base‘𝐺))
5	1	fvexi 6905	. . 3 ⊢ 𝑈 ∈ V
6		eqid 2731	. . . . 5 ⊢ (mulGrp‘𝑅) = (mulGrp‘𝑅)
7		eqid 2731	. . . . 5 ⊢ (._r‘𝑅) = (._r‘𝑅)
8	6, 7	mgpplusg 20033	. . . 4 ⊢ (._r‘𝑅) = (+_g‘(mulGrp‘𝑅))
9	2, 8	ressplusg 17240	. . 3 ⊢ (𝑈 ∈ V → (._r‘𝑅) = (+_g‘𝐺))
10	5, 9	mp1i 13	. 2 ⊢ (𝑅 ∈ Ring → (._r‘𝑅) = (+_g‘𝐺))
11	1, 7	unitmulcl 20272	. 2 ⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈) → (𝑥(._r‘𝑅)𝑦) ∈ 𝑈)
12		eqid 2731	. . . . 5 ⊢ (Base‘𝑅) = (Base‘𝑅)
13	12, 1	unitcl 20267	. . . 4 ⊢ (𝑥 ∈ 𝑈 → 𝑥 ∈ (Base‘𝑅))
14	12, 1	unitcl 20267	. . . 4 ⊢ (𝑦 ∈ 𝑈 → 𝑦 ∈ (Base‘𝑅))
15	12, 1	unitcl 20267	. . . 4 ⊢ (𝑧 ∈ 𝑈 → 𝑧 ∈ (Base‘𝑅))
16	13, 14, 15	3anim123i 1150	. . 3 ⊢ ((𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈) → (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅) ∧ 𝑧 ∈ (Base‘𝑅)))
17	12, 7	ringass 20148	. . 3 ⊢ ((𝑅 ∈ Ring ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅) ∧ 𝑧 ∈ (Base‘𝑅))) → ((𝑥(._r‘𝑅)𝑦)(._r‘𝑅)𝑧) = (𝑥(._r‘𝑅)(𝑦(._r‘𝑅)𝑧)))
18	16, 17	sylan2 592	. 2 ⊢ ((𝑅 ∈ Ring ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈)) → ((𝑥(._r‘𝑅)𝑦)(._r‘𝑅)𝑧) = (𝑥(._r‘𝑅)(𝑦(._r‘𝑅)𝑧)))
19		eqid 2731	. . 3 ⊢ (1_r‘𝑅) = (1_r‘𝑅)
20	1, 19	1unit 20266	. 2 ⊢ (𝑅 ∈ Ring → (1_r‘𝑅) ∈ 𝑈)
21	12, 7, 19	ringlidm 20158	. . 3 ⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ (Base‘𝑅)) → ((1_r‘𝑅)(._r‘𝑅)𝑥) = 𝑥)
22	13, 21	sylan2 592	. 2 ⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) → ((1_r‘𝑅)(._r‘𝑅)𝑥) = 𝑥)
23		simpr 484	. . . 4 ⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) → 𝑥 ∈ 𝑈)
24		eqid 2731	. . . . 5 ⊢ (∥_r‘𝑅) = (∥_r‘𝑅)
25		eqid 2731	. . . . 5 ⊢ (opp_r‘𝑅) = (opp_r‘𝑅)
26		eqid 2731	. . . . 5 ⊢ (∥_r‘(opp_r‘𝑅)) = (∥_r‘(opp_r‘𝑅))
27	1, 19, 24, 25, 26	isunit 20265	. . . 4 ⊢ (𝑥 ∈ 𝑈 ↔ (𝑥(∥_r‘𝑅)(1_r‘𝑅) ∧ 𝑥(∥_r‘(opp_r‘𝑅))(1_r‘𝑅)))
28	23, 27	sylib 217	. . 3 ⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) → (𝑥(∥_r‘𝑅)(1_r‘𝑅) ∧ 𝑥(∥_r‘(opp_r‘𝑅))(1_r‘𝑅)))
29	13	adantl 481	. . . . . 6 ⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) → 𝑥 ∈ (Base‘𝑅))
30	12, 24, 7	dvdsr2 20255	. . . . . 6 ⊢ (𝑥 ∈ (Base‘𝑅) → (𝑥(∥_r‘𝑅)(1_r‘𝑅) ↔ ∃𝑦 ∈ (Base‘𝑅)(𝑦(._r‘𝑅)𝑥) = (1_r‘𝑅)))
31	29, 30	syl 17	. . . . 5 ⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) → (𝑥(∥_r‘𝑅)(1_r‘𝑅) ↔ ∃𝑦 ∈ (Base‘𝑅)(𝑦(._r‘𝑅)𝑥) = (1_r‘𝑅)))
32	25, 12	opprbas 20233	. . . . . . 7 ⊢ (Base‘𝑅) = (Base‘(opp_r‘𝑅))
33		eqid 2731	. . . . . . 7 ⊢ (._r‘(opp_r‘𝑅)) = (._r‘(opp_r‘𝑅))
34	32, 26, 33	dvdsr2 20255	. . . . . 6 ⊢ (𝑥 ∈ (Base‘𝑅) → (𝑥(∥_r‘(opp_r‘𝑅))(1_r‘𝑅) ↔ ∃𝑚 ∈ (Base‘𝑅)(𝑚(._r‘(opp_r‘𝑅))𝑥) = (1_r‘𝑅)))
35	29, 34	syl 17	. . . . 5 ⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) → (𝑥(∥_r‘(opp_r‘𝑅))(1_r‘𝑅) ↔ ∃𝑚 ∈ (Base‘𝑅)(𝑚(._r‘(opp_r‘𝑅))𝑥) = (1_r‘𝑅)))
36	31, 35	anbi12d 630	. . . 4 ⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) → ((𝑥(∥_r‘𝑅)(1_r‘𝑅) ∧ 𝑥(∥_r‘(opp_r‘𝑅))(1_r‘𝑅)) ↔ (∃𝑦 ∈ (Base‘𝑅)(𝑦(._r‘𝑅)𝑥) = (1_r‘𝑅) ∧ ∃𝑚 ∈ (Base‘𝑅)(𝑚(._r‘(opp_r‘𝑅))𝑥) = (1_r‘𝑅))))
37		reeanv 3225	. . . . 5 ⊢ (∃𝑦 ∈ (Base‘𝑅)∃𝑚 ∈ (Base‘𝑅)((𝑦(._r‘𝑅)𝑥) = (1_r‘𝑅) ∧ (𝑚(._r‘(opp_r‘𝑅))𝑥) = (1_r‘𝑅)) ↔ (∃𝑦 ∈ (Base‘𝑅)(𝑦(._r‘𝑅)𝑥) = (1_r‘𝑅) ∧ ∃𝑚 ∈ (Base‘𝑅)(𝑚(._r‘(opp_r‘𝑅))𝑥) = (1_r‘𝑅)))
38		simprl 768	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑚 ∈ (Base‘𝑅) ∧ ((𝑦(._r‘𝑅)𝑥) = (1_r‘𝑅) ∧ (𝑚(._r‘(opp_r‘𝑅))𝑥) = (1_r‘𝑅)))) → 𝑚 ∈ (Base‘𝑅))
39	29	ad2antrr 723	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑚 ∈ (Base‘𝑅) ∧ ((𝑦(._r‘𝑅)𝑥) = (1_r‘𝑅) ∧ (𝑚(._r‘(opp_r‘𝑅))𝑥) = (1_r‘𝑅)))) → 𝑥 ∈ (Base‘𝑅))
40	12, 24, 7	dvdsrmul 20256	. . . . . . . . . . . 12 ⊢ ((𝑚 ∈ (Base‘𝑅) ∧ 𝑥 ∈ (Base‘𝑅)) → 𝑚(∥_r‘𝑅)(𝑥(._r‘𝑅)𝑚))
41	38, 39, 40	syl2anc 583	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑚 ∈ (Base‘𝑅) ∧ ((𝑦(._r‘𝑅)𝑥) = (1_r‘𝑅) ∧ (𝑚(._r‘(opp_r‘𝑅))𝑥) = (1_r‘𝑅)))) → 𝑚(∥_r‘𝑅)(𝑥(._r‘𝑅)𝑚))
42		simplll 772	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑚 ∈ (Base‘𝑅) ∧ ((𝑦(._r‘𝑅)𝑥) = (1_r‘𝑅) ∧ (𝑚(._r‘(opp_r‘𝑅))𝑥) = (1_r‘𝑅)))) → 𝑅 ∈ Ring)
43		simplr 766	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑚 ∈ (Base‘𝑅) ∧ ((𝑦(._r‘𝑅)𝑥) = (1_r‘𝑅) ∧ (𝑚(._r‘(opp_r‘𝑅))𝑥) = (1_r‘𝑅)))) → 𝑦 ∈ (Base‘𝑅))
44	12, 7	ringass 20148	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ Ring ∧ (𝑦 ∈ (Base‘𝑅) ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑚 ∈ (Base‘𝑅))) → ((𝑦(._r‘𝑅)𝑥)(._r‘𝑅)𝑚) = (𝑦(._r‘𝑅)(𝑥(._r‘𝑅)𝑚)))
45	42, 43, 39, 38, 44	syl13anc 1371	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑚 ∈ (Base‘𝑅) ∧ ((𝑦(._r‘𝑅)𝑥) = (1_r‘𝑅) ∧ (𝑚(._r‘(opp_r‘𝑅))𝑥) = (1_r‘𝑅)))) → ((𝑦(._r‘𝑅)𝑥)(._r‘𝑅)𝑚) = (𝑦(._r‘𝑅)(𝑥(._r‘𝑅)𝑚)))
46		simprrl 778	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑚 ∈ (Base‘𝑅) ∧ ((𝑦(._r‘𝑅)𝑥) = (1_r‘𝑅) ∧ (𝑚(._r‘(opp_r‘𝑅))𝑥) = (1_r‘𝑅)))) → (𝑦(._r‘𝑅)𝑥) = (1_r‘𝑅))
47	46	oveq1d 7427	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑚 ∈ (Base‘𝑅) ∧ ((𝑦(._r‘𝑅)𝑥) = (1_r‘𝑅) ∧ (𝑚(._r‘(opp_r‘𝑅))𝑥) = (1_r‘𝑅)))) → ((𝑦(._r‘𝑅)𝑥)(._r‘𝑅)𝑚) = ((1_r‘𝑅)(._r‘𝑅)𝑚))
48	12, 7, 25, 33	opprmul 20229	. . . . . . . . . . . . . . 15 ⊢ (𝑚(._r‘(opp_r‘𝑅))𝑥) = (𝑥(._r‘𝑅)𝑚)
49		simprrr 779	. . . . . . . . . . . . . . 15 ⊢ ((((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑚 ∈ (Base‘𝑅) ∧ ((𝑦(._r‘𝑅)𝑥) = (1_r‘𝑅) ∧ (𝑚(._r‘(opp_r‘𝑅))𝑥) = (1_r‘𝑅)))) → (𝑚(._r‘(opp_r‘𝑅))𝑥) = (1_r‘𝑅))
50	48, 49	eqtr3id 2785	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑚 ∈ (Base‘𝑅) ∧ ((𝑦(._r‘𝑅)𝑥) = (1_r‘𝑅) ∧ (𝑚(._r‘(opp_r‘𝑅))𝑥) = (1_r‘𝑅)))) → (𝑥(._r‘𝑅)𝑚) = (1_r‘𝑅))
51	50	oveq2d 7428	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑚 ∈ (Base‘𝑅) ∧ ((𝑦(._r‘𝑅)𝑥) = (1_r‘𝑅) ∧ (𝑚(._r‘(opp_r‘𝑅))𝑥) = (1_r‘𝑅)))) → (𝑦(._r‘𝑅)(𝑥(._r‘𝑅)𝑚)) = (𝑦(._r‘𝑅)(1_r‘𝑅)))
52	45, 47, 51	3eqtr3d 2779	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑚 ∈ (Base‘𝑅) ∧ ((𝑦(._r‘𝑅)𝑥) = (1_r‘𝑅) ∧ (𝑚(._r‘(opp_r‘𝑅))𝑥) = (1_r‘𝑅)))) → ((1_r‘𝑅)(._r‘𝑅)𝑚) = (𝑦(._r‘𝑅)(1_r‘𝑅)))
53	12, 7, 19	ringlidm 20158	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ Ring ∧ 𝑚 ∈ (Base‘𝑅)) → ((1_r‘𝑅)(._r‘𝑅)𝑚) = 𝑚)
54	42, 38, 53	syl2anc 583	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑚 ∈ (Base‘𝑅) ∧ ((𝑦(._r‘𝑅)𝑥) = (1_r‘𝑅) ∧ (𝑚(._r‘(opp_r‘𝑅))𝑥) = (1_r‘𝑅)))) → ((1_r‘𝑅)(._r‘𝑅)𝑚) = 𝑚)
55	12, 7, 19	ringridm 20159	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ Ring ∧ 𝑦 ∈ (Base‘𝑅)) → (𝑦(._r‘𝑅)(1_r‘𝑅)) = 𝑦)
56	42, 43, 55	syl2anc 583	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑚 ∈ (Base‘𝑅) ∧ ((𝑦(._r‘𝑅)𝑥) = (1_r‘𝑅) ∧ (𝑚(._r‘(opp_r‘𝑅))𝑥) = (1_r‘𝑅)))) → (𝑦(._r‘𝑅)(1_r‘𝑅)) = 𝑦)
57	52, 54, 56	3eqtr3d 2779	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑚 ∈ (Base‘𝑅) ∧ ((𝑦(._r‘𝑅)𝑥) = (1_r‘𝑅) ∧ (𝑚(._r‘(opp_r‘𝑅))𝑥) = (1_r‘𝑅)))) → 𝑚 = 𝑦)
58	41, 57, 50	3brtr3d 5179	. . . . . . . . . 10 ⊢ ((((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑚 ∈ (Base‘𝑅) ∧ ((𝑦(._r‘𝑅)𝑥) = (1_r‘𝑅) ∧ (𝑚(._r‘(opp_r‘𝑅))𝑥) = (1_r‘𝑅)))) → 𝑦(∥_r‘𝑅)(1_r‘𝑅))
59	32, 26, 33	dvdsrmul 20256	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ (Base‘𝑅) ∧ 𝑥 ∈ (Base‘𝑅)) → 𝑦(∥_r‘(opp_r‘𝑅))(𝑥(._r‘(opp_r‘𝑅))𝑦))
60	43, 39, 59	syl2anc 583	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑚 ∈ (Base‘𝑅) ∧ ((𝑦(._r‘𝑅)𝑥) = (1_r‘𝑅) ∧ (𝑚(._r‘(opp_r‘𝑅))𝑥) = (1_r‘𝑅)))) → 𝑦(∥_r‘(opp_r‘𝑅))(𝑥(._r‘(opp_r‘𝑅))𝑦))
61	12, 7, 25, 33	opprmul 20229	. . . . . . . . . . . 12 ⊢ (𝑥(._r‘(opp_r‘𝑅))𝑦) = (𝑦(._r‘𝑅)𝑥)
62	61, 46	eqtrid 2783	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑚 ∈ (Base‘𝑅) ∧ ((𝑦(._r‘𝑅)𝑥) = (1_r‘𝑅) ∧ (𝑚(._r‘(opp_r‘𝑅))𝑥) = (1_r‘𝑅)))) → (𝑥(._r‘(opp_r‘𝑅))𝑦) = (1_r‘𝑅))
63	60, 62	breqtrd 5174	. . . . . . . . . 10 ⊢ ((((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑚 ∈ (Base‘𝑅) ∧ ((𝑦(._r‘𝑅)𝑥) = (1_r‘𝑅) ∧ (𝑚(._r‘(opp_r‘𝑅))𝑥) = (1_r‘𝑅)))) → 𝑦(∥_r‘(opp_r‘𝑅))(1_r‘𝑅))
64	1, 19, 24, 25, 26	isunit 20265	. . . . . . . . . 10 ⊢ (𝑦 ∈ 𝑈 ↔ (𝑦(∥_r‘𝑅)(1_r‘𝑅) ∧ 𝑦(∥_r‘(opp_r‘𝑅))(1_r‘𝑅)))
65	58, 63, 64	sylanbrc 582	. . . . . . . . 9 ⊢ ((((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑚 ∈ (Base‘𝑅) ∧ ((𝑦(._r‘𝑅)𝑥) = (1_r‘𝑅) ∧ (𝑚(._r‘(opp_r‘𝑅))𝑥) = (1_r‘𝑅)))) → 𝑦 ∈ 𝑈)
66	65, 46	jca 511	. . . . . . . 8 ⊢ ((((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑚 ∈ (Base‘𝑅) ∧ ((𝑦(._r‘𝑅)𝑥) = (1_r‘𝑅) ∧ (𝑚(._r‘(opp_r‘𝑅))𝑥) = (1_r‘𝑅)))) → (𝑦 ∈ 𝑈 ∧ (𝑦(._r‘𝑅)𝑥) = (1_r‘𝑅)))
67	66	rexlimdvaa 3155	. . . . . . 7 ⊢ (((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ (Base‘𝑅)) → (∃𝑚 ∈ (Base‘𝑅)((𝑦(._r‘𝑅)𝑥) = (1_r‘𝑅) ∧ (𝑚(._r‘(opp_r‘𝑅))𝑥) = (1_r‘𝑅)) → (𝑦 ∈ 𝑈 ∧ (𝑦(._r‘𝑅)𝑥) = (1_r‘𝑅))))
68	67	expimpd 453	. . . . . 6 ⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) → ((𝑦 ∈ (Base‘𝑅) ∧ ∃𝑚 ∈ (Base‘𝑅)((𝑦(._r‘𝑅)𝑥) = (1_r‘𝑅) ∧ (𝑚(._r‘(opp_r‘𝑅))𝑥) = (1_r‘𝑅))) → (𝑦 ∈ 𝑈 ∧ (𝑦(._r‘𝑅)𝑥) = (1_r‘𝑅))))
69	68	reximdv2 3163	. . . . 5 ⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) → (∃𝑦 ∈ (Base‘𝑅)∃𝑚 ∈ (Base‘𝑅)((𝑦(._r‘𝑅)𝑥) = (1_r‘𝑅) ∧ (𝑚(._r‘(opp_r‘𝑅))𝑥) = (1_r‘𝑅)) → ∃𝑦 ∈ 𝑈 (𝑦(._r‘𝑅)𝑥) = (1_r‘𝑅)))
70	37, 69	biimtrrid 242	. . . 4 ⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) → ((∃𝑦 ∈ (Base‘𝑅)(𝑦(._r‘𝑅)𝑥) = (1_r‘𝑅) ∧ ∃𝑚 ∈ (Base‘𝑅)(𝑚(._r‘(opp_r‘𝑅))𝑥) = (1_r‘𝑅)) → ∃𝑦 ∈ 𝑈 (𝑦(._r‘𝑅)𝑥) = (1_r‘𝑅)))
71	36, 70	sylbid 239	. . 3 ⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) → ((𝑥(∥_r‘𝑅)(1_r‘𝑅) ∧ 𝑥(∥_r‘(opp_r‘𝑅))(1_r‘𝑅)) → ∃𝑦 ∈ 𝑈 (𝑦(._r‘𝑅)𝑥) = (1_r‘𝑅)))
72	28, 71	mpd 15	. 2 ⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈) → ∃𝑦 ∈ 𝑈 (𝑦(._r‘𝑅)𝑥) = (1_r‘𝑅))
73	4, 10, 11, 18, 20, 22, 72	isgrpde 18880	1 ⊢ (𝑅 ∈ Ring → 𝐺 ∈ Grp)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 395 ∧ w3a 1086 = wceq 1540 ∈ wcel 2105 ∃wrex 3069 Vcvv 3473 class class class wbr 5148 ‘cfv 6543 (class class class)co 7412 Basecbs 17149 ↾_s cress 17178 +_gcplusg 17202 ._rcmulr 17203 Grpcgrp 18856 mulGrpcmgp 20029 1_rcur 20076 Ringcrg 20128 opp_rcoppr 20225 ∥_rcdsr 20246 Unitcui 20247

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2153 ax-12 2170 ax-ext 2702 ax-rep 5285 ax-sep 5299 ax-nul 5306 ax-pow 5363 ax-pr 5427 ax-un 7728 ax-cnex 11169 ax-resscn 11170 ax-1cn 11171 ax-icn 11172 ax-addcl 11173 ax-addrcl 11174 ax-mulcl 11175 ax-mulrcl 11176 ax-mulcom 11177 ax-addass 11178 ax-mulass 11179 ax-distr 11180 ax-i2m1 11181 ax-1ne0 11182 ax-1rid 11183 ax-rnegex 11184 ax-rrecex 11185 ax-cnre 11186 ax-pre-lttri 11187 ax-pre-lttrn 11188 ax-pre-ltadd 11189 ax-pre-mulgt0 11190

This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1781 df-nf 1785 df-sb 2067 df-mo 2533 df-eu 2562 df-clab 2709 df-cleq 2723 df-clel 2809 df-nfc 2884 df-ne 2940 df-nel 3046 df-ral 3061 df-rex 3070 df-rmo 3375 df-reu 3376 df-rab 3432 df-v 3475 df-sbc 3778 df-csb 3894 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-pss 3967 df-nul 4323 df-if 4529 df-pw 4604 df-sn 4629 df-pr 4631 df-op 4635 df-uni 4909 df-iun 4999 df-br 5149 df-opab 5211 df-mpt 5232 df-tr 5266 df-id 5574 df-eprel 5580 df-po 5588 df-so 5589 df-fr 5631 df-we 5633 df-xp 5682 df-rel 5683 df-cnv 5684 df-co 5685 df-dm 5686 df-rn 5687 df-res 5688 df-ima 5689 df-pred 6300 df-ord 6367 df-on 6368 df-lim 6369 df-suc 6370 df-iota 6495 df-fun 6545 df-fn 6546 df-f 6547 df-f1 6548 df-fo 6549 df-f1o 6550 df-fv 6551 df-riota 7368 df-ov 7415 df-oprab 7416 df-mpo 7417 df-om 7859 df-2nd 7979 df-tpos 8214 df-frecs 8269 df-wrecs 8300 df-recs 8374 df-rdg 8413 df-er 8706 df-en 8943 df-dom 8944 df-sdom 8945 df-pnf 11255 df-mnf 11256 df-xr 11257 df-ltxr 11258 df-le 11259 df-sub 11451 df-neg 11452 df-nn 12218 df-2 12280 df-3 12281 df-sets 17102 df-slot 17120 df-ndx 17132 df-base 17150 df-ress 17179 df-plusg 17215 df-mulr 17216 df-0g 17392 df-mgm 18566 df-sgrp 18645 df-mnd 18661 df-grp 18859 df-minusg 18860 df-cmn 19692 df-abl 19693 df-mgp 20030 df-rng 20048 df-ur 20077 df-ring 20130 df-oppr 20226 df-dvdsr 20249 df-unit 20250

This theorem is referenced by: unitabl 20276 unitsubm 20278 unitinvcl 20282 unitinvinv 20283 unitlinv 20285 unitrinv 20286 rdivmuldivd 20305 rhmunitinv 20403 subrgugrp 20482 isdrng2 20515 expghm 21247 invrvald 22399 nrginvrcn 24430 nrgtdrg 24431 dchrfi 26995 dchrghm 26996 dchrabs 27000 dchrptlem1 27004 dchrptlem2 27005 dchrptlem3 27006 dchrsum2 27008 dvrcan5 32656 idomodle 42241 proot1mul 42244 proot1hash 42245 proot1ex 42246

W3C validator