Metamath Proof Explorer

Theorem isdrng3lem2

Description: Lemma for isdrng3 (for the right to left implication). Formerly part of proof for isdrng3 . (Contributed by Jeff Madsen, 8-Jun-2010) (Revised by AV, 22-Jul-2026)

Ref Expression
Hypotheses isdrng3.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
isdrng3.0 ⊢ 0 = ( 0g ‘ 𝑅 )
isdrng3.1 ⊢ 1 = ( 1r ‘ 𝑅 )
isdrng3.t ⊢ · = ( .r ‘ 𝑅 )
Assertion isdrng3lem2 ( ( 𝑅 ∈ Ring ∧ 1 ≠ 0 ∧ ∀ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ∃ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ( 𝑦 · 𝑥 ) = 1 ) → ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ∈ Grp )

Proof

Step Hyp Ref Expression
1 isdrng3.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 isdrng3.0 ⊢ 0 = ( 0g ‘ 𝑅 )
3 isdrng3.1 ⊢ 1 = ( 1r ‘ 𝑅 )
4 isdrng3.t ⊢ · = ( .r ‘ 𝑅 )
5 1 isdrng3lem0 ⊢ ( Base ‘ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ) = ( 𝐵 ∖ { 0 } )
6 5 eqcomi ⊢ ( 𝐵 ∖ { 0 } ) = ( Base ‘ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) )
7 6 a1i ⊢ ( ( 𝑅 ∈ Ring ∧ 1 ≠ 0 ∧ ∀ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ∃ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ( 𝑦 · 𝑥 ) = 1 ) → ( 𝐵 ∖ { 0 } ) = ( Base ‘ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ) )
8 1 fvexi ⊢ 𝐵 ∈ V
9 8 a1i ⊢ ( ( 𝑅 ∈ Ring ∧ 1 ≠ 0 ∧ ∀ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ∃ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ( 𝑦 · 𝑥 ) = 1 ) → 𝐵 ∈ V )
10 9 difexd ⊢ ( ( 𝑅 ∈ Ring ∧ 1 ≠ 0 ∧ ∀ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ∃ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ( 𝑦 · 𝑥 ) = 1 ) → ( 𝐵 ∖ { 0 } ) ∈ V )
11 eqid ⊢ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) = ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) )
12 eqid ⊢ ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
13 12 4 mgpplusg ⊢ · = ( +g ‘ ( mulGrp ‘ 𝑅 ) )
14 11 13 ressplusg ⊢ ( ( 𝐵 ∖ { 0 } ) ∈ V → · = ( +g ‘ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ) )
15 10 14 syl ⊢ ( ( 𝑅 ∈ Ring ∧ 1 ≠ 0 ∧ ∀ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ∃ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ( 𝑦 · 𝑥 ) = 1 ) → · = ( +g ‘ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ) )
16 simp1 ⊢ ( ( 𝑅 ∈ Ring ∧ 1 ≠ 0 ∧ ∀ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ∃ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ( 𝑦 · 𝑥 ) = 1 ) → 𝑅 ∈ Ring )
17 eldifi ⊢ ( 𝑎 ∈ ( 𝐵 ∖ { 0 } ) → 𝑎 ∈ 𝐵 )
18 eldifi ⊢ ( 𝑏 ∈ ( 𝐵 ∖ { 0 } ) → 𝑏 ∈ 𝐵 )
19 1 4 ringcl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑎 · 𝑏 ) ∈ 𝐵 )
20 16 17 18 19 syl3an ⊢ ( ( ( 𝑅 ∈ Ring ∧ 1 ≠ 0 ∧ ∀ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ∃ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ( 𝑦 · 𝑥 ) = 1 ) ∧ 𝑎 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑏 ∈ ( 𝐵 ∖ { 0 } ) ) → ( 𝑎 · 𝑏 ) ∈ 𝐵 )
21 oveq2 ⊢ ( 𝑥 = 𝑎 → ( 𝑦 · 𝑥 ) = ( 𝑦 · 𝑎 ) )
22 21 eqeq1d ⊢ ( 𝑥 = 𝑎 → ( ( 𝑦 · 𝑥 ) = 1 ↔ ( 𝑦 · 𝑎 ) = 1 ) )
23 22 rexbidv ⊢ ( 𝑥 = 𝑎 → ( ∃ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ( 𝑦 · 𝑥 ) = 1 ↔ ∃ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ( 𝑦 · 𝑎 ) = 1 ) )
24 23 rspcv ⊢ ( 𝑎 ∈ ( 𝐵 ∖ { 0 } ) → ( ∀ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ∃ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ( 𝑦 · 𝑥 ) = 1 → ∃ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ( 𝑦 · 𝑎 ) = 1 ) )
25 24 imdistanri ⊢ ( ( ∀ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ∃ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ( 𝑦 · 𝑥 ) = 1 ∧ 𝑎 ∈ ( 𝐵 ∖ { 0 } ) ) → ( ∃ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ( 𝑦 · 𝑎 ) = 1 ∧ 𝑎 ∈ ( 𝐵 ∖ { 0 } ) ) )
26 eldifsn ⊢ ( 𝑏 ∈ ( 𝐵 ∖ { 0 } ) ↔ ( 𝑏 ∈ 𝐵 ∧ 𝑏 ≠ 0 ) )
27 simp1 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑎 ∈ 𝐵 ∧ ∃ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ( 𝑦 · 𝑎 ) = 1 ) → 𝑅 ∈ Ring )
28 27 adantr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑎 ∈ 𝐵 ∧ ∃ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ( 𝑦 · 𝑎 ) = 1 ) ∧ 𝑏 ∈ 𝐵 ) → 𝑅 ∈ Ring )
29 simpl2 ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑎 ∈ 𝐵 ∧ ∃ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ( 𝑦 · 𝑎 ) = 1 ) ∧ 𝑏 ∈ 𝐵 ) → 𝑎 ∈ 𝐵 )
30 difss ⊢ ( 𝐵 ∖ { 0 } ) ⊆ 𝐵
31 ssrexv ⊢ ( ( 𝐵 ∖ { 0 } ) ⊆ 𝐵 → ( ∃ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ( 𝑦 · 𝑎 ) = 1 → ∃ 𝑦 ∈ 𝐵 ( 𝑦 · 𝑎 ) = 1 ) )
32 30 31 ax-mp ⊢ ( ∃ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ( 𝑦 · 𝑎 ) = 1 → ∃ 𝑦 ∈ 𝐵 ( 𝑦 · 𝑎 ) = 1 )
33 oveq1 ⊢ ( 𝑦 = 𝑐 → ( 𝑦 · 𝑎 ) = ( 𝑐 · 𝑎 ) )
34 33 eqeq1d ⊢ ( 𝑦 = 𝑐 → ( ( 𝑦 · 𝑎 ) = 1 ↔ ( 𝑐 · 𝑎 ) = 1 ) )
35 34 cbvrexvw ⊢ ( ∃ 𝑦 ∈ 𝐵 ( 𝑦 · 𝑎 ) = 1 ↔ ∃ 𝑐 ∈ 𝐵 ( 𝑐 · 𝑎 ) = 1 )
36 32 35 sylib ⊢ ( ∃ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ( 𝑦 · 𝑎 ) = 1 → ∃ 𝑐 ∈ 𝐵 ( 𝑐 · 𝑎 ) = 1 )
37 36 3ad2ant3 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑎 ∈ 𝐵 ∧ ∃ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ( 𝑦 · 𝑎 ) = 1 ) → ∃ 𝑐 ∈ 𝐵 ( 𝑐 · 𝑎 ) = 1 )
38 37 adantr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑎 ∈ 𝐵 ∧ ∃ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ( 𝑦 · 𝑎 ) = 1 ) ∧ 𝑏 ∈ 𝐵 ) → ∃ 𝑐 ∈ 𝐵 ( 𝑐 · 𝑎 ) = 1 )
39 simpr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑎 ∈ 𝐵 ∧ ∃ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ( 𝑦 · 𝑎 ) = 1 ) ∧ 𝑏 ∈ 𝐵 ) → 𝑏 ∈ 𝐵 )
40 1 4 3 2 28 29 38 39 ringinvnzdiv ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑎 ∈ 𝐵 ∧ ∃ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ( 𝑦 · 𝑎 ) = 1 ) ∧ 𝑏 ∈ 𝐵 ) → ( ( 𝑎 · 𝑏 ) = 0 ↔ 𝑏 = 0 ) )
41 40 biimpd ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑎 ∈ 𝐵 ∧ ∃ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ( 𝑦 · 𝑎 ) = 1 ) ∧ 𝑏 ∈ 𝐵 ) → ( ( 𝑎 · 𝑏 ) = 0 → 𝑏 = 0 ) )
42 41 ex ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑎 ∈ 𝐵 ∧ ∃ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ( 𝑦 · 𝑎 ) = 1 ) → ( 𝑏 ∈ 𝐵 → ( ( 𝑎 · 𝑏 ) = 0 → 𝑏 = 0 ) ) )
43 17 42 syl3an2 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑎 ∈ ( 𝐵 ∖ { 0 } ) ∧ ∃ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ( 𝑦 · 𝑎 ) = 1 ) → ( 𝑏 ∈ 𝐵 → ( ( 𝑎 · 𝑏 ) = 0 → 𝑏 = 0 ) ) )
44 43 3expb ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑎 ∈ ( 𝐵 ∖ { 0 } ) ∧ ∃ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ( 𝑦 · 𝑎 ) = 1 ) ) → ( 𝑏 ∈ 𝐵 → ( ( 𝑎 · 𝑏 ) = 0 → 𝑏 = 0 ) ) )
45 44 imp ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑎 ∈ ( 𝐵 ∖ { 0 } ) ∧ ∃ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ( 𝑦 · 𝑎 ) = 1 ) ) ∧ 𝑏 ∈ 𝐵 ) → ( ( 𝑎 · 𝑏 ) = 0 → 𝑏 = 0 ) )
46 45 necon3d ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑎 ∈ ( 𝐵 ∖ { 0 } ) ∧ ∃ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ( 𝑦 · 𝑎 ) = 1 ) ) ∧ 𝑏 ∈ 𝐵 ) → ( 𝑏 ≠ 0 → ( 𝑎 · 𝑏 ) ≠ 0 ) )
47 46 impr ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑎 ∈ ( 𝐵 ∖ { 0 } ) ∧ ∃ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ( 𝑦 · 𝑎 ) = 1 ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑏 ≠ 0 ) ) → ( 𝑎 · 𝑏 ) ≠ 0 )
48 26 47 sylan2b ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑎 ∈ ( 𝐵 ∖ { 0 } ) ∧ ∃ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ( 𝑦 · 𝑎 ) = 1 ) ) ∧ 𝑏 ∈ ( 𝐵 ∖ { 0 } ) ) → ( 𝑎 · 𝑏 ) ≠ 0 )
49 48 an32s ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑏 ∈ ( 𝐵 ∖ { 0 } ) ) ∧ ( 𝑎 ∈ ( 𝐵 ∖ { 0 } ) ∧ ∃ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ( 𝑦 · 𝑎 ) = 1 ) ) → ( 𝑎 · 𝑏 ) ≠ 0 )
50 49 ancom2s ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑏 ∈ ( 𝐵 ∖ { 0 } ) ) ∧ ( ∃ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ( 𝑦 · 𝑎 ) = 1 ∧ 𝑎 ∈ ( 𝐵 ∖ { 0 } ) ) ) → ( 𝑎 · 𝑏 ) ≠ 0 )
51 25 50 sylan2 ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑏 ∈ ( 𝐵 ∖ { 0 } ) ) ∧ ( ∀ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ∃ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ( 𝑦 · 𝑥 ) = 1 ∧ 𝑎 ∈ ( 𝐵 ∖ { 0 } ) ) ) → ( 𝑎 · 𝑏 ) ≠ 0 )
52 51 an42s ⊢ ( ( ( 𝑅 ∈ Ring ∧ ∀ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ∃ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ( 𝑦 · 𝑥 ) = 1 ) ∧ ( 𝑎 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑏 ∈ ( 𝐵 ∖ { 0 } ) ) ) → ( 𝑎 · 𝑏 ) ≠ 0 )
53 52 exp32 ⊢ ( ( 𝑅 ∈ Ring ∧ ∀ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ∃ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ( 𝑦 · 𝑥 ) = 1 ) → ( 𝑎 ∈ ( 𝐵 ∖ { 0 } ) → ( 𝑏 ∈ ( 𝐵 ∖ { 0 } ) → ( 𝑎 · 𝑏 ) ≠ 0 ) ) )
54 53 3adant2 ⊢ ( ( 𝑅 ∈ Ring ∧ 1 ≠ 0 ∧ ∀ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ∃ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ( 𝑦 · 𝑥 ) = 1 ) → ( 𝑎 ∈ ( 𝐵 ∖ { 0 } ) → ( 𝑏 ∈ ( 𝐵 ∖ { 0 } ) → ( 𝑎 · 𝑏 ) ≠ 0 ) ) )
55 54 3imp ⊢ ( ( ( 𝑅 ∈ Ring ∧ 1 ≠ 0 ∧ ∀ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ∃ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ( 𝑦 · 𝑥 ) = 1 ) ∧ 𝑎 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑏 ∈ ( 𝐵 ∖ { 0 } ) ) → ( 𝑎 · 𝑏 ) ≠ 0 )
56 20 55 eldifsnd ⊢ ( ( ( 𝑅 ∈ Ring ∧ 1 ≠ 0 ∧ ∀ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ∃ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ( 𝑦 · 𝑥 ) = 1 ) ∧ 𝑎 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑏 ∈ ( 𝐵 ∖ { 0 } ) ) → ( 𝑎 · 𝑏 ) ∈ ( 𝐵 ∖ { 0 } ) )
57 eldifi ⊢ ( 𝑐 ∈ ( 𝐵 ∖ { 0 } ) → 𝑐 ∈ 𝐵 )
58 17 18 57 3anim123i ⊢ ( ( 𝑎 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑏 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑐 ∈ ( 𝐵 ∖ { 0 } ) ) → ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) )
59 1 4 ringass ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) → ( ( 𝑎 · 𝑏 ) · 𝑐 ) = ( 𝑎 · ( 𝑏 · 𝑐 ) ) )
60 16 58 59 syl2an ⊢ ( ( ( 𝑅 ∈ Ring ∧ 1 ≠ 0 ∧ ∀ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ∃ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ( 𝑦 · 𝑥 ) = 1 ) ∧ ( 𝑎 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑏 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑐 ∈ ( 𝐵 ∖ { 0 } ) ) ) → ( ( 𝑎 · 𝑏 ) · 𝑐 ) = ( 𝑎 · ( 𝑏 · 𝑐 ) ) )
61 1 3 ringidcl ⊢ ( 𝑅 ∈ Ring → 1 ∈ 𝐵 )
62 nelsn ⊢ ( 1 ≠ 0 → ¬ 1 ∈ { 0 } )
63 61 62 anim12i ⊢ ( ( 𝑅 ∈ Ring ∧ 1 ≠ 0 ) → ( 1 ∈ 𝐵 ∧ ¬ 1 ∈ { 0 } ) )
64 eldif ⊢ ( 1 ∈ ( 𝐵 ∖ { 0 } ) ↔ ( 1 ∈ 𝐵 ∧ ¬ 1 ∈ { 0 } ) )
65 63 64 sylibr ⊢ ( ( 𝑅 ∈ Ring ∧ 1 ≠ 0 ) → 1 ∈ ( 𝐵 ∖ { 0 } ) )
66 65 3adant3 ⊢ ( ( 𝑅 ∈ Ring ∧ 1 ≠ 0 ∧ ∀ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ∃ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ( 𝑦 · 𝑥 ) = 1 ) → 1 ∈ ( 𝐵 ∖ { 0 } ) )
67 1 4 3 ringlidm ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑎 ∈ 𝐵 ) → ( 1 · 𝑎 ) = 𝑎 )
68 16 17 67 syl2an ⊢ ( ( ( 𝑅 ∈ Ring ∧ 1 ≠ 0 ∧ ∀ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ∃ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ( 𝑦 · 𝑥 ) = 1 ) ∧ 𝑎 ∈ ( 𝐵 ∖ { 0 } ) ) → ( 1 · 𝑎 ) = 𝑎 )
69 oveq1 ⊢ ( 𝑦 = 𝑏 → ( 𝑦 · 𝑎 ) = ( 𝑏 · 𝑎 ) )
70 69 eqeq1d ⊢ ( 𝑦 = 𝑏 → ( ( 𝑦 · 𝑎 ) = 1 ↔ ( 𝑏 · 𝑎 ) = 1 ) )
71 70 cbvrexvw ⊢ ( ∃ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ( 𝑦 · 𝑎 ) = 1 ↔ ∃ 𝑏 ∈ ( 𝐵 ∖ { 0 } ) ( 𝑏 · 𝑎 ) = 1 )
72 23 71 bitrdi ⊢ ( 𝑥 = 𝑎 → ( ∃ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ( 𝑦 · 𝑥 ) = 1 ↔ ∃ 𝑏 ∈ ( 𝐵 ∖ { 0 } ) ( 𝑏 · 𝑎 ) = 1 ) )
73 72 rspccv ⊢ ( ∀ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ∃ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ( 𝑦 · 𝑥 ) = 1 → ( 𝑎 ∈ ( 𝐵 ∖ { 0 } ) → ∃ 𝑏 ∈ ( 𝐵 ∖ { 0 } ) ( 𝑏 · 𝑎 ) = 1 ) )
74 73 3ad2ant3 ⊢ ( ( 𝑅 ∈ Ring ∧ 1 ≠ 0 ∧ ∀ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ∃ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ( 𝑦 · 𝑥 ) = 1 ) → ( 𝑎 ∈ ( 𝐵 ∖ { 0 } ) → ∃ 𝑏 ∈ ( 𝐵 ∖ { 0 } ) ( 𝑏 · 𝑎 ) = 1 ) )
75 74 imp ⊢ ( ( ( 𝑅 ∈ Ring ∧ 1 ≠ 0 ∧ ∀ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ∃ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ( 𝑦 · 𝑥 ) = 1 ) ∧ 𝑎 ∈ ( 𝐵 ∖ { 0 } ) ) → ∃ 𝑏 ∈ ( 𝐵 ∖ { 0 } ) ( 𝑏 · 𝑎 ) = 1 )
76 7 15 56 60 66 68 75 isgrpde ⊢ ( ( 𝑅 ∈ Ring ∧ 1 ≠ 0 ∧ ∀ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ∃ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ( 𝑦 · 𝑥 ) = 1 ) → ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ∈ Grp )