Step |
Hyp |
Ref |
Expression |
1 |
|
df-nr |
|- R. = ( ( P. X. P. ) /. ~R ) |
2 |
|
oveq1 |
|- ( [ <. x , y >. ] ~R = A -> ( [ <. x , y >. ] ~R +R 0R ) = ( A +R 0R ) ) |
3 |
|
id |
|- ( [ <. x , y >. ] ~R = A -> [ <. x , y >. ] ~R = A ) |
4 |
2 3
|
eqeq12d |
|- ( [ <. x , y >. ] ~R = A -> ( ( [ <. x , y >. ] ~R +R 0R ) = [ <. x , y >. ] ~R <-> ( A +R 0R ) = A ) ) |
5 |
|
df-0r |
|- 0R = [ <. 1P , 1P >. ] ~R |
6 |
5
|
oveq2i |
|- ( [ <. x , y >. ] ~R +R 0R ) = ( [ <. x , y >. ] ~R +R [ <. 1P , 1P >. ] ~R ) |
7 |
|
1pr |
|- 1P e. P. |
8 |
|
addsrpr |
|- ( ( ( x e. P. /\ y e. P. ) /\ ( 1P e. P. /\ 1P e. P. ) ) -> ( [ <. x , y >. ] ~R +R [ <. 1P , 1P >. ] ~R ) = [ <. ( x +P. 1P ) , ( y +P. 1P ) >. ] ~R ) |
9 |
7 7 8
|
mpanr12 |
|- ( ( x e. P. /\ y e. P. ) -> ( [ <. x , y >. ] ~R +R [ <. 1P , 1P >. ] ~R ) = [ <. ( x +P. 1P ) , ( y +P. 1P ) >. ] ~R ) |
10 |
|
addclpr |
|- ( ( x e. P. /\ 1P e. P. ) -> ( x +P. 1P ) e. P. ) |
11 |
7 10
|
mpan2 |
|- ( x e. P. -> ( x +P. 1P ) e. P. ) |
12 |
|
addclpr |
|- ( ( y e. P. /\ 1P e. P. ) -> ( y +P. 1P ) e. P. ) |
13 |
7 12
|
mpan2 |
|- ( y e. P. -> ( y +P. 1P ) e. P. ) |
14 |
11 13
|
anim12i |
|- ( ( x e. P. /\ y e. P. ) -> ( ( x +P. 1P ) e. P. /\ ( y +P. 1P ) e. P. ) ) |
15 |
|
vex |
|- x e. _V |
16 |
|
vex |
|- y e. _V |
17 |
7
|
elexi |
|- 1P e. _V |
18 |
|
addcompr |
|- ( z +P. w ) = ( w +P. z ) |
19 |
|
addasspr |
|- ( ( z +P. w ) +P. v ) = ( z +P. ( w +P. v ) ) |
20 |
15 16 17 18 19
|
caov12 |
|- ( x +P. ( y +P. 1P ) ) = ( y +P. ( x +P. 1P ) ) |
21 |
|
enreceq |
|- ( ( ( x e. P. /\ y e. P. ) /\ ( ( x +P. 1P ) e. P. /\ ( y +P. 1P ) e. P. ) ) -> ( [ <. x , y >. ] ~R = [ <. ( x +P. 1P ) , ( y +P. 1P ) >. ] ~R <-> ( x +P. ( y +P. 1P ) ) = ( y +P. ( x +P. 1P ) ) ) ) |
22 |
20 21
|
mpbiri |
|- ( ( ( x e. P. /\ y e. P. ) /\ ( ( x +P. 1P ) e. P. /\ ( y +P. 1P ) e. P. ) ) -> [ <. x , y >. ] ~R = [ <. ( x +P. 1P ) , ( y +P. 1P ) >. ] ~R ) |
23 |
14 22
|
mpdan |
|- ( ( x e. P. /\ y e. P. ) -> [ <. x , y >. ] ~R = [ <. ( x +P. 1P ) , ( y +P. 1P ) >. ] ~R ) |
24 |
9 23
|
eqtr4d |
|- ( ( x e. P. /\ y e. P. ) -> ( [ <. x , y >. ] ~R +R [ <. 1P , 1P >. ] ~R ) = [ <. x , y >. ] ~R ) |
25 |
6 24
|
eqtrid |
|- ( ( x e. P. /\ y e. P. ) -> ( [ <. x , y >. ] ~R +R 0R ) = [ <. x , y >. ] ~R ) |
26 |
1 4 25
|
ecoptocl |
|- ( A e. R. -> ( A +R 0R ) = A ) |