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 simpr ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈 ) → 𝑥 ∈ 𝑈 )
24 eqid ⊢ ( ∥r ‘ 𝑅 ) = ( ∥r ‘ 𝑅 )
25 eqid ⊢ ( oppr ‘ 𝑅 ) = ( oppr ‘ 𝑅 )
26 eqid ⊢ ( ∥r ‘ ( oppr ‘ 𝑅 ) ) = ( ∥r ‘ ( oppr ‘ 𝑅 ) )
27 1 19 24 25 26 isunit ⊢ ( 𝑥 ∈ 𝑈 ↔ ( 𝑥 ( ∥r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ∧ 𝑥 ( ∥r ‘ ( oppr ‘ 𝑅 ) ) ( 1r ‘ 𝑅 ) ) )
28 23 27 sylib ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈 ) → ( 𝑥 ( ∥r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ∧ 𝑥 ( ∥r ‘ ( oppr ‘ 𝑅 ) ) ( 1r ‘ 𝑅 ) ) )
29 13 adantl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈 ) → 𝑥 ∈ ( Base ‘ 𝑅 ) )
30 12 24 7 dvdsr2 ⊢ ( 𝑥 ∈ ( Base ‘ 𝑅 ) → ( 𝑥 ( ∥r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ↔ ∃ 𝑦 ∈ ( Base ‘ 𝑅 ) ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = ( 1r ‘ 𝑅 ) ) )
31 29 30 syl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈 ) → ( 𝑥 ( ∥r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ↔ ∃ 𝑦 ∈ ( Base ‘ 𝑅 ) ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = ( 1r ‘ 𝑅 ) ) )
32 25 12 opprbas ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ ( oppr ‘ 𝑅 ) )
33 eqid ⊢ ( .r ‘ ( oppr ‘ 𝑅 ) ) = ( .r ‘ ( oppr ‘ 𝑅 ) )
34 32 26 33 dvdsr2 ⊢ ( 𝑥 ∈ ( Base ‘ 𝑅 ) → ( 𝑥 ( ∥r ‘ ( oppr ‘ 𝑅 ) ) ( 1r ‘ 𝑅 ) ↔ ∃ 𝑚 ∈ ( Base ‘ 𝑅 ) ( 𝑚 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑥 ) = ( 1r ‘ 𝑅 ) ) )
35 29 34 syl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈 ) → ( 𝑥 ( ∥r ‘ ( oppr ‘ 𝑅 ) ) ( 1r ‘ 𝑅 ) ↔ ∃ 𝑚 ∈ ( Base ‘ 𝑅 ) ( 𝑚 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑥 ) = ( 1r ‘ 𝑅 ) ) )
36 31 35 anbi12d ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈 ) → ( ( 𝑥 ( ∥r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ∧ 𝑥 ( ∥r ‘ ( oppr ‘ 𝑅 ) ) ( 1r ‘ 𝑅 ) ) ↔ ( ∃ 𝑦 ∈ ( Base ‘ 𝑅 ) ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = ( 1r ‘ 𝑅 ) ∧ ∃ 𝑚 ∈ ( Base ‘ 𝑅 ) ( 𝑚 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑥 ) = ( 1r ‘ 𝑅 ) ) ) )
37 reeanv ⊢ ( ∃ 𝑦 ∈ ( Base ‘ 𝑅 ) ∃ 𝑚 ∈ ( Base ‘ 𝑅 ) ( ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = ( 1r ‘ 𝑅 ) ∧ ( 𝑚 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑥 ) = ( 1r ‘ 𝑅 ) ) ↔ ( ∃ 𝑦 ∈ ( Base ‘ 𝑅 ) ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = ( 1r ‘ 𝑅 ) ∧ ∃ 𝑚 ∈ ( Base ‘ 𝑅 ) ( 𝑚 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑥 ) = ( 1r ‘ 𝑅 ) ) )
38 simprl ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑚 ∈ ( Base ‘ 𝑅 ) ∧ ( ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = ( 1r ‘ 𝑅 ) ∧ ( 𝑚 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑥 ) = ( 1r ‘ 𝑅 ) ) ) ) → 𝑚 ∈ ( Base ‘ 𝑅 ) )
39 29 ad2antrr ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑚 ∈ ( Base ‘ 𝑅 ) ∧ ( ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = ( 1r ‘ 𝑅 ) ∧ ( 𝑚 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑥 ) = ( 1r ‘ 𝑅 ) ) ) ) → 𝑥 ∈ ( Base ‘ 𝑅 ) )
40 12 24 7 dvdsrmul ⊢ ( ( 𝑚 ∈ ( Base ‘ 𝑅 ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) → 𝑚 ( ∥r ‘ 𝑅 ) ( 𝑥 ( .r ‘ 𝑅 ) 𝑚 ) )
41 38 39 40 syl2anc ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑚 ∈ ( Base ‘ 𝑅 ) ∧ ( ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = ( 1r ‘ 𝑅 ) ∧ ( 𝑚 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑥 ) = ( 1r ‘ 𝑅 ) ) ) ) → 𝑚 ( ∥r ‘ 𝑅 ) ( 𝑥 ( .r ‘ 𝑅 ) 𝑚 ) )
42 simplll ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑚 ∈ ( Base ‘ 𝑅 ) ∧ ( ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = ( 1r ‘ 𝑅 ) ∧ ( 𝑚 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑥 ) = ( 1r ‘ 𝑅 ) ) ) ) → 𝑅 ∈ Ring )
43 simplr ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑚 ∈ ( Base ‘ 𝑅 ) ∧ ( ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = ( 1r ‘ 𝑅 ) ∧ ( 𝑚 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑥 ) = ( 1r ‘ 𝑅 ) ) ) ) → 𝑦 ∈ ( Base ‘ 𝑅 ) )
44 12 7 ringass ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑚 ∈ ( Base ‘ 𝑅 ) ) ) → ( ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) ( .r ‘ 𝑅 ) 𝑚 ) = ( 𝑦 ( .r ‘ 𝑅 ) ( 𝑥 ( .r ‘ 𝑅 ) 𝑚 ) ) )
45 42 43 39 38 44 syl13anc ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑚 ∈ ( Base ‘ 𝑅 ) ∧ ( ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = ( 1r ‘ 𝑅 ) ∧ ( 𝑚 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑥 ) = ( 1r ‘ 𝑅 ) ) ) ) → ( ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) ( .r ‘ 𝑅 ) 𝑚 ) = ( 𝑦 ( .r ‘ 𝑅 ) ( 𝑥 ( .r ‘ 𝑅 ) 𝑚 ) ) )
46 simprrl ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑚 ∈ ( Base ‘ 𝑅 ) ∧ ( ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = ( 1r ‘ 𝑅 ) ∧ ( 𝑚 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑥 ) = ( 1r ‘ 𝑅 ) ) ) ) → ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = ( 1r ‘ 𝑅 ) )
47 46 oveq1d ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑚 ∈ ( Base ‘ 𝑅 ) ∧ ( ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = ( 1r ‘ 𝑅 ) ∧ ( 𝑚 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑥 ) = ( 1r ‘ 𝑅 ) ) ) ) → ( ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) ( .r ‘ 𝑅 ) 𝑚 ) = ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) 𝑚 ) )
48 12 7 25 33 opprmul ⊢ ( 𝑚 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑥 ) = ( 𝑥 ( .r ‘ 𝑅 ) 𝑚 )
49 simprrr ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑚 ∈ ( Base ‘ 𝑅 ) ∧ ( ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = ( 1r ‘ 𝑅 ) ∧ ( 𝑚 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑥 ) = ( 1r ‘ 𝑅 ) ) ) ) → ( 𝑚 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑥 ) = ( 1r ‘ 𝑅 ) )
50 48 49 eqtr3id ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑚 ∈ ( Base ‘ 𝑅 ) ∧ ( ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = ( 1r ‘ 𝑅 ) ∧ ( 𝑚 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑥 ) = ( 1r ‘ 𝑅 ) ) ) ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑚 ) = ( 1r ‘ 𝑅 ) )
51 50 oveq2d ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑚 ∈ ( Base ‘ 𝑅 ) ∧ ( ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = ( 1r ‘ 𝑅 ) ∧ ( 𝑚 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑥 ) = ( 1r ‘ 𝑅 ) ) ) ) → ( 𝑦 ( .r ‘ 𝑅 ) ( 𝑥 ( .r ‘ 𝑅 ) 𝑚 ) ) = ( 𝑦 ( .r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) )
52 45 47 51 3eqtr3d ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑚 ∈ ( Base ‘ 𝑅 ) ∧ ( ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = ( 1r ‘ 𝑅 ) ∧ ( 𝑚 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑥 ) = ( 1r ‘ 𝑅 ) ) ) ) → ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) 𝑚 ) = ( 𝑦 ( .r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) )
53 12 7 19 ringlidm ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑚 ∈ ( Base ‘ 𝑅 ) ) → ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) 𝑚 ) = 𝑚 )
54 42 38 53 syl2anc ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑚 ∈ ( Base ‘ 𝑅 ) ∧ ( ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = ( 1r ‘ 𝑅 ) ∧ ( 𝑚 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑥 ) = ( 1r ‘ 𝑅 ) ) ) ) → ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) 𝑚 ) = 𝑚 )
55 12 7 19 ringridm ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑦 ( .r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) = 𝑦 )
56 42 43 55 syl2anc ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑚 ∈ ( Base ‘ 𝑅 ) ∧ ( ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = ( 1r ‘ 𝑅 ) ∧ ( 𝑚 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑥 ) = ( 1r ‘ 𝑅 ) ) ) ) → ( 𝑦 ( .r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) = 𝑦 )
57 52 54 56 3eqtr3d ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑚 ∈ ( Base ‘ 𝑅 ) ∧ ( ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = ( 1r ‘ 𝑅 ) ∧ ( 𝑚 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑥 ) = ( 1r ‘ 𝑅 ) ) ) ) → 𝑚 = 𝑦 )
58 41 57 50 3brtr3d ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑚 ∈ ( Base ‘ 𝑅 ) ∧ ( ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = ( 1r ‘ 𝑅 ) ∧ ( 𝑚 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑥 ) = ( 1r ‘ 𝑅 ) ) ) ) → 𝑦 ( ∥r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) )
59 32 26 33 dvdsrmul ⊢ ( ( 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) → 𝑦 ( ∥r ‘ ( oppr ‘ 𝑅 ) ) ( 𝑥 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑦 ) )
60 43 39 59 syl2anc ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑚 ∈ ( Base ‘ 𝑅 ) ∧ ( ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = ( 1r ‘ 𝑅 ) ∧ ( 𝑚 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑥 ) = ( 1r ‘ 𝑅 ) ) ) ) → 𝑦 ( ∥r ‘ ( oppr ‘ 𝑅 ) ) ( 𝑥 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑦 ) )
61 12 7 25 33 opprmul ⊢ ( 𝑥 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑦 ) = ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 )
62 61 46 syl5eq ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑚 ∈ ( Base ‘ 𝑅 ) ∧ ( ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = ( 1r ‘ 𝑅 ) ∧ ( 𝑚 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑥 ) = ( 1r ‘ 𝑅 ) ) ) ) → ( 𝑥 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑦 ) = ( 1r ‘ 𝑅 ) )
63 60 62 breqtrd ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑚 ∈ ( Base ‘ 𝑅 ) ∧ ( ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = ( 1r ‘ 𝑅 ) ∧ ( 𝑚 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑥 ) = ( 1r ‘ 𝑅 ) ) ) ) → 𝑦 ( ∥r ‘ ( oppr ‘ 𝑅 ) ) ( 1r ‘ 𝑅 ) )
64 1 19 24 25 26 isunit ⊢ ( 𝑦 ∈ 𝑈 ↔ ( 𝑦 ( ∥r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ∧ 𝑦 ( ∥r ‘ ( oppr ‘ 𝑅 ) ) ( 1r ‘ 𝑅 ) ) )
65 58 63 64 sylanbrc ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑚 ∈ ( Base ‘ 𝑅 ) ∧ ( ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = ( 1r ‘ 𝑅 ) ∧ ( 𝑚 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑥 ) = ( 1r ‘ 𝑅 ) ) ) ) → 𝑦 ∈ 𝑈 )
66 65 46 jca ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑚 ∈ ( Base ‘ 𝑅 ) ∧ ( ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = ( 1r ‘ 𝑅 ) ∧ ( 𝑚 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑥 ) = ( 1r ‘ 𝑅 ) ) ) ) → ( 𝑦 ∈ 𝑈 ∧ ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = ( 1r ‘ 𝑅 ) ) )
67 66 rexlimdvaa ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) → ( ∃ 𝑚 ∈ ( Base ‘ 𝑅 ) ( ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = ( 1r ‘ 𝑅 ) ∧ ( 𝑚 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑥 ) = ( 1r ‘ 𝑅 ) ) → ( 𝑦 ∈ 𝑈 ∧ ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = ( 1r ‘ 𝑅 ) ) ) )
68 67 expimpd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈 ) → ( ( 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ ∃ 𝑚 ∈ ( Base ‘ 𝑅 ) ( ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = ( 1r ‘ 𝑅 ) ∧ ( 𝑚 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑥 ) = ( 1r ‘ 𝑅 ) ) ) → ( 𝑦 ∈ 𝑈 ∧ ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = ( 1r ‘ 𝑅 ) ) ) )
69 68 reximdv2 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈 ) → ( ∃ 𝑦 ∈ ( Base ‘ 𝑅 ) ∃ 𝑚 ∈ ( Base ‘ 𝑅 ) ( ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = ( 1r ‘ 𝑅 ) ∧ ( 𝑚 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑥 ) = ( 1r ‘ 𝑅 ) ) → ∃ 𝑦 ∈ 𝑈 ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = ( 1r ‘ 𝑅 ) ) )
70 37 69 syl5bir ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈 ) → ( ( ∃ 𝑦 ∈ ( Base ‘ 𝑅 ) ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = ( 1r ‘ 𝑅 ) ∧ ∃ 𝑚 ∈ ( Base ‘ 𝑅 ) ( 𝑚 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑥 ) = ( 1r ‘ 𝑅 ) ) → ∃ 𝑦 ∈ 𝑈 ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = ( 1r ‘ 𝑅 ) ) )
71 36 70 sylbid ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈 ) → ( ( 𝑥 ( ∥r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ∧ 𝑥 ( ∥r ‘ ( oppr ‘ 𝑅 ) ) ( 1r ‘ 𝑅 ) ) → ∃ 𝑦 ∈ 𝑈 ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = ( 1r ‘ 𝑅 ) ) )
72 28 71 mpd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈 ) → ∃ 𝑦 ∈ 𝑈 ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = ( 1r ‘ 𝑅 ) )
73 4 10 11 18 20 22 72 isgrpde ⊢ ( 𝑅 ∈ Ring → 𝐺 ∈ Grp )