Theorem xpcan2

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

	Ref	Expression
Assertion	xpcan2	$$⊢C\ne \varnothing \to \left(A\times C=B\times C\leftrightarrow A=B\right)$$

Proof

Step	Hyp	Ref	Expression
1		xp11	$$⊢\left(A\ne \varnothing \wedge C\ne \varnothing \right)\to \left(A\times C=B\times C\leftrightarrow \left(A=B\wedge C=C\right)\right)$$
2		eqid	$$⊢C=C$$
3	2	biantru	$$⊢A=B\leftrightarrow \left(A=B\wedge C=C\right)$$
4	1 3	bitr4di	$$⊢\left(A\ne \varnothing \wedge C\ne \varnothing \right)\to \left(A\times C=B\times C\leftrightarrow A=B\right)$$
5		nne	$$⊢\neg A\ne \varnothing \leftrightarrow A=\varnothing$$
6		simpl	$$⊢\left(A=\varnothing \wedge C\ne \varnothing \right)\to A=\varnothing$$
7		xpeq1	$$⊢A=\varnothing \to A\times C=\varnothing \times C$$
8		0xp	$$⊢\varnothing \times C=\varnothing$$
9	7 8	eqtrdi	$$⊢A=\varnothing \to A\times C=\varnothing$$
10	9	eqeq1d	$$⊢A=\varnothing \to \left(A\times C=B\times C\leftrightarrow \varnothing =B\times C\right)$$
11		eqcom	$$⊢\varnothing =B\times C\leftrightarrow B\times C=\varnothing$$
12	10 11	bitrdi	$$⊢A=\varnothing \to \left(A\times C=B\times C\leftrightarrow B\times C=\varnothing \right)$$
13	12	adantr	$$⊢\left(A=\varnothing \wedge C\ne \varnothing \right)\to \left(A\times C=B\times C\leftrightarrow B\times C=\varnothing \right)$$
14		df-ne	$$⊢C\ne \varnothing \leftrightarrow \neg C=\varnothing$$
15		xpeq0	$$⊢B\times C=\varnothing \leftrightarrow \left(B=\varnothing \vee C=\varnothing \right)$$
16		orel2	$$⊢\neg C=\varnothing \to \left(\left(B=\varnothing \vee C=\varnothing \right)\to B=\varnothing \right)$$
17	15 16	syl5bi	$$⊢\neg C=\varnothing \to \left(B\times C=\varnothing \to B=\varnothing \right)$$
18	14 17	sylbi	$$⊢C\ne \varnothing \to \left(B\times C=\varnothing \to B=\varnothing \right)$$
19	18	adantl	$$⊢\left(A=\varnothing \wedge C\ne \varnothing \right)\to \left(B\times C=\varnothing \to B=\varnothing \right)$$
20	13 19	sylbid	$$⊢\left(A=\varnothing \wedge C\ne \varnothing \right)\to \left(A\times C=B\times C\to B=\varnothing \right)$$
21		eqtr3	$$⊢\left(A=\varnothing \wedge B=\varnothing \right)\to A=B$$
22	6 20 21	syl6an	$$⊢\left(A=\varnothing \wedge C\ne \varnothing \right)\to \left(A\times C=B\times C\to A=B\right)$$
23		xpeq1	$$⊢A=B\to A\times C=B\times C$$
24	22 23	impbid1	$$⊢\left(A=\varnothing \wedge C\ne \varnothing \right)\to \left(A\times C=B\times C\leftrightarrow A=B\right)$$
25	5 24	sylanb	$$⊢\left(\neg A\ne \varnothing \wedge C\ne \varnothing \right)\to \left(A\times C=B\times C\leftrightarrow A=B\right)$$
26	4 25	pm2.61ian	$$⊢C\ne \varnothing \to \left(A\times C=B\times C\leftrightarrow A=B\right)$$