Step |
Hyp |
Ref |
Expression |
1 |
|
addclpr |
|- ( ( A e. P. /\ B e. P. ) -> ( A +P. B ) e. P. ) |
2 |
|
eleq1 |
|- ( ( A +P. B ) = ( A +P. C ) -> ( ( A +P. B ) e. P. <-> ( A +P. C ) e. P. ) ) |
3 |
|
dmplp |
|- dom +P. = ( P. X. P. ) |
4 |
|
0npr |
|- -. (/) e. P. |
5 |
3 4
|
ndmovrcl |
|- ( ( A +P. C ) e. P. -> ( A e. P. /\ C e. P. ) ) |
6 |
2 5
|
syl6bi |
|- ( ( A +P. B ) = ( A +P. C ) -> ( ( A +P. B ) e. P. -> ( A e. P. /\ C e. P. ) ) ) |
7 |
1 6
|
syl5com |
|- ( ( A e. P. /\ B e. P. ) -> ( ( A +P. B ) = ( A +P. C ) -> ( A e. P. /\ C e. P. ) ) ) |
8 |
|
ltapr |
|- ( A e. P. -> ( B ( A +P. B ) |
9 |
|
ltapr |
|- ( A e. P. -> ( C ( A +P. C ) |
10 |
8 9
|
orbi12d |
|- ( A e. P. -> ( ( B ( ( A +P. B ) |
11 |
10
|
notbid |
|- ( A e. P. -> ( -. ( B -. ( ( A +P. B ) |
12 |
11
|
ad2antrr |
|- ( ( ( A e. P. /\ B e. P. ) /\ ( A e. P. /\ C e. P. ) ) -> ( -. ( B -. ( ( A +P. B ) |
13 |
|
ltsopr |
|- |
14 |
|
sotrieq |
|- ( ( ( B = C <-> -. ( B |
15 |
13 14
|
mpan |
|- ( ( B e. P. /\ C e. P. ) -> ( B = C <-> -. ( B |
16 |
15
|
ad2ant2l |
|- ( ( ( A e. P. /\ B e. P. ) /\ ( A e. P. /\ C e. P. ) ) -> ( B = C <-> -. ( B |
17 |
|
addclpr |
|- ( ( A e. P. /\ C e. P. ) -> ( A +P. C ) e. P. ) |
18 |
|
sotrieq |
|- ( ( ( ( A +P. B ) = ( A +P. C ) <-> -. ( ( A +P. B ) |
19 |
13 18
|
mpan |
|- ( ( ( A +P. B ) e. P. /\ ( A +P. C ) e. P. ) -> ( ( A +P. B ) = ( A +P. C ) <-> -. ( ( A +P. B ) |
20 |
1 17 19
|
syl2an |
|- ( ( ( A e. P. /\ B e. P. ) /\ ( A e. P. /\ C e. P. ) ) -> ( ( A +P. B ) = ( A +P. C ) <-> -. ( ( A +P. B ) |
21 |
12 16 20
|
3bitr4d |
|- ( ( ( A e. P. /\ B e. P. ) /\ ( A e. P. /\ C e. P. ) ) -> ( B = C <-> ( A +P. B ) = ( A +P. C ) ) ) |
22 |
21
|
exbiri |
|- ( ( A e. P. /\ B e. P. ) -> ( ( A e. P. /\ C e. P. ) -> ( ( A +P. B ) = ( A +P. C ) -> B = C ) ) ) |
23 |
7 22
|
syld |
|- ( ( A e. P. /\ B e. P. ) -> ( ( A +P. B ) = ( A +P. C ) -> ( ( A +P. B ) = ( A +P. C ) -> B = C ) ) ) |
24 |
23
|
pm2.43d |
|- ( ( A e. P. /\ B e. P. ) -> ( ( A +P. B ) = ( A +P. C ) -> B = C ) ) |