| Step |
Hyp |
Ref |
Expression |
| 1 |
|
xp11 |
|- ( ( A =/= (/) /\ C =/= (/) ) -> ( ( A X. C ) = ( B X. C ) <-> ( A = B /\ C = C ) ) ) |
| 2 |
|
eqid |
|- C = C |
| 3 |
2
|
biantru |
|- ( A = B <-> ( A = B /\ C = C ) ) |
| 4 |
1 3
|
bitr4di |
|- ( ( A =/= (/) /\ C =/= (/) ) -> ( ( A X. C ) = ( B X. C ) <-> A = B ) ) |
| 5 |
|
nne |
|- ( -. A =/= (/) <-> A = (/) ) |
| 6 |
|
simpl |
|- ( ( A = (/) /\ C =/= (/) ) -> A = (/) ) |
| 7 |
|
xpeq1 |
|- ( A = (/) -> ( A X. C ) = ( (/) X. C ) ) |
| 8 |
|
0xp |
|- ( (/) X. C ) = (/) |
| 9 |
7 8
|
eqtrdi |
|- ( A = (/) -> ( A X. C ) = (/) ) |
| 10 |
9
|
eqeq1d |
|- ( A = (/) -> ( ( A X. C ) = ( B X. C ) <-> (/) = ( B X. C ) ) ) |
| 11 |
|
eqcom |
|- ( (/) = ( B X. C ) <-> ( B X. C ) = (/) ) |
| 12 |
10 11
|
bitrdi |
|- ( A = (/) -> ( ( A X. C ) = ( B X. C ) <-> ( B X. C ) = (/) ) ) |
| 13 |
12
|
adantr |
|- ( ( A = (/) /\ C =/= (/) ) -> ( ( A X. C ) = ( B X. C ) <-> ( B X. C ) = (/) ) ) |
| 14 |
|
df-ne |
|- ( C =/= (/) <-> -. C = (/) ) |
| 15 |
|
xpeq0 |
|- ( ( B X. C ) = (/) <-> ( B = (/) \/ C = (/) ) ) |
| 16 |
|
orel2 |
|- ( -. C = (/) -> ( ( B = (/) \/ C = (/) ) -> B = (/) ) ) |
| 17 |
15 16
|
biimtrid |
|- ( -. C = (/) -> ( ( B X. C ) = (/) -> B = (/) ) ) |
| 18 |
14 17
|
sylbi |
|- ( C =/= (/) -> ( ( B X. C ) = (/) -> B = (/) ) ) |
| 19 |
18
|
adantl |
|- ( ( A = (/) /\ C =/= (/) ) -> ( ( B X. C ) = (/) -> B = (/) ) ) |
| 20 |
13 19
|
sylbid |
|- ( ( A = (/) /\ C =/= (/) ) -> ( ( A X. C ) = ( B X. C ) -> B = (/) ) ) |
| 21 |
|
eqtr3 |
|- ( ( A = (/) /\ B = (/) ) -> A = B ) |
| 22 |
6 20 21
|
syl6an |
|- ( ( A = (/) /\ C =/= (/) ) -> ( ( A X. C ) = ( B X. C ) -> A = B ) ) |
| 23 |
|
xpeq1 |
|- ( A = B -> ( A X. C ) = ( B X. C ) ) |
| 24 |
22 23
|
impbid1 |
|- ( ( A = (/) /\ C =/= (/) ) -> ( ( A X. C ) = ( B X. C ) <-> A = B ) ) |
| 25 |
5 24
|
sylanb |
|- ( ( -. A =/= (/) /\ C =/= (/) ) -> ( ( A X. C ) = ( B X. C ) <-> A = B ) ) |
| 26 |
4 25
|
pm2.61ian |
|- ( C =/= (/) -> ( ( A X. C ) = ( B X. C ) <-> A = B ) ) |