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
|
eqtrid |
|- ( -. 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
|
eqtrdi |
|- ( -. 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. ) } |