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

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 a1i 
 |-  ( ( R e. Ring /\ .1. =/= .0. /\ A. x e. ( B \ { .0. } ) E. y e. ( B \ { .0. } ) ( y .x. x ) = .1. ) -> ( B \ { .0. } ) = ( Base ` ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) ) )
8 1 fvexi 
 |-  B e. _V
9 8 a1i 
 |-  ( ( R e. Ring /\ .1. =/= .0. /\ A. x e. ( B \ { .0. } ) E. y e. ( B \ { .0. } ) ( y .x. x ) = .1. ) -> B e. _V )
10 9 difexd 
 |-  ( ( R e. Ring /\ .1. =/= .0. /\ A. x e. ( B \ { .0. } ) E. y e. ( B \ { .0. } ) ( y .x. x ) = .1. ) -> ( B \ { .0. } ) e. _V )
11 eqid 
 |-  ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) = ( ( mulGrp ` R ) |`s ( B \ { .0. } ) )
12 eqid 
 |-  ( mulGrp ` R ) = ( mulGrp ` R )
13 12 4 mgpplusg 
 |-  .x. = ( +g ` ( mulGrp ` R ) )
14 11 13 ressplusg 
 |-  ( ( B \ { .0. } ) e. _V -> .x. = ( +g ` ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) ) )
15 10 14 syl 
 |-  ( ( R e. Ring /\ .1. =/= .0. /\ A. x e. ( B \ { .0. } ) E. y e. ( B \ { .0. } ) ( y .x. x ) = .1. ) -> .x. = ( +g ` ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) ) )
16 simp1 
 |-  ( ( R e. Ring /\ .1. =/= .0. /\ A. x e. ( B \ { .0. } ) E. y e. ( B \ { .0. } ) ( y .x. x ) = .1. ) -> R e. Ring )
17 eldifi 
 |-  ( a e. ( B \ { .0. } ) -> a e. B )
18 eldifi 
 |-  ( b e. ( B \ { .0. } ) -> b e. B )
19 1 4 ringcl 
 |-  ( ( R e. Ring /\ a e. B /\ b e. B ) -> ( a .x. b ) e. B )
20 16 17 18 19 syl3an 
 |-  ( ( ( R e. Ring /\ .1. =/= .0. /\ A. x e. ( B \ { .0. } ) E. y e. ( B \ { .0. } ) ( y .x. x ) = .1. ) /\ a e. ( B \ { .0. } ) /\ b e. ( B \ { .0. } ) ) -> ( a .x. b ) e. B )
21 oveq2 
 |-  ( x = a -> ( y .x. x ) = ( y .x. a ) )
22 21 eqeq1d 
 |-  ( x = a -> ( ( y .x. x ) = .1. <-> ( y .x. a ) = .1. ) )
23 22 rexbidv 
 |-  ( x = a -> ( E. y e. ( B \ { .0. } ) ( y .x. x ) = .1. <-> E. y e. ( B \ { .0. } ) ( y .x. a ) = .1. ) )
24 23 rspcv 
 |-  ( a e. ( B \ { .0. } ) -> ( A. x e. ( B \ { .0. } ) E. y e. ( B \ { .0. } ) ( y .x. x ) = .1. -> E. y e. ( B \ { .0. } ) ( y .x. a ) = .1. ) )
25 24 imdistanri 
 |-  ( ( A. x e. ( B \ { .0. } ) E. y e. ( B \ { .0. } ) ( y .x. x ) = .1. /\ a e. ( B \ { .0. } ) ) -> ( E. y e. ( B \ { .0. } ) ( y .x. a ) = .1. /\ a e. ( B \ { .0. } ) ) )
26 eldifsn 
 |-  ( b e. ( B \ { .0. } ) <-> ( b e. B /\ b =/= .0. ) )
27 simp1 
 |-  ( ( R e. Ring /\ a e. B /\ E. y e. ( B \ { .0. } ) ( y .x. a ) = .1. ) -> R e. Ring )
28 27 adantr 
 |-  ( ( ( R e. Ring /\ a e. B /\ E. y e. ( B \ { .0. } ) ( y .x. a ) = .1. ) /\ b e. B ) -> R e. Ring )
29 simpl2 
 |-  ( ( ( R e. Ring /\ a e. B /\ E. y e. ( B \ { .0. } ) ( y .x. a ) = .1. ) /\ b e. B ) -> a e. B )
30 difss 
 |-  ( B \ { .0. } ) C_ B
31 ssrexv 
 |-  ( ( B \ { .0. } ) C_ B -> ( E. y e. ( B \ { .0. } ) ( y .x. a ) = .1. -> E. y e. B ( y .x. a ) = .1. ) )
32 30 31 ax-mp 
 |-  ( E. y e. ( B \ { .0. } ) ( y .x. a ) = .1. -> E. y e. B ( y .x. a ) = .1. )
33 oveq1 
 |-  ( y = c -> ( y .x. a ) = ( c .x. a ) )
34 33 eqeq1d 
 |-  ( y = c -> ( ( y .x. a ) = .1. <-> ( c .x. a ) = .1. ) )
35 34 cbvrexvw 
 |-  ( E. y e. B ( y .x. a ) = .1. <-> E. c e. B ( c .x. a ) = .1. )
36 32 35 sylib 
 |-  ( E. y e. ( B \ { .0. } ) ( y .x. a ) = .1. -> E. c e. B ( c .x. a ) = .1. )
37 36 3ad2ant3 
 |-  ( ( R e. Ring /\ a e. B /\ E. y e. ( B \ { .0. } ) ( y .x. a ) = .1. ) -> E. c e. B ( c .x. a ) = .1. )
38 37 adantr 
 |-  ( ( ( R e. Ring /\ a e. B /\ E. y e. ( B \ { .0. } ) ( y .x. a ) = .1. ) /\ b e. B ) -> E. c e. B ( c .x. a ) = .1. )
39 simpr 
 |-  ( ( ( R e. Ring /\ a e. B /\ E. y e. ( B \ { .0. } ) ( y .x. a ) = .1. ) /\ b e. B ) -> b e. B )
40 1 4 3 2 28 29 38 39 ringinvnzdiv 
 |-  ( ( ( R e. Ring /\ a e. B /\ E. y e. ( B \ { .0. } ) ( y .x. a ) = .1. ) /\ b e. B ) -> ( ( a .x. b ) = .0. <-> b = .0. ) )
41 40 biimpd 
 |-  ( ( ( R e. Ring /\ a e. B /\ E. y e. ( B \ { .0. } ) ( y .x. a ) = .1. ) /\ b e. B ) -> ( ( a .x. b ) = .0. -> b = .0. ) )
42 41 ex 
 |-  ( ( R e. Ring /\ a e. B /\ E. y e. ( B \ { .0. } ) ( y .x. a ) = .1. ) -> ( b e. B -> ( ( a .x. b ) = .0. -> b = .0. ) ) )
43 17 42 syl3an2 
 |-  ( ( R e. Ring /\ a e. ( B \ { .0. } ) /\ E. y e. ( B \ { .0. } ) ( y .x. a ) = .1. ) -> ( b e. B -> ( ( a .x. b ) = .0. -> b = .0. ) ) )
44 43 3expb 
 |-  ( ( R e. Ring /\ ( a e. ( B \ { .0. } ) /\ E. y e. ( B \ { .0. } ) ( y .x. a ) = .1. ) ) -> ( b e. B -> ( ( a .x. b ) = .0. -> b = .0. ) ) )
45 44 imp 
 |-  ( ( ( R e. Ring /\ ( a e. ( B \ { .0. } ) /\ E. y e. ( B \ { .0. } ) ( y .x. a ) = .1. ) ) /\ b e. B ) -> ( ( a .x. b ) = .0. -> b = .0. ) )
46 45 necon3d 
 |-  ( ( ( R e. Ring /\ ( a e. ( B \ { .0. } ) /\ E. y e. ( B \ { .0. } ) ( y .x. a ) = .1. ) ) /\ b e. B ) -> ( b =/= .0. -> ( a .x. b ) =/= .0. ) )
47 46 impr 
 |-  ( ( ( R e. Ring /\ ( a e. ( B \ { .0. } ) /\ E. y e. ( B \ { .0. } ) ( y .x. a ) = .1. ) ) /\ ( b e. B /\ b =/= .0. ) ) -> ( a .x. b ) =/= .0. )
48 26 47 sylan2b 
 |-  ( ( ( R e. Ring /\ ( a e. ( B \ { .0. } ) /\ E. y e. ( B \ { .0. } ) ( y .x. a ) = .1. ) ) /\ b e. ( B \ { .0. } ) ) -> ( a .x. b ) =/= .0. )
49 48 an32s 
 |-  ( ( ( R e. Ring /\ b e. ( B \ { .0. } ) ) /\ ( a e. ( B \ { .0. } ) /\ E. y e. ( B \ { .0. } ) ( y .x. a ) = .1. ) ) -> ( a .x. b ) =/= .0. )
50 49 ancom2s 
 |-  ( ( ( R e. Ring /\ b e. ( B \ { .0. } ) ) /\ ( E. y e. ( B \ { .0. } ) ( y .x. a ) = .1. /\ a e. ( B \ { .0. } ) ) ) -> ( a .x. b ) =/= .0. )
51 25 50 sylan2 
 |-  ( ( ( R e. Ring /\ b e. ( B \ { .0. } ) ) /\ ( A. x e. ( B \ { .0. } ) E. y e. ( B \ { .0. } ) ( y .x. x ) = .1. /\ a e. ( B \ { .0. } ) ) ) -> ( a .x. b ) =/= .0. )
52 51 an42s 
 |-  ( ( ( R e. Ring /\ A. x e. ( B \ { .0. } ) E. y e. ( B \ { .0. } ) ( y .x. x ) = .1. ) /\ ( a e. ( B \ { .0. } ) /\ b e. ( B \ { .0. } ) ) ) -> ( a .x. b ) =/= .0. )
53 52 exp32 
 |-  ( ( R e. Ring /\ A. x e. ( B \ { .0. } ) E. y e. ( B \ { .0. } ) ( y .x. x ) = .1. ) -> ( a e. ( B \ { .0. } ) -> ( b e. ( B \ { .0. } ) -> ( a .x. b ) =/= .0. ) ) )
54 53 3adant2 
 |-  ( ( R e. Ring /\ .1. =/= .0. /\ A. x e. ( B \ { .0. } ) E. y e. ( B \ { .0. } ) ( y .x. x ) = .1. ) -> ( a e. ( B \ { .0. } ) -> ( b e. ( B \ { .0. } ) -> ( a .x. b ) =/= .0. ) ) )
55 54 3imp 
 |-  ( ( ( R e. Ring /\ .1. =/= .0. /\ A. x e. ( B \ { .0. } ) E. y e. ( B \ { .0. } ) ( y .x. x ) = .1. ) /\ a e. ( B \ { .0. } ) /\ b e. ( B \ { .0. } ) ) -> ( a .x. b ) =/= .0. )
56 20 55 eldifsnd 
 |-  ( ( ( R e. Ring /\ .1. =/= .0. /\ A. x e. ( B \ { .0. } ) E. y e. ( B \ { .0. } ) ( y .x. x ) = .1. ) /\ a e. ( B \ { .0. } ) /\ b e. ( B \ { .0. } ) ) -> ( a .x. b ) e. ( B \ { .0. } ) )
57 eldifi 
 |-  ( c e. ( B \ { .0. } ) -> c e. B )
58 17 18 57 3anim123i 
 |-  ( ( a e. ( B \ { .0. } ) /\ b e. ( B \ { .0. } ) /\ c e. ( B \ { .0. } ) ) -> ( a e. B /\ b e. B /\ c e. B ) )
59 1 4 ringass 
 |-  ( ( R e. Ring /\ ( a e. B /\ b e. B /\ c e. B ) ) -> ( ( a .x. b ) .x. c ) = ( a .x. ( b .x. c ) ) )
60 16 58 59 syl2an 
 |-  ( ( ( R e. Ring /\ .1. =/= .0. /\ A. x e. ( B \ { .0. } ) E. y e. ( B \ { .0. } ) ( y .x. x ) = .1. ) /\ ( a e. ( B \ { .0. } ) /\ b e. ( B \ { .0. } ) /\ c e. ( B \ { .0. } ) ) ) -> ( ( a .x. b ) .x. c ) = ( a .x. ( b .x. c ) ) )
61 1 3 ringidcl 
 |-  ( R e. Ring -> .1. e. B )
62 nelsn 
 |-  ( .1. =/= .0. -> -. .1. e. { .0. } )
63 61 62 anim12i 
 |-  ( ( R e. Ring /\ .1. =/= .0. ) -> ( .1. e. B /\ -. .1. e. { .0. } ) )
64 eldif 
 |-  ( .1. e. ( B \ { .0. } ) <-> ( .1. e. B /\ -. .1. e. { .0. } ) )
65 63 64 sylibr 
 |-  ( ( R e. Ring /\ .1. =/= .0. ) -> .1. e. ( B \ { .0. } ) )
66 65 3adant3 
 |-  ( ( R e. Ring /\ .1. =/= .0. /\ A. x e. ( B \ { .0. } ) E. y e. ( B \ { .0. } ) ( y .x. x ) = .1. ) -> .1. e. ( B \ { .0. } ) )
67 1 4 3 ringlidm 
 |-  ( ( R e. Ring /\ a e. B ) -> ( .1. .x. a ) = a )
68 16 17 67 syl2an 
 |-  ( ( ( R e. Ring /\ .1. =/= .0. /\ A. x e. ( B \ { .0. } ) E. y e. ( B \ { .0. } ) ( y .x. x ) = .1. ) /\ a e. ( B \ { .0. } ) ) -> ( .1. .x. a ) = a )
69 oveq1 
 |-  ( y = b -> ( y .x. a ) = ( b .x. a ) )
70 69 eqeq1d 
 |-  ( y = b -> ( ( y .x. a ) = .1. <-> ( b .x. a ) = .1. ) )
71 70 cbvrexvw 
 |-  ( E. y e. ( B \ { .0. } ) ( y .x. a ) = .1. <-> E. b e. ( B \ { .0. } ) ( b .x. a ) = .1. )
72 23 71 bitrdi 
 |-  ( x = a -> ( E. y e. ( B \ { .0. } ) ( y .x. x ) = .1. <-> E. b e. ( B \ { .0. } ) ( b .x. a ) = .1. ) )
73 72 rspccv 
 |-  ( A. x e. ( B \ { .0. } ) E. y e. ( B \ { .0. } ) ( y .x. x ) = .1. -> ( a e. ( B \ { .0. } ) -> E. b e. ( B \ { .0. } ) ( b .x. a ) = .1. ) )
74 73 3ad2ant3 
 |-  ( ( R e. Ring /\ .1. =/= .0. /\ A. x e. ( B \ { .0. } ) E. y e. ( B \ { .0. } ) ( y .x. x ) = .1. ) -> ( a e. ( B \ { .0. } ) -> E. b e. ( B \ { .0. } ) ( b .x. a ) = .1. ) )
75 74 imp 
 |-  ( ( ( R e. Ring /\ .1. =/= .0. /\ A. x e. ( B \ { .0. } ) E. y e. ( B \ { .0. } ) ( y .x. x ) = .1. ) /\ a e. ( B \ { .0. } ) ) -> E. b e. ( B \ { .0. } ) ( b .x. a ) = .1. )
76 7 15 56 60 66 68 75 isgrpde 
 |-  ( ( R e. Ring /\ .1. =/= .0. /\ A. x e. ( B \ { .0. } ) E. y e. ( B \ { .0. } ) ( y .x. x ) = .1. ) -> ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) e. Grp )