This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem xpcan2

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

Ref Expression
Assertion xpcan2 ( 𝐶 ≠ ∅ → ( ( 𝐴 × 𝐶 ) = ( 𝐵 × 𝐶 ) ↔ 𝐴 = 𝐵 ) )

Proof

Step Hyp Ref Expression
1 xp11 ⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐶 ≠ ∅ ) → ( ( 𝐴 × 𝐶 ) = ( 𝐵 × 𝐶 ) ↔ ( 𝐴 = 𝐵 ∧ 𝐶 = 𝐶 ) ) )
2 eqid ⊢ 𝐶 = 𝐶
3 2 biantru ⊢ ( 𝐴 = 𝐵 ↔ ( 𝐴 = 𝐵 ∧ 𝐶 = 𝐶 ) )
4 1 3 bitr4di ⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐶 ≠ ∅ ) → ( ( 𝐴 × 𝐶 ) = ( 𝐵 × 𝐶 ) ↔ 𝐴 = 𝐵 ) )
5 nne ⊢ ( ¬ 𝐴 ≠ ∅ ↔ 𝐴 = ∅ )
6 simpl ⊢ ( ( 𝐴 = ∅ ∧ 𝐶 ≠ ∅ ) → 𝐴 = ∅ )
7 xpeq1 ⊢ ( 𝐴 = ∅ → ( 𝐴 × 𝐶 ) = ( ∅ × 𝐶 ) )
8 0xp ⊢ ( ∅ × 𝐶 ) = ∅
9 7 8 eqtrdi ⊢ ( 𝐴 = ∅ → ( 𝐴 × 𝐶 ) = ∅ )
10 9 eqeq1d ⊢ ( 𝐴 = ∅ → ( ( 𝐴 × 𝐶 ) = ( 𝐵 × 𝐶 ) ↔ ∅ = ( 𝐵 × 𝐶 ) ) )
11 eqcom ⊢ ( ∅ = ( 𝐵 × 𝐶 ) ↔ ( 𝐵 × 𝐶 ) = ∅ )
12 10 11 bitrdi ⊢ ( 𝐴 = ∅ → ( ( 𝐴 × 𝐶 ) = ( 𝐵 × 𝐶 ) ↔ ( 𝐵 × 𝐶 ) = ∅ ) )
13 12 adantr ⊢ ( ( 𝐴 = ∅ ∧ 𝐶 ≠ ∅ ) → ( ( 𝐴 × 𝐶 ) = ( 𝐵 × 𝐶 ) ↔ ( 𝐵 × 𝐶 ) = ∅ ) )
14 df-ne ⊢ ( 𝐶 ≠ ∅ ↔ ¬ 𝐶 = ∅ )
15 xpeq0 ⊢ ( ( 𝐵 × 𝐶 ) = ∅ ↔ ( 𝐵 = ∅ ∨ 𝐶 = ∅ ) )
16 orel2 ⊢ ( ¬ 𝐶 = ∅ → ( ( 𝐵 = ∅ ∨ 𝐶 = ∅ ) → 𝐵 = ∅ ) )
17 15 16 biimtrid ⊢ ( ¬ 𝐶 = ∅ → ( ( 𝐵 × 𝐶 ) = ∅ → 𝐵 = ∅ ) )
18 14 17 sylbi ⊢ ( 𝐶 ≠ ∅ → ( ( 𝐵 × 𝐶 ) = ∅ → 𝐵 = ∅ ) )
19 18 adantl ⊢ ( ( 𝐴 = ∅ ∧ 𝐶 ≠ ∅ ) → ( ( 𝐵 × 𝐶 ) = ∅ → 𝐵 = ∅ ) )
20 13 19 sylbid ⊢ ( ( 𝐴 = ∅ ∧ 𝐶 ≠ ∅ ) → ( ( 𝐴 × 𝐶 ) = ( 𝐵 × 𝐶 ) → 𝐵 = ∅ ) )
21 eqtr3 ⊢ ( ( 𝐴 = ∅ ∧ 𝐵 = ∅ ) → 𝐴 = 𝐵 )
22 6 20 21 syl6an ⊢ ( ( 𝐴 = ∅ ∧ 𝐶 ≠ ∅ ) → ( ( 𝐴 × 𝐶 ) = ( 𝐵 × 𝐶 ) → 𝐴 = 𝐵 ) )
23 xpeq1 ⊢ ( 𝐴 = 𝐵 → ( 𝐴 × 𝐶 ) = ( 𝐵 × 𝐶 ) )
24 22 23 impbid1 ⊢ ( ( 𝐴 = ∅ ∧ 𝐶 ≠ ∅ ) → ( ( 𝐴 × 𝐶 ) = ( 𝐵 × 𝐶 ) ↔ 𝐴 = 𝐵 ) )
25 5 24 sylanb ⊢ ( ( ¬ 𝐴 ≠ ∅ ∧ 𝐶 ≠ ∅ ) → ( ( 𝐴 × 𝐶 ) = ( 𝐵 × 𝐶 ) ↔ 𝐴 = 𝐵 ) )
26 4 25 pm2.61ian ⊢ ( 𝐶 ≠ ∅ → ( ( 𝐴 × 𝐶 ) = ( 𝐵 × 𝐶 ) ↔ 𝐴 = 𝐵 ) )