Metamath Proof Explorer

Theorem isdrng3lem1

Description: Lemma for isdrng3 (for the left to right 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 isdrng3lem1 ( ( 𝑅 ∈ Ring ∧ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ∈ Grp ) → ∀ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ∃ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ( 𝑦 · 𝑥 ) = 1 )

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 eleq2i ⊢ ( 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ↔ 𝑥 ∈ ( Base ‘ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ) )
8 oveq1 ⊢ ( 𝑦 = ( ( invg ‘ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ) ‘ 𝑥 ) → ( 𝑦 ( +g ‘ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ) 𝑥 ) = ( ( ( invg ‘ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ) ‘ 𝑥 ) ( +g ‘ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ) 𝑥 ) )
9 8 eqeq1d ⊢ ( 𝑦 = ( ( invg ‘ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ) ‘ 𝑥 ) → ( ( 𝑦 ( +g ‘ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ) 𝑥 ) = 1 ↔ ( ( ( invg ‘ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ) ‘ 𝑥 ) ( +g ‘ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ) 𝑥 ) = 1 ) )
10 eqid ⊢ ( Base ‘ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ) = ( Base ‘ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) )
11 eqid ⊢ ( invg ‘ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ) = ( invg ‘ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) )
12 10 11 grpinvcl ⊢ ( ( ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ∈ Grp ∧ 𝑥 ∈ ( Base ‘ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ) ) → ( ( invg ‘ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ) ‘ 𝑥 ) ∈ ( Base ‘ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ) )
13 12 adantll ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ∈ Grp ) ∧ 𝑥 ∈ ( Base ‘ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ) ) → ( ( invg ‘ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ) ‘ 𝑥 ) ∈ ( Base ‘ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ) )
14 eqid ⊢ ( +g ‘ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ) = ( +g ‘ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) )
15 eqid ⊢ ( 0g ‘ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ) = ( 0g ‘ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) )
16 10 14 15 11 grplinv ⊢ ( ( ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ∈ Grp ∧ 𝑥 ∈ ( Base ‘ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ) ) → ( ( ( invg ‘ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ) ‘ 𝑥 ) ( +g ‘ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ) 𝑥 ) = ( 0g ‘ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ) )
17 16 adantll ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ∈ Grp ) ∧ 𝑥 ∈ ( Base ‘ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ) ) → ( ( ( invg ‘ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ) ‘ 𝑥 ) ( +g ‘ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ) 𝑥 ) = ( 0g ‘ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ) )
18 eqid ⊢ ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
19 18 ringmgp ⊢ ( 𝑅 ∈ Ring → ( mulGrp ‘ 𝑅 ) ∈ Mnd )
20 19 adantr ⊢ ( ( 𝑅 ∈ Ring ∧ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ∈ Grp ) → ( mulGrp ‘ 𝑅 ) ∈ Mnd )
21 1 3 ringidcl ⊢ ( 𝑅 ∈ Ring → 1 ∈ 𝐵 )
22 21 adantr ⊢ ( ( 𝑅 ∈ Ring ∧ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ∈ Grp ) → 1 ∈ 𝐵 )
23 eqid ⊢ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) = ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) )
24 1 2 23 isdrng2 ⊢ ( 𝑅 ∈ DivRing ↔ ( 𝑅 ∈ Ring ∧ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ∈ Grp ) )
25 2 3 drngunz ⊢ ( 𝑅 ∈ DivRing → 1 ≠ 0 )
26 24 25 sylbir ⊢ ( ( 𝑅 ∈ Ring ∧ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ∈ Grp ) → 1 ≠ 0 )
27 22 26 eldifsnd ⊢ ( ( 𝑅 ∈ Ring ∧ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ∈ Grp ) → 1 ∈ ( 𝐵 ∖ { 0 } ) )
28 difssd ⊢ ( ( 𝑅 ∈ Ring ∧ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ∈ Grp ) → ( 𝐵 ∖ { 0 } ) ⊆ 𝐵 )
29 18 1 mgpbas ⊢ 𝐵 = ( Base ‘ ( mulGrp ‘ 𝑅 ) )
30 18 3 ringidval ⊢ 1 = ( 0g ‘ ( mulGrp ‘ 𝑅 ) )
31 23 29 30 ress0g ⊢ ( ( ( mulGrp ‘ 𝑅 ) ∈ Mnd ∧ 1 ∈ ( 𝐵 ∖ { 0 } ) ∧ ( 𝐵 ∖ { 0 } ) ⊆ 𝐵 ) → 1 = ( 0g ‘ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ) )
32 31 eqcomd ⊢ ( ( ( mulGrp ‘ 𝑅 ) ∈ Mnd ∧ 1 ∈ ( 𝐵 ∖ { 0 } ) ∧ ( 𝐵 ∖ { 0 } ) ⊆ 𝐵 ) → ( 0g ‘ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ) = 1 )
33 20 27 28 32 syl3anc ⊢ ( ( 𝑅 ∈ Ring ∧ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ∈ Grp ) → ( 0g ‘ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ) = 1 )
34 33 adantr ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ∈ Grp ) ∧ 𝑥 ∈ ( Base ‘ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ) ) → ( 0g ‘ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ) = 1 )
35 17 34 eqtrd ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ∈ Grp ) ∧ 𝑥 ∈ ( Base ‘ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ) ) → ( ( ( invg ‘ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ) ‘ 𝑥 ) ( +g ‘ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ) 𝑥 ) = 1 )
36 9 13 35 rspcedvdw ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ∈ Grp ) ∧ 𝑥 ∈ ( Base ‘ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ) ) → ∃ 𝑦 ∈ ( Base ‘ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ) ( 𝑦 ( +g ‘ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ) 𝑥 ) = 1 )
37 7 36 sylan2b ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ∈ Grp ) ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) → ∃ 𝑦 ∈ ( Base ‘ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ) ( 𝑦 ( +g ‘ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ) 𝑥 ) = 1 )
38 5 a1i ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ∈ Grp ) ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) → ( Base ‘ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ) = ( 𝐵 ∖ { 0 } ) )
39 38 rexeqdv ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ∈ Grp ) ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) → ( ∃ 𝑦 ∈ ( Base ‘ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ) ( 𝑦 ( +g ‘ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ) 𝑥 ) = 1 ↔ ∃ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ( 𝑦 ( +g ‘ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ) 𝑥 ) = 1 ) )
40 18 4 mgpplusg ⊢ · = ( +g ‘ ( mulGrp ‘ 𝑅 ) )
41 1 fvexi ⊢ 𝐵 ∈ V
42 41 difexi ⊢ ( 𝐵 ∖ { 0 } ) ∈ V
43 eqid ⊢ ( +g ‘ ( mulGrp ‘ 𝑅 ) ) = ( +g ‘ ( mulGrp ‘ 𝑅 ) )
44 23 43 ressplusg ⊢ ( ( 𝐵 ∖ { 0 } ) ∈ V → ( +g ‘ ( mulGrp ‘ 𝑅 ) ) = ( +g ‘ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ) )
45 42 44 ax-mp ⊢ ( +g ‘ ( mulGrp ‘ 𝑅 ) ) = ( +g ‘ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) )
46 40 45 eqtr2i ⊢ ( +g ‘ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ) = ·
47 46 oveqi ⊢ ( 𝑦 ( +g ‘ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ) 𝑥 ) = ( 𝑦 · 𝑥 )
48 47 eqeq1i ⊢ ( ( 𝑦 ( +g ‘ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ) 𝑥 ) = 1 ↔ ( 𝑦 · 𝑥 ) = 1 )
49 48 rexbii ⊢ ( ∃ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ( 𝑦 ( +g ‘ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ) 𝑥 ) = 1 ↔ ∃ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ( 𝑦 · 𝑥 ) = 1 )
50 39 49 bitrdi ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ∈ Grp ) ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) → ( ∃ 𝑦 ∈ ( Base ‘ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ) ( 𝑦 ( +g ‘ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ) 𝑥 ) = 1 ↔ ∃ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ( 𝑦 · 𝑥 ) = 1 ) )
51 37 50 mpbid ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ∈ Grp ) ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) → ∃ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ( 𝑦 · 𝑥 ) = 1 )
52 51 ralrimiva ⊢ ( ( 𝑅 ∈ Ring ∧ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ∈ Grp ) → ∀ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ∃ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ( 𝑦 · 𝑥 ) = 1 )