Metamath Proof Explorer

Theorem xpcan

Description: Cancellation law for Cartesian product. (Contributed by NM, 30-Aug-2011)

Ref Expression
Assertion xpcan ⊢C≠∅→C×A=C×B↔A=B

Proof

Step Hyp Ref Expression
1 xp11 ⊢C≠∅∧A≠∅→C×A=C×B↔C=C∧A=B
2 eqid ⊢C=C
3 2 biantrur ⊢A=B↔C=C∧A=B
4 1 3 bitr4di ⊢C≠∅∧A≠∅→C×A=C×B↔A=B
5 nne ⊢¬A≠∅↔A=∅
6 simpr ⊢C≠∅∧A=∅→A=∅
7 xpeq2 ⊢A=∅→C×A=C×∅
8 xp0 ⊢C×∅=∅
9 7 8 eqtrdi ⊢A=∅→C×A=∅
10 9 eqeq1d ⊢A=∅→C×A=C×B↔∅=C×B
11 eqcom ⊢∅=C×B↔C×B=∅
12 10 11 bitrdi ⊢A=∅→C×A=C×B↔C×B=∅
13 12 adantl ⊢C≠∅∧A=∅→C×A=C×B↔C×B=∅
14 df-ne ⊢C≠∅↔¬C=∅
15 xpeq0 ⊢C×B=∅↔C=∅∨B=∅
16 orel1 ⊢¬C=∅→C=∅∨B=∅→B=∅
17 15 16 biimtrid ⊢¬C=∅→C×B=∅→B=∅
18 14 17 sylbi ⊢C≠∅→C×B=∅→B=∅
19 18 adantr ⊢C≠∅∧A=∅→C×B=∅→B=∅
20 13 19 sylbid ⊢C≠∅∧A=∅→C×A=C×B→B=∅
21 eqtr3 ⊢A=∅∧B=∅→A=B
22 6 20 21 syl6an ⊢C≠∅∧A=∅→C×A=C×B→A=B
23 5 22 sylan2b ⊢C≠∅∧¬A≠∅→C×A=C×B→A=B
24 xpeq2 ⊢A=B→C×A=C×B
25 23 24 impbid1 ⊢C≠∅∧¬A≠∅→C×A=C×B↔A=B
26 4 25 pm2.61dan ⊢C≠∅→C×A=C×B↔A=B