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 
|- B = ( Base ` R )
isdrng3.0 
|- .0. = ( 0g ` R )
isdrng3.1 
|- .1. = ( 1r ` R )
isdrng3.t 
|- .x. = ( .r ` R )
Assertion isdrng3lem1 
|- ( ( R e. Ring /\ ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) e. Grp ) -> A. x e. ( B \ { .0. } ) E. y e. ( B \ { .0. } ) ( y .x. x ) = .1. )

Proof

Step Hyp Ref Expression
1 isdrng3.b 
 |-  B = ( Base ` R )
2 isdrng3.0 
 |-  .0. = ( 0g ` R )
3 isdrng3.1 
 |-  .1. = ( 1r ` R )
4 isdrng3.t 
 |-  .x. = ( .r ` R )
5 1 isdrng3lem0 
 |-  ( Base ` ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) ) = ( B \ { .0. } )
6 5 eqcomi 
 |-  ( B \ { .0. } ) = ( Base ` ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) )
7 6 eleq2i 
 |-  ( x e. ( B \ { .0. } ) <-> x e. ( Base ` ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) ) )
8 oveq1 
 |-  ( y = ( ( invg ` ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) ) ` x ) -> ( y ( +g ` ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) ) x ) = ( ( ( invg ` ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) ) ` x ) ( +g ` ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) ) x ) )
9 8 eqeq1d 
 |-  ( y = ( ( invg ` ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) ) ` x ) -> ( ( y ( +g ` ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) ) x ) = .1. <-> ( ( ( invg ` ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) ) ` x ) ( +g ` ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) ) x ) = .1. ) )
10 eqid 
 |-  ( Base ` ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) ) = ( Base ` ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) )
11 eqid 
 |-  ( invg ` ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) ) = ( invg ` ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) )
12 10 11 grpinvcl 
 |-  ( ( ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) e. Grp /\ x e. ( Base ` ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) ) ) -> ( ( invg ` ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) ) ` x ) e. ( Base ` ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) ) )
13 12 adantll 
 |-  ( ( ( R e. Ring /\ ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) e. Grp ) /\ x e. ( Base ` ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) ) ) -> ( ( invg ` ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) ) ` x ) e. ( Base ` ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) ) )
14 eqid 
 |-  ( +g ` ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) ) = ( +g ` ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) )
15 eqid 
 |-  ( 0g ` ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) ) = ( 0g ` ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) )
16 10 14 15 11 grplinv 
 |-  ( ( ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) e. Grp /\ x e. ( Base ` ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) ) ) -> ( ( ( invg ` ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) ) ` x ) ( +g ` ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) ) x ) = ( 0g ` ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) ) )
17 16 adantll 
 |-  ( ( ( R e. Ring /\ ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) e. Grp ) /\ x e. ( Base ` ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) ) ) -> ( ( ( invg ` ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) ) ` x ) ( +g ` ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) ) x ) = ( 0g ` ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) ) )
18 eqid 
 |-  ( mulGrp ` R ) = ( mulGrp ` R )
19 18 ringmgp 
 |-  ( R e. Ring -> ( mulGrp ` R ) e. Mnd )
20 19 adantr 
 |-  ( ( R e. Ring /\ ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) e. Grp ) -> ( mulGrp ` R ) e. Mnd )
21 1 3 ringidcl 
 |-  ( R e. Ring -> .1. e. B )
22 21 adantr 
 |-  ( ( R e. Ring /\ ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) e. Grp ) -> .1. e. B )
23 eqid 
 |-  ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) = ( ( mulGrp ` R ) |`s ( B \ { .0. } ) )
24 1 2 23 isdrng2 
 |-  ( R e. DivRing <-> ( R e. Ring /\ ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) e. Grp ) )
25 2 3 drngunz 
 |-  ( R e. DivRing -> .1. =/= .0. )
26 24 25 sylbir 
 |-  ( ( R e. Ring /\ ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) e. Grp ) -> .1. =/= .0. )
27 22 26 eldifsnd 
 |-  ( ( R e. Ring /\ ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) e. Grp ) -> .1. e. ( B \ { .0. } ) )
28 difssd 
 |-  ( ( R e. Ring /\ ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) e. Grp ) -> ( B \ { .0. } ) C_ B )
29 18 1 mgpbas 
 |-  B = ( Base ` ( mulGrp ` R ) )
30 18 3 ringidval 
 |-  .1. = ( 0g ` ( mulGrp ` R ) )
31 23 29 30 ress0g 
 |-  ( ( ( mulGrp ` R ) e. Mnd /\ .1. e. ( B \ { .0. } ) /\ ( B \ { .0. } ) C_ B ) -> .1. = ( 0g ` ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) ) )
32 31 eqcomd 
 |-  ( ( ( mulGrp ` R ) e. Mnd /\ .1. e. ( B \ { .0. } ) /\ ( B \ { .0. } ) C_ B ) -> ( 0g ` ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) ) = .1. )
33 20 27 28 32 syl3anc 
 |-  ( ( R e. Ring /\ ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) e. Grp ) -> ( 0g ` ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) ) = .1. )
34 33 adantr 
 |-  ( ( ( R e. Ring /\ ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) e. Grp ) /\ x e. ( Base ` ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) ) ) -> ( 0g ` ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) ) = .1. )
35 17 34 eqtrd 
 |-  ( ( ( R e. Ring /\ ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) e. Grp ) /\ x e. ( Base ` ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) ) ) -> ( ( ( invg ` ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) ) ` x ) ( +g ` ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) ) x ) = .1. )
36 9 13 35 rspcedvdw 
 |-  ( ( ( R e. Ring /\ ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) e. Grp ) /\ x e. ( Base ` ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) ) ) -> E. y e. ( Base ` ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) ) ( y ( +g ` ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) ) x ) = .1. )
37 7 36 sylan2b 
 |-  ( ( ( R e. Ring /\ ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) e. Grp ) /\ x e. ( B \ { .0. } ) ) -> E. y e. ( Base ` ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) ) ( y ( +g ` ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) ) x ) = .1. )
38 5 a1i 
 |-  ( ( ( R e. Ring /\ ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) e. Grp ) /\ x e. ( B \ { .0. } ) ) -> ( Base ` ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) ) = ( B \ { .0. } ) )
39 38 rexeqdv 
 |-  ( ( ( R e. Ring /\ ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) e. Grp ) /\ x e. ( B \ { .0. } ) ) -> ( E. y e. ( Base ` ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) ) ( y ( +g ` ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) ) x ) = .1. <-> E. y e. ( B \ { .0. } ) ( y ( +g ` ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) ) x ) = .1. ) )
40 18 4 mgpplusg 
 |-  .x. = ( +g ` ( mulGrp ` R ) )
41 1 fvexi 
 |-  B e. _V
42 41 difexi 
 |-  ( B \ { .0. } ) e. _V
43 eqid 
 |-  ( +g ` ( mulGrp ` R ) ) = ( +g ` ( mulGrp ` R ) )
44 23 43 ressplusg 
 |-  ( ( B \ { .0. } ) e. _V -> ( +g ` ( mulGrp ` R ) ) = ( +g ` ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) ) )
45 42 44 ax-mp 
 |-  ( +g ` ( mulGrp ` R ) ) = ( +g ` ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) )
46 40 45 eqtr2i 
 |-  ( +g ` ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) ) = .x.
47 46 oveqi 
 |-  ( y ( +g ` ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) ) x ) = ( y .x. x )
48 47 eqeq1i 
 |-  ( ( y ( +g ` ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) ) x ) = .1. <-> ( y .x. x ) = .1. )
49 48 rexbii 
 |-  ( E. y e. ( B \ { .0. } ) ( y ( +g ` ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) ) x ) = .1. <-> E. y e. ( B \ { .0. } ) ( y .x. x ) = .1. )
50 39 49 bitrdi 
 |-  ( ( ( R e. Ring /\ ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) e. Grp ) /\ x e. ( B \ { .0. } ) ) -> ( E. y e. ( Base ` ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) ) ( y ( +g ` ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) ) x ) = .1. <-> E. y e. ( B \ { .0. } ) ( y .x. x ) = .1. ) )
51 37 50 mpbid 
 |-  ( ( ( R e. Ring /\ ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) e. Grp ) /\ x e. ( B \ { .0. } ) ) -> E. y e. ( B \ { .0. } ) ( y .x. x ) = .1. )
52 51 ralrimiva 
 |-  ( ( R e. Ring /\ ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) e. Grp ) -> A. x e. ( B \ { .0. } ) E. y e. ( B \ { .0. } ) ( y .x. x ) = .1. )