Step |
Hyp |
Ref |
Expression |
1 |
|
enrer |
|- ~R Er ( P. X. P. ) |
2 |
|
erdm |
|- ( ~R Er ( P. X. P. ) -> dom ~R = ( P. X. P. ) ) |
3 |
1 2
|
ax-mp |
|- dom ~R = ( P. X. P. ) |
4 |
|
df-nr |
|- R. = ( ( P. X. P. ) /. ~R ) |
5 |
|
ltrelsr |
|- |
6 |
|
ltrelpr |
|- |
7 |
|
0npr |
|- -. (/) e. P. |
8 |
|
dmplp |
|- dom +P. = ( P. X. P. ) |
9 |
|
enrex |
|- ~R e. _V |
10 |
|
df-ltr |
|- . | ( ( x e. R. /\ y e. R. ) /\ E. z E. w E. v E. u ( ( x = [ <. z , w >. ] ~R /\ y = [ <. v , u >. ] ~R ) /\ ( z +P. u ) |
11 |
|
addclpr |
|- ( ( w e. P. /\ v e. P. ) -> ( w +P. v ) e. P. ) |
12 |
11
|
ad2ant2lr |
|- ( ( ( z e. P. /\ w e. P. ) /\ ( v e. P. /\ u e. P. ) ) -> ( w +P. v ) e. P. ) |
13 |
|
addclpr |
|- ( ( B e. P. /\ C e. P. ) -> ( B +P. C ) e. P. ) |
14 |
13
|
ad2ant2lr |
|- ( ( ( A e. P. /\ B e. P. ) /\ ( C e. P. /\ D e. P. ) ) -> ( B +P. C ) e. P. ) |
15 |
12 14
|
anim12ci |
|- ( ( ( ( z e. P. /\ w e. P. ) /\ ( v e. P. /\ u e. P. ) ) /\ ( ( A e. P. /\ B e. P. ) /\ ( C e. P. /\ D e. P. ) ) ) -> ( ( B +P. C ) e. P. /\ ( w +P. v ) e. P. ) ) |
16 |
15
|
an4s |
|- ( ( ( ( z e. P. /\ w e. P. ) /\ ( A e. P. /\ B e. P. ) ) /\ ( ( v e. P. /\ u e. P. ) /\ ( C e. P. /\ D e. P. ) ) ) -> ( ( B +P. C ) e. P. /\ ( w +P. v ) e. P. ) ) |
17 |
|
enreceq |
|- ( ( ( z e. P. /\ w e. P. ) /\ ( A e. P. /\ B e. P. ) ) -> ( [ <. z , w >. ] ~R = [ <. A , B >. ] ~R <-> ( z +P. B ) = ( w +P. A ) ) ) |
18 |
|
enreceq |
|- ( ( ( v e. P. /\ u e. P. ) /\ ( C e. P. /\ D e. P. ) ) -> ( [ <. v , u >. ] ~R = [ <. C , D >. ] ~R <-> ( v +P. D ) = ( u +P. C ) ) ) |
19 |
|
eqcom |
|- ( ( v +P. D ) = ( u +P. C ) <-> ( u +P. C ) = ( v +P. D ) ) |
20 |
18 19
|
bitrdi |
|- ( ( ( v e. P. /\ u e. P. ) /\ ( C e. P. /\ D e. P. ) ) -> ( [ <. v , u >. ] ~R = [ <. C , D >. ] ~R <-> ( u +P. C ) = ( v +P. D ) ) ) |
21 |
17 20
|
bi2anan9 |
|- ( ( ( ( z e. P. /\ w e. P. ) /\ ( A e. P. /\ B e. P. ) ) /\ ( ( v e. P. /\ u e. P. ) /\ ( C e. P. /\ D e. P. ) ) ) -> ( ( [ <. z , w >. ] ~R = [ <. A , B >. ] ~R /\ [ <. v , u >. ] ~R = [ <. C , D >. ] ~R ) <-> ( ( z +P. B ) = ( w +P. A ) /\ ( u +P. C ) = ( v +P. D ) ) ) ) |
22 |
|
oveq12 |
|- ( ( ( z +P. B ) = ( w +P. A ) /\ ( u +P. C ) = ( v +P. D ) ) -> ( ( z +P. B ) +P. ( u +P. C ) ) = ( ( w +P. A ) +P. ( v +P. D ) ) ) |
23 |
|
addcompr |
|- ( u +P. B ) = ( B +P. u ) |
24 |
23
|
oveq1i |
|- ( ( u +P. B ) +P. C ) = ( ( B +P. u ) +P. C ) |
25 |
|
addasspr |
|- ( ( u +P. B ) +P. C ) = ( u +P. ( B +P. C ) ) |
26 |
|
addasspr |
|- ( ( B +P. u ) +P. C ) = ( B +P. ( u +P. C ) ) |
27 |
24 25 26
|
3eqtr3i |
|- ( u +P. ( B +P. C ) ) = ( B +P. ( u +P. C ) ) |
28 |
27
|
oveq2i |
|- ( z +P. ( u +P. ( B +P. C ) ) ) = ( z +P. ( B +P. ( u +P. C ) ) ) |
29 |
|
addasspr |
|- ( ( z +P. u ) +P. ( B +P. C ) ) = ( z +P. ( u +P. ( B +P. C ) ) ) |
30 |
|
addasspr |
|- ( ( z +P. B ) +P. ( u +P. C ) ) = ( z +P. ( B +P. ( u +P. C ) ) ) |
31 |
28 29 30
|
3eqtr4i |
|- ( ( z +P. u ) +P. ( B +P. C ) ) = ( ( z +P. B ) +P. ( u +P. C ) ) |
32 |
|
addcompr |
|- ( v +P. A ) = ( A +P. v ) |
33 |
32
|
oveq1i |
|- ( ( v +P. A ) +P. D ) = ( ( A +P. v ) +P. D ) |
34 |
|
addasspr |
|- ( ( v +P. A ) +P. D ) = ( v +P. ( A +P. D ) ) |
35 |
|
addasspr |
|- ( ( A +P. v ) +P. D ) = ( A +P. ( v +P. D ) ) |
36 |
33 34 35
|
3eqtr3i |
|- ( v +P. ( A +P. D ) ) = ( A +P. ( v +P. D ) ) |
37 |
36
|
oveq2i |
|- ( w +P. ( v +P. ( A +P. D ) ) ) = ( w +P. ( A +P. ( v +P. D ) ) ) |
38 |
|
addasspr |
|- ( ( w +P. v ) +P. ( A +P. D ) ) = ( w +P. ( v +P. ( A +P. D ) ) ) |
39 |
|
addasspr |
|- ( ( w +P. A ) +P. ( v +P. D ) ) = ( w +P. ( A +P. ( v +P. D ) ) ) |
40 |
37 38 39
|
3eqtr4i |
|- ( ( w +P. v ) +P. ( A +P. D ) ) = ( ( w +P. A ) +P. ( v +P. D ) ) |
41 |
22 31 40
|
3eqtr4g |
|- ( ( ( z +P. B ) = ( w +P. A ) /\ ( u +P. C ) = ( v +P. D ) ) -> ( ( z +P. u ) +P. ( B +P. C ) ) = ( ( w +P. v ) +P. ( A +P. D ) ) ) |
42 |
21 41
|
syl6bi |
|- ( ( ( ( z e. P. /\ w e. P. ) /\ ( A e. P. /\ B e. P. ) ) /\ ( ( v e. P. /\ u e. P. ) /\ ( C e. P. /\ D e. P. ) ) ) -> ( ( [ <. z , w >. ] ~R = [ <. A , B >. ] ~R /\ [ <. v , u >. ] ~R = [ <. C , D >. ] ~R ) -> ( ( z +P. u ) +P. ( B +P. C ) ) = ( ( w +P. v ) +P. ( A +P. D ) ) ) ) |
43 |
|
ovex |
|- ( z +P. u ) e. _V |
44 |
|
ovex |
|- ( B +P. C ) e. _V |
45 |
|
ltapr |
|- ( f e. P. -> ( x ( f +P. x ) |
46 |
|
ovex |
|- ( w +P. v ) e. _V |
47 |
|
addcompr |
|- ( x +P. y ) = ( y +P. x ) |
48 |
|
ovex |
|- ( A +P. D ) e. _V |
49 |
43 44 45 46 47 48
|
caovord3 |
|- ( ( ( ( B +P. C ) e. P. /\ ( w +P. v ) e. P. ) /\ ( ( z +P. u ) +P. ( B +P. C ) ) = ( ( w +P. v ) +P. ( A +P. D ) ) ) -> ( ( z +P. u ) ( A +P. D ) |
50 |
16 42 49
|
syl6an |
|- ( ( ( ( z e. P. /\ w e. P. ) /\ ( A e. P. /\ B e. P. ) ) /\ ( ( v e. P. /\ u e. P. ) /\ ( C e. P. /\ D e. P. ) ) ) -> ( ( [ <. z , w >. ] ~R = [ <. A , B >. ] ~R /\ [ <. v , u >. ] ~R = [ <. C , D >. ] ~R ) -> ( ( z +P. u ) ( A +P. D ) |
51 |
9 1 4 10 50
|
brecop |
|- ( ( ( A e. P. /\ B e. P. ) /\ ( C e. P. /\ D e. P. ) ) -> ( [ <. A , B >. ] ~R . ] ~R <-> ( A +P. D ) |
52 |
3 4 5 6 7 8 51
|
brecop2 |
|- ( [ <. A , B >. ] ~R . ] ~R <-> ( A +P. D ) |