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	syl5bi	⊢ ( ¬ 𝐶 = ∅ → ( ( 𝐵 × 𝐶 ) = ∅ → 𝐵 = ∅ ) )
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	⊢ ( 𝐶 ≠ ∅ → ( ( 𝐴 × 𝐶 ) = ( 𝐵 × 𝐶 ) ↔ 𝐴 = 𝐵 ) )