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