Metamath Proof Explorer

Theorem unitgrp

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

Ref Expression
Hypotheses unitmulcl.1 ⊢ 𝑈 = ( Unit ‘ 𝑅 )
unitgrp.2 ⊢ 𝐺 = ( ( mulGrp ‘ 𝑅 ) ↾s 𝑈 )
Assertion unitgrp ( 𝑅 ∈ Ring → 𝐺 ∈ Grp )

Proof

Step Hyp Ref Expression
1 unitmulcl.1 ⊢ 𝑈 = ( Unit ‘ 𝑅 )
2 unitgrp.2 ⊢ 𝐺 = ( ( mulGrp ‘ 𝑅 ) ↾s 𝑈 )
3 1 2 unitgrpbas ⊢ 𝑈 = ( Base ‘ 𝐺 )
4 3 a1i ⊢ ( 𝑅 ∈ Ring → 𝑈 = ( Base ‘ 𝐺 ) )
5 1 fvexi ⊢ 𝑈 ∈ V
6 eqid ⊢ ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
7 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
8 6 7 mgpplusg ⊢ ( .r ‘ 𝑅 ) = ( +g ‘ ( mulGrp ‘ 𝑅 ) )
9 2 8 ressplusg ⊢ ( 𝑈 ∈ V → ( .r ‘ 𝑅 ) = ( +g ‘ 𝐺 ) )
10 5 9 mp1i ⊢ ( 𝑅 ∈ Ring → ( .r ‘ 𝑅 ) = ( +g ‘ 𝐺 ) )
11 1 7 unitmulcl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ 𝑈 )
12 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
13 12 1 unitcl ⊢ ( 𝑥 ∈ 𝑈 → 𝑥 ∈ ( Base ‘ 𝑅 ) )
14 12 1 unitcl ⊢ ( 𝑦 ∈ 𝑈 → 𝑦 ∈ ( Base ‘ 𝑅 ) )
15 12 1 unitcl ⊢ ( 𝑧 ∈ 𝑈 → 𝑧 ∈ ( Base ‘ 𝑅 ) )
16 13 14 15 3anim123i ⊢ ( ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈 ) → ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) )
17 12 7 ringass ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) ) → ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ( .r ‘ 𝑅 ) 𝑧 ) = ( 𝑥 ( .r ‘ 𝑅 ) ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) ) )
18 16 17 sylan2 ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈 ) ) → ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ( .r ‘ 𝑅 ) 𝑧 ) = ( 𝑥 ( .r ‘ 𝑅 ) ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) ) )
19 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
20 1 19 1unit ⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) ∈ 𝑈 )
21 12 7 19 ringlidm ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) → ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) 𝑥 ) = 𝑥 )
22 13 21 sylan2 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈 ) → ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) 𝑥 ) = 𝑥 )
23 eqid ⊢ ( ∥r ‘ 𝑅 ) = ( ∥r ‘ 𝑅 )
24 eqid ⊢ ( oppr ‘ 𝑅 ) = ( oppr ‘ 𝑅 )
25 eqid ⊢ ( ∥r ‘ ( oppr ‘ 𝑅 ) ) = ( ∥r ‘ ( oppr ‘ 𝑅 ) )
26 1 19 23 24 25 isunit ⊢ ( 𝑥 ∈ 𝑈 ↔ ( 𝑥 ( ∥r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ∧ 𝑥 ( ∥r ‘ ( oppr ‘ 𝑅 ) ) ( 1r ‘ 𝑅 ) ) )
27 26 bilani ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈 ) → ( 𝑥 ( ∥r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ∧ 𝑥 ( ∥r ‘ ( oppr ‘ 𝑅 ) ) ( 1r ‘ 𝑅 ) ) )
28 13 adantl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈 ) → 𝑥 ∈ ( Base ‘ 𝑅 ) )
29 12 23 7 dvdsr2 ⊢ ( 𝑥 ∈ ( Base ‘ 𝑅 ) → ( 𝑥 ( ∥r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ↔ ∃ 𝑦 ∈ ( Base ‘ 𝑅 ) ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = ( 1r ‘ 𝑅 ) ) )
30 28 29 syl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈 ) → ( 𝑥 ( ∥r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ↔ ∃ 𝑦 ∈ ( Base ‘ 𝑅 ) ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = ( 1r ‘ 𝑅 ) ) )
31 24 12 opprbas ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ ( oppr ‘ 𝑅 ) )
32 eqid ⊢ ( .r ‘ ( oppr ‘ 𝑅 ) ) = ( .r ‘ ( oppr ‘ 𝑅 ) )
33 31 25 32 dvdsr2 ⊢ ( 𝑥 ∈ ( Base ‘ 𝑅 ) → ( 𝑥 ( ∥r ‘ ( oppr ‘ 𝑅 ) ) ( 1r ‘ 𝑅 ) ↔ ∃ 𝑚 ∈ ( Base ‘ 𝑅 ) ( 𝑚 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑥 ) = ( 1r ‘ 𝑅 ) ) )
34 28 33 syl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈 ) → ( 𝑥 ( ∥r ‘ ( oppr ‘ 𝑅 ) ) ( 1r ‘ 𝑅 ) ↔ ∃ 𝑚 ∈ ( Base ‘ 𝑅 ) ( 𝑚 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑥 ) = ( 1r ‘ 𝑅 ) ) )
35 30 34 anbi12d ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈 ) → ( ( 𝑥 ( ∥r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ∧ 𝑥 ( ∥r ‘ ( oppr ‘ 𝑅 ) ) ( 1r ‘ 𝑅 ) ) ↔ ( ∃ 𝑦 ∈ ( Base ‘ 𝑅 ) ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = ( 1r ‘ 𝑅 ) ∧ ∃ 𝑚 ∈ ( Base ‘ 𝑅 ) ( 𝑚 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑥 ) = ( 1r ‘ 𝑅 ) ) ) )
36 reeanv ⊢ ( ∃ 𝑦 ∈ ( Base ‘ 𝑅 ) ∃ 𝑚 ∈ ( Base ‘ 𝑅 ) ( ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = ( 1r ‘ 𝑅 ) ∧ ( 𝑚 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑥 ) = ( 1r ‘ 𝑅 ) ) ↔ ( ∃ 𝑦 ∈ ( Base ‘ 𝑅 ) ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = ( 1r ‘ 𝑅 ) ∧ ∃ 𝑚 ∈ ( Base ‘ 𝑅 ) ( 𝑚 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑥 ) = ( 1r ‘ 𝑅 ) ) )
37 simprl ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑚 ∈ ( Base ‘ 𝑅 ) ∧ ( ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = ( 1r ‘ 𝑅 ) ∧ ( 𝑚 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑥 ) = ( 1r ‘ 𝑅 ) ) ) ) → 𝑚 ∈ ( Base ‘ 𝑅 ) )
38 28 ad2antrr ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑚 ∈ ( Base ‘ 𝑅 ) ∧ ( ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = ( 1r ‘ 𝑅 ) ∧ ( 𝑚 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑥 ) = ( 1r ‘ 𝑅 ) ) ) ) → 𝑥 ∈ ( Base ‘ 𝑅 ) )
39 12 23 7 dvdsrmul ⊢ ( ( 𝑚 ∈ ( Base ‘ 𝑅 ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) → 𝑚 ( ∥r ‘ 𝑅 ) ( 𝑥 ( .r ‘ 𝑅 ) 𝑚 ) )
40 37 38 39 syl2anc ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑚 ∈ ( Base ‘ 𝑅 ) ∧ ( ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = ( 1r ‘ 𝑅 ) ∧ ( 𝑚 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑥 ) = ( 1r ‘ 𝑅 ) ) ) ) → 𝑚 ( ∥r ‘ 𝑅 ) ( 𝑥 ( .r ‘ 𝑅 ) 𝑚 ) )
41 simplll ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑚 ∈ ( Base ‘ 𝑅 ) ∧ ( ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = ( 1r ‘ 𝑅 ) ∧ ( 𝑚 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑥 ) = ( 1r ‘ 𝑅 ) ) ) ) → 𝑅 ∈ Ring )
42 simplr ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑚 ∈ ( Base ‘ 𝑅 ) ∧ ( ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = ( 1r ‘ 𝑅 ) ∧ ( 𝑚 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑥 ) = ( 1r ‘ 𝑅 ) ) ) ) → 𝑦 ∈ ( Base ‘ 𝑅 ) )
43 12 7 ringass ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑚 ∈ ( Base ‘ 𝑅 ) ) ) → ( ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) ( .r ‘ 𝑅 ) 𝑚 ) = ( 𝑦 ( .r ‘ 𝑅 ) ( 𝑥 ( .r ‘ 𝑅 ) 𝑚 ) ) )
44 41 42 38 37 43 syl13anc ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑚 ∈ ( Base ‘ 𝑅 ) ∧ ( ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = ( 1r ‘ 𝑅 ) ∧ ( 𝑚 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑥 ) = ( 1r ‘ 𝑅 ) ) ) ) → ( ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) ( .r ‘ 𝑅 ) 𝑚 ) = ( 𝑦 ( .r ‘ 𝑅 ) ( 𝑥 ( .r ‘ 𝑅 ) 𝑚 ) ) )
45 simprrl ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑚 ∈ ( Base ‘ 𝑅 ) ∧ ( ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = ( 1r ‘ 𝑅 ) ∧ ( 𝑚 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑥 ) = ( 1r ‘ 𝑅 ) ) ) ) → ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = ( 1r ‘ 𝑅 ) )
46 45 oveq1d ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑚 ∈ ( Base ‘ 𝑅 ) ∧ ( ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = ( 1r ‘ 𝑅 ) ∧ ( 𝑚 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑥 ) = ( 1r ‘ 𝑅 ) ) ) ) → ( ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) ( .r ‘ 𝑅 ) 𝑚 ) = ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) 𝑚 ) )
47 12 7 24 32 opprmul ⊢ ( 𝑚 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑥 ) = ( 𝑥 ( .r ‘ 𝑅 ) 𝑚 )
48 simprrr ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑚 ∈ ( Base ‘ 𝑅 ) ∧ ( ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = ( 1r ‘ 𝑅 ) ∧ ( 𝑚 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑥 ) = ( 1r ‘ 𝑅 ) ) ) ) → ( 𝑚 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑥 ) = ( 1r ‘ 𝑅 ) )
49 47 48 eqtr3id ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑚 ∈ ( Base ‘ 𝑅 ) ∧ ( ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = ( 1r ‘ 𝑅 ) ∧ ( 𝑚 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑥 ) = ( 1r ‘ 𝑅 ) ) ) ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑚 ) = ( 1r ‘ 𝑅 ) )
50 49 oveq2d ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑚 ∈ ( Base ‘ 𝑅 ) ∧ ( ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = ( 1r ‘ 𝑅 ) ∧ ( 𝑚 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑥 ) = ( 1r ‘ 𝑅 ) ) ) ) → ( 𝑦 ( .r ‘ 𝑅 ) ( 𝑥 ( .r ‘ 𝑅 ) 𝑚 ) ) = ( 𝑦 ( .r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) )
51 44 46 50 3eqtr3d ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑚 ∈ ( Base ‘ 𝑅 ) ∧ ( ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = ( 1r ‘ 𝑅 ) ∧ ( 𝑚 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑥 ) = ( 1r ‘ 𝑅 ) ) ) ) → ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) 𝑚 ) = ( 𝑦 ( .r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) )
52 12 7 19 ringlidm ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑚 ∈ ( Base ‘ 𝑅 ) ) → ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) 𝑚 ) = 𝑚 )
53 41 37 52 syl2anc ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑚 ∈ ( Base ‘ 𝑅 ) ∧ ( ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = ( 1r ‘ 𝑅 ) ∧ ( 𝑚 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑥 ) = ( 1r ‘ 𝑅 ) ) ) ) → ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) 𝑚 ) = 𝑚 )
54 12 7 19 ringridm ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑦 ( .r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) = 𝑦 )
55 41 42 54 syl2anc ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑚 ∈ ( Base ‘ 𝑅 ) ∧ ( ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = ( 1r ‘ 𝑅 ) ∧ ( 𝑚 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑥 ) = ( 1r ‘ 𝑅 ) ) ) ) → ( 𝑦 ( .r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) = 𝑦 )
56 51 53 55 3eqtr3d ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑚 ∈ ( Base ‘ 𝑅 ) ∧ ( ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = ( 1r ‘ 𝑅 ) ∧ ( 𝑚 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑥 ) = ( 1r ‘ 𝑅 ) ) ) ) → 𝑚 = 𝑦 )
57 40 56 49 3brtr3d ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑚 ∈ ( Base ‘ 𝑅 ) ∧ ( ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = ( 1r ‘ 𝑅 ) ∧ ( 𝑚 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑥 ) = ( 1r ‘ 𝑅 ) ) ) ) → 𝑦 ( ∥r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) )
58 31 25 32 dvdsrmul ⊢ ( ( 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) → 𝑦 ( ∥r ‘ ( oppr ‘ 𝑅 ) ) ( 𝑥 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑦 ) )
59 42 38 58 syl2anc ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑚 ∈ ( Base ‘ 𝑅 ) ∧ ( ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = ( 1r ‘ 𝑅 ) ∧ ( 𝑚 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑥 ) = ( 1r ‘ 𝑅 ) ) ) ) → 𝑦 ( ∥r ‘ ( oppr ‘ 𝑅 ) ) ( 𝑥 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑦 ) )
60 12 7 24 32 opprmul ⊢ ( 𝑥 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑦 ) = ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 )
61 60 45 eqtrid ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑚 ∈ ( Base ‘ 𝑅 ) ∧ ( ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = ( 1r ‘ 𝑅 ) ∧ ( 𝑚 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑥 ) = ( 1r ‘ 𝑅 ) ) ) ) → ( 𝑥 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑦 ) = ( 1r ‘ 𝑅 ) )
62 59 61 breqtrd ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑚 ∈ ( Base ‘ 𝑅 ) ∧ ( ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = ( 1r ‘ 𝑅 ) ∧ ( 𝑚 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑥 ) = ( 1r ‘ 𝑅 ) ) ) ) → 𝑦 ( ∥r ‘ ( oppr ‘ 𝑅 ) ) ( 1r ‘ 𝑅 ) )
63 1 19 23 24 25 isunit ⊢ ( 𝑦 ∈ 𝑈 ↔ ( 𝑦 ( ∥r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ∧ 𝑦 ( ∥r ‘ ( oppr ‘ 𝑅 ) ) ( 1r ‘ 𝑅 ) ) )
64 57 62 63 sylanbrc ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑚 ∈ ( Base ‘ 𝑅 ) ∧ ( ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = ( 1r ‘ 𝑅 ) ∧ ( 𝑚 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑥 ) = ( 1r ‘ 𝑅 ) ) ) ) → 𝑦 ∈ 𝑈 )
65 64 45 jca ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑚 ∈ ( Base ‘ 𝑅 ) ∧ ( ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = ( 1r ‘ 𝑅 ) ∧ ( 𝑚 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑥 ) = ( 1r ‘ 𝑅 ) ) ) ) → ( 𝑦 ∈ 𝑈 ∧ ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = ( 1r ‘ 𝑅 ) ) )
66 65 rexlimdvaa ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) → ( ∃ 𝑚 ∈ ( Base ‘ 𝑅 ) ( ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = ( 1r ‘ 𝑅 ) ∧ ( 𝑚 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑥 ) = ( 1r ‘ 𝑅 ) ) → ( 𝑦 ∈ 𝑈 ∧ ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = ( 1r ‘ 𝑅 ) ) ) )
67 66 expimpd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈 ) → ( ( 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ ∃ 𝑚 ∈ ( Base ‘ 𝑅 ) ( ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = ( 1r ‘ 𝑅 ) ∧ ( 𝑚 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑥 ) = ( 1r ‘ 𝑅 ) ) ) → ( 𝑦 ∈ 𝑈 ∧ ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = ( 1r ‘ 𝑅 ) ) ) )
68 67 reximdv2 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈 ) → ( ∃ 𝑦 ∈ ( Base ‘ 𝑅 ) ∃ 𝑚 ∈ ( Base ‘ 𝑅 ) ( ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = ( 1r ‘ 𝑅 ) ∧ ( 𝑚 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑥 ) = ( 1r ‘ 𝑅 ) ) → ∃ 𝑦 ∈ 𝑈 ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = ( 1r ‘ 𝑅 ) ) )
69 36 68 biimtrrid ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈 ) → ( ( ∃ 𝑦 ∈ ( Base ‘ 𝑅 ) ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = ( 1r ‘ 𝑅 ) ∧ ∃ 𝑚 ∈ ( Base ‘ 𝑅 ) ( 𝑚 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑥 ) = ( 1r ‘ 𝑅 ) ) → ∃ 𝑦 ∈ 𝑈 ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = ( 1r ‘ 𝑅 ) ) )
70 35 69 sylbid ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈 ) → ( ( 𝑥 ( ∥r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ∧ 𝑥 ( ∥r ‘ ( oppr ‘ 𝑅 ) ) ( 1r ‘ 𝑅 ) ) → ∃ 𝑦 ∈ 𝑈 ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = ( 1r ‘ 𝑅 ) ) )
71 27 70 mpd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈 ) → ∃ 𝑦 ∈ 𝑈 ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = ( 1r ‘ 𝑅 ) )
72 4 10 11 18 20 22 71 isgrpde ⊢ ( 𝑅 ∈ Ring → 𝐺 ∈ Grp )