Metamath Proof Explorer

Theorem rrgval

Description: Value of the set or left-regular elements in a ring. (Contributed by Stefan O'Rear, 22-Mar-2015)

Ref Expression
Hypotheses rrgval.e 
|- E = ( RLReg ` R )
rrgval.b 
|- B = ( Base ` R )
rrgval.t 
|- .x. = ( .r ` R )
rrgval.z 
|- .0. = ( 0g ` R )
Assertion rrgval 
|- E = { x e. B | A. y e. B ( ( x .x. y ) = .0. -> y = .0. ) }

Proof

Step Hyp Ref Expression
1 rrgval.e 
 |-  E = ( RLReg ` R )
2 rrgval.b 
 |-  B = ( Base ` R )
3 rrgval.t 
 |-  .x. = ( .r ` R )
4 rrgval.z 
 |-  .0. = ( 0g ` R )
5 fveq2 
 |-  ( r = R -> ( Base ` r ) = ( Base ` R ) )
6 5 2 eqtr4di 
 |-  ( r = R -> ( Base ` r ) = B )
7 fveq2 
 |-  ( r = R -> ( .r ` r ) = ( .r ` R ) )
8 7 3 eqtr4di 
 |-  ( r = R -> ( .r ` r ) = .x. )
9 8 oveqd 
 |-  ( r = R -> ( x ( .r ` r ) y ) = ( x .x. y ) )
10 fveq2 
 |-  ( r = R -> ( 0g ` r ) = ( 0g ` R ) )
11 10 4 eqtr4di 
 |-  ( r = R -> ( 0g ` r ) = .0. )
12 9 11 eqeq12d 
 |-  ( r = R -> ( ( x ( .r ` r ) y ) = ( 0g ` r ) <-> ( x .x. y ) = .0. ) )
13 11 eqeq2d 
 |-  ( r = R -> ( y = ( 0g ` r ) <-> y = .0. ) )
14 12 13 imbi12d 
 |-  ( r = R -> ( ( ( x ( .r ` r ) y ) = ( 0g ` r ) -> y = ( 0g ` r ) ) <-> ( ( x .x. y ) = .0. -> y = .0. ) ) )
15 6 14 raleqbidv 
 |-  ( r = R -> ( A. y e. ( Base ` r ) ( ( x ( .r ` r ) y ) = ( 0g ` r ) -> y = ( 0g ` r ) ) <-> A. y e. B ( ( x .x. y ) = .0. -> y = .0. ) ) )
16 6 15 rabeqbidv 
 |-  ( r = R -> { x e. ( Base ` r ) | A. y e. ( Base ` r ) ( ( x ( .r ` r ) y ) = ( 0g ` r ) -> y = ( 0g ` r ) ) } = { x e. B | A. y e. B ( ( x .x. y ) = .0. -> y = .0. ) } )
17 df-rlreg 
 |-  RLReg = ( r e. _V |-> { x e. ( Base ` r ) | A. y e. ( Base ` r ) ( ( x ( .r ` r ) y ) = ( 0g ` r ) -> y = ( 0g ` r ) ) } )
18 2 fvexi 
 |-  B e. _V
19 18 rabex 
 |-  { x e. B | A. y e. B ( ( x .x. y ) = .0. -> y = .0. ) } e. _V
20 16 17 19 fvmpt 
 |-  ( R e. _V -> ( RLReg ` R ) = { x e. B | A. y e. B ( ( x .x. y ) = .0. -> y = .0. ) } )
21 fvprc 
 |-  ( -. R e. _V -> ( RLReg ` R ) = (/) )
22 fvprc 
 |-  ( -. R e. _V -> ( Base ` R ) = (/) )
23 2 22 syl5eq 
 |-  ( -. R e. _V -> B = (/) )
24 23 rabeqdv 
 |-  ( -. R e. _V -> { x e. B | A. y e. B ( ( x .x. y ) = .0. -> y = .0. ) } = { x e. (/) | A. y e. B ( ( x .x. y ) = .0. -> y = .0. ) } )
25 rab0 
 |-  { x e. (/) | A. y e. B ( ( x .x. y ) = .0. -> y = .0. ) } = (/)
26 24 25 syl6eq 
 |-  ( -. R e. _V -> { x e. B | A. y e. B ( ( x .x. y ) = .0. -> y = .0. ) } = (/) )
27 21 26 eqtr4d 
 |-  ( -. R e. _V -> ( RLReg ` R ) = { x e. B | A. y e. B ( ( x .x. y ) = .0. -> y = .0. ) } )
28 20 27 pm2.61i 
 |-  ( RLReg ` R ) = { x e. B | A. y e. B ( ( x .x. y ) = .0. -> y = .0. ) }
29 1 28 eqtri 
 |-  E = { x e. B | A. y e. B ( ( x .x. y ) = .0. -> y = .0. ) }